The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
Lutsig: a verified Verilog compiler for verified circuit development
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
Abstract
We report on a new verified Verilog compiler called Lutsig. Lutsig currently targets (a class of) FPGAs and is capable of producing technology mapped netlists for FPGAs. We have connected Lutsig to existing Verilog development tools, and in this paper we show how Lutsig, as a consequence of this connection, fits into a hardware development methodology for verified circuits in the HOL4 theorem prover. One important step in the methodology is transporting properties proved at the behavioral Verilog level down to technology mapped netlists, and Lutsig is the component in the methodology that enables such transportation.
@misc{loow2021lutsig,
title = {Lutsig: a verified Verilog compiler for verified circuit development},
author = {Andreas Lööw},
year = {2021},
journal = {ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP)},
pages = {46--60},
doi = {10.1145/3437992.3439916},
}