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

Erik,

 

Please check your example #3.

 

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);

...

// p1 inherits clock and disable from calling context

p1: assert property (a);

        always @(posedge clk2)

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

p2: assert property (b);

...

Endchecker

 

It appeared to me that you were inheriting the clk2 signal and clock
from the RTL in which it is instnatiated (similar to the way a vunit
does).  I would now expect that the interface would have a clk2 signal
in it.  I also would have expected the interface to pass in the disable
and clk using default inferred arguments, and the assertion statements
to have these present in them or the default define.  For debug
purposes,  I do not want to have to go up a level in the hierarchy to
see what is used.  I would want it as a port.).   

 

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.