RE: [sv-ac] Mantis 1900. Checkers

Hi Lisa,

 

Please, see my comments below. I uploaded the updated version to Mantis.

 

Thanks,

Dmitry

 

________________________________

From: Lisa Piper [mailto:piper@cadence.com] 
Sent: Saturday, December 01, 2007 7:29 AM
To: Korchemny, Dmitry
Subject: RE: [sv-ac] Mantis 1900. Checkers

 

Hi Dimitry,

 

I am looking athe 1900 checker proposal and have a few
comments/questions:

 

1.     In the following, you accidentally dropped the first line 

 

REPLACE in Syntax 16-16-Concurrent assert construct syntax

 

procedural_assertion_statement ::=

concurrent_assertion_statement

| immediate_assert_statement

 

WITH:

 

concurrent_assertion_statement

| immediate_assert_statement

| ...

 

[Korchemny, Dmitry] Fixed.

 

2.     at the top of page 7, can #2, 4, and 5 be combined to one
reference (#2 and #5 are worded awkwardly)?

1) It shall be illegal to use the freevar type qualifier outside of
checkers.

2) In checkers only always_check constructs may be specified.

3) It shall be illegal for a checker_generate_item to include any item
that would be illegal in a

checker_declaration outside of a checker_generate_item.

4) It shall be illegal to specify always_check or initial_check outside
of a checker body.

              5) In checkers only initial_check constructs may be
specified.

 

[Korchemny, Dmitry] I merged 2, 4 and 5 into "2)  initial, always,
always_comb, always_latch, and always_ff shall be illegal in a checker
body. initial_check and always_check shall be illegal outside of a
checker body." I also attached this note to the keywords, and not to the
productions, changed the keyword font to bold red and updated Annex A
accordingly.

 

3.           You state that  "Checkers may assign values to their formal
arguments, treating them as output arguments, though no explicit
notation of this is required in the checker declaration statement."
Prior to that you state "if a checker is instantiated in a procedure,
its contents are inserted after this procedure, otherwise they are
inserted in place."   Isn't there an issue if I have an output that is
used in the procedural code, since the checker is inserted after the
procedure.? Also, what happens when a checker appears in a for loop,
especially if the index is an argument to the checker?

 

[Korchemny, Dmitry] I don't see an issue here unless a checker assigns
the value to an automatic variable. Essentially, automatic variables in
assertions are handled in a separate Mantis (2091). Since we intend to
allow using checkers in loops (though this is a subject of a separate
proposal 2110), and loop indices may be automatic, I added the following
note: "The output actual argument shall have a static lifetime." which
will have to be modified in 2110 to forbid modifying loop indices
through checker output arguments. The current proposal does not allow
instantiating checkers in loops.

 

4.            "but the data types of checker formal arguments are not
necessary limited to those legal for a property."    Where is it defined
what is legal?

 

[Korchemny, Dmitry] It is written in 16.12.1 "The supported data types
for property formal arguments are the types that are allowed for
operands in assertion expressions (see 16.5.1)." I added a reference to
16.12.1.

 

5.           It states that "In the initial_check and the always_check
procedures all events from the explicit sensitivity list of their event
control are inferred"   The syntax does not seem to require an explicit
event - it says "statement_or_null".

[Korchemny, Dmitry] I added a note: (if any specified), but from the
logical point of view the original statement is correct: if none
specified, none is inferred.

 

6.           Why are the clock inferencing rules different for
initial_check versus initial and always_check and always?  Was there a
reason for the original limitation that does not apply here?

[Korchemny, Dmitry] The main reason is to allow passing an arbitrary
clock event to a checker. Consider the following example:

 

checker mycheck(even clk, logic a, ...);

            ...

            always_check(@clk) begin

                        ...

                        assert always(a); // We need inference of @clk
here

            end

endchecker

 

// Instantiation

mycheck check_1(posedge clk, x, ...);

 

In modules we infer only posedge/negedge clk

 

7.         in the section on bind, I think assertion-checker will be
confused with "checker".  Also notice typos "interfacsse" and
"anon-intrusive":

 

[Korchemny, Dmitry] Fixed.

 

"It is often desired to keep verification code separate from the design
code. SystemVerilog provides a bind

construct that is used to specify one or more instantiations of a
module, interfacsse, or program block, or

checker without modifying the code of the target. So for example, an
assertion-based checker that is assertions

encapsulated in a module, interface, or program, or checker can be
instantiated in a target module or a module instance in

anon-intrusive manner. Similarly, an assertion-checker that is
assertions encapsulated in an interface can be bound to a

target interface or interface instance."

 

[Korchemny, Dmitry] I rewrote it as:

 

It is often desired to keep verification code separate from the design
code. SystemVerilog provides a bind construct that is used to specify
one or more instantiations of a module, interface, or program block, or
checker without modifying the code of the target. So for example, an
assertion-based checker that is instrumental code or assertions
encapsulated in a module, interface, or program, or checker can be
instantiated in a target module or a module instance in a non-intrusive
manner. Similarly, an assertion-checker that is instrumental code
encapsulated in an interface can be bound to a target interface or
interface instance.

 

 

This is a very long proposal.  I have not yet finished it.

 

[Korchemny, Dmitry] I split the proposal and moved checker VPI stuff to
a separate proposal 2182.


Lisa

---------------------------------------------------------------------
Intel Israel (74) Limited

This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.