Specifying instruction-set architectures in HOL: A primer
- 1 January 1994
- book chapter
- Published by Springer Nature
- p. 440-455
- https://doi.org/10.1007/3-540-58450-1_59
Abstract
No abstract availableKeywords
This publication has 12 references indexed in Scilit:
- Reverification of a microprocessorPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Implementing a methodology for formally verifying RISC processors in HOLPublished by Springer Nature ,1994
- Formal verification of a pipelined microprocessorIEEE Software, 1990
- A hierarchical methodology for verifying microprogrammed microprocessorsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1990
- Microprocessor design verificationJournal of Automated Reasoning, 1989
- Correctness Properties of the Viper Block Model: The Second LevelPublished by Springer Nature ,1989
- Formal Verification and Implementation of a MicroprocessorPublished by Springer Nature ,1988
- A Proof of Correctness of the Viper Microprocessor: The First LevelPublished by Springer Nature ,1988
- Formal specification and documentation of microprocessor instruction setsMicroprocessing and Microprogramming, 1987
- Models and logic of MOS circuitsPublished by Springer Nature ,1987