Defining an enhanced RTL semantics

Author

Zhao, Shuqing ; Gajski, Daniel D.

Author_Institution

Center for Embedded Comput. Syst., California Univ., Irvine, CA, USA

fYear

2005

fDate

7-11 March 2005

Firstpage

548

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Design, Automation and Test in Europe, 2005. Proceedings

ISSN

1530-1591

Print_ISBN

0-7695-2288-2

Type

conf

DOI

10.1109/DATE.2005.111

Filename

1395624