[PDF] Lutsig: A Verified Verilog Compiler for Verified Circuit Development
A Lööw
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 …
•Cites: The essence of Bluespec: a core language for rule-based …