Claire Xen  🏳️‍⚧️ 🏳️‍🌈 🧙🏻‍♀️ BLM  🏴 🚩

Solvers are weird "Does my processor corrupt its instruction fetch?" -> writes flawless 10 instruction RISC-V program without ever reading the spec "Does my processor lock up?" -> stalls bus forever, is this good, do you like this

Keep extending the BMC depth, and the solver finds new combinations of multiplies, bus stalls and branch mispredicts that make my processor stall for that long. Currently at 100 cycle check bound (with trigger at cycle 25), max bus stall 20 cycles

So this trace features - Issuing loads before branches so the load data phase can extend the jump data phase - Issuing multiplies in the mispredict path of the same branch - Issuing invalid opcodes *inside an invalid opcode trap* All at once, breathtaking

So far I have learned: - I should hook up that kill signal on the multiplier so that mispredicts aren't quite so painful - I REALLY need to implement double fault condition