A. He, P. Sule, Y. Kim, and N. Mansouri (USA)
assertion-based design, OVL, verification, theorem proving, modeling, formal semantics
Assertion-based design is becoming more and more widely used in industry to increase verifica tion efficiency. Currently most assertions are used in simulation-based verification environments to monitor the design. There are also some PSL/Sugar properties being used in model checking tools. However, despite the fact that theorem proving is the most suitable paradigm for verification of certain classes of designs, little has been done to take advantage of existing design assertions in the theorem-proving verification environments. In this paper, we focus on this problem, and present our work on de velopment of the semi-automated theorem-proving based verification system PROVERIFIC. We have defined generic predicate templates that capture the semantics of the stan dard assertion language OVL, and a subset of the hard ware description language Verilog. PROVERIFIC has two engines that use these templates, and automatically com pile a design under verification (specified in Verilog) and its correctness properties (specified in OVL) into the higher order predicates of the PVS [1] theorem proving environ ment. Design verification can be subsequently conducted by proving the correctness properties. We provide a de tailed example of a design with assertions, and its transla tion and its correctness proof to demonstrate the effective ness of our methodology.
Important Links:
Go Back
