The Essence of Verilog: A Tractable and Tested Operational Semantics for Verilog

Explore a groundbreaking approach to defining the formal semantics of Verilog in this 18-minute conference talk from OOPSLA2 2023. Delve into the novel core language λV, designed to capture Verilog's essence using minimal language structures. Learn how this comprehensive semantic definition addresses common pitfalls, covers an extensive set of language features, and serves as a reliable reference for detecting bugs in Verilog simulators. Discover the potential applications of λV in developing tools like state-space explorers and concolic execution tools for Verilog, and understand its role in exposing ambiguities in Verilog's standard specification. Gain insights into the rigorous implementation and testing process, involving 27,000 lines of Java code, that ensures λV's totality and conformance with Verilog.