How is Coq used in hardware verification?
Some of my (very incomplete) thoughts:
hardware is mostly expressing boolean circuits. But that is decidable. Then why even bother with Coq in that case?
Google scholar has plenty of recent papers that use Coq for hardware verification. I suggest using “coq hardware verification” as your keywords.
hardware is mostly expressing boolean circuits.
Combinational circuits, yes; stateful ones, not really. Asynchronous logic is another interesting can of worms.
But that is decidable.
?
1 Like