Non-cycle-accurate sequential equivalence checking

ABSTRACT

We present a novel technique for Sequential Equivalence Checking (SEC) between non-cycle-accurate designs. The problem is routinely encountered in verifying the correctness of a system-level model versus an RTL design which has been derived from the former either manually or through high-level synthesis. The existing state-of-the-art in formal verification/SEC does not provide an efficient mechanism to perform such an equivalence check. Our technique reduces the SEC problem to a cycle-accurate equivalence-checking problem by constructing a pair of normalized cycle-accurate designs from the original designs, on which standard equivalence-checking techniques can then be deployed. We report the results of deploying our techniques on several industrial examples.

REFERENCES

• 1: M. Aagaard, B. Cook, N. A. Day, and R. B. Jones. A framework for microprocessor correctness statements. In CHARME, pp. 433--448, 2001.
• 2: J. Baumgartner, H. Mony, V. Paruthi, R. Kanzelman, and G. Janssen. Scalable sequential equivalence checking across arbitrary design transformations. In ICCD, pp. 259--266, 2006.
• 3: P. Bjesse and J. Kukula. Automatic generalized phase abstraction for formal verification. In ICCAD, pp. 1076--1082, 2005.
• 4: Calypto Design Systems. Sequential Equivalence Checking: A new approach to functional verification of datapath and control logic changes. http://www.calypto.com/wp_request.php?paper=sequential, 2007.
• 5: E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 2000.
• 6: E. M. Clarke, D. Kroening, and K. Yorav. Behavioral consistency of C and Verilog programs using bounded model checking. In DAC, pp. 368--371, 2003.
• 7: M. Haldar, G. Singh, S. Prabhakar, B. Dwivedi, and A. Ghosh. Construction of concrete verification models from C++. In DAC, pp. 942--947, 2008.
• 8: S.-Y. Huang, K.-T. Cheng, K.-C. Chen, C.-Y. Huang, and F. Brewer. AQUILA: An equivalence checking system for large sequential designs. IEEE TOC, 49(5):443--464, 2000.
• 9: D. Kaiss, M. Skaba, Z. Hanna, and Z. Khasidashvili. Industrial strength SAT-based alignability algorithm for hardware equivalence verification. In FMCAD, pp. 20--26, 2007.
• 10: Z. Khasidashvili, M. Skaba, D. Kaiss, and Z. Hanna. Post-reboot equivalence and compositional verification of hardware. In FMCAD, pp. 11--18, 2006.
• 11: A. Koelbl, J. R. Burch, and C. Pixley. Memory modeling in ESL-RTL equivalence checking. In DAC, pp. 205--209, 2007.
• 12: A. Kuehlmann. Dynamic transition relation simplification for bounded property checking. In ICCAD, pp. 50--57, 2004.
• 13: A. Kuehlmann, V. Paruthi, F. Krohm, and M. K. Ganai. Robust Boolean reasoning for equivalence checking and functional property verification. IEEE TCAD, 21:1377--1394, 2002.
• 14: Y.-L. Lin. Recent developments in high-level synthesis. ACM TODAES, 2(1):2--21, 1997.
• 15: F. Lu and K.-T. Cheng. Sequential equivalence checking based on k^th invariants and circuit sat solving. In HLDVT, pp. 45--51, 2005.
• 16: A. Mishchenko, M. L. Case, R. K. Brayton, and S. Jang. Scalable and scalably-verifiable sequential synthesis. In ICCAD, 2008.
• 17: D. Park. Concurrency and automata on infinite sequences. In P. Deussen, editor, 5^th GI-Conference, volume 104 of Theoretical Computer Science, pp. 167--183, Karlsruhe, 1981. Springer-Verlag.
• 18: C. Pixley. A theory and implementation of sequential hardware equivalence. IEEE TCAD, 11(12):1469--1478, 1992.
• 19: V. Singhal, C. Pixley, A. Aziz, S. Qadeer, and R. K. Brayton. Sequential optimization in the absence of global reset. ACM TODAES, 8(2):222--251, 2003.
• 20: C. A. J. van Eijk. Sequential equivalence checking based on structural similarities. IEEE TCAD, 19(7):814--819, 2000.
• 21: C. A. J. van Eijk and J. A. G. Jess. Exploiting functional dependencies in finite state machine verification. In DATE, pp. 266--271, 1996.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.5 REGISTER-TRANSFER-LEVEL IMPLEMENTATION
      B.5.2 Design Aids

Additional Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
  B.7 INTEGRATED CIRCUITS
      B.7.2 Design Aids

General Terms:
Algorithms, Verification

Keywords:
formal verification, high level synthesis, model checking, sequential equivalence checking, unit product machine