Abstract Stobjs and Their Application to ISA Modeling
Shilpi Goel (Department of Computer Science, University of Texas at, Austin), Warren A Hunt, Jr. (Department of Computer Science, University of, Texas at Austin), Matt Kaufmann (Department of Computer Science, University, of Texas at Austin)
TL;DR
This paper introduces abstract stobjs in ACL2, a new feature that enhances ISA modeling by enabling faster execution, symbolic simulation, and more efficient reasoning, improving proof resilience.
Contribution
The paper presents the novel concept of abstract stobjs in ACL2 and demonstrates their advantages over traditional stobjs for ISA modeling.
Findings
Abstract stobjs enable faster execution of models.
They support symbolic simulation effectively.
They improve reasoning efficiency and proof resilience.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsEmbedded Systems Design Techniques · Parallel Computing and Optimization Techniques · Formal Methods in Verification