Title :
Defining an enhanced RTL semantics
Author :
Zhao, Shuqing ; Gajski, Daniel D.
Author_Institution :
Center for Embedded Comput. Syst., California Univ., Irvine, CA, USA
Abstract :
In this paper, we formally define an enhanced RTL semantics. This is intended to elevate the RTL design abstraction level and help bridge the HDL semantic gap among synthesis, simulation and formal verification tools. We define the enhanced semantics based on a new RTL++ language that supports pipelined operations using a new pipelined register variable concept. The execution semantics of RTL++ is specified in a structural operational semantics style aimed at forming the basis for related simulation and formal verification algorithm development. An RFSM model is defined to support natively the synthesis semantics of RTL++. We also present an example of extending SystemC to support the notion of a pipelined register variable.
Keywords :
formal verification; hardware description languages; high level synthesis; logic simulation; pipeline processing; programming language semantics; system-on-chip; HDL; HDL semantic gap; RFSM model; RTL design abstraction level; RTL++ execution semantics; RTL++ language; SoC design; SystemC; enhanced RTL semantics; formal verification tools; hardware design language; high-level synthesis; logic simulation; logic synthesis; pipelined operations; pipelined register variable; structural operational semantics; Application software; Automatic control; Bridge circuits; Circuit simulation; Computational modeling; Data engineering; Embedded computing; Formal verification; Hardware design languages; Logic design;
Conference_Titel :
Design, Automation and Test in Europe, 2005. Proceedings
Print_ISBN :
0-7695-2288-2
DOI :
10.1109/DATE.2005.111
