Verilog Synthesis in the Higher-Order Transformation Framework of TL

The complexity of formalizing the semantics of Verilog is significant. This presents an impediment when attempting to provide high assurance in the correctness of Verilog synthesis. This paper explores the use of higher-order transformation as a paradigm for implementing a synthesis system for a small subset of Verilog. The resulting system is capable of synthesizing net lists in the Xilinx Net list Format that are suitable for downloading to an FPGA. Transformations realizing the synthesis are based on algebraic laws whose correctness can be justified in terms of the operational semantics of Verilog.