loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Design, Automation and Test in Europe (DATE'05) Volume 1
Defining an Enhanced RTL Semantics
Munich, Germany
March 07-March 11
ISBN: 0-7695-2288-2
Shuqing Zhao, University of California, Irvine
Daniel D. Gajski, University of California, Irvine
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 to form the basis for related simulation and formal verification algorithm development. A 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 pipelined register variable.
Citation:
Shuqing Zhao, Daniel D. Gajski, "Defining an Enhanced RTL Semantics," date, vol. 1, pp.548-553, Design, Automation and Test in Europe (DATE'05) Volume 1, 2005
Usage of this product signifies your acceptance of the Terms of Use.