David Jeffrey Ljung Madison
Verification Engineer Success Stories
Formal Block Verification
Background
My favorite success story with formal verification was when I was
working for a CPU design company in Silicon Valley. This was for
a high performance pipelined, superscalar CPU used in a PC/laptop
as opposed to an embedded CPU, so the design was fairly complex.
I was given two chip blocks to verify (the CPU was divided into
blocks the size and complexity of an ALU unit).
Environment
I created a test environment for both blocks that I like to call
"formal testcase" with "directed random" testing.
It consisted of:
- A golden, cycle-accurate model of each block, written in
behavioral verilog
- A 'piping/decoding' unit which allowed me to write my
tests in verilog as a series of assembly instructions,
and then allowed the results to be depiped for easy comparison.
- Directed Random: A set of random 'templates' that would randomly generate a 'type'
of test that followed a template, i.e., a random addition,
a random number of cycles, then a random branch cancel..
- Formal Testcases: A set of formal 'templates' that would formally test a
set of instructions, i.e., all addition instructions followed
by all dependent subtraction operations.
The formal tool I used at this site was ESP created by Innologic
but in purely formal mode (not using the random hybrid capabilities).
This was not just used for testing a simple set of design assertions,
this did a complete formal check of the golden model versus the block
for a given 'testcase.'
The reason for choosing a split approach was because:
- We were evaluating the formal tools and I didn't want to
put all my eggs in one basket just yet
- It had a faster turnaround - abour 1 hour - to do a "full"
run on block updates
I believe that a pure formal solution could also have worked - but
at that time Innologic did not have coverage analysis.
Capabilities
Every time a block change was checked in, I could run my entire suite
of directed random and formal tests in about an hour. I was usually
able to root-cause and file bugs faster than they could get fixed.
Results
In the end, this process turned out to be even more successful than
I hoped. Usually about half of the verification of a CPU happens
after the first CPU designs are fabricated, in 'post-silicon' - where
your turnaround time for a design is very high, but your test run time
is orders of magnitude faster.
The above methodology of directed-random combined with formal testcases
found a mass of bugs in the pre-silicon phase. In fact, exactly
zero bugs were found in post-silicon, the blocks are clean.
In all my years of working with CPU verification, I had never heard of a
block where all the bugs were found in pre-silicon. If you know of a
situation like this, please
contact me and let me know what your methodology was!
Post-Mortem
The good news is that the chip went into production and could be found
in a number of high-profile laptop designs. To date, exactly zero
bugs have been found in the blocks that I verified with this methodology.
Interested in having a success story like this at your company?
Consider hiring me to see
how it can be done.
