We started our use of
formal methods by verifying an in-house developed IP called the Sensor
Control Block (SCB). This design periodically monitors on-chip
temperature and generates the appropriate power control interrupts to
enable circuit switch-off.
The SCB is well specified and well
understood, so it was a good test case for our first steps in formal.
The SCB enabled us to identify formal’s complementary added value to the
constrained random approach. Also, the SCB is small enough to avoid the
state-space explosion problem — an undesirable complication for our
initial study. The block had been extensively unit tested by the
designer prior to verification. In addition, we developed a constrained
random test-bench so that we could compare the two approaches.
used JasperGold to check the APB interface; the interrupt properties;
the min, max and averaging functionality; the output signals and the
register interface (see Figure 2).
Figure 2: Formal proof status during a run on the Sensor Control Block
green areas indicate the proportion of properties that have been proved
while yellow denotes the properties that have not yet been evaluated.
Red areas show properties that have failed. Each failed property is
accompanied by a counter example that can be analyzed to understand the
We found three bugs, all in the
first week of using formal. One bug was a problem with the ‘PREADY’
signal on the APB interface. This issue had not been previously detected
despite constrained random testing. The second bug was an RTL problem,
namely an erroneously inverted ‘or’ concatenation on the sensor overflow
/ underflow bits. The third problem was a specification error. Two
registers were specified as requiring a ‘Write 1’ to be cleared,
whereas, the desired (and verified) behavior was that these registers
were also clearable by writing 0.
In the case of the SCB, our
constrained random test-bench detected only one further issue of
significance in addition to those found by the formal tool. Moreover, it
took approximately seven engineer-weeks of development for the
constrained random test-bench to reach sufficient maturity. By contrast,
formal methods discovered three bugs within the first week of use, and
produced a list of Property Specification Language (PSL) properties that
can be embedded in the RTL. These properties can now be reused in both
the system-level verification and the SoC integration.