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

Hi Ed,

That is a good idea.  That could make our checkers more impervious to race
conditions.

My example illustrates how we write checkers today.  Of course, we don't have
the checker construct, so we use modules and binds to bind the modules to the
design.  But this approach works today with both simulation, and all of the
formal verification tools we work with.

I am soliciting feedback from others in Sun regarding this proposal.

Tom

Eduard Cerny wrote On 07/24/07 06:43 PM,:
> 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.
>>
>>

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