Re: [sv-ac] SV-AC 0.79 comments ch 11 - 11.6.8

Subject: Re: [sv-ac] SV-AC 0.79 comments ch 11 - 11.6.8
From: Adam Krolnik (krolnik@lsil.com)
Date: Tue Jan 28 2003 - 09:29:45 PST

Hi Steve;

Thanks for responding.

Here is the BNF for check statements:

immediate_assertion :== ... check ... action_block

action_block :== statement_or_null [ else statement_or_null ]

statement_or_null :==
    statement
    | ';'

Here is a fragment from SV 3.1 draft 2:

statement :==
    ...
    | immediate_assertion

I had thought a semicolon ended this production. However
given that the pass statement is also statement_or_null, I
must place a semicolon before the 'else' clause. Do we want this?

     check (a || b); else $error ("Must be in state A or B");

Or would it be preferrable to have:

     check (a || b) else $error();

Of course, this also must be legal
     check (a || b)
        begin
        end
       else
        begin
        end

For 11.6.4 AND with length restrictions;

    The word 'congruent' most closely relates to the operation:

    Congruent:
      2 Mathematics.
         a. Coinciding exactly when superimposed: congruent triangles.

    Suggestions: match, correlate, '=='

For 11.6.7 - implications.

   The discussions may be clearer with usage of the terms (antecedent and consequent) vs.
   boolean_expr and sequence_expr which one must refer back to the syntax to see their
   usage.

For Figure 11-10 (active low signals)

Okay, though these days, its common to denote active low signals by name (irdy#, irdy_,
irdy_n)

> explain 11.8 example with error further.

 From the doc:

   sequence e_with_id = (valid_in // 1
      => (( int x = pipe_in, id = id_in) // 2
          ([1:inf] ((id_out == id && valid_out)
      => (pipe_out == x + 1))))); // 3

   Simplified, it says,
       v => [1:inf] vo => p

   If 'vo' never occurrs, there is no error since
       a => b => c is grouped as (a => b) => c

   The example can be fixed by replacing the second implication with zero delay
   concatenation, " ;[0] ".

     Thanks Steve.

     Adam Krolnik
     Verification Mgr.
     LSI Logic Corp.
     Plano TX. 75074

   Correctness - example sequence e_with_id

     See, this is not as simple as 'adding an id to each input data'.
     As written, if (id_out == id && valid_out) is not ever true, then
     you won't get an error about pipe_out1 being wrong. It should be
     written with only 1 implication operator. Also, the range
     for finding the valid_out should be less than 'inf'. This would allow
     someone to get an error reported early in simulation rather than after
     a global timeout.

This archive was generated by hypermail 2b28 : Tue Jan 28 2003 - 09:30:42 PST