Verilog Synthesis in the Higher-Order Transformation Framework of TL

Victor Winter, Shiraz Hussain

Research output: Contribution to journalConference article


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.

Original languageEnglish (US)
Article number7027411
Pages (from-to)26-35
Number of pages10
JournalProceedings of IEEE International Symposium on High Assurance Systems Engineering
Issue numberJanuary
Publication statusPublished - Jan 29 2015
Event16th IEEE International Symposium on High Assurance Systems Engineering, HASE 2015 - Daytona Beach, United States
Duration: Jan 8 2015Jan 10 2015



  • TL program transformation
  • Verilog
  • synthesis

ASJC Scopus subject areas

  • Software
  • Safety, Risk, Reliability and Quality

Cite this