SVa assertion question - verilog

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