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

Slight corrections:


> -----Original Message-----
> From: owner-sv-bc@server.eda.org [mailto:owner-sv-bc@server.eda.org]
On
> Behalf Of Korchemny, Dmitry
> Sent: Monday, February 26, 2007 8:27 AM
> To: sv-ac@server.eda-stds.org; sv-bc@server.eda.org
> Cc: sv-cc@server.eda.org; sv-ec@server.eda.org; sv-xc@server.eda.org
> Subject: [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

[SB] Mantis 1620.

> 
> 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.

[SB] Mantis 1566.

> 
> 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

[SB] Should be Mantis ##1084, 1563, 1571, 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.

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