The Essence of Verilog: A Tractable and Tested Operational Semantics for Verilo...
summary
Claim: a compact operational semantics captures Verilog’s tricky behaviors and serves as a reference. The work defines a λV core language that desugars real Verilog, ships a 27,000-line Java implementation, and runs both on >800 test cases plus nontrivial open-source designs. Results show near-total conformance, rejected unsafe implicit conversions, and detected semantic bugs and ambiguities in existing simulators; a student builds a working concolic tool in ~100 hours, demonstrating the semantics is practical and actionable.
AI-written summary · about
chapters (11)
- 0:00Verilog semantics overview
- 1:29Hardware vs software compilation
- 2:33Domain-specific design challenges
- 3:17Verilog semantic pitfalls
- 6:28Lambda V formal semantics
- 7:32Lambda V features and implementation
- 8:37Bugs and ambiguities detection
- 9:42Lambda V totality and conformance
- 11:32Concolic execution case study
- 12:41Conclusion and future work
- 13:26Q&A
related talks
23mVellvm: Formalizing the Informal
31mProgramming Languages Must Have Formal Semantics. Period.
40mFormal semantics for multi-language programs- 40mFormal semantics for multi-language programs
31mFormal Specification
19mA Pure Demand Operational Semantics with Applications to Program Analysis
53mSemantics-based program manipulation in the age of LLMs
16mExtrinsically Typed Operational Semantics for Functional Languages