Verilog Synthesis in the Higher-Order Transformation Framework of TL

Victor Winter; Shiraz Hussain

doi:10.1109/HASE.2015.13

Verilog Synthesis in the Higher-Order Transformation Framework of TL

Victor Winter, Shiraz Hussain

Computer Science

Research output: Contribution to journal › Conference article › peer-review

Abstract

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 language	English (US)
Article number	7027411
Pages (from-to)	26-35
Number of pages	10
Journal	Proceedings of IEEE International Symposium on High Assurance Systems Engineering
Volume	2015-January
Issue number	January
DOIs	https://doi.org/10.1109/HASE.2015.13
State	Published - Jan 29 2015
Event	16th IEEE International Symposium on High Assurance Systems Engineering, HASE 2015 - Daytona Beach, United States Duration: Jan 8 2015 → Jan 10 2015

Keywords

TL program transformation
Verilog
synthesis

ASJC Scopus subject areas

Software
Safety, Risk, Reliability and Quality

Access to Document

10.1109/HASE.2015.13

Cite this

@article{5b272df8610244ada7a00f7e3c6bd646,

title = "Verilog Synthesis in the Higher-Order Transformation Framework of TL",

abstract = "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.",

keywords = "TL program transformation, Verilog, synthesis",

author = "Victor Winter and Shiraz Hussain",

note = "Publisher Copyright: {\textcopyright} 2015 IEEE.; 16th IEEE International Symposium on High Assurance Systems Engineering, HASE 2015 ; Conference date: 08-01-2015 Through 10-01-2015",

year = "2015",

month = jan,

day = "29",

doi = "10.1109/HASE.2015.13",

language = "English (US)",

volume = "2015-January",

pages = "26--35",

journal = "Proceedings of IEEE International Symposium on High Assurance Systems Engineering",

issn = "1530-2059",

publisher = "IEEE Computer Society",

number = "January",

}

TY - JOUR

T1 - Verilog Synthesis in the Higher-Order Transformation Framework of TL

AU - Winter, Victor

AU - Hussain, Shiraz

PY - 2015/1/29

Y1 - 2015/1/29

N2 - 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.

AB - 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.

KW - TL program transformation

KW - Verilog

KW - synthesis

UR - http://www.scopus.com/inward/record.url?scp=84936884815&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84936884815&partnerID=8YFLogxK

U2 - 10.1109/HASE.2015.13

DO - 10.1109/HASE.2015.13

M3 - Conference article

AN - SCOPUS:84936884815

SN - 1530-2059

VL - 2015-January

SP - 26

EP - 35

JO - Proceedings of IEEE International Symposium on High Assurance Systems Engineering

JF - Proceedings of IEEE International Symposium on High Assurance Systems Engineering

IS - January

M1 - 7027411

T2 - 16th IEEE International Symposium on High Assurance Systems Engineering, HASE 2015

Y2 - 8 January 2015 through 10 January 2015

ER -

Verilog Synthesis in the Higher-Order Transformation Framework of TL

Abstract

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this