Subject: Re: FW: Minutes of Assertion meeting 3/21/02
From: Adam Krolnik (krolnik@lsil.com)
Date: Thu Mar 28 2002 - 15:58:38 PST
HI Harry;
You asked:
"Isn't the goal with the delay mechanism to provide a succinct
way or creating an expression, without having to build an RTL pipe
stage to trap previous expression values?"
Yes - this is the goal.
Using your example, (I like the syntax - I remember a tool I
once wrote...) but I would like to invert it (it fails if the expression
does occur.)
assert_forbid ((a^b)<-2> & (a==b));
Which I would have to code now like:
reg assert0015_delay[1:0];
always @(posedge clk) // hopefully
begin
...
assert_forbid (assert0015_delay[1] & a == b);
//synthesis translate_off
assert0015_delay = {assert0015_delay[0], a^b};
//synthesis translate_on
...
Is this equivalent to?
assert (a^b; 1; a==b);
Yes, is it equivalent in the inverted case? No the equation is
longer.
There are two other forms where they are not equivalent.
1. obtaining a vector value from the past
assert (address<-2> == address)
@@(posedge clock);
This is not covertable to a expression sequence.
2. Implication (or fancy if() ) functionality.
So many temporal assertions require implication before
the expression can be checked.
assert (req_valid triggers in_address<-1> == in_address)
@@ (posedge clock);
I used 'trigger' as a fancy if - if you prefer the other way:
if (req_valid) assert (in_address<-1> == in_address)
@@ (posedge clock);
If there is a request valid, I want to compare the previous address
to the current. Note, the previous address is the address before
the sampling of req_valid.
Your last statement is worth debating:
"Of course relating a sampling event to the expression [of
the delay mechanism] is an issue."
If you can assign the @@(posedge clock) statement as the sampling
event in a sequence, then why can't you assign the same sampling
event to the delay mechanism. Maybe I should be proposing a
syntax to identify past and future values of a signal?
Then one could write
a<-2> & b<-1> & c
or
a & b<1> & c<2>
depending on how they think...
I.e.
transient_expr ::=
expression '<' time_cycle '>'
;
time_cycle ::= integer ;
regexp ::= <boolexp>
| transient_expr
| ...
;
Adam Krolnik
Verification Mgr.
LSI Logic Corp.
Plano TX. 75074
This archive was generated by hypermail 2b28 : Thu Mar 28 2002 - 16:00:05 PST