Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Date: Wed, 26 Apr 95 22:41:31 BST
From: Mike.Gordon@cl.cam.ac.uk
Message-Id: <9504262141.AA02884@skua.cl.cam.ac.uk>
To: info-hol@leopard.cs.byu.edu
Subject: design verification of the PowerPC


The article below from comp.lang.verilog might interest people working
on the formal verification of processors (see last paragraph).

Mike Gordon
http://www.cl.cam.ac.uk/users/mjcg/

N.B. gordon@eden.com is no relation (and unknown) to me.
===

-----------------------------------------------------------------------
From: Gordon <gordon@eden.com>
Newsgroups: comp.lang.verilog
Subject: Re: Recent article on design verification
Date: 26 Apr 1995 08:34:08 GMT
Organization: Adhesive Media, Inc.
NNTP-Posting-Host: net-1-115.eden.com
Mime-Version: 1.0
Content-Type: text/plain; charset=iso-8859-1
Content-Transfer-Encoding: 7bit
X-Mailer: Mozilla 1.1b3 (Windows; I; 16bit)

I am currently involved in design verification of the PowerPC 
microprocessors. In my frame of reference, the current methods 
and vendor supplied simulation tools are not sufficient for 
the complexity of designs being considered. 
 
Currently the "state of the art" methodologies consist of 
random test generation with a mix of "best guess" test suites. 
In the random test method, a set of instructions is randomly 
generated and then ran against a reference model to generate 
a set of results. The instructions are then ran against the 
model and the results are compared. The implementations of this 
are as varied as there are implementors but the methods fall in this 
category. Some implement the generation, reference model and comparison   
as part of the simulation model, some implement them seperately, to some   
it is a mix. The metric for being done with random testing is not 
satisfying, it is usually so many of something ... 1 billion   
instructions, 1 billion cycles, 1 billion tests but you're never sure 
if you covered that particular state transition or if you divided 
some astronomically large number by some small number in your floating   
point. Can you cross your fingers? By the way, random testing requires   
more CPU time than you will ever have for any large problem especially   
with a simulator like Verilog. 
 
So most of the time we verification types make our best guess at the   
"boundary conditions" for particular problems and the write specific   
tests for them. Things like a miss in the cache while my MMU is doing a   
tablewalk and another processor is hitting on that block int the same   
cycle. This is also not satisfying because you know you missed something. 
The fingers on the other hand are now crossed. For any large problem   
these tests can take many people and hours to write. 
 
On the one hand, you have a methodolgy (random) that is CPU intensive but   
requires fewer people and on the other hand you have a method with   
requires many people and fewer CPU resources. Most DV folk use both   
methods. 
 
My problems with the current vendor simulation tools are they are just   
too slow for large problems using random instruction sequences of any 
significent length. I require a minimum of 30 instructions per second 
to be executed by my model. On a reasonable number of machines that will 
give me 200 million random cycles per day. That is what is required for 
a complex design. This can be done by allowing the simulator to have 
only two logic values - 0 or 1 and by levelizing the logic (no feedback). 
 
Another significent problem is the ability of a simulator to give me   
information about what parts of the design have been covered (no I don't   
mean stuck at fault grading). I mean functional coverage analysis. In   
software they define a heirarchy of coverage metrics. This mostly boils   
down to path coverage or some subset of it. You see, if I have a system   
that is randomly generating tests that cover the same functions over and 
over I probably should re-bias the generator. Most people measure this 
by the number of fails - no fails means re-bias. This directs the testing   
and is utilized in the later stages of verification. 
 
The advent of formal verification may prove to alleviate many of the   
simulation problems by allowing specification languages, model checkers   
and theorem provers do perform the verification of an implementation.