[sv-ec] Properties in clocking blocks, and Mantis 1541

hi AC and EC,

Mantis 1541 raises two issues with the example code
in 24.5.5 (the item says 20.4.5, but that's an obsolete
reference to 1800-2005).  The first is definitely a 
simple typo.  The second is more tricky, and concerns
access to signals from properties within a clocking block.

16.17 specifies properties in a clocking block, but it
is not very clear about this issue.  I'd like to check
with AC and EC before I raise a proposal for 1541 which
would modify the normative text in 16.17.

Consider:

  module M;

    logic clk, A, B, C, D, E;

    clocking c @(posedge clk);
      input A;
      inout B;
      output D;
      output F = E;
      property p; A |=> (B & C & D & E & F); endproperty : p
    endclocking : c

  endmodule : M

Property p reads all of A,B,C,D,E,F.  Some of these
references are legal, some (I think) are not:

A: legal, reads input clockvar c.A as sampled by clocking, with
   the restriction that the input sampling must be #1step. 
    
B: legal, reads input clockvar c.B just as for A, because 
   a clocking inout is in fact the combination of an 
   input clockvar and an output clockvar of the same name.

C: legal, reads M.C with regular assertion sampling (Preponed)
   because C is not a clockvar of the clocking block; the 
   only C that's in scope is M.C .

D: legal, reads M.D with regular assertion sampling because
   c.D is an output clockvar that cannot be read.

E: legal, same reasoning as C (even though E appears in a
   clocking signal hierarchical_expression).

F: illegal, because the only thing called F that's in scope
   is an output clockvar that cannot be read.

This list is my own interpretation; it's pretty tough to get
a clear decision from 16.17.  

Of the six cases listed above, the only one I'm unsure about
is D; there *is* a D in the clocking block, and it's *visible*
but not *accessible* to the property, so I'm asking for the 
name D to resolve into the next scope outward, skipping c.D, 
in this special case.  That sounds strange, but if we don't 
make this exception we get inconvenient behaviour that must 
be worked-around by making D an inout rather than an output 
of the clocking block.

If there are no objections, I'll add a proposal to Mantis 1541 
saying that the 24.5.5 example's access to a clocking output 
signal is legal (like D in my example) and adding text to 
16.17 to make my interpretation explicit.

Thanks in advance
-- 
Jonathan Bromley, Consultant

DOULOS - Developing Design Know-how
VHDL * Verilog * SystemC * e * Perl * Tcl/Tk * Project Services

Doulos Ltd. Church Hatch, 22 Market Place, Ringwood, Hampshire, BH24 1AW, UK
Tel: +44 (0)1425 471223                   Email: jonathan.bromley@doulos.com
Fax: +44 (0)1425 471573                           Web: http://www.doulos.com

The contents of this message may contain personal views which 
are not the views of Doulos Ltd., unless specifically stated.

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