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.
> 


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