Hardware verification using ANSI-C programs as a reference

ABSTRACT

We describe an algorithm to verify a hardware design given in Verilog using an ANSI-C program as a specification. We use SAT based Bounded Model Checking [1] in order to reduce the equivalence problem to a bit vector logic decision problem. As a case study, we describe experimental results on a hardware and a software implementation of the data encryption standard (DES) algorithm.

REFERENCES

• 1: Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Yunshan Zhu, Symbolic Model Checking without BDDs, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.193-207, March 22-28, 1999
• 2: Carl Pixley, Guest Editor's Introduction: Formal Verification of Commercial Integrated Circuits, IEEE Design & Test, v.18 n.4, p.4-5, July 2001 [doi>10.1109/MDT.2001.936243]
• 3: Luc Sèmèria , Renu Mehra , Barry Pangrle , Arjuna Ekanayake , Andrew Seawright , Daniel Ng, RTL c-based methodology for designing and verifying a multi-threaded processor, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA [doi>10.1145/513918.513951]
• 4: http://www.systemc.org.
• 5: A. Biere , A. Cimatti , E. M. Clarke , M. Fujita , Y. Zhu, Symbolic model checking using SAT procedures instead of BDDs, Proceedings of the 36th ACM/IEEE conference on Design automation, p.317-320, June 21-25, 1999, New Orleans, Louisiana, United States [doi>10.1145/309847.309942]
• 6: International Organization for Standardization. ISO/IEC 9899:1999: Programming languages --- C. International Organization for Standardization, Geneva, Switzerland, 1999.
• 7: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]