FoCs Property Checkers Generator
A productivity tool for automatic generation of simulation monitors from formal specifications.
Date Posted: November 18, 2002
|
|
 |
|
 |
|
|
|
A property (also known as a "rule" or "assertion") is a description of a required behavior of the design. Typically, properties are derived from the design specification documents, where they are informally written in English. Once the properties of interest are identified as target properties for FoCs Property Checkers Generator, they are formulated in Sugar, which is the input language of the tool. Note that in this context we are concerned solely with functional properties, that is, requirements and restrictions on design function. This is different than what are sometimes called "design rules," which pertain to the form and structure of the design.
As an example of a property, consider a requirement that prescribes that if there are five consecutive clock cycles, where the request signal is asserted and not acknowledged, then the busy_flag should be set on the fifth cycle. The Sugar formulation of this property is as follows: {[*], {request & !acknowledge}[5]}(busy_flag)
| | |
|
The input for FoCs Property Checkers Generator is a file with properties written in the Sugar language. Another optional input is a file that defines the mapping between the names of the signals in the design and the names used in the properties file.
The output of FoCs Property Checkers Generator is a checker file written in VHDL or Verilog.
Optionally, FoCs Property Checkers Generator produces files with code fragments for instantiating the checkers. These code fragments are used to ease the connection of the checkers to the simulation environment.
| | |
|
Manually writing checkers in Verilog/VHDL or C/C++ is a very time-consuming and error-prone process. In contrast, the conciseness and expressive power of Sugar on one hand, and the automation of FoCs Property Checkers Generator on the other, enable the generation of correct-by-construction checkers which are easy to create, debug, and reuse. Additionally, FoCs Property Checkers Generator supports the sharing of Sugar properties between formal verification (FV) and simulation. Experience in many projects has demonstrated productivity improvements of up to 50% in the verification effort, as well a significant increase in verification coverage and quality.
| | |
|
Verilog and VHDL (availability of C/C++ expected in 2003).
| | |
|
Naturally, adding any checking code to simulation adds some overhead to the simulation process. The level of overhead depends on the number of properties embodied in the checker. A reasonable use of FoCs-generated checkers will slow simulation by 10% to 20%. | | |
|
FoCs Property Checkers Generator is very easy to install and use. It has a simple GUI which makes the process of generating a checker as simple as pressing a button. All user-defined settings are simple and can be defined via the GUI. It is actually quite simple to learn the subset of Sugar that is sufficient for writing useful checkers. Most properties can be easily described using a single Sugar construct that defines sequences of events. These sequences may be regarded as a textual representation of a timing diagram, and are therefore very intuitive for designers. | | |
|
There are several advantages to using FoCs-generated checkers in the simulation of designs that were previously formally verified against the same Sugar properties:
- Often, the input constraints (a.k.a. environment models) defined for formal verification are more restricted than the real environment modeled in simulation. Thus, in simulation, one can exercise the design against inputs whose effect on the design has not been explored by FV. It follows that the enhanced checking capability of FoCs Property Checkers Generator provides better coverage and greater confidence in the quality of verification.
- FoCs checkers can help find problems in the input constraints defined for FV. For example, if the results of FV and simulation (relative to the same properties) do not agree, it is likely that the input constraints for FV were not correctly defined.
- Using FoCs Property Checkers Generator, users can validate the assumptions made in the FV process. These assumptions can be formulated as Sugar properties, translated by FoCs into checkers, and then checked during simulation.
| |
|
|
|
|
| |
