Test generation using SAT-based bounded model checking for validation of pipelined processors

ABSTRACT

Functional verification is one of the major bottlenecks in microprocessor design. Simulation-based techniques are the most widely used form of processor verification. Efficient test generation is crucial for the simulation-based verification. We present an efficient test generation methodology using SAT-based bounded model checking (BMC). This paper addresses two important challenges in test generation using SAT-based BMC: determination of bound for each property, and application of design and property decompositions to improve test generation time as well as memory requirement. Our experimental results using a MIPS processor demonstrate the feasibility and usefulness of our approach.

REFERENCES

• 1: Allon Adir , Eli Almog , Laurent Fournier , Eitan Marcus , Michal Rimon , Michael Vinov , Avi Ziv, Genesys-Pro: Innovations in Test Program Generation for Functional Processor Verification, IEEE Design & Test, v.21 n.2, p.84-93, March 2004 [doi>10.1109/MDT.2004.1277900]
• 2: N. Amla et al. An analysis of SAT-based model checking techniques in an industrial environment. CHARME 2005.
• 3: A. Biere et al. Bounded model checking. Advances in Computers 2003.
• 4: 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
• 5: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 6: Fady Copty , Limor Fix , Ranan Fraer , Enrico Giunchiglia , Gila Kamhi , Armando Tacchella , Moshe Y. Vardi, Benefits of Bounded Model Checking at an Industrial Setting, Proceedings of the 13th International Conference on Computer Aided Verification, p.436-453, July 18-22, 2001
• 7: Angelo Gargantini , Constance Heitmeyer, Using model checking to generate tests from requirements specifications, ACM SIGSOFT Software Engineering Notes, v.24 n.6, p.146-162, Nov. 1999
• 8: E. Goldberg , Y. Novikov, BerkMin: A Fast and Robust Sat-Solver, Proceedings of the conference on Design, automation and test in Europe, p.142, March 04-08, 2002
• 9: S. Gurumurthy et al. Automated mapping of pre-computed module-level test sequences to processor instructions. ITC 2005.
• 10: John L. Hennessy , David A. Patterson, Computer architecture: a quantitative approach, Morgan Kaufmann Publishers Inc., San Francisco, CA, 02
• 11: Kazuyoshi Kohno , Nobu Matsumoto, A new verification methodology for complex pipeline behavior, Proceedings of the 38th conference on Design automation, p.816-821, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379072]
• 12: Heon-Mo Koo , Prabhat Mishra, Functional test generation using property decompositions for validation of pipelined processors, Proceedings of the conference on Design, automation and test in Europe: Proceedings, March 06-10, 2006, Munich, Germany
• 13: 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]
• 14: M. R. Prasad et al. A survey of recent advances in SAT-based formal verification. Intl. Journal on Software Tools for Technology Transfer (STTT), 2005.
• 15: Jian Shen , Jacob A. Abraham, An RTL Abstraction Technique for Processor MicroarchitectureValidation and Test Generation, Journal of Electronic Testing: Theory and Applications, v.16 n.1-2, p.67-81, Feb/April 2000 [doi>10.1023/A:1008388623771]
• 16: Shmuel Ur , Yaov Yadin, Micro architecture coverage directed generation of test programs, Proceedings of the 36th ACM/IEEE conference on Design automation, p.175-180, June 21-25, 1999, New Orleans, Louisiana, United States [doi>10.1145/309847.309909]
• 17: www-cad.eecs.berkeley.edu/kenmcmil/smv. Cadence SMV.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Verification

General Terms:
Verification

Keywords:
functional validation, test generation