A methodology for efficient hardware verification |
| |
Authors: | Mark Aagaard Miriam Leeser |
| |
Affiliation: | (1) School of Electrical Engineering, Cornell University, 14853 Ithaca, NY |
| |
Abstract: | We present a methodology which helps structure the design and verification of hardware circuits. Our methodology supports reusable proofs of hardware components, provides for multiple implementations of the same specification, and allows both bottom up and top down verification styles. We provide mechanical assistance for our methodology in the Nuprl proof development system. Our method exploits Nuprl's rich type theory to encode the specification of a module in the type of the module. This allows us to elegantly describe parameterized hardware modules. The methodology is efficient because: the automated support reduces the amount of information that users must provide and the use of parameterized hardware modules eliminates redundant reasoning among proofs of hardware components. In this paper we explain our methodology and illustrate our approach with several examples of circuit verification. |
| |
Keywords: | Hardware verification methodology theorem proving dependent type theory register transfer level design |
本文献已被 SpringerLink 等数据库收录! |