[sv-ac] Comments on Assertions proposal 0.75

Subject: [sv-ac] Comments on Assertions proposal 0.75
From: Adam Krolnik (krolnik@lsil.com)
Date: Tue Dec 03 2002 - 14:38:38 PST

Next message: Adam Krolnik: "[sv-ac] Additional though on Assertion templates"
Previous message: David W. Smith: "[sv-ac] RE: $sv-ec SV 3.1 draft 1 LRM available"
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

Good afternoon everyone;

I am writing my comments on the proposal for consideration by the committee.

1. Immediate assertions vs. Concurrent assertions.

The two forms of assertions look very similar. Consider this example

...
check ($onehot(selector)) (1)
else $error();

...
assert $onehot(selector) (2)
else $error();

Aside from the optional parenthesis on the assert property directive,
they look very similar. I understand that immediate assertions may be
placed within clocked blocks and combinatorial blocks and they evaluate
their results and act immediately. Consider this code:

...
if (!$onehot(selector)) $error(<msg>); (3)
check ($onehot(selector)) else $error(<msg>); (4)

;

if (!a) $error(<msg>); (5)
check (a) else $error(<msg>); (6)

It seems to me that the addition of the $error() (or warning or info system task)
has more value for users than the addition of immediate assertions.

Can one not switch an immediate assertion for a concurrent (including a
clocking specification) and achieve the same results? If so, the value of immediate
assertions is small.

I compare these because a common change to make in an assertion is to extend
the expression used in an assertion. Many times it involes using a signal from
another timestep. Thus if one uses an immediate assertions and needs to use a
value from another timestep they would then switch to concurrent assertions.
Why not save them the trouble of changing 'check' to 'assert' and only have one.

[Q: what if they forgot the clock and wanted one and had a boolean and were in
nonclocked context?]
   It would seem that forgetting a clock would produce false failures. Thus
   they would be fixed. The question is would there be any false positives?
   It would seem no unless one of the registers is assigned from another
   place and then there may be other problems too.

2. Declaring Clocks (events)

I do not believe this additional syntax provides a great benefit. It names (and thus
shortens) an event expression, but it does not provide much more. E.g.

event my_special_event = !reset && clk_en && posedge clk; // Legality in ? (7)

vs.

always @(posedge clk) if (!reset && clk_en) ->my_special_event; (8)

3. Sequence elements

o Is the word 'true' being proposed as a keyword? Its use seems superfluous.
o The keyword 'inf' seems to have a very limited usefulness. Only one context
and only to disambiguate syntax error from forever. Hmmm, 'forever' instead?

o The examples provided for explaining delay and repeat count could include some
where both values are greater than 1. For example, what does this mean (1 or 2)?

(a; [2] b * [2]) (9)

1. (a; [1]; [1] b; [1]; [1] b) (10)
2. (a; [1]; [1] b; [1] b) (11)

o Requiring ";[1]" to mean the next cycle is a lengthy separator in my opinion.

4. Sequence operator (and with length restriction)

It seems to me that this idea could be considered equivalence of sequences (in length.)
Though it also means matched too, something like:

s1 intersect s2 :== s1 and s1 == s2

Maybe we could use the equivalence operator for this to disambiguate 'both occur' from
'both end at the same time'. Current usage of 'and' and 'intersect' doesn't help me
disambiguate them because I think of intersect as a partial match, not a full
one as currently expected. [Think intersection of two streets.]

5. Conditional sequences

The SV-EC committee has proposals to introduce the implication operator '=>'.
The current proposal has the conditional sequence mean the same thing. E.g.

if (trigger) sequence

trigger => sequence

This is becoming a common idiom today. I would recommend using this operator
instead of a set of if() statements. Placment of the operator between the two
operands visually separates them, compare to the use of then ending parenthesis
in the "if()" operation. When placed on the same line, the

Similarly, instead of an if else set of
operations, I would recommend the ternary (a ? b : c) operation instead (though
I do understand it is a bit terse.)

6. Boolean expression of conditional sequences.

I wonder about the grumblings of the users in requiring them to type:

if (a) ( [1] if (b) ( [1] if (c) ( d; [1] e; [1] f))); (12)

vs.

if (a;[1] b;[1] c) (d;[1] e;[1] f) (13)

or
(a;[1] b;[1] c => d;[1] e;[1] f) (14)

It seems that given the grammar to be able to chain conditional sequences together
you may as well given them the short hand to type a sequence as the antecedent.
[You know, #12 somewhat looks like lisp.]

7. Conditions over sequences.

I have termed this idea 'dynamic until'. I.e.

expression until sequence (15)

I term it dynamic because the 'until' ends when the sequence completes. Maybe this
is an alternative and simpler syntax. The idea of having keyword pairs to define
a function is somewhat strange for me.

8. Sequences with length specification

I have termed this idea 'static until' in contrast to the above. In this version
the length is predefined by a specified range of time. Thus:

expression until range (16)

The "length range within sequence" seems reversed in the specification. I would have
expected the sequence first and the range second. The static until idea reverses
these. Also, these keywords do not shorten the writing (the other form is shorter
in keystrokes.)

9. Sequence occurrence within another sequence.

I don't quite understand this definition. Written is "the start point of sequence_expr1
must be between the start point..." Don't both sequences start at the same time? E.g.

occurrs seq1 within seq2 (17)

Seems both seq1 and seq2 start when this operation begins. If this is true, then
it seems to me that you are writing that the length of seq1 must be less than or
equal to the length (end time) of seq2. So I think of this as:

seq1 && seq1 <= seq2.

Maybe we could consider using 'less than or equal to (<=) as an operator for
this functionality. It would mean the composition of the above operation, which
is (obviously) not strictly '<='

10. Boolean declarations

I don't understand the need for this functionality. We already have three methods
of implementing this:

   wire name = expression;
   `define name(a,b,c) a && b && c // IEEE1364-2000 defined capability.
   function name (a, b, c)

11. Manipulating data in a sequence.

I also would like to see the allowance of data assignment within a sequence rather
than require two keywords to delimit it. E.g.

let (int x = pipe_in) within ; [5] (pipe_out == x); (18)

vs.
(assign x = pipe_in; [5] pipe_out == x); (19)

I would like to see how one could incorporate incrementing of counters
so that one could produce a fifo checking assertion that requires
the use of a range of time. I.e. something like:

(id = inc, push // See a push, save the inc counter
    => (inc++, din == pipe_in; // Increment counter, save data in.
       [1:20] oinc == id // Matching decrement now.
           && head == din // Data matches
           && pop && oinc++); // Pop the Q/fifo and increment the other counter

12. System functions

I think $isunknown(), $insetz(), $onehot(), $onehot0() are valueable in addition to
$countones. Also, rose/fell and stable.

13. Property declarations.

You define prop_expr to also be an identifier, with an optional expression list. But you
restrict the identifier to a property. Do you mean a sequence? or both?

You also write about the (asynchronous) accept clause. Since this is supposed to be
thought of as an adjunct or afterthought to the property, should it be prominent at
the front? I would think that it would be better at the end (somewhat out of the way of
presenting the property.)

If we are going to use the keyword 'not' to imply a property should never occur it would
be best to put it upfront as opposed to the middle to let it stick out. Otherwise it
seems to look like a postfix operator, "I like icecream, not!"

I don't understand the need for a one (first) cycle property. If the idea is to check
a reset sequence or something, shouldn't it start something like:

if (reset) ...

There must be some event that must occur for the hardware to do something that should be
checked. Using 'initial' masks this event.

14. Property directives.

I think the grammar for a property_directive should not allow multiple properties for
one action block. Maybe this came from a simplification of the grammer to allow one
directive to specify several properties. E.g. I'd rather not allow

assert (a; [1]b; [1]c),
(d; [1]e; [1]f) do this_stmt else that_stmt;

Since the sequence definition allow specification of a clocking event first for a group
of sequences, why does the property block not follow this form?

seq @(posedge clk)
s1 = a ; [1] b,
s2 = c ; [2] f;

property
s1 = @(posedge clk) a ; [1] b,
...

I would expect that assert <sequence>;

I don't understand the desires for assert (*) and cover (*).

What is the intended way to use the language?

property p1 = <sequence>;

assert p1 else $error(msg);
cover (*);

c2: cover (this; [1:10] that);

15. Embedding properties in procedural code.

Rather than allow:

always @(posedge clk)
   begin
   ...
   property rule = ...; (20)
   ...
   end

Follow verilog (allow in named blocks) and instead use:

always @(posedge clk)
   begin
   ...
   rule: assert ...; (21)
   ...
   end

It is stated that "a property when instantiated in a procedural block uses a similar
mechanism as synthesis to infer the context of the clock, reset, and enabling condition."
So you are saying:

           clock
          V
always @(posedge clk or negedge rst_n)
   begin
   if (!rst_n) <- reset
     begin
     q <= -1'b0;
     ...
     end
   else
    if (enable) <- enable
      begin
      q <= d;

      assert $onehot(d) else $error("Whoops, John, this isn't onehot.");
      end
   end

If one places an assertion in such a block, that you can infer these three
conditions. And the assertion won't fire (or will be canceled if reset
is happening, or enable is not true.)

What about this legal example?

always @(posedge clk or negedge rst_n)
   begin
   if (!rst_n)
     begin
     ...
     end
   else
    if (enable) <- enable
      begin
      q <= d;
      assert $onehot(d) else $error("Whoops, John, this isn't onehot.");
      end
   end

Does 'q' have a reset? If it does not, what is the reset for the assertion?

16. Assertion templates.

The interface construct is taking a beating from users who wanted to see
it's capabilities folded into modules. I would expect the same thing
to be done here for templates. It may be wise to explain the need for
something different from a subset module.

Are templates a separate namespace (from modules, etc)?
I don't understand the need for defining parameter types, and direction.
Why do you need output/inout? I don't think one can define how to use a let type
variable outside of its context.

With a template instantiated without a name, can you refer to anything inside it
in a reusable way (reuse with other tools?) Is it just a shorthand?

17. Binding properties to scopes/instances.

This section needs an example. All I understand is that I have a file
with some named properties and I do:

include <file with properties>
bind_module mymod::property1_from_above_file;

Won't there be errors generated when including a property that does not bind to
any matching names?