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

Jonathan,

As another assertion non-expert, I can't answer you well enough, but if
the question is good enough for you to ask, perhaps the LRM should have
a sentence or two explaining it. 

Regarding the loop, I think that Mantis 1995 specifies that the
assertion will be evaluated once for each iteration of the loop.

Shalom 

> -----Original Message-----
> From: owner-sv-ac@server.eda.org 
> [mailto:owner-sv-ac@server.eda.org] On Behalf Of Jonathan Bromley
> Sent: Saturday, February 16, 2008 7:01 PM
> To: Thomas.Thatcher@sun.com; john.havlicek@freescale.com
> Cc: sv-ac@server.eda.org; Korchemny, Dmitry
> 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.