Adding 32-bit Mode to the ACL2 Model of the x86 ISA
Alessandro Coglio (Kestrel Technology LLC, Palo Alto, CA (USA)),, Shilpi Goel (Centaur Technology, Inc., Austin, TX (USA))
TL;DR
This paper details the extension of the ACL2 x86 ISA model to include 32-bit mode support, enhancing its accuracy and applicability for different processor modes.
Contribution
The paper introduces a significant extension to the ACL2 x86 model, enabling it to accurately simulate 32-bit mode operations, which was not previously supported.
Findings
Successfully integrated 32-bit mode into the existing model
Identified key challenges in extending the model
Enhanced the model's applicability for broader analysis
Abstract
The ACL2 model of the x86 Instruction Set Architecture was built for the 64-bit mode of operation of the processor. This paper reports on our work to extend the model with support for 32-bit mode, recounting the salient aspects of this activity and identifying the ones that required the most work.
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
TopicsParallel Computing and Optimization Techniques · Embedded Systems Design Techniques · Interconnection Networks and Systems