Abstract Stobjs and Their Application to ISA Modeling

2013/04/30 by Shilpi Goel, Warren A Hunt, Jr., Matt Kaufmann
Computer Science · #cs.LO #cs.AR #cs.SC

paper · pdf · doi:10.4204/eptcs.114.5

published as EPTCS 114, 2013, pp. 54-69 · In Proceedings ACL2 2013, arXiv:1304.7123

arxiv created 2013/04/30 · arxiv updated 2013/05/01

Abstract

We introduce a new ACL2 feature, the abstract stobj, and show how to apply it to modeling the instruction set architecture of a microprocessor. Benefits of abstract stobjs over traditional ("concrete") stobjs can include faster execution, support for symbolic simulation, more efficient reasoning, and resilience of proof developments under modeling optimization.

Citations

• Proceedings International Workshop on the ACL2 Theorem Prover and its Applications