Authors : Sandeep Dasgupta , Daejun Park , Theodoros Kasampalis , Vikram S. Adve , Grigore Roşu Authors Info & Claims
Pages 1133 - 1148
Published : 08 June 2019 Publication History
30 citation 2,047 Downloads
Total Citations 30
Total Downloads 2,047
Last 12 Months 492
Last 6 weeks 65
Get Citation Alerts
This alert has been successfully added and will be sent to: You will be notified whenever a record that you have chosen has been cited.
To manage your alert preferences, click on the button below. Manage my Alerts
We present the most complete and thoroughly tested formal semantics of x86-64 to date. Our semantics faithfully formalizes all the non-deprecated, sequential user-level instructions of the x86-64 Haswell instruction set architecture. This totals 3155 instruction variants, corresponding to 774 mnemonics. The semantics is fully executable and has been tested against more than 7,000 instruction-level test cases and the GCC torture test suite. This extensive testing paid off, revealing bugs in both the x86-64 reference manual and other existing semantics. We also illustrate potential applications of our semantics in different formal analyses, and discuss how it can be useful for processor verification.
WEBM File (p1133-dasgupta.webm)
