SVa assertion question

P

Paul Richardson

Guest
I am new to the world of assertions, I am tryinng to do the following

sequence/property/assertion which does the following:

I have a bus that is driven to a particular value, if a different bus,
2 cycles later does not assume
the same value, I want to assert that fact , I am trying to figure out
how to construct the sequence/property/assertion code such that I wait
for a value (or at least a non zero value), and if I do not
see that value the sequence/property/assertion combination does not
fire. This a clock based design,
I suppose I could write verilog to do the test for the inital value and
then use sequence/properties
within that verilog to fire an assertion as I described above.

This running under VCS 7.2 with sva switched on, any tips will be much
appreciated


/pgr
 
I'm new to assertions myself, but from my presentation materials you
might try:

parameter VALUE = 55;

property bus_set;
@ (posedge clk) bus1 == VALUE |-> ##2 bus2 == VALUE;
endproperty

bus_test: assert property bus_set;

Property says: at every rising edge of clk, if bus1 is the value I'm
looking for, two clocks later bus2 must be that same value (note that
value is hard-coded.) Property is recursive so multiple VALUE on bus1
will be checked for on bus2.

If you need a free-running compare, perhaps:

sequence s1;
bus2 ##2 $past(bus1,2);
endsequence

property p1;
@ (posedge clk) s1;
endproperty

bus_test: assert property(p1);

might work, but do not go too deep on $past as it will slow your sim
(e.g. $past(sig, 100).

On Fri, 18 Aug 2006 18:13:24 -0700, Paul Richardson
<prich@earthlink.net> wrote:

I am new to the world of assertions, I am tryinng to do the following

sequence/property/assertion which does the following:

I have a bus that is driven to a particular value, if a different bus,
2 cycles later does not assume
the same value, I want to assert that fact , I am trying to figure out
how to construct the sequence/property/assertion code such that I wait
for a value (or at least a non zero value), and if I do not
see that value the sequence/property/assertion combination does not
fire. This a clock based design,
I suppose I could write verilog to do the test for the inital value and
then use sequence/properties
within that verilog to fire an assertion as I described above.

This running under VCS 7.2 with sva switched on, any tips will be much
appreciated


/pgr
 

Welcome to EDABoard.com

Sponsor

Back
Top