Subject: problems with current definition/document
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Wed Jul 17 2002 - 09:09:15 PDT
colleagues,
at the previous meeting, we were asked to address problems with the current
definition/document. please find my input below.
===========================================================================
1. on page 48 the comment of the first example says "'a' is evaluated only
once at 10".
however, according to the english text above the example, "if the
sequential assert
statement is executed again before the sequence spawned by the
original execution
has expired, then a new process shall be spawned that looks for the
sequence starting
at the current timestep." this seems to imply that 'a' should be
evaluated multiple times,
at 10, 20, 30, etc. which is correct?
===========================================================================
2. what about an assertion that appears in a loop statement, as follows:
always @(posedge clk)
for (i=0; i<=31;i=i+1)
if (busa[i])
assert (1;busa[i] || busb[i]) @@ (posedge clk);
end
the above fragment seems to check that whenever bit i of busa is
asserted, it will stay
asserted until bit i of busb is asserted. however, the use of i is
problematical, since it
does not necessarily hold its value until the next clock cycle. in
addition, as per the
current definition (page 48), ``an assertion shall only spawn a single
process to
evaluate the next expression in the sequence at the next step control
event. if the step
control event occurs multiple times at the same timestep, then in a
clocked immediate
assertion the current expression in the sequence shall be
re-evaluated." the above
code fragment contains only a single assertion, so it should spawn
only a single
process, and thus checks only a single bit, which is clearly not the
intention of the user,
and probably this situation was not intended to be covered by the
above excerpt. what
was the intent, and how is this stated precisely? are there any other
constructs with
similar problems?
===========================================================================
3. the current definition defines the semantics in terms of spawning
processes (on page
48, for instance). it would be better to have semantics defined in
terms of what the
assertion means, leaving it up to the tool to decide whether to
implement an assertion
by spawning a process or by some other means. with the current
definition, it is
impossible to know what an assertion means in formal verification,
because the idea of
spawning a process at a certain point of evaluation is foreign to a
formal verification
tool. furthermore, even for simulation the current definition is
over-restrictive. for
instance, multiple processes may be in-flight, each monitoring the
same sequence, but
offset in time (page 48). however, in order to check for multiple
instances of the same
sequence offset in time, it is possible to use a single monitor, built
by determinizing a
non-deterministic state machine, as implemented in ibm's focs tool,
for instance. in this
case, hard-coding the implementation into the definition results in a
lack of flexibility to
implmement future optimizations.
===========================================================================
4. the current definition seems to allow the use of assertions in such a
way that the
design itself is affected. for instance, consider this example,
slightly modified from
page 46:
always @(posedge clk)
if (state == REQ)
b7: assert(req1)
@(posedge clk) assert(gnt)
@(posedge clk) assert(!req1);
state = #1 WAIT;
i am not sure if this is legal (and my verilog is very rusty, so
perhaps i have syntax
problems in the one line i have added), but nothing in the current
definition seems to
prevent this. now, running the simulation with assertions turned on
has the effect of
assigning the value WAIT to signal state on the third clock after it
gets the value REQ,
while running the simulation with assertions turned off will give
different behavior.
perhaps the point of the "no semicolon" comment in the example on page
46 was that
somehow the next two posedges should not affect the statements
following the
assertion. (if that was not the point, what was?) if so, then adding
semicolons would
make the point. there should be some way to prevent this kind of
effect. for instance, if
delay controls are not allowed on assertions.
regards,
cindy.
Cindy Eisner
Formal Methods Group Tel: +972-4-8296-266
IBM Haifa Research Laboratory Fax: +972-4-8296-114
Haifa 31905, Israel e-mail:
eisner@il.ibm.com
This archive was generated by hypermail 2b28 : Wed Jul 17 2002 - 09:09:34 PDT