Name
Abstract | ||
|---|---|---|
Sequential verification methods based on reachability analysis are still limited by the size of the BDDs involved in computations. Extending their applicability to larger and real circuits is still a key issue.Within this framework, we explore a new way to improve symbolic traversal performance, working on the representation of state sets. We exploit retiming to reduce the number of latches of a FSM, and to relocate them in order to obtain a simplified state set representation. We consider retiming as a temporary state space transformation to increase the efficiency of sequential verification. We discuss it as a state space transformation and we formally analyze the conditions under which such a transformation is equivalence preserving for a given property under verification.We lower image computation cost, and we reduce the size of BDDs representing intermediate results and state sets. Experimental results show considerable memory and time improvements on some benchmark and home made circuits. |
Year | DOI | Venue |
|---|---|---|
2000 | 10.1145/337292.337591 | DAC |
Keywords | Field | DocType |
considerable memory,sequential verification method,state set representation,sequential verification,state space transformation,state set,retiming transformation,temporary state space transformation,intermediate result,key issue,automatic target recognition,sequential circuits,simd,data structures,state space,scheduling,formal verification,mpeg 2,boolean functions | Computer science,Electronic engineering,Real-time computing,Theoretical computer science,Reachability,Equivalence (measure theory),Retiming,Data structure,Tree traversal,Sequential logic,Algorithm,State space,Formal verification | Conference |
ISSN | ISBN | Citations |
0738-100X | 1-58113-187-9 | 8 |
PageRank | References | Authors |
0.69 | 7 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Gianpiero Cabodi | 1 | 352 | 37.41 |
| Stefano Quer | 2 | 396 | 37.74 |
| Fabio Somenzi | 3 | 3394 | 302.47 |