Abstract
Digital circuit designs are usually given as Register-Transfer-Level (RTL) specifications, but most of today’s hardware verification tools are based on bit-level methods, using SAT or BDD-based techniques. RTL specifications contain more explicite structural information than bit-level descriptions. This paper presents a new approach to scale down design sizes before verification by exploiting word-level information. We introduce a one-to-one abstraction technique for RTL property checking, which computes a scaled-down abstract model of a design, in which signal widths are reduced with respect to a property. The property holds for the abstract RTL if and only if it holds for the original RTL. If the property fails, counterexamples for the original design are computed from counterexamples found on the reduced model. The verification task is completely carried out on the scaled-down version of the design; false-negatives cannot occur. Linear signal width reductions result in exponentially smaller state spaces and have a significant impact on the runtimes of verification tools. Experimental results on large industrial circuits have demonstrated applicability and efficiency of our method.
The original version of this chapter was revised: The copyright line was incorrect. This has been corrected. The Erratum to this chapter is available at DOI: 10.1007/978-0-387-35597-9_40
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
A Biere, A Cimatti, E M Clarke, M Fujita, and Y Zhu. “Symbolic Model Checking Using SAT Procedures instead of BDDs”. In Proc. DAC, pages 317–320, 1999.
C W Barrett, D L Dill, and J R Levitt. “A Decision Procedure for Bitvector Arithmetic”. In Proc. DAC, pages 522–527, 1998.
R E Bryant. “Graph-Based Algorithms for Boolean Function Manipulation”. IEEE Transactions on Computers, 35 (8): 677–691, 1986.
E M Clarke, E A Emerson, S Jha, and A P Sistla. “Symmetry Reductions in Model Checking”. In Proc. CAV, pages 147–158, 1998.
E M Clarke, O Grumberg, and D E Long. “Model Checking and Abstraction”. In Proc. POPL, pages 342–354, 1992.
D Cyrluk, M O Möller, and H Rueß. “An Efficient Decision Procedure for the Theory of Fixed-Sized Bit-Vectors”. In Proc. CAV, pages 60–71, 1997.
D J901 N Dershowitz and J P Jouannaud. “Handbook of Theoretical Computer Science, Formal Models and Semantics”, chapter “Rewrite Systems”, pages 243–320. J.v. Leeuwen, Elsevier, 1990.
R Drechsler. Formal Verification of Circuits. Kluwer Academic Publishers, 2000.
E A Emerson and R J Trefler. “From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking”. In Proc. CHARME, pages 142–156, 1999.
P Johannsen “BooSTER: Speeding Up RTL Property Checking of Digital Designs by Word-Level Abstraction”. In Proc. CAV’01,pages 373–377, 2001.
P Johannsen. “Reducing Bitvector Satisfiability Problems to Scale Down Design Sizes for RTL Property Checking”. In IEEE Proc. HLDVT’01, 2001.
J P M Silva. “Search Algorithmss for Satisfiability Problems in Combinational Switching Circuits”. PhD thesis, University of Michigan, 1995.
J P M Silva and K A Sakallah. “Boolean satisfiability in electronic design automation”. In Proc. DAC, pages 675–680, 2000.
Z Zeng, P Kalla, and M Ciesielski. “LPSAT: A Unified Approach to RTL Satisfiability”. In Proc. DATE, pages 398–402, 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Johannsen, P., Drechsler, R. (2002). Speeding Up Verification of RTL Designs by Computing One-to-One Abstractions with Reduced Signal Widths. In: Robert, M., Rouzeyre, B., Piguet, C., Flottes, ML. (eds) SOC Design Methodologies. IFIP — The International Federation for Information Processing, vol 90. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35597-9_31
Download citation
DOI: https://doi.org/10.1007/978-0-387-35597-9_31
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-6530-4
Online ISBN: 978-0-387-35597-9
eBook Packages: Springer Book Archive