RE: [sv-ac] RE: [sv-bc] New Proposal uploaded for Mantis 2005

Hi Doug--
 
Thanks for posting that proposal.  I think you're right, the 'disable'
looks like a cleaner way to allow some manual flushing if desired.  Am I
correct that you are still revising this, since I don't see the _2
version posted in Mantis yet?  In that case, rather than attempting to
edit again right now, I'll send you my current questions & comments:
 
 
1. As the reasoning for using the Observed rather than the Postponed
region, we state  "While the Postponed region is also a candidate for
the execution of deferred assertion reports, it is risky to allow
execution of action block code in the Postponed region. Currently
SystemVerilog has no such requirement. "  But is it really 'risky',
given the restrictions later described on the action block?
 
I see one strong argument for the Postponed region:  in that region, it
is illegal to reschedule any previous regions, so we know it will only
be executed once per time step.  If we use the Observed region, it could
get executed multiple times-- which might mean we will get glitches
anyway, defeating the main purpose of this proposal.  Am I interpreting
the simulation rules incorrectly?  Or is there a reason we shouldn't be
worried about a glitch due to region iterations within a time step?
 
 
2. Isn't there a way we can redefine the behavior with event controls so
your last example behaves more intuitively, and a42 does get executed?
 
module fsm(input clk, rst, a, b);

...

always_comb begin : b1

    a42: assert @(posedge clk) (a == b);

    ...

end

 

always_ff (@posedge clk) begin : b2

    state <= nextstate;

    if (somecond) begin

        b <= !b;

        ...

    end

    ...

end

endmodule

 
When a42 is encountered, its report is scheduled for the next occurrence
of (posedge clk).  You point out that b1 may be running again in an
active region before that, causing a flush point.   Is there really no
way a simulator can use the fact that (posedge clk) occurred during the
current time step, in order to schedule a42 to be reported during the
upcoming Observed/Postponed region?  I guess this hints back at what was
in the original proposal...  I didn't fully understand why a filtering
method can't work.
 
What's bothering me is that this seems like a very typical usage, where
a designer wants an immediate assertion in b1 but doesn't want to see
glitches on an in-between clock, and this example seems to show that the
deferred asserts with event controls can't be used for this pupose,
making them a lot less useful.
 
 
3.  Have you thought more about this suggested extension that Dmitry
emailed?  Or do you still prefer to defer it for now? 
I would extend it to allow the forms like "assert #0 (@clk expr);".  The
reason of doing that is to be able to use (degenerate) sequences to
specify the assertion body. This will allow building assertion libraries
for boolean assertions. E.g.,

sequence same(a, b, rst, clk)

    @clk rst || a == b;

endsequence : same

assert #0 (same(x, y, 0, posedge clk));

If only syntax "assert @clk (expr);" is permitted, it will be difficult
to build libraries of these assertions.

 
4.  I think we should probably add an example to the proposal in which
one function is called from two processes, showing how a deferred
assertion in the function is executed/flushed independently for each.
 
 

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.