RE: [sv-ac] call to vote on 1698

Hi Jonathan,

Consider the following example:

always @(posedge clk) begin
	...
	if (en) begin
		...
	a1: assert property(req |=> gnt);
	end
end

As Ed wrote, this assertion is equivalent to

a1: assert property(@(posedge clk) en |-> req |=> gnt);

I think that the rationale under the LRM definition was not only to use
sampled value of en, but also to consider en as an enabler signal of the
attempt to start, and not as a mean to gate the clock. It is hard to
tell which definition is more intuitive, probably the LRM definition is
simpler.

The definition you suggest differs from this one in two points, one of
them was mentioned by Ed - that the LRM definition will take the sampled
value of en, while your definition will not. There is one more
difference: consider that at some clock tick both en and req were high,
at the next clock tick en was low and so was gnt, and at the following
clock tick both en and gnt were high. Using the LRM definition the
assertion would fail: there were no gnt at the clock tick of @(posedge
clk) following req, while using your definition the assertion would
pass: at the next tick of @(posedge clk iff en) gnt is high.

Thanks,
Dmitry

-----Original Message-----
From: Eduard Cerny [mailto:Eduard.Cerny@synopsys.com] 
Sent: Sunday, February 17, 2008 4:54 PM
To: Jonathan Bromley; Thomas.Thatcher@sun.com;
john.havlicek@freescale.com
Cc: sv-ac@eda.org; Korchemny, Dmitry
Subject: RE: [sv-ac] call to vote on 1698

Hello Jonathan,

Regarding the inference of conditions from if and case statements, this
is already in the LRM. The enabling condition is inferred from the
conditional path leading to the assertion and is placed in the
antecedent of an implication (not as part of the clock expression
because the values must be sampled the same way as the rest of the
variables in the assertion.)

Best regards,
Ed


> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
> Jonathan Bromley
> Sent: Saturday, February 16, 2008 12:01 PM
> To: Thomas.Thatcher@sun.com; john.havlicek@freescale.com
> Cc: sv-ac@eda.org; dmitry.korchemny@intel.com
> Subject: RE: [sv-ac] call to vote on 1698
> 
> [Thomas Thatcher]
> 
> > I don't quite understand the new rules for inferring clocks from
> > procedural blocks.   For example:
> >
> > In the clock inference section, what does this phrase mean???
> > 	"the event expression is maximal among those of these forms"
> 
> I too had difficulty in understanding this, and I could not see how
> there would be any ambiguity if that requirement were to be deleted.
> 
> I think there are also some missed opportunities about
> disable (reset) inference, but perhaps that would be
> rather hard to define robustly.
> 
> So, here's a very stupid question from someone who's not an
> assertions expert:  Would it not be easier simply to define
> an assertion's clock to occur whenever the flow of procedural
> execution encounters its "assert property" statement?  That
> rule would also allow you to enable and disable the clock based
> on branches of conditionals, a very useful feature that is already
> present in some formal tools:
> 
>   always @(posedge clock) begin
>     assert property (!enable1 |=> $stable(Q1));  // A1
>     assert property (!enable2 |=> $stable(Q2));  // A2
>     if (enable1) begin
>       assert property (Q1 == $past(D));          // A3
>       Q1 <= D;
>     end
>     if (enable2) begin
>       assert property (Q2 == $past(D));          // A4
>       Q2 <= D;
>     end
>   end
> 
> In this example, the effective clocks are:
> for A1 and A2, (posedge clock);
> for A3, (posedge clock iff (enable1));
> for A4, (posedge clock iff (enable2)).
> 
> I'm sure there must be some good reason why you don't wish
> to do that, but it looks a lot simpler to me....
> Loops are OK, because (in synthesisable code) loops always
> occur in zero time in the scheduler's Active region and therefore
> will give rise to only one assertion evaluation (in Observed)
> for each real clock event.  For example, here's a "count ones"
> design, with an assertion to check its behaviour.  The assertion
> is (unnecessarily) placed inside a loop, and so the flow of
> procedural execution passes it eight times in each timeslot
> where there is a clock.  However, that should give rise to
> only one evaluation of the assertion.
> 
>   logic [7:0] y;
>   logic [3:0] count;
>   always @(posedge clock) begin : Count_Ones
>     logic [3:0] n;
>     n = 0;
>     for (int i=7; i>=0; i++) begin
>       n += y[i];
>       assert property (count == $past($countones(y));
>     end
>     count <= n;
>   end
> 
> Thanks, and apologies if this is wildly off.
> --
> Jonathan Bromley, Consultant
> 
> DOULOS - Developing Design Know-how
> VHDL * Verilog * SystemC * e * Perl * Tcl/Tk * Project Services
> 
> Doulos Ltd. Church Hatch, 22 Market Place, Ringwood, Hampshire, BH24
1AW,
> UK
> Tel: +44 (0)1425 471223                   Email:
> jonathan.bromley@doulos.com
> Fax: +44 (0)1425 471573                           Web:
> http://www.doulos.com
> 
> The contents of this message may contain personal views which
> are not the views of Doulos Ltd., unless specifically stated.
> 
> --
> This message has been scanned for viruses and
> dangerous content by MailScanner, and is
> believed to be clean.
> 

---------------------------------------------------------------------
Intel Israel (74) Limited

This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.


-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.