Leveraging sequential equivalence checking to enable system-level to RTL flows

ABSTRACT

It has long been the practice to create models in C or C++ for architectural studies, software prototyping and RTL verification in the design of Systems-on-Chip (SoC). It is often the case that by the end of a design project, multiple C models exist for different uses. Since a lot of time is invested in ensuring the functional correctness of these models via their use in system-level simulations, they often become "golden" functional reference models. Design teams are moving towards leveraging these system-level models to reduce the time needed for design and verification of RTL. On the design side, the use of high-level synthesis tools to synthesize RTL from C/C++ models is gaining ground for certain classes of blocks within a design. On the verification front, temporal differences at interfaces and in internal states between system-level models and RTL prevent the use of combinational equivalence checkers. This paper focuses on the use of sequential equivalence checking to verify functional equivalence between system-level models and RTL and describes the challenges and vale of using it in system-level to RTL flows.

REFERENCES

• 1: Calypto Design Systems. calypto.com/products.
• 2: Philippe Georgelin , Venkat Krishnaswamy, Towards a C++-based design methodology facilitating sequential equivalence checking, Proceedings of the 43rd annual conference on Design automation, July 24-28, 2006, San Francisco, CA, USA [doi>10.1145/1146909.1146938]
• 3: Edmund Clarke , Daniel Kroening , Karen Yorav, Behavioral consistency of C and verilog programs using bounded model checking, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.775928]
• 4: Anmol Mathur , Venkat Krishnaswamy, Design for verification in system-level models and RTL, Proceedings of the 44th annual conference on Design automation, June 04-08, 2007, San Diego, California [doi>10.1145/1278480.1278528]

INDEX TERMS

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

General Terms:
Reliability, Verification

Keywords:
RTL models, equivalence checking, formal verification, high-level synthesis, system-level models