Multiway Decision Graphs for Automated Hardware Verification |
| |
Authors: | F. Corella Z. Zhou X. Song M. Langevin E. Cerny |
| |
Affiliation: | (1) Hewlett-Packard Company, Canada;(2) Nortel Technology, Canada;(3) Dép. dI. R.O., Univ.de Montréal, Canada |
| |
Abstract: | Traditional ROBDD-based methods of automated verification suffer from the drawback that they require a binary representation of the circuit. To overcome this limitation we propose a broader class of decision graphs, called Multiway Decision Graphs (MDGs), of which ROBDDs are a special case. With MDGs, a data value is represented by a single variable of abstract type, rather than by 32 or 64 boolean variables, and a data operation is represented by an uninterpreted function symbol. MDGs are thus much more compact than ROBDDs, and this greatly increases the range of circuits that can be verified. We give algorithms for MDG manipulation, and for implicit state enumeration using MDGs. We have implemented an MDG package and provide experimental results. |
| |
Keywords: | multiway decision graphs binary decision diagrams automated hardware verification state machine verification reachability analysis |
本文献已被 SpringerLink 等数据库收录! |
|