> If you want to prove something about code, you probably have to prove microop semantics upward from verilog What if your chip fab doesn't obey the HDL's inst

> If you want to prove something about code, you probably have to prove microop semantics upward from verilog What if your chip fab doesn't obey the HDL's instructions? You're always "trusting trust" at some level. See also this horror story: https://www.teamten.com/lawrence/writings/coding-machines/ https://www.teamten.com/lawrence/writings/coding-machines/.