Name
Abstract | ||
|---|---|---|
Logic synthesis and formal verification both rely on scalable reachable state characterization for numerous purposes. One popular technique is over-approximate reachability analysis using an iterative ternary simulation. This method trades precision of reachability characterization for a high degree of computational efficiency. Although effective on many industrial designs, it breaks down when the design has registers that have complex initial states or has extremely deep deterministic subcircuits. In this paper, we improve upon the precision of ternary simulation-based approximate reachability while retaining its scalability by representing certain variables as symbols vs. unknowns, and by selectively saturating subcircuits which would otherwise preclude convergence. These techniques are particularly beneficial for enhancing the scalability of industrial sequential equivalence checking problems, occasionally solving such problems outright with no need for more costly and precise analysis. |
Year | Venue | Keywords |
|---|---|---|
2011 | Formal Methods in Computer-Aided Design | ternary simulation-based approximate reachability,industrial sequential equivalence checking,over-approximate reachability analysis,method trades precision,precise analysis,deep deterministic subcircuits,reachability characterization,industrial design,saturating subcircuits,iterative ternary simulation,logic gate,iterative methods,approximation algorithms,oscillations,equivalence checking,oscillators,formal verification,logic synthesis,registers,logic gates |
Field | DocType | ISBN |
Logic synthesis,Formal equivalence checking,Convergence (routing),Approximation algorithm,Computer science,Iterative method,Algorithm,Theoretical computer science,Reachability,Formal verification,Scalability | Conference | 978-1-4673-0896-0 |
Citations | PageRank | References |
1 | 0.37 | 4 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Michael Case | 1 | 44 | 6.66 |
| Jason Baumgartner | 2 | 313 | 23.36 |
| Hari Mony | 3 | 186 | 13.30 |
| Robert Kanzelman | 4 | 107 | 6.16 |