Abstract
Symbolic simulation extends standard digital circuit simulation with symbolic representations of values, covering behaviors of a circuit for all possible instantiations of the symbolic values in a single simulation. Used as a formal verification method, symbolic simulation is algorithmically simple and intuitive, which enables precise analysis and fine-grained mitigation of computational complexity, allowing the method to handle circuits that are above the capacity of most standard formal model checking tools, as well as circuits with highly enmeshed pipelines. Symbolic simulation excels in verification of deep targeted properties of fixed-length pipelines, in particular arithmetic and other datapath circuits. It has been extensively applied in industrial verification of different kinds of integer and floating-point arithmetic circuits, such as adders, multipliers, and fused multiply-adders and dividers. Thanks to repeatable systematic verification strategies for complexity management and mitigation, such verification can be carried out routinely in development projects with rapidly evolving designs. Symbolic simulation is less optimal for verification of general consistency invariants and other inductive properties, as the method does not automate reachable-state analysis and requires a higher degree of human interaction and expertise than standard model checking tools.
Intel provides these materials as-is, with no express or implied warranties. Intel processors might contain design defects or errors known as errata, which might cause the product to deviate from published specifications. Intel, Intel Core, Intel Atom, Pentium and Intel logo are trademarks of Intel Corporation. Other names and brands might be claimed as the property of others.
Similar content being viewed by others
References
Aagaard M, Seger C-J (1995) The formal verification of a pipelined double-precision IEEE floating-point multiplier. In: Proceedings of IEEE international conference on computer aided design (ICCAD), pp 7–10
Aagaard MD, Jones RB, Seger C-JH (1999a) Formal verification using parametric representations of Boolean constraints. In: Proceedings of the 36th annual ACM/IEEE design automation conference, pp 402–407
Aagaard MD, Jones RB, Seger C-JH (1999b) Lifted-FL: a pragmatic implementation of combined model checking and theorem proving. In: Theorem proving in higher order logics. Springer, pp 323–340
Aagaard MD, Melham TF, O’Leary JW (1999c) Xs are for trajectory evaluation, Booleans are for theorem proving. In: Pierre L, Kropf T (eds) Correct hardware design and verification methods. Springer, pp 202–218
Aagaard MD, Jones RB, Kaivola R, Kohatsu KR, Seger C-JH (2000) Formal verification of iterative algorithms in microprocessors. In: Proceedings of the 37th annual design automation conference, pp 201–206
Adams S, Bjork M, Melham T, Seger C-J (2007) Automatic abstraction in symbolic trajectory evaluation. In: Formal methods in computer aided design (FMCAD’07), pp 127–135
Akers SB (1978) Binary decision diagrams. IEEE Trans Comput C-27:509–516
Bar Kama N, Kaivola R (2021) Hardware security leak detection by symbolic simulation. In: 2021 formal methods in computer aided design (FMCAD), pp 34–41
Beatty DL, Bryant RE, Seger C-JH (1990) Synchronous circuit verification by symbolic simulation: an illustration. In: Proceedings of the sixth MIT conference on advanced research in VLSI, pp 98–112
Bertacco V (2006) Scalable hardware verification with symbolic simulation. Springer
Bingham JD (2015) Universal Boolean functional vectors. In: Formal methods in computer-aided design (FMCAD), pp 25–32
Bingham J, Leslie-Hurd J (2014) Verifying relative error bounds using symbolic simulation. In: Biere A, Bloem R (eds) Proceedings of the 26th international conference on computer aided verification (CAV 2014). Lecture notes in computer science, vol 8559. Springer, pp 277–292
Bjesse P, Boralv A (2004) DAG-aware circuit compression for formal verification. In: IEEE/ACM international conference on computer aided design, 2004. ICCAD-2004, pp 42–49
Booth AD (1951) A signed binary multiplication technique. Q J Mech Appl Math 4:236–240
Bryant RE (1985) Symbolic verification of MOS circuits. In: 1985 Chapel Hill conference on VLSI, pp 419–438
Bryant RE (1986) Graph-based algorithms for Boolean function manipulation. IEEE Trans Comput C-35:677–691
Bryant RE (1990) Verification of synchronous circuits by symbolic logic simulation. In: Hardware specification, verification and synthesis: mathematical aspects. Lecture notes in computer science, vol 408. Springer, pp 14–24
Bryant RE, Seger C-JH (1990) Formal verification of digital circuits using symbolic ternary system models. In: International conference on computer aided verification, pp 33–43
Chakraborty S, Khasidashvili Z, Seger C-JH, Gajavelly R, Haldankar T, Chhatani D, Mistry R (2017) Symbolic trajectory evaluation for word-level verification: theory and implementation. Formal Methods Syst Des 50(2–3):317–352
Darringer J (1979) The application of program verification techniques to hardware verification. In: 16th design automation conference, pp 375–381
Darringer J, King JC (1978) Applications of symbolic execution to program testing. IEEE Des Test Comput 51–60
Drane T, Kiran Kumar MA (2022) C-to-RTL equivalence checking. In: Chattopadhyay A (ed) Handbook of computer architecture. Springer
Goel S, Slobodova A, Sumners R, Swords S (2021) Balancing automation and control for formal verification of microprocessors. In: Silva A, Leino KRM (eds) Computer aided verification. Springer, pp 26–45
Grundy J, Melham T, O’Leary J (2006) A reflective functional language for hardware design and theorem proving. J Funct Program 16(2):157–196
Gupta A, Kaivola R, Mehta M, Singh V (2022) Error correction code algorithm and implementation verification using symbolic representations. In: Griggio A, Rungta N (eds) Formal methods in computer aided design (FMCAD), pp 151–159
Harrison J (2009) Handbook of practical logic and automated reasoning. Cambridge University Press
Hazelhurst S, Seger C-JH (1997) Symbolic trajectory evaluation. In: Kropf T (ed) Formal hardware verification: methods and systems in comparison. Springer, pp 3–78
IEEE standard for binary floating-point arithmetic (1985) Institute of Electrical and Electronics Engineers. Note: Standard 754–1985
IEEE standard for SystemVerilog–unified hardware design, specification, and verification language (2018) IEEE Std 1800-2017 (Revision of IEEE Std 1800-2012), pp 1–1315
Jacobi C, Weber K, Paruthi V, Baumgartner J (2005) Automatic formal verification of fused-multiply-add FPUs. In: Proceedings of the conference on design, automation and test in Europe – Volume 2, DATE’05. IEEE Computer Society, pp 1298–1303
Jones RB (2002) Symbolic simulation methods for industrial formal verification. Springer
Jones RB, O’Leary JW, Seger C-JH, Aagaard MD, Melham TF (2001) Practical formal verification in microprocessor design. IEEE Des Test Comput 18(4):16–25
Kaivola R (2005) Formal verification of Pentium 4 components with symbolic simulation and inductive invariants. In: Etessami K, Rajamani SK (eds) Computer aided verification. Springer, pp 170–184
Kaivola R, Aagaard M (2000) Divider circuit verification with model checking and theorem proving. In: Theorem proving in higher order logics. TPHOLs 2000. Lecture notes in computer science, vol 1869. Springer, pp 338–355
Kaivola R, Kohatsu KR (2003) Proof engineering in the large: formal verification of Pentium 4 floating-point divider. Int J Softw Tools Technol Transf 4(3):323–334
Kaivola R, Naik A (2005) Formal verification of high-level conformance with symbolic simulation. In: Tenth IEEE international high-level design validation and test workshop, 2005, pp 153–159
Kaivola R, Narasimhan N (2001) Formal verification of the Pentium 4 multiplier. In: Proceedings sixth IEEE international high-level design validation and test workshop, Los Alamitos. IEEE Computer Society, pp 115–120
Kaivola R, Ghughal R, Narasimhan N, Telfer A, Whittemore J, Pandav S, Slobodová A, Taylor C, Frolov V, Reeber E, Naik A (2009) Replacing testing with formal verification in Intel Core i7 processor execution engine validation. In: Bouajjani A, Maler O (eds) Computer aided verification. Springer, pp 414–429
Kaivola R, Bar Kama N (2022) Timed causal fanin analysis for symbolic circuit simulation. In: Griggio A, Rungta N (eds) Formal methods in computer aided design (FMCAD), pp 99–107
King JC (1979) Symbolic execution and program testing. Commun ACM 19(7):385–394
KiranKumar VMA, Gupta A, Ghughal R (2012) Symbolic trajectory evaluation: the primary validation vehicle for next generation Intel processor graphics FPU. In: 2012 formal methods in computer-aided design (FMCAD), pp 149–156
Krishnamurthy N, Martin AK, Abadir MS, Abraham JA (2000) Validating PowerPC microprocessor custom memories. IEEE Des Test Comput 17(4):61–76
Kuehlmann A, Paruthi V, Krohm F, Ganai M (2002) Robust Boolean reasoning for equivalence checking and functional property verification. IEEE Trans Comput-Aided Des Integr Circuits Syst 21(12):1377–1394
Melham T (2018) Symbolic trajectory evaluation. In: Clarke EM, Henzinger TA, Veith H, Bloem R (eds) Handbook of model checking, ch. 25. Springer, pp 831–870
O’Leary J, Zhao X, Gerth RT, Seger C-JH (1999) Formally verifying IEEE compliance of floating-point hardware. Intel Tech J, pp 1–14
O’Leary J, Kaivola R, Melham T (2013) Relational STE and theorem proving for formal verification of industrial circuit designs. In: 2013 formal methods in computer-aided design, pp 97–104
Pandey M, Raimi R, Beatty DL, Bryant RE (1996) Formal verification of PowerPC arrays using symbolic trajectory evaluation. In: DAC’96: proceedings of the 33rd annual design automation conference. Association for Computing Machinery, pp 649–654
Pratt V (1995) Anatomy of the Pentium bug. In: Mosses PD, Nielsen M, Schwartzbach MI (eds) TAPSOFT’95: theory and practice of software development. Springer, pp 97–107
Ray S, Goel S (2022) Theorem proving. In: Chattopadhyay A (ed) Handbook of computer architecture. Springer
Roorda J-W, Claessen K (2006) SAT-based assistance in abstraction refinement for symbolic trajectory evaluation. In: Ball T, Jones RB (eds) Computer aided verification. Springer, pp 175–189
Russinoff DM (1998) A mechanically checked proof of IEEE compliance of the floating point multiplication, division and square root algorithms of the AMD-K7 processor. LMS J Comput Math 1:148–200
Russinoff D (2019) Formal verification of floating-point hardware design. Springer
Seger C-JH (1993) Voss – a formal hardware verification system user’s guide. https://doi.org/10.5555/901942
Seger C-JH, Bryant RE (1995) Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods Syst Des 6:147–190
Seger C-J, Jones R, O’Leary J, Melham T, Aagaard M, Barrett C, Syme D (2005) An industrially effective environment for formal hardware verification. IEEE Trans Comput-Aided Des Integr Circuits Syst 24(9):1381–1405
Seligman E, Schubert T, Kiran Kumar MVA (2015) Formal verification: an essential toolkit for modern VLSI design. Morgan Kaufmann Publishers Inc.
Slobodova A (2006) Challenges for formal verification in industrial setting. In: FMICS’06/PDMC’06: Proceedings of the 11th international workshop, FMICS 2006 and 5th international workshop, PDMC conference on formal methods: applications and technology. Springer, pp 1–22
Slobodova A, Nagalla K (2004) Formal verification of floating point multiply add on Itanium processor. In: Fifth international workshop on designing correct circuits, ETAPS 2004
Slobodova A, Davis J, Swords S, Hunt W (2011) A flexible formal verification environment for industrial scale verification. In: Ninth ACM/IEEE international conference on formal methods and models for codesign (MEMOCODE2011), pp 89–97
Swords SO (2010) A verified framework for symbolic execution in the ACL2 theorem prover. PhD thesis, University of Texas at Austin. http://hdl.handle.net/2152/ETD-UT-2010-12-2210
Swords S (2017) Term-level reasoning in support of bit-blasting. In: Slobodova A, Hunt WA Jr (eds) Proceedings 14th international workshop on the ACL2 theorem prover and its applications, Austin, 22–23 May 2017. Electronic proceedings in theoretical computer science, vol 249. Open Publishing Association, pp 95–111
Swords S, Davis J (2011) Bit-blasting ACL2 theorems. In: Hardin D, Schmaltz J (eds) Proceedings 10th international workshop on the ACL2 theorem prover and its applications, Austin, 3–4 Nov 2011. Electronic proceedings in theoretical computer science, vol 70. Open Publishing Association, pp 84–102
Tzoref R, Grumberg O (2006) Automatic refinement and vacuity detection for symbolic trajectory evaluation. In: Ball T, Jones RB (eds) Computer aided verification. Springer, pp 190–204
Vizel Y, Ivrii A (2022) Bit level model checking algorithms. In: Chattopadhyay A (ed) Handbook of computer architecture. Springer
VossII (2020). https://github.com/TeamVoss/VossII. Accessed: 8 June 2021
Yang J, Seger C-J (2003) Introduction to generalized symbolic trajectory evaluation. IEEE Trans Very Large Scale Integr (VLSI) Syst 11(3):345–353
Acknowledgements
This chapter summarizes almost three decades of work. At the time of its writing, more than 60 people have directly contributed to Intel’s shared arithmetic verification code-base on over 50 design projects. A much higher number have contributed intellectually to the endeavor, both inside Intel and at large. It has been a team effort. We would like to express our sincere thanks to each and every member of the team.
We would also like to thank Intel’s design and validation management over the years for trusting and encouraging this work. There are more names than we can mention; however, we would like to express our special thanks to Bob Bentley and Alon Flaisher for their crucial long-term support.
Finally, we would like to thank Jesse Bingham, Levent Erkok, Robert Jones, Joe Leslie-Hurd, Sayak Ray, and Annette Upton for their detailed feedback on the drafts of this text.
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Section Editor information
Rights and permissions
Copyright information
© 2022 Springer Nature Singapore Pte Ltd.
About this entry
Cite this entry
Kaivola, R., O’Leary, J. (2022). Verification of Arithmetic and Datapath Circuits with Symbolic Simulation. In: Chattopadhyay, A. (eds) Handbook of Computer Architecture. Springer, Singapore. https://doi.org/10.1007/978-981-15-6401-7_37-1
Download citation
DOI: https://doi.org/10.1007/978-981-15-6401-7_37-1
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-15-6401-7
Online ISBN: 978-981-15-6401-7
eBook Packages: Springer Reference EngineeringReference Module Computer Science and Engineering