Specification-oriented hardware design tools
LEVETATE Design Systems is an EDA Company developing hardware verification technology that addresses the problem of ensuring correct RTL designs. Our two major projects are LevBencher V&V, a test bench generation system nearing its beta release, and LevChecker V&V, a formal verification system being developed under a Small Business Innovation Research (SBIR) Contract with the NASA-Langley Research Center. LEVETATE's mission is to raise hardware design focus to higher levels of abstraction through the research, development, and marketing of specification-based design tools. As depicted in the following figure, this activity progresses through three distinct phases that increase the level of design automation and rigor over today's labor-intensive simulation methods. The first step employs formal specifications written in the LEVETATE-developed Versatile Interface Language (VIL). These specifications define expected design behavior with respect to a set of required properties. Properties are boolean-valued formulas representing statements such as: "every request shall be granted within 128 clock cycles" and "the bus master shall be at high impedance while the target drives data onto the bus." Such statements over intervals of time cannot be represented very well using Verilog or VHDL. The final two steps in the figure use VIL for abstraction models, with Verilog or VHDL behavioral models serving as specifications. Here, VIL models provide the linkage between designs expressed at the RTL and these behavioral specifications, where behavioral signals are defined with respect to RTL signals and vice versa. These mappings represent statements such as "the address is the value on the AD bus at the beginning of the transaction" and "the WR signal is low at transaction start for Read transactions." These definitions over signals expressed at different levels of data and temporal abstraction cannot be accomodated very well using Verilog or VHDL.
The use of a formal specification/abstraction language (SAL) such as VIL is fundamental to achieving substantial improvements in design automation and rigor. LevBencher and LevChecker both employ VIL specification and abstraction models in implementing RTL design verifications against property specifications and behavioral specifications, respectively. These activities are represented by the property verification and behavioral verification steps within the above figure. The right-most behavioral synthesis step is a natural follow-on to LevChecker. Future work on LevDesigner is expected to produce a behavioral synthesis tool operating over specification models common to LevChecker and LevBencher.
|
