A formal spec of the RISC-V Instruction Set Architecture, written in Bluespec BSV (executable, synthesizable) - Rishiyur S. Nikhil - rsnikhil