RE: [sv-ac] Issues for SV-BC (resent)

Hi Dave,

Please, see my comments below.

Thanks,
Dmitry

-----Original Message-----
From: Rich, Dave [mailto:Dave_Rich@mentor.com] 
Sent: Thursday, January 18, 2007 1:55 AM
To: Korchemny, Dmitry; sv-ac@server.eda-stds.org
Subject: RE: [sv-ac] Issues for SV-BC (resent)

Dmitry,

See comments below.

Dave


> -----Original Message-----
> From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
> Behalf Of Korchemny, Dmitry
> Sent: Wednesday, January 17, 2007 10:21 AM
> To: sv-ac@server.eda-stds.org
> Subject: [sv-ac] Issues for SV-BC (resent)
> 
> Hi all,
> 
> Here is the list of enhancements I wanted to address for submission to SV-
> BC. Please, send your feedback.
> 
> Thanks,
> Dmitry
> 
> 
> Operators for logical implication and equivalence
> =================================================
> Enhancement: introduce operators for logical implication and equivalence
> (e.g., -> for implication and <-> for equivalence)

[DR>] We already have implication-like operator for random constraints and I think a general Boolean expression would be useful. I just hope it can be fit in without breaking backwards BNF compatibility. I would also suggest defining these operators for use with all singular types by defining truth as being non-zero or non-null. Also, we would need to define behavior with unknowns.

[Korchemny, Dmitry] I agree. As far as I can see, BNF remains backward compatible (there is a need for a thorough check).

> 
> 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 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. Should be
> something 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)
>       $error ("illegal num_cks parameter"); // User-given compile time
> message
>     ...
> endmodule

[DR>] You will not always be able to check at compile time because the values of parameters will not be known until elaboration. You should at least be able to do the check during elaboration by using a conditional_generate:

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) begin : check
     initial 
       ovl_error_t("illegal num_cks parameter");
    end : check
 endmodule

If you want any control over how errors are handled, you're going to have to leave this as an initial block.

[Korchemny, Dmitry] Yes, it is better to say at the elaboration time, though some simulators can do this check during model build, before loading the model for simulation. Unfortunately, putting the error message into the initial block does not solve the problem: formal verification tools will just ignore it. Also, it makes the compile check impossible even when all necessary data is present. I think that early error detection is very important to increase the designer's productivity.

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

[DR>] This is really two enhancements. One is the ability to have a variable number of arguments, and the other is to a typeless argument, or at least be able to inherit the type for the actual argument. 

[Korchemny, Dmitry] We can split it into two. It is important to stress that arrays won't work here unless we want to allow arrays of untyped elements.

> 
> 
> Assertions within procedural for-loops
> ======================================
> Enhancement: Allow writing concurrent assertions within procedural for-
> loops with statically computable bounds.
> 
> Motivation. Currently the following specification is illegal:
> 
> always @(posedge clk) begin
>       for (int i = 0; i < 5; i++) begin loop
>             a[i] <= !b[i];
>             assert property(!a[i] |=> b[i]);
>       end
> end
> 
> and one has to put assertions within a generate loop:
> 
> for (genvar i = 0; i < 5; i++) begin loop1:
>       assert property(!a[i] |=> b[i]);
> end
> 
> always @(posedge clk) begin
>       for (int i = 0; i < 5; i++) begin : loop
>             a[i] <= !b[i];
>       end
> end
> 
> This is inconvenient - the locality is lost. It should be possible to
> write concurrent assertions within procedural loops with statically
> computable bounds and to treat such assertions as if written in an outer
> generate loop. This approach requires scope definition for such
> assertions.
> 
> Note: We can avoid sending this issue to SV-BC. One can define that
> writing a concurrent assertion within a procedural for-loop with the
> statically computable bounds is equivalent to creating a corresponding
> virtual generate loop outside of the procedural block with  concurrent
> assertions in it after doing the appropriate context inference to the
> assertions. If so, we can keep this issue in the competence of SV-AC, just
> sending it to SV-BC for review.


[DR>] I see this as totally an sv-ac issue.
[Korchemny, Dmitry] OK

> 
> 
> let statement
> =============
> Enhancement: Need a "compile time" macro
> 
> 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_hot(~sig1));
> q2: assert (one_hot(~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.

[DR>] The original OVA donation had a boolean construct which was a level below a sequence construct. It was dropped because it was just a special case of a sequence with just one cycle. If you allow immediate assertions to have one cycle sequences, then you could write your assertion as

sequence ap;
$past(a);
endsequence
assert property(@(posedge clk) ap);

But a better solution is to come up with a general purpose template construct instead of all the special case templates for properties, sequences and Booleans. I'm pretty sure the synthesis folks would also like to see something like this for module compilation.

[Korchemny, Dmitry] This is exactly an attempt to define such a template. This is a template for an arbitrary expression. One could define a template to wrap several statements together as well. I see problems with BNF definition - it becomes too vague when there are template statements, since you have to verbally describe what kind of statements is allowed to be in the template in a given context. One could, of course, define SV grammar in two stages: a meta-language stage defining generate constructs and templates, and a pure language stage when all the meta-language constructs have already been resolved.

As for using once cycle sequences, unfortunately, it does not solve the problem. Let's consider the following example:

sequence ap;
$past(a);
endsequence
assert property(@(posedge clk) & ap); // and reduction here

It means that have to allow sequence instantiation in ANY boolean expression, which is very close to what a let-statement is aimed to do.


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


[DR>] My personal option is that compiler directives should be avoided. They create so many problems for debug and compilation dependencies. They also don't deal with instance specific parameterization. The best think to do is to address the core language issues above.

[Korchemny, Dmitry] I agree that the best thing is to make necessary extensions in the meta-language instead of doing them in compiler directives. Still it is not feasible to avoid using compiler directives altogether: they are important for customization. Therefore some extension of compiler directive capabilities is needed for assertion customization: current compiler directives are almost useless for assertions.

> 
> 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
> 
> Thanks,
> Dmitry
> 
> --
> 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.