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) 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 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. 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. 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. 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. 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.Received on Wed Jan 17 10:07:12 2007
This archive was generated by hypermail 2.1.8 : Wed Jan 17 2007 - 10:07:34 PST