RE: [sv-ac] Feedback on 1900 (new 'checker' construct)

From: Eduard Cerny <Eduard.Cerny_at_.....>
Date: Tue Jul 24 2007 - 18:43:00 PDT
Hi Tom,

I think that you should use $sampled on a and b in the assignmens of
your example to avoid discrepancy between what the assertion and the
asssignments observe.

Best..
ed

> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> Behalf Of Thomas Thatcher
> Sent: Tuesday, July 24, 2007 5:22 PM
> To: Seligman, Erik
> Cc: sv-ac@eda-stds.org
> Subject: Re: [sv-ac] Feedback on 1900 (new 'checker' construct)
> 
> Hi Erik,
> 
> Just putting in writing what I said in the committee meeting today.
> 
> We are in favor of the checker construct, and are very 
> interested in seeing it
> implemented.
> 
> We have the following suggestion:  Allow the inclusion of 
> reg, wire, logic
> variables, as well as always block constructs.  However, any 
> construct within
> a checker should be defined as non-synthesizable, and won't 
> result in extra
> hardware in the design.
> 
> My reasoning is that people writing checker code may be more 
> comfortable with
> that syntax than with the new free variable syntax.  (I will 
> check around Sun
> to see if others agree with me on this).
> 
> For example, we might write a checker like this:
> 
> checker follows (clk = $inferred_clk, a, b);
> 
>     reg a_active = 1'b0;
>     always @(posedge clk) {
> 	if (a) a_active <= 1'b1;
> 	else if (b) a_active <= 1'b0;
> 	else a_active <= a_active;
> 
>     a1 : assert property (!a_active |-> !b);
> endchecker
> 
> 
> 
> This would be pretty much equivalent to this
> 
> checker follows (clk = $inferred_clk, a, b);
> 
>     bit a_active = 1'b0;
> 
>     function bit next_a_active;
> 	if (a) return 1'b1;
> 	else if (b) return 1'b0;
> 	else return a_active
>     endfunction
> 
>     a_active <= @(clk) next_a_active;
>     a1 : assert property (!a_active |-> !b);
> endchecker
> 
> with the exceptions of sampling regions, etc.  Either syntax 
> should work,
> either in simulation or in the formal tools.  In fact, in 
> this case, with the
> if-then-else, the first syntax may be slightly more 
> convenient.  A function
> wasn't needed to contain the if-then-else construct.
> 
> Free variables would have advantages, and advanced people 
> would probably use
> them exclusively, but average designers would have a choice 
> to use familiar
> syntax.
> 
> Tom
> 
> Seligman, Erik wrote On 07/23/07 11:53 AM,:
> >  
> > Hi guys--
> > I'm going to start working on the 'real' proposal (manual 
> format) for
> > item 1900.  Please try to send any feedback you have at this point.
> > Thanks!
> > 
> 
> -- 
> ------------------
> Thomas J. Thatcher
> Sun Microsystems
> 408-616-5589
> ------------------
> 
> -- 
> 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.
Received on Tue Jul 24 18:43:14 2007

This archive was generated by hypermail 2.1.8 : Tue Jul 24 2007 - 18:43:28 PDT