Verifying X86 Instructions

Stream: general

[Tim Daly]

@Mario Carneiro You might find this paper of interest: Verifying X86 Instruction Implementations (https://arxiv.org/pdf/1912.10285.pdf)

[Tim Daly]

@Mario Carneiro The x86 instruction verification paper is impressive. They start with the RTL (register transfer logic) specified in SystemVerilog (hardware circuit definitions), move through micro-ops, all the way up to user-visible instructions. I worked with their example instruction (SHRD, shift right double) in a different context and I'm quite impressed. Apparently their work is available on github.