ompaq Computer Corp. has traditionally made extensive use of Verilog simulation to verify its ASIC designs, which has proved very effective for most types of designs. However, there are certain ones that traditional simulation methods cannot verify effectively, including counters, address decoders and exclusive-or trees.
To attack those difficult problems, Compaq has adopted a methodology called static functional verification. This article describes Compaq's experience using the Averant static functional verification tool, Solidify, to completely verify the operation of a 7-bit error-correcting circuit (ECC) generator-decoder for a memory interface design.
Static functional verification allows a designer to completely verify the operation of a design without having to establish a verification testbench or develop simulation vector patterns. Instead, the technique uses a set of properties that describe the behavior of the design to prove proper functionality using formal verification techniques.
The ECC design was required to protect 29 bits of data with single-bit-error correction and double-bit-error detection. A custom ECC algorithm was developed. However, the developer of the algorithm was not available for consultation, which made the verification effort crucial to prove proper functionality.
Exhaustive verification using Verilog simulation would require the circuit to be simulated with every possible 29-bit input data value for every possible 1-bit error and checking that the error had no effect on the 29-bit decoded value. Likewise, every possible 29-bit input data value would need to be simulated for every possible 2-bit error and checking that the error was detected. There are 229 possible input data values.
Since the input data is encoded into a 36-bit value, there are 36 possible bit positions for an error and the error can be either "stuck-at-1" or "stuck-at-0." Therefore, there are 2 x 36 = 72 possible single-bit errors and each of these must be tested for all 229 data values. For 2-bit errors, there are 36 possible bit locations for the first error, 35 remaining locations for the second error and each error can be independently stuck-at-1 or stuck-at-0. Therefore, there are (2 x 36) x ( 2 x 35) = 5,040 possible 2-bit errors that must be tested for 229 different data-values. The total number of tests is then (72 + 5,040) x 229, or about 2.74 x 1012.
To calibrate the magnitude of the number of tests needed to exhaustively verify this design, suppose it had a 100-ns code-decode cycle time when built in hardware. It could then process 107 tests per second, so it would require about 2.74 x 105 seconds, or a little over three days to write and read all the test cases. Emulation speeds are less than 1 percent of real time, so it would take more than a year using emulation to process all of the test cases. At simulation speeds, it would take more than a lifetime.
There are so many test vectors because simulation requires that every signal bit has a specific value-simulation requires fully constrained conditions. Verifying a circuit that processes any combination of values requires a test vector for each unique combination.
On the other hand, static verification naturally processes unconstrained signals. Its starting assumption is that any signal can have any value. Constraints are added to reduce the scope of the proof. Using Solidify, Compaq was able to completely verify operation of the design in a few hours.
In addition to verifying designs that are difficult to verify using Verilog, Compaq has found that static functional verification increases the verification productivity in other areas as well. First, designers are able to verify design functionality early. This allows bugs to be flushed out at the submodule level before the entire design is assembled in a testbench. Designers are able to verify submodules as soon as they are created rather than waiting for all designs to be completed. The earlier bugs are detected and corrected, the less of an impact they have on the verification process.
Second, designers are able to exhaustively prove correct functionality. By creating properties, which exercise difficult corner cases, designers are able to guarantee that the design operates through all modes of operation. Third, the speed at which static functional verification runs allows for quicker results as well as freeing simulation hardware resources.
Compaq has found Solidify to be a very useful tool to implement static functional verification. Design properties are constructed using Solidify's Hardware Property Language. Most properties are verified within a few seconds.
However, Compaq did find that static functional verification is not the magic bullet to solve all verification problems. It does poorly for complex designs where the control is distributed across many design blocks. For these, creating the properties for static functional verification begins to resemble the testbench environment used for system simulation.
Paul Rawlins is a member of the Senior Technical Staff at Compaq Computer Corp. (Houston).
