Fix more

1 files changed, 18 insertions, 0 deletions

diff --git a/references.bib b/references.bib
index 7d53f71..44e8be8 100644
--- a/references.bib
+++ b/references.bib
@@ -934,3 +934,21 @@ year = {2020},
 	numpages = {28},
 	keywords = {Generation of Object Files, Assembler Verification, Verified Separate Compilation}
 }
+
+@inproceedings{10.1145/3437992.3439916,
+author = {L\"{o}\"{o}w, Andreas},
+title = {Lutsig: A Verified Verilog Compiler for Verified Circuit Development},
+year = {2021},
+isbn = {9781450382991},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+url = {https://doi.org/10.1145/3437992.3439916},
+doi = {10.1145/3437992.3439916},
+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.},
+booktitle = {Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs},
+pages = {46–60},
+numpages = {15},
+keywords = {hardware verification, hardware synthesis, compiler verification},
+location = {Virtual, Denmark},
+series = {CPP 2021}
+}