Reconciling verified-circuit development and Verilog development
File(s)
Author(s)
Lööw, Andreas
Type
Conference Paper
Abstract
In software development, verified compilers like
the CompCert compiler and the CakeML compiler enable a
methodology for software development and verification that allows
software developers to establish program-correctness properties on
the verified compiler’s target level. Inspired by verified compilers
for software development, the verified Verilog synthesis tool
Lutsig enables the same methodology for Verilog hardware
development. In this paper, we address how Verilog features
that must be understood as hardware constructs, rather than as
software constructs, fit into hardware development methodologies,
such as Lutsig’s, inspired the development methodology enabled
by software compilers. We explore this issue by extending
the subset of Verilog supported by Lutsig with one such
feature: always_comb blocks. In extending Lutsig’s Verilog
support with this, seemingly minor, feature, we are, perhaps
surprisingly, required to revisit Lutsig’s methodology for circuit
development and verification; this revisit, it turns out, requires
reconciling traditional Verilog development and the traditional
program-verification methodology offered by verified software
compilers. All development for this paper has been carried out
in the HOL4 theorem prover.
the CompCert compiler and the CakeML compiler enable a
methodology for software development and verification that allows
software developers to establish program-correctness properties on
the verified compiler’s target level. Inspired by verified compilers
for software development, the verified Verilog synthesis tool
Lutsig enables the same methodology for Verilog hardware
development. In this paper, we address how Verilog features
that must be understood as hardware constructs, rather than as
software constructs, fit into hardware development methodologies,
such as Lutsig’s, inspired the development methodology enabled
by software compilers. We explore this issue by extending
the subset of Verilog supported by Lutsig with one such
feature: always_comb blocks. In extending Lutsig’s Verilog
support with this, seemingly minor, feature, we are, perhaps
surprisingly, required to revisit Lutsig’s methodology for circuit
development and verification; this revisit, it turns out, requires
reconciling traditional Verilog development and the traditional
program-verification methodology offered by verified software
compilers. All development for this paper has been carried out
in the HOL4 theorem prover.
Date Issued
2023-02-03
Date Acceptance
2022-07-10
Citation
2023, pp.89-98
Publisher
IEEE
Start Page
89
End Page
98
Copyright Statement
© 2022 The Author(s). This article is licensed under a Creative
Commons Attribution 4.0 International License
Commons Attribution 4.0 International License
License URL
Identifier
https://ieeexplore.ieee.org/document/10026557
Source
Formal Methods in Computer-Aided Design (fmcad 2022)
Publication Status
Published
Start Date
2022-10-17
Finish Date
2022-10-21
Coverage Spatial
Trento, Italy
Date Publish Online
2023-02-03