ACL2 theorems about commercial microprocessors
- 1 January 1996
- book chapter
- Published by Springer Nature
- p. 275-293
- https://doi.org/10.1007/bfb0031816
Abstract
No abstract availableKeywords
This publication has 13 references indexed in Scilit:
- ACL2: an industrial strength version of NqthmPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theoremJournal of Automated Reasoning, 1996
- Verifying the SRT division algorithm using theorem proving techniquesPublished by Springer Nature ,1996
- Automated proofs of object code for a widely used microprocessorJournal of the ACM, 1996
- Verification of arithmetic circuits with binary moment diagramsPublished by Association for Computing Machinery (ACM) ,1995
- Architecture of a complex arithmetic processor for communication signal processingPublished by SPIE-Intl Soc Optical Eng ,1994
- Gordon's computer: A hardware verification case study in OBJ3Formal Methods in System Design, 1994
- Symbolic model checking for sequential circuit verificationIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1994
- Formal verification of a pipelined microprocessorIEEE Software, 1990
- Software for Analytical Development of Communications ProtocolsAT&T Technical Journal, 1990