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

From: Thomas Thatcher <Thomas.Thatcher_at_.....>
Date: Tue Jul 24 2007 - 14:22:05 PDT
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.
Received on Tue Jul 24 14:22:21 2007

This archive was generated by hypermail 2.1.8 : Tue Jul 24 2007 - 14:22:30 PDT