[sv-bc] Enhancements important for assertion specification (with Mantis numbers)

Hi all,

I am resending this list with Mantis numbers attached.

Thanks,
Dmitry

---
Dear SV-BC members,
 
Please, find below the list of SystemVerilog enhancements belonging to
the competence of SV-BC that
SV-AC sees important for assertion specification usability, especially
for creation of checker libraries.
 
 
Operators for logical implication and equivalence
=================================================
Enhancement: introduce operators for logical implication and equivalence
(e.g., -> for implication and <-> for equivalence)
 
Motivation:
 
1. No corresponding operators for immediate assertions.
 
Workaround: use <= for implication and == for equivalence. This notation
is not intuitive and works for one-bit values only.
 
Example:
 
1) Whenever a request is high the ready signal should be asserted.
 
Current notation:
assert (request <= ready);
 
Should be something like:
assert (request -> ready);
 
2) Error should be raised iff the address value is greater than 4'hffff
 
Current notation:
assert (error == (addr > 4'hffff));
 
Should be something like:
assert (error <-> (addr > 4'hffff));
 
Note: these operators are also useful for temporal properties, e.g., to
check that two properties are equivalent:
 
assert property (@(posedge clk)(!b[*1:$] |-> a) <-> ((a[*0:$] ##1 b) or
(1[*1:$]|->a)));
 
 
Compile-time user given messages
================================
Enhancement: introduce user-given compile-time messages
 
Motivation:
Need to check the consistency of the checker data and to issue a
compile-time or elaboration time
error message when the data are inconsistent. At present one should
either rely on a syntax error
or to perform the check at the simulation time. The latter solution is
unacceptable because it
reveals the issue too late and does not work for formal verification
tools.
 
Example from OVL:
 
module assert_cycle_sequence (clk, reset_n, event_sequence);
  parameter severity_level = `OVL_ERROR;
  parameter num_cks=2;  // number of clocks for the sequence
  ...
  reg [num_cks-1:0]  seq_queue;
 
  initial begin
    if (num_cks < 2) begin
      ovl_error_t("illegal num_cks parameter");
    end
  end
 
  ...
endmodule
 
Note a run-time error message here in the initial block. The message
should look like:
 
module assert_cycle_sequence (clk, reset_n, event_sequence);
  parameter severity_level = `OVL_ERROR;
  parameter num_cks=2;  // number of clocks for the sequence
  ...
  reg [num_cks-1:0]  seq_queue;
 
  if (num_cks < 2)
      $compile_error ("illegal num_cks parameter"); // User-given
compile time message
    ...
endmodule
 
 
Multiple argument support
=========================
Enhancement: Allow specification and processing of multiple arguments in
modules, properties, etc.
 
Motivation. Several checkers require multiple arguments, and these
arguments have different type.
The following example shows a property having an argument list (but the
same is relevant for
modules, functions, etc.)
 
Example:
The signals should have the same value. The syntax should be very simple
and intuitive, like
 
same(a, b, c)
 
Note that the number of signals, their size and their type may vary,
therefore arrays won't work here.
 
Need a capability to specify lists of (differently) typed arguments and
means to process them.
 
 
let statement
=============
Enhancement: Need a "compile time" macro

*** Mantis #1728
 
Example.
 
let ap = $past(a);
assert property(@(posedge clk) ap);
 
In this case let operator acts almost as a `define, but it is processed
at the compile time and
it checks for its argument validity. Note that in this example a plain
assignment won't do,
since it requires to specify the clocking event for $past, which is
inferred in the assert
statement only, and is not known in the let statement itself.
 
Motivation.
1. let statement as a template for immediate assertions. Concurrent
assertions may have
templates (properties, sequences), but immediate assertions have none.
E.g.,
 
concurrent assertions:
 
property triggers(ante, cons, clk = proj_clk, rst = 1'b0);
      @(posedge clk) disable iff(rst) ante |-> cons;
endproperty
 
p1: assert property(triggers(a1, c1));
p2: assert property(triggers(a2, c2));
 
but immediate assertions should be written each time from scratch
 
q1: assert(rst || $onehot(~sig1));
q2: assert(rst || $onehot(~sig2));
 
instead of:
 
let one_zero(sig, rst = 1'b0) = rst || $onehot(~sig);
q1: assert (one_zero(~sig1));
q2: assert (one_zero(~sig2));
 
Note that function cannot be used instead of let statement here, since
one has to specify
a separate function for each size of its argument. The only alternative
is preprocessor macro:
 
`define one_zero(sig, rst) ((rst) || $onehot(~(sig)))
 
which is a worse solution since the compiler has no information about
assertion templates:
it cannot collect statistics on assertion usage, linting is problematic,
etc.
 
2. let statement for assertion modeling
One needs sometimes to perform auxiliary computations to write a
checker. Usually SV RTL
level is used for this purpose. E.g.,
 
wire type(a + b) c = a + b;
...
assert property(@(posedge clk) cond |=> c < d);
 
Such practice is problematic for several reasons. One of them is that a
synthesis tool will
treat such auxiliary signals (c) as real ones and will synthesize them
into silicon.
Workarounds using `ifdef are needed for this purpose. Another reason is
that an exact
type must be specified, and it is not always easy to the user to specify
it. "type"
operator may be used for this purpose, but it looks clumsy when the
signal names are
long. Even worse, the "type" operator represents the self-determined
type of the result
while the user needs the context-determined type. Thus, if both a and b
are two bit
long then c will also two-bit long, and the result will sometimes be
truncated. Using
let operator makes writing more elegant and safe:
 
let c = a + b;
...
assert property(@(posedge clk) cond |=> c < d);
 
Note again that using functions may solve the synthesis problem, but not
a usability
problem (the function requires a type specification and the full context
for sampled
value functions such as $past).
 
3. let statement is useful to solve the problem of multiple arguments
(see above),
since combining let statements with generate (or other similar)
constructs is a
natural way to handle multiple arguments.
 
The following example shows how a sum of arguments may be computed using
let statements
and generate constructs. It is illustrated for an array (which obviously
does not
require a let statement introduction, but the same idea is applicable
for processing
an arbitrary list): 
 
int args[50:1];
for (genvar i = 0; i <= 50; i++) begin : b1
     if (i == 0) begin : b2
        let res = '0;
     end
     else begin : b2
     let res = b1[i-1].res + args[i];
     end
 end
 let res = b1[50].b2.res;
 
 
Compiler directives
===================
Enhancement: Make SV compiler directives more powerful, e.g., allow
default argument values for macros, handling the macro argument list as
a whole, introduce macro blocks, conditional macro evaluation, etc.
 
*** Mantis ##1084, 1563, 1566, 1571, 1620, 1621, 1697

Example (the syntax is used for illustration purposes only):
`define ASSERT_BEFORE(*) assert property (before(*)) 
 
Motivation. Current SV macro-processor has very limited capabilities.
Though macro
capabilities may be easily abused and alternative language constructs
should be
preferred (like a let statement described above), they are still very
handy, especially
for writing checkers.
 
Consider the following examples.
 
1. Combinatorial checkers may be implemented either as immediate or as
concurrent
assertions. They cannot be implemented only as immediate assertions
since the
immediate assertions cannot be used outside of the procedural blocks,
but they
cannot be implemented only as concurrent assertions as well since
concurrent
assertions cannot be used inside functions. Still, it is convenient to
have one
checker for both purposes. One solution would be to write a macro which
will check
whether the clock argument has been provided: if yes -generate a
concurrent
assertion, otherwise, generate an immediate one. Therefore an
implementation of
the following pseudo-code is needed (I am omitting the property
templates in the
sake of simplicity):
 
`define ASSERT_HIGH(a, clk)
     if defined clk then assert property(@(clk) a)
     else assert(a)
 
2. For different reasons it may be useful to wrap assertions into a
macro (see the
previous example as one of them). Currently this cannot be done since a
macro has
only a predefined number of arguments. Here is an illustration:
 
One can write now:
 
property triggers_next(ante, cons, clk = proj_clk);
     @(clk) ante |=> cons;
endproperty
 
p1: assert property (triggers_next(a1, b1)); // proj_clk will be
inferred
p2: assert property (triggers_next(a2, b2, posedge clk)); // Clock
explicitly specified
 
But one cannot wrap assertions into a macro:
 
`define ASSERT_TRIGGERS_NEXT(ante, cons, clk) assert
property(triggers_next((ante), (cons), (clk)))
 
p1: `ASSERT_TRIGGERS_NEXT(a1, b1); // Syntax error - only two arguments
specified
p2: `ASSERT_TRIGGERS_NEXT(a2, b2, posedge clk); //OK

*** Peripherally related Mantis ##96, 98

We believe that SV-AC should also be actively involved into the
definition of these
enhancements, and its direct representatives will be Ed Cerny (Synopsys)
and Dmitry
Korchemny (Intel).
 

Thank you,
IEEE P1800 SV-AC

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