Mike Gordon and Hardware Verification
2 days ago
- #hardware verification
- #Mike Gordon
- #higher-order logic
- Mike Gordon made hardware verification a reality using higher-order logic.
- Hardware circuits were modeled as relations on ports without distinguishing between inputs and outputs.
- Verification involved proving that the implementation's behavior (Imp) implies the specification (Spec).
- Partial correctness (Imp→Spec) could be trivial in cases like short circuits, requiring additional proofs.
- The model ignored physical design criteria like fan-out, gate delays, and overheating, focusing only on logical functionality.
- Mike Gordon's simple, relational models proved effective, while more complex models did not gain traction.
- Software verification was deemed more difficult than hardware due to complex interfaces and component replication.