Processor Verification Methodolgies

miket · Posted: Fri Aug 12, 2011 8:33 am **Post subject:**

One key concept here is that to verify a processor, you don't really need to generate programs. This may be counter-intuitive, but its true. What you need to develop is a set of rules that define legal and illegal instruction sequences. That is, given the last instruction, and the state of the DUT (e.g. which GRS are in use, and which are free), what are the rules for generating the next legal instruction? For exception testing you'll then need to have rules for illegal instructions as well. In a constrained-random environment, these rules are implemented as constraints on random variables of a data class that models an instruction. The paper I referenced provides a good introduction to this.

That takes care of generation. You'll also need a Reference Model (RM) to predict what the processor will do with these instructions. The good news is that the RM need not be very complex. Try to avoid any cycle-accurate modeling. If you think you must have cycle timing in your RM, ask yourself if an Assertion in the RTL would do the trick.

Lastly, you'll need functional coverage to ensure you generated all the instructions, operands and combinations you could think of.

The beauty of this approach is that is it much less work to generate the constraints, simplified RM, RTL Assertions and functional coverage than it would be to generate all the 'real' programs (directed tests) required to verify the processor.

Let the tools do the work for you. Really. This shit works - I'm not making it up.

---mike

alexg · Senior Joined: Jan 07, 2004 Posts: 586 Location: Ottawa

IBM accumulated over 20 years of experience developing tools for processor verification. One of important concepts in their tool is an existence of "Testing Knowledge". This is, in fact, the set of smart and not-obvious constraints that express previous experience with processor verification.

I would recommend to read more about Genesys and Genesys- Pro tools from IBM:

https://www.research.ibm.com/haifa/projects/verification/genesys_pro/i
ndex.shtml

https://www.research.ibm.com/haifa/projects/verification/genesys.html

Regards,
-Alex

tblackmore · Posted: Wed Aug 17, 2011 12:58 am **Post subject:**

I certainly meant to recommend a constrained-random verification approach, among others. An Instruction Stream Generator should be CRV.

I'd also strongly agree with a couple of subsequent remarks. It's no good trying to generate programs. You need to find corner cases that would take far too long to find with application-like scenarios. And to find these corner cases it's important to build knowledge into your constraints based on the experience of those in the processor development team (including verification engineers) and any other infomation that you can access, just as IBM have done over the years. Thus for instance you would want to ensure the clashing of synchronous (e.g instruction execution) and external asynchronous events (e.g. interrupts) far more than you may get in real applications.

I also agree tha tthe trade-off between a cycle-accurate model and an architectural Instruction Set Simulator in terms RFE would usually favour the ISS, although this is likely to lead to some limitations in how well you can verify the interaction of synchronous and external asynchronous events.

fredinashed · Junior Joined: Oct 19, 2009 Posts: 9

Thanks for continuing my original post, it has been very informative. From what I have gathered most of the effort needs to focus on the rules used to generated the random stimulus. I feel that without previous experience in generating these rules it might be quite an interesting an steep learning curve.
In regard to the IBM tools, is it a case of just a case of telling the tool about he opcodes for your target processor, and the tool has a set of test it is able to run?

I am looking at using systemc to create a reference model for the design as this can be transaction based rather than cycle based. Has any one used systemc for this purpose?

I am also looking at some floating point tests, There seems to be a wealth of standard test available, does anyone have any recommendations ?

fredinashed · Junior Joined: Oct 19, 2009 Posts: 9

Hi jim,
Thanks for the link to the packages I had already downloaded them prior to you post, hopefully I will find a use for them.

On a separate note, I tried to join the vhdl email reflector but was not able to, does it still function?

miket · Posted: Mon Aug 22, 2011 8:51 pm **Post subject:**

You can tell that I've got a lot of energy around this one. Very Happy

I just get so depressed watching people fall into the trap of doing it the bad-old-fashioned-way because they are worried about the learning curve.

So about that learning curve. You are going to have to climb it no matter what. One way or another you will need to understand the rules that define the generation of legal (and illegal) op-codes. There really is no other way to get this thing verified. Once you have that, the next question is, how are you going to express it in a machine readable form that you can use to verify the DUT? One way is to write a set of several hundred (thousand?) directed testcases. Another way is to write a set of properties for a formal tool. Obviously, I am advocating for writing a set of constraints... it is the easiest of the three. The learning curves as pretty much the same.

One last thing: before you introduce a new language to the mix, consider using your "native" language to write that transaction based reference model. SystemC is great for that stuff, but so is SystemVerilog or VHDL.

---mike

fredinashed · Junior Joined: Oct 19, 2009 Posts: 9

Hi miket, you are right, I have been seduced by the lure of SV over my 'native' language of VHDL. I think it has been driven by my desire to upgrade my tools to get 2008 vhdl (psl) assertions, at which point I also get SV support.

I think prior to looking at the random packages for VHDL I didn't think it was possible to get random generation in a way offered by SV.

war_isbest · Senior Joined: Dec 05, 2007 Posts: 23

miket · Posted: Fri May 25, 2012 8:04 am **Post subject:**

war_isbest · Senior Joined: Dec 05, 2007 Posts: 23

thanks miket for the post.

cpixley · Newbie Joined: Jun 30, 2005 Posts: 1

This is a reply to a question of fredinashed. One can use the floating point libary to check your hardware implementation, if you have the right tool. At Synopsys we have a tool called Hector for that purpose. Contact your local Synopsys sales person for this.

war_isbest · Senior Joined: Dec 05, 2007 Posts: 23

Dear members,
I have landed in another dilemma. I finished writing the model for ALU. I was thinking about the test cases for the multiplier and divider.

Can anyone please suggest or point to some good test cases or how to approach it for Multiplier and divider units.(The multiplier is booth algorithm based ,divider is non-restoring division).
regards

tblackmore · Posted: Mon Jun 04, 2012 3:13 am **Post subject:**

For the ALU you may want to consider using formal verification, at least in part. If the ALU is combinatorial it will be very easy to write the properties. You may run into capacity issues - especially for the more complex issues - in which case you may only be able to formally verify particular bit-slices (wiht other bits tied to constants). Still this will give you much more coverage than simulating one set of operand values at a time.

For the coverage you need to consider interesting values (or ranges of values for the formal tool) from a blackbox (e.g. 0 as an operand, ...) and a whitebox (where does the implemenation become non-uniform) point of view. Any information you can find on bugs found in similar implementations would be good.

war_isbest · Senior Joined: Dec 05, 2007 Posts: 23

we dont have a full formal verification tool but have a simulator which supports assertions.
Do you intend to say that a model for ALU may not be required and assertions can be used to verify it.
Then we will have to write a model for say control transfer instructions ?
then what type of environment (checker?) do you suggest .
regards

tblackmore · Posted: Mon Jun 11, 2012 12:05 am **Post subject:**

My suggestion requires use of a formal verification tool to get the higher levels of coverage mentioned (due to the fact that the formal tool will explore the behaviour of the design for all input values not explicitely constrained away). I agree there is little value in using assertions to model an ALU unless you are going to use a formal tool - other languages would be a least as good for this.