| Autor: |
Goos, Gerhard, Hartmanis, Juris, van Leeuwen, Jan, Hunt, Warren A., Johnson, Steven D., Aagaard, Mark D., Jones, Robert B., Melham, Thomas F., O'Leary, John W., Seger, Carl-Johan H. |
| Zdroj: |
Formal Methods in Computer-Aided Design (978-3-540-41219-9); 2000, p300-319, 20p |
| Abstrakt: |
We present a formal verification methodology for datapathdominated hardware. This provides a systematic but flexible framework within which to organize the activities undertaken in large-scale verification efforts and to structure the associated code and proof-script artifacts. The methodology deploys a combination of model checking and lightweight theorem proving in higher-order logic, tightly integrated within a general-purpose functional programming language that allows the framework to be easily customized and also serves as a specification language. We illustrate the methodology-which has has proved highly effective in large-scale industrial trials-with the verification of an IEEE- compliant, extended precision floating-point adder. [ABSTRACT FROM AUTHOR] |
| Databáze: |
Supplemental Index |
| Externí odkaz: |
|
