The rtl++ language, semantics, and program verification
Shuqing Zhao, Daniel D. Gajski · 2005
Hardware design and verification based on traditional RTL HDLs has not been able to meet the productivity demand driven by the increasing complexity of ASIC/SoC and has also been a major source of chip failures. In this dissertation we propose a behavioral RTL design description language: RTL++. The synchronous language raise the usual RT level of abstraction by natively supporting modeling of pipelined and/or multi-cycled operations. In order to avoid ambiguity we use a formal structural operational semantic framework to define the execution semantics of RTL++. We also define a formal RFSM model that extends the FSMD model of computation such that multi-cycled or pipelined operations can be reasoned within the RFSM framework. The simulation of programs in RTL++ is achieved by translating them to SystemC which is extended to support the new RTL++ variable types. The fully synthesizable language is aimed to enable design-for-verifiability as well. The compiler control flow analysis of the program can extract a cycle block transition graph from which a FSM model abstraction of the program is generated and used to extract temporal characteristics of the RTL++ program. The all states and all transitions coverage properties are generated as CTL formulas and formally verified by model checker NuSMV. In addition data flow properties such as proper def-use of register〈 i,l〉 type of variables are generated as RTCTL formulas and formally checked.