Verification in Verilog

[Vinilkant Tejaswi]

I am have written and tested an AHB[ARM sytem bus] arbiter in verilog
and have tested using simple tests. Here is the problem

For arbiter
Since the arbiter has lot of signals as inputs and outputs. I can
generate stimulus quite easily. The input signals eventually goes
through lot of different states. I am going to write assertions for
them in vera.

Q1. How to write the response generator or monitor for this ? or How do
you generate the expected response to compare against the actual
response for correctness ? I have read some books/[chapters] on
verification I still dont see how to generate these response

Q1a. Should the assertions be embedded into the module or they should
be separate from the actual module and binded. Please share your
experience ?

Q2. How does one know when to use Vera, or System Verilog or SystemC.
Is it based on the comfort factor or other criteria.

Q3. I also want to know if there are reference testbenches[self
checking testbenches or stimulus and response monitors] that I can look
at. If some body can provide a complete example, I would greatly
appreciate.



-vinil

 

[Vinilkant Tejaswi]

I check that out, but my problem is that I want to learn about
assertions and write my code. This would serve as part where I can
connect other devices like SRAM, SDRAM, DMAC, mips core. These are the
independent work done by me.

That is proprietary and I wonder if I can get it only to test it, not
for business reasons. Transeda, is the one that developed verification
methodology manual based on their verification navigator. Licensing
for that software is another issue, as I cant pay them for that
software.

 

[Neo]

Here are my opinions about your questions:
(1) of course as pointed in earlier post you need to have a behavioral
model for your arbiter which you can take as reference. this is
particularly needed if you are resorting to random stimulus. The model
can be in any high level language of your choice. it need not also be
cycle timed.
(1a) The assertions need not be in a seperate assertion file if its one
person doing both but depending on your design complexity and reuse you
might think on alternatives.
(2)vera or systemC or Sv can only be decided depending on what your
desing environment is and how comfortable you are in using them all can
do your job.

 

[Alex]

I don't think that there is a need to model an arbiter to verify it.
Modeling low-level circuitry such as AHB arbiter will lead you to yet
another RTL-like implementation, and then comparing between the two of
these implementations.
There are two problems with this approach:
1. There is no guarantee, that second "golden" implementation in more
functionally robust that the first one
2. The basic properties of arbiter still remain unverified.

In general, there is low value of doing verification for
"implementation vs. yet another implementation". There is much more
value of doing verification for "implementation vs. specification",
where specification contains implementation-independent higher-level
properties.

For arbiter, general properties may be:
- after reset, all sgnals/registers get correct reset values
- always there is at most one grant
- no grant is given, while bus is busy
- there is no grant without request
- request eventually leads to grant
- each request gets it's grant fairly

It is possible to formalize these properties as an assertions and run
constraint-random sims to verify them.
However, formal model checking is the best way to completely verify the
arbiter properties.
As an introduction to formal verification of arbiter properties, you
may look at priority example included into the Cadence SMV
distribution:

http://www-cad.eecs.berkeley.edu/~kenmcmil/smv/

Regards,
Alexander Gnusin

Vinilkant Tejaswi wrote:

arbiter in verilog
and have tested using simple tests. Here is the problem

For arbiter
Since the arbiter has lot of signals as inputs and outputs. I can
generate stimulus quite easily. The input signals eventually goes
through lot of different states. I am going to write assertions for
them in vera.

Q1. How to write the response generator or monitor for this ? or How
do
you generate the expected response to compare against the actual
response for correctness ? I have read some books/[chapters] on
verification I still dont see how to generate these response

Q1a. Should the assertions be embedded into the module or they
should
be separate from the actual module and binded. Please share your
experience ?

Q2. How does one know when to use Vera, or System Verilog or SystemC.
Is it based on the comfort factor or other criteria.

Q3. I also want to know if there are reference testbenches[self
checking testbenches or stimulus and response monitors] that I can
look
at. If some body can provide a complete example, I would greatly
appreciate.



-vinil