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

Hi guys-- I think I've just about caught up with my email.  
One issue that sticks out as possibly requiring further discussion is
the probelm of a potential 'always' within an 'always'.  
 
Lisa's example below shows a good reason we need to allow this, to meet
our goal of enabling generalized OVL-like libraries:  'mycheck' can now
be used both outside an always loop (like current OVL checkers), and
inside an always loop.  If we did not allow the always within a checker,
we could not do this.  I believe the semantics we currently had in mind
is that the new always completely overrides the previous context.
 
However, as I stare at this, I'm wondering if this may lead to some
counter-intuitive results.  For example. suppose a DE has been given a
library including the 'mycheck' below (without the default_disable), and
uses it in the following code:
 
always @(posedge clk or negedge rstnn)
    if (!rstnn)
        mycheck(foo,bar,clk);
 
A reasonable designer might think they have accounted for the reset
case, since the checker is inside an 'if (!rstnn)'. But from the
proposal as we have it now, it looks to me like p2 will be checked even
during reset.
 
Perhaps this is unavoidable if we want to support 'always' within
checkers.  A bit ugly, but with a correctly written checker library that
handles all the inferred values reasonably, it should be fine.  On the
other hand, is there a better way to define things & make these cases
simpler?    
 

________________________________


default disable my_disable;

always @(posedge clk) begin

...

// checker will inherit posedge clk, my_disable

mycheck mycheck1(.a(a),.b(b));

...

end

...

checker mycheck(a,b, clk2, clk = $inferred_clk, rst = $inferred_rst);

 

default disable rst;...

// p1 inherits clock and disable from calling context

p1: assert property @(posedge clk) (a);

 

        always @(posedge clk2)

          // No inferences here, since inside new always block.

           p2: assert property (b);

...

Endchecker

 

 

The other thing that makes this complex is in essence having an always
block within an always block. How does this work?  Is it only when both
events occur?  Is it legal to have different clocks? 

 

I think the example that Dimitry sent was very simple and clear.  

 

Lisa

 

________________________________

From: Lisa Piper 
Sent: Monday, July 23, 2007 3:23 PM
To: 'Seligman, Erik'; sv-ac@eda-stds.org
Subject: RE: [sv-ac] Feedback on 1900 (new 'checker' construct)

 

Erik,

 

I have reviewed the checker proposal. The application and use model for
this is still not clear to me.  How does this compare with using
parametized properties in a package? My biggest concern is that this is
yet another way that things could be done. The average user is going to
become overwhelmed with trying to understand the alternatives. 

 

More specific questions:

1.              You state that it is similar to a PSL vunit, A PSL vunit
is essentially an extension of the module scope.  It has the advantage
over SVA bind that you do not have to bundle the code into a module with
a complete port list.  The signals in the vunit connect to the signals
of the same name in the associated module.  But you still need to know
the names of the signals in the design, which resticts re-use. And it
does not allow for instantiating a checker in procedural code as you
have shown in these examples.  (Note that PSL is adding parameter lists
to vunits to address the reuse issue.)

2.              How will checkers be documented to make the use easy?
Is it only the clock and disable that can be inferred from context?  How
does the user know what will be inferred?  It would be very confusing
from a debug perspective if some properties do infer and some do not, as
shown in example 3. My fear is that it will be as difficult to learn
libraries as it is to just learn the underlying language.

3.              To debug a failure, won't the user need to be able to
understand SVA? Is the goal of the user not needing to understand SVA
realistic or desired?

4.              This will allow always blocks within always blocks,
where the top level always block has what effect? 

5.              Instantiation of a 'checker' inside an 'always' block
makes this equivalent to a kind of module inside an always block. This
is against the Verilog language in general. It also allows user to put
things inside an always block which are not otherwise legal in Verilog
(e.g assign statements). This will make things confusing without any
real benefit.

6.              There is a statement that checkers may not include
module, interface, or cell declarations or instantiations.  What is a
"cell"?

7.              In example 4, is this PSL?  Will PSL be allowed in a
checker?

        ovl_width_a1:  assert always ((checking & !test_sig) |-> (t >=
width))

 

8.              How is a free variable different from a local variable?

 

The bottom line is that I do not see any compelling reason for this new
construct. 

 

Lisa

 

-----Original Message-----
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Seligman, Erik
Sent: Monday, July 23, 2007 2:54 PM
To: sv-ac@eda-stds.org
Subject: [sv-ac] Feedback on 1900 (new 'checker' construct)

 

 

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!

 

-- 

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.