[sv-ac] Proposal for 1392 - Clocking event syntax corrections

From: Miller Hillel-R53776 <r53776_at_.....>
Date: Tue Jun 20 2006 - 10:26:47 PDT
 
Any references to clocking_event should be preceded with an @ character.
The author needs to check what is the correct wording for "occurences of
clocking events". Below are the corrections in the LRM that are
required.


1) Change the wording on page 223 from:

The variable j is an output to two clocking blocks using different
clocking events (posedge versus negedge). When driven, the variable j
shall take on the value most recently assigned by either clocking block.

To:

The variable j is an output to two clocking blocks using different
clocking events @(posedge clk) versus @(negedge clk). When driven, the
variable j shall take on the value most recently assigned by either
clocking
block.

2) Change the example on page 234 from:

assert property ( @(posedge clk)
    disable iff (a && $rose(b, posedge clk)) trigger |=> test_expr );

To:

assert property ( @(posedge clk)
    disable iff (a && $rose(b, @(posedge clk))) trigger |=> test_expr );


3) Change the wording on page 247 from:

In this example, the clocking event (posedge clk) is applied to $rose.
$rose is true whenever the sampled value of b changed to 1 from its
sampled value at the previous tick of the clocking event.

to:

In this example, the clocking event @(posedge clk) is applied to $rose.
$rose is true whenever the sampled value of b changed to 1 from its
sampled value at the previous tick of the clocking event.

4) Change the wording on page 248 from:

In this example, the clocking event (posedge clk) is applied to $past.
$past is evaluated in the current occurrence of (posedge clk) and
returns the value of b sampled at the previous occurrence of (posedge
clk).

to:

In this example, the clocking event @(posedge clk) is applied to $past.
$past is evaluated in the current occurrence of (posedge clk) and
returns the value of b sampled at the previous occurrence of (posedge
clk).

5) Change the wording on page 278 from:

is legal only if neither s1 nor s2 can match the empty word. The
clocking event posedge clk1 applies throughout the match of s1, while
the clocking event posedge clk2 applies throughout the match of s2.
Because the match of s1 is nonempty, there is an end point of this match
at posedge clk1. The #1 synchronizes between this end point and the
first occurrence of posedge clk2 strictly after it. That occurrence of
posedge clk2 is the start point of the match of s2.

to:

is legal only if neither s1 nor s2 can match the empty word. The
clocking event @(posedge clk1) applies throughout the match of s1, while
the clocking event @(posedge clk2) applies throughout the match of s2.
Because the match of s1 is nonempty, there is an end point of this match
at posedge clk1. The #1 synchronizes between this end point and the
first occurrence of posedge clk2 strictly after it. That occurrence of
(posedge clk2) is the start point of the match of s2.

6) Change the wording on page 278 from:

is illegal because of the possibility of an empty match of sig1[*0:1],
which would make ambiguous whether the ending clocking event is posedge
clk0 or posedge clk1.

To:

is illegal because of the possibility of an empty match of sig1[*0:1],
which would make ambiguous whether the ending clocking event is
@(posedge clk0) or @(posedge clk1).

7) Change wording on page 300 from:
The property evaluation starts on the clocking event (posedge clk)
following the 200 ms delay. If the sequence is matched, the process is
unblocked and continues to execute on the statement labeled ABC. If the
sequence fails to match, then the else clause is executed, which in this
case generates a run-time error. For the expect above to succeed, the
sequence a #1 b #1 c must match starting on the clocking event (posedge
clk) immediately after time 200ms. The sequence will not match if a, b,
or c is evaluated to be false at the first, second, or third
clocking event, respectively. 

to:

The property evaluation starts on the clocking event occurence (posedge
clk) following the 200 ms delay. If the sequence is matched, the process
is
unblocked and continues to execute on the statement labeled ABC. If the
sequence fails to match, then the else clause is executed, which in this
case generates a run-time error. For the expect above to succeed, the
sequence a #1 b #1 c must match starting on the clocking event occurence
(posedge clk) immediately after time 200ms. The sequence will not match
if a, b, or c is evaluated to be false at the first, second, or third
clocking event occurence, respectively. 


The syntax on page 246 requires the "clocking_event" BNF definition. The
clocking_event definition requires "@( )" for "posedge clk. 

Hillel Miller>


-----Original Message-----
From: owner-sv-ac@eda-stds.org [mailto:owner-sv-ac@eda-stds.org] On
Behalf Of Eduard Cerny
Sent: Tuesday, June 20, 2006 6:53 PM
To: sv-ac@server.eda.org; sv-ac@verilog.org
Subject: [sv-ac] FW: SV-AC Proposals - updated HAVE you received it over
the weekend?

 

-----Original Message-----
From: Eduard Cerny
Sent: Saturday, June 17, 2006 8:40 AM
To: sv-ac@verilog.org
Cc: Eduard Cerny
Subject: FW: SV-AC Proposals - updated

Hello,

I went through mantis and the recent emails. Here is a summary of the
state of errata assigned to sv-ac. Please let me know if any correction
is needed.

Best regards,
ed

------------------------------
 
 
1036 - Incorporate by reference Accellera PSL  - Not at this time
1296 - Annex E does not cover all clocked derived forms  - clarification
1325 - Clarify references to items declared in unnamed clocking blocks -
clarification proposal exists, voted by email 7 yes, 0 no
1326 - No semantics for boolean abbreviation with sequence match item -
clarification proposal exists - voted by email 7 yes, 1 no,
1361 - need a way to control execution of action blocks  - fix
1381 - vacuous success is not well defined in the LRM - clarification
proposal exists
1383 - Property coverage definition  - clarification
1392 - Inconsistent description of clock event argument to sampled value
functions - fix 1420 - Rules governing passing of arguments to recursive
properties are not sufficient - fix 1460 - Allow actions within assume
property statement  - enhancement proposal exists
1466 - shortcuts for delay and consecutive repetition  - enhancement
proposal exists
1494 - Infering enabling condition for coverage statement  -
clarification/fix proposal exists
805  - disable iff condition should produce vacuous match  -
clarification proposal exists, eventually needs review by SV-CC
921  -  Semantics of "calling subroutines on match of a sequence" is not
well defined - Major Clarification
928  - list_of_formals superfluous (BNF)  - correction proposal exists
(does it affect vpi?)
966  - $isunbounded()  - fix proposal under internal SNPS discussion
1495 - A problem with the rules of local variables flow rules  - fix
1498 - new, treat disable iff differently for cover property statement
1502 - new, formal definition of an assertion evaluation attempt,
success & failure
 
----

Priority for next meeting:
 928 - discussion / vote
 966 - discussion, proposal sent by email
1325 - voted by email, resolve?
1381 - discuss proposal, ready to vote
1326 - discuss Manisha's concern, resolve?
805 -  close on wording of proposal following emails
1392 - discuss if needed, simple solution

If time permits:
1494 - discuss proposal
1489 - discuss
1502 - discuss
1498 - discuss
1502 - discuss
 
need dates for following proposals:

1361 - Manisha to update proposal
1392 - Hillel
 
Un assigned proposals in MANTIS. We believe the proposed assignments are
as follows:

1383 - Dimitry
1420 - Doron
 921 - Doron
1495 - unassigned, but seems to have a simple solution as per comments
 
 
 
Received on Tue Jun 20 10:27:09 2006

This archive was generated by hypermail 2.1.8 : Tue Jun 20 2006 - 10:27:23 PDT