Adding 32-bit Mode to the ACL2 Model of the x86 ISA

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.

Bibliographic Details
Main Authors: Alessandro Coglio, Shilpi Goel
Format: Article
Language:English
Published: Open Publishing Association 2018-10-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1810.04313v1