|
|
|---|
|
|
|
|---|
S. Goel, W. A. Hunt, Jr., and M. Kaufmann, “Abstract Stobjs and Their
Application to ISA Modeling”, in R. Gamboa and J. Davis, editors,
Proceedings of ACL2 Workshop 2013, Electronic Proceedings in
Theoretical Computer Science, Volume 114, pp. 54-69, 2013.
Relevance: an ACL2 feature introduced to support
operational semantic models
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.
Aside from the specific advantages abstract stobjs (see defabsstobj) confer on ACL2 state machines, this papers illustrates how attention to operational semantics has influenced the development of ACL2.