ISSN:
1572-8102
Keywords:
multiway decision graphs
;
binary decision diagrams
;
automated hardware verification
;
state machine verification
;
reachability analysis
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
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.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1023/A:1008663530211
Permalink
