I was given two chip blocks to verify (the CPU was divided into blocks the size and complexity of an ALU unit). Both of them were verified using the described methodology.

- A golden, cycle-accurate model of each block, which I wrote in
*behavioral verilog* - A 'piping/decoding' unit which allowed me to write my
tests
*directly in verilog*yet 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,.. so forth -
**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 (since acquired by Synopsys) 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 (about 1 hour) to do a "full" run on block updates

As a simple example of how the ESP tool works, consider a simple 16b adder without carry-in/out:

_____ A --| | |Adder|--> C B --|_____|The first step in testing this block formally, we need to symbolize the inputs:

initial $esp_var(a,b);

Since a golden model needs to be written that correctly encapsulates the expected behavior, a design specification needs to be complete. In writing the golden model according to the spec we were able to find bugs and ambiguities in the spec that could be cleared up before simulation had even begun.

To continue our hypothetical case above, our simple golden model is: (a+b) & 16'hffff

To test this, we simply formally look for a set of symbols where these conditions are not met:

initial begin $esp_var(a,b); #10; exp_c = (a+b) & 16'hffff; if (c !== exp_c) $esp_error("Found adder failure: "); endThe ESP simulator would symbolically simulate both the block under test and the golden model. If there were any possible symbols that fulfilled the '!==' conditional which triggered the $esp_error call, then we would see the error as well as a possible set of inputs to create it.

In the simple adder example above, let's imagine that the A and B inputs are actually 32b inputs to the block, but we are only testing them as 16b in the adder. In this case we can immediately cut down on the symbol space by:

a = a & 16'hffff; b = b & 16'hffff;Which suddenly makes the top bits of the symbols irrelevant.

In reality, the cases are not this simple, and we need to find other ways to manage the symbol space. Control signals cause the most problems, since they generally cause the largest expansion of formal paths. Apart from masking off bits that we don't care about, we can also try to find inputs that are not generally interrelated and test them separately. To accomplish this with the blocks, I had a number of formal 'test cases,' each one would symbolize a different set of inputs and then randomize the other inputs. Then running each of the formal tests a small number of times would be enough to find bugs in the design. Obviously this is riskier than doing a formal simulation with all inputs completely symbolized, but since such a full case was impossible, we resorted to subdividing the problem and then using the random-directed tests as a backup.

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 have been found in post-silicon. The blocks are **clean**.

In all my years of working with CPU verification, I had never heard of a case where all the bugs in a block were found in pre-silicon. If you know of a situation like this, please contact me and let me know what your methodology was!

Interested in having a success story like this at your company? Consider hiring me to see how it can be done.