SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal
Thu 26 Oct 2023 11:00 - 11:18 at Room II - language semantics Chair(s): Sebastian Erdweg

With the increasing need to apply modern software techniques to hardware design, Verilog, the most popular Hardware Description Language (HDL), plays an infrastructure role. However, Verilog has several semantic pitfalls that often confuse software and hardware developers. Although prior research on formal semantics for Verilog exists, it is not comprehensive and has not fully addressed these issues. In this work, we present a novel scheme inspired by previous work on defining core languages for software languages like JavaScript and Python. Specifically, we define the formal semantics of Verilog using a core language called $\lambda_V$, which captures the essence of Verilog using as few language structures as possible. $\lambda_V$ not only covers the most complete set of language features to date, but also addresses the aforementioned pitfalls. We implemented $\lambda_V$ with about 27,000 lines of Java code, and comprehensively tested its totality and conformance with Verilog. As a reliable reference semantics, $\lambda_V$ can detect semantic bugs in real-world Verilog simulators and expose ambiguities in Verilog's standard specification. Moreover, as a useful core language, $\lambda_V$ has the potential to facilitate the development of tools such as a state-space explorer and a concolic execution tool for Verilog.

Thu 26 Oct

Displayed time zone: Lisbon change

11:00 - 12:30
language semanticsOOPSLA at Room II
Chair(s): Sebastian Erdweg JGU Mainz
11:00
18m
Talk
The Essence of Verilog: A Tractable and Tested Operational Semantics for Verilog
OOPSLA
Qinlin Chen Nanjing University, Nairen Zhang Nanjing University, Jinpeng Wang Nanjing University, Tian Tan Nanjing University, Chang Xu Nanjing University, Xiaoxing Ma Nanjing University, Yue Li Nanjing University
DOI
11:18
18m
Talk
Regular Expression Matching using Bit Vector Automata
OOPSLA
Alexis Le Glaunec Rice University, Lingkun Kong Rice University, Konstantinos Mamouras Rice University
DOI
11:36
18m
Talk
Bidirectional Object-Oriented Programming: Towards Programmatic and Direct Manipulation of Objects
OOPSLA
Xing Zhang Peking University, Guanchen Guo Peking University, Xiao He University of Science and Technology Beijing, Zhenjiang Hu Peking University
DOI
11:54
18m
Talk
Bring Your Own Data Structures to DatalogDistinguished Paper
OOPSLA
Arash Sahebolamri Syracuse University, Langston Barrett Galois, Scott Moore Galois, Kristopher Micinski Syracuse University
DOI
12:12
18m
Talk
Rhombus: A New Spin on Macros without All the Parentheses
OOPSLA
Matthew Flatt University of Utah, Taylor Allred University of Utah, Nia Angle independent, Stephen De Gabrielle independent, Robert Bruce Findler Northwestern University, Jack Firth independent, Kiran Gopinathan National University of Singapore, Ben Greenman University of Utah, Siddhartha Kasivajhula independent, Alex Knauth independent, Jay McCarthy Reach, Sam Phillips independent, Sorawee Porncharoenwase University of Washington, Jens Axel S√łgaard independent, Sam Tobin-Hochstadt Indiana University
DOI Pre-print