Subject: Re: [sv-ac] Initial proposal text for messages in sequences.
From: John Havlicek (john.havlicek@motorola.com)
Date: Tue Dec 09 2003 - 12:12:57 PST
Hi Adam:
I have several comments.
I. In
> property follow_req(a, b, c, address)
> reg [31:0] req_addr;
> @(posedge clk) // Simple example
> (a, (req_addr = address)
> => b ##1 c)
> endproperty
I think you want "=>" to be "|=>".
II. Using the action block as in
> assert follow_req(a, b, c, address)
> else
> $error("C (%0d) did not follow b after a with address %0h.\n", c, req_addr);
> // 'c' and req_addr may show the wrong value.
has the problem that the sampled values may not be the ones appearing in
the error message, right?
III.
> Messages are added within the sequence, after an expression.
>
> sequence_expr ::=
> ...
> | expression, blocking_assign_or_message
>
> As an example, after 'a' we expect 'b' and we store the value of 'v' into the local
> variable 'loc_v'. We then report a message using $display() with the shown string.
> We then proceed to expect 'c' one cycle later.
>
> a ##1 b, (loc_v = v, $display("loc_v is %0h at time %d.", loc_v, $stime))
> ##1 c
The change is going in that parentheses will be required whenever "attaching"
things to booleans or sequences using comma. So I think this should be
sequence_expr ::=
...
| ( expression, blocking_assign_or_message )
and
a ##1 (b, loc_v = v, $display("loc_v is %0h at time %d.", loc_v, $stime))
##1 c
I think it is important to pause here and recall the discussion from a couple
of weeks ago. There were several questions:
a. Do we allow attaching of a message only to booleans, or more generally
to sequences?
b. Does the message execute unconditionally or does its execution depend
on whether the boolean is satisfied or the sequence is matched?
We said in our discussion that, to keep things simple, we would allow
attaching of messages only to booleans and that the message would execute
unconditionally on the test of the boolean. One reason we said that
the message should execute unconditionally is that if we use if-else
to sort out what to do, we will want to write something like
a |=> if (b)
(1, $display(<pass-message>))
else
(0, $display(<fail-message>))
instead of having to write something like
a |=> if (b)
(1, $display(<pass-message>))
else
(1, $display(<fail-message>)) ##0 0
After not thinking about this for a while and coming back to it, I
think the decision to execute the message unconditionally is bad for several
reasons.
1. It means we will expect a $display from
a ##1 (b, loc_v = v, $display("loc_v is %0h at time %d.", loc_v, $stime))
##1 c
whether or not the test of b in the second cycle passes or fails. This
is untidy, since the intuition is that if the test of b fails, then
the local variable doesn't get sampled, and we ought to say what gets
displayed in that case.
2. I forsee trouble when people write things like
a
##1
(
b,
loc_v = v,
$display("b is true and loc_v is %0h at time %d.", loc_v, $stime)
)
##1
c
or like
a
##1
(
my_seq(loc_v).ended,
$display("my_seq ended and returned loc_v %0h at time %d.", loc_v, $stime)
)
##1
c
3. The unconditional execution of the message does not extend well
to attachment to sequences, where the usefulness of unconditional
messages seems limited.
So I am coming to the conclusion that introducing unconditional messages
as a first step in 3.1a is not a good idea.
Ultimately, we will want to get to both passing messages and failing messages.
One possibility is to introduce a syntactic flag to distinguish whether the
message should execute on passing, failing, or unconditionally. That way
there is a clear marker to avoid traps like in 2 above.
Another possibility is to introduce just one of the passing or failing modes
in 3.1a with no syntactic flag. Later, we could introduce other modes with
some different syntax altogether or with a syntactic flag to distinguish
them from the passing mode. Until then, there will just have to be some
hackery to get the effect of the other mode when it is possible.
To me, the best limited solution right now seems to be the following.
1. Introduce only the passing mode message. It has the syntax you
described, with no extra flag to say "passing mode". The reason
to make it passing instead of failing is to keep the intuition simple
in comparison to the local variable sampling.
2. Allow a passing message to be attached either to a boolean or to a sequence.
The message executes at each match point of the boolean or sequence. The
message does not execute otherwise.
If attaching the passing message to a sequence is too much, we could
limit it to booleans for 3.1a.
3. The failing mode can be achieved for 3.1a for booleans, but with some
hackery. In a property context, the idiom from above works:
if (b)
(1, $display(<pass-message>))
else
(1, $display(<fail-message>)) ##0 0
In a sequence context there is no if-else, so the hackery is a bit more
involved:
a
##1
(
(b, loc_v = v, $display(<pass-message>))
or
(!b, loc_v = <dummy-value>, $display(<fail-message>)) ##0 0
)
##1
c
This assumes, of course, that the second disjunct of the "or" is
not optimized away. The assignment of a dummy value to the local
variable after !b is needed to ensure that the local variable flows
out of the "or".
4. Achieving the failing mode for sequences requires substantial rewriting.
For example, to get the failing message on
a |-> ##[1:10] b
you would have to rewrite as something like
a |=> !b[*10] |=> b
and then attach the failing message to the last b, as in
a |=> !b[*10] |=> if (!b) (1, $display(<fail-message>)) ##0 0
In the future, we could work on getting a better solution for the failing
mode, including attaching to sequences. After 3.1a, I would want to explore:
a. Using some syntax like "failing" to signal the failing mode message.
b. Attaching failing mode messages to sequences and what this will mean.
c. Attaching a single message to a property, both for passing mode and
failing mode.
IV.
> a |-> if (##[1:10] b) 1 else 0, $error("Did not receive b within 10 cycles.")
As you pointed out, the "if" in my proposal takes only a boolean condition.
Giving a meaning to the "else" in the case of a sequence condition requires
defining when the sequence fails and which thread(s) that witness failure
proceed to the "else" clause. We don't have time to achieve this for 3.1a
in my opinion.
V.
> a |-> not ##[1:10] b |-> 0, $error("Did not receive b within 10 cycles.");
The only way this parses is as
a
|->
not
(
##[1:10] b
|->
(0, $error("Did not receive b within 10 cycles."))
)
which doesn't give you what you want. If we negate a sequence, then it
is really the negation of the promotion of the sequence to a property, and
that cannot be the antecedent of a "|->" implication.
For the future, I see solving this with the failing mode of message
for sequences or for properties.
Comments and discussion welcome.
Best regards,
John H.
> Date: Wed, 26 Nov 2003 15:08:19 -0600
> From: Adam Krolnik<krolnik@lsil.com>
> X-Accept-Language: en-us, en
> Sender: owner-sv-ac@eda.org
> Precedence: bulk
>
> This is a multi-part message in MIME format.
> --------------090003090304070602020709
> Content-Type: text/plain; charset=us-ascii; format=flowed
> Content-Transfer-Encoding: 7bit
>
>
> Hello;
>
>
> Here is an initial wording on the proposal. I wrote it and then saw that
> John's if() proposal only allows for a boolean if expression. I will have
> to remove that section or we can discuss alternatives.
>
> Thanks.
>
> Adam Krolnik
> Verification Mgr.
> LSI Logic Corp.
> Plano TX. 75074
> Co-author "Assertion Based Design"
>
>
>
>
> --------------090003090304070602020709
> Content-Type: text/plain;
> name="seq_message.txt"
> Content-Transfer-Encoding: 7bit
> Content-Disposition: inline;
> filename="seq_message.txt"
>
>
>
> Problem:
>
> The problem with error reporting is that the error message does not
> directly have access to the signal values and local variables used
> in the property to determine a legal sequence of actions or an illegal
> sequence.
>
> For example, this property has signals and variables:
>
> property follow_req(a, b, c, address)
> reg [31:0] req_addr;
> @(posedge clk) // Simple example
> (a, (req_addr = address)
> => b ##1 c)
> endproperty
>
> assert follow_req(a, b, c, address)
> else
> $error("C (%0d) did not follow b after a with address %0h.\n", c, req_addr);
> // 'c' and req_addr may show the wrong value.
>
> In addition to the difficulty in creating an error message, it will be difficult
> to track operation of some sequences and the setting of local variables.
>
> Motivation:
>
> 1. Provide support for error messages using same context of signal values as the property.
> 2. Provide support for error messages using local variables from the assertion context.
> 3. Provide debug support for debugging the flow of sequences and local variable settings.
>
>
>
> Solution:
>
> [We currently can not define a solution to provide for one error message for the failure
> of properties. There are too many questions to be resolved to come up with a full
> definition.]
>
> Insert after section 17.8 "Manipulating data in a sequence"
>
> 17.9 Messages within sequences.
>
> Messages can be included in sequences to aid in debug of sequences, or to produce
> error messages with contextual information. Messages are produced through these
> system tasks: $display, $fatal $error, $warning, $info.
>
> Messages are added within the sequence, after an expression.
>
> sequence_expr ::=
> ...
> | expression, blocking_assign_or_message
>
> As an example, after 'a' we expect 'b' and we store the value of 'v' into the local
> variable 'loc_v'. We then report a message using $display() with the shown string.
> We then proceed to expect 'c' one cycle later.
>
> a ##1 b, (loc_v = v, $display("loc_v is %0h at time %d.", loc_v, $stime))
> ##1 c
>
> These system tasks do not produce a value (a function) they simply execute in the
> order they are listed. These messages can be for debug or for error reporting.
>
> [ Not yet. if (b |-> pass_p) and (!b |-> fail_p) then why not
> (first_match(b_p) |-> pass_p) and (!first_match(b_p) |-> fail_p)
> This would make it easier for messages. ]
> For error messages, the if() structure allows for checking of the failure of
> a sequence or property and subsequent failing of the property and provision
> of a correct error message.
>
>
> a |-> if (##[1:10] b) 1 else 0, $error("Did not receive b within 10 cycles.")
>
> Here if the sequence (##[1:10] b) fails then the else branch is taken which yields 0
> and executes the $error() routine. This routine shall replace any implicit $error()
> routine call (when there is no fail statement in an action block.) If a fail statement
> is included in an action block, any $error() (or fatal or warning) calls shall override
> the error routine from the property or sequence.
>
> Messages shall not be attached to the success of a sequence. Only a boolean expression
> may preceed a message statement. When a sequence is expected to fail, inversion of the
> sequence followed by a message will suffice.
>
> a |-> not ##[1:10] b |-> 0, $error("Did not receive b within 10 cycles.");
>
>
>
>
>
> --------------090003090304070602020709--
This archive was generated by hypermail 2b28 : Tue Dec 09 2003 - 12:13:39 PST