Subject: Re: OVL suggestions
From: Adam Krolnik (krolnik@lsil.com)
Date: Tue May 07 2002 - 10:30:40 PDT
Good morning Dave, everyone;
>4. "pipelined" assertions - One of the few things I've picked out >from Adam Krolink's discussions on future assertion languages is the >concept of "pipelined" assertions. This is where assertions have the >ability to overlap without the use of some external logic. So there
>would be only one implementation of an assertion, but there might be
>several outstanding instances of this one assertion tracking different
>occurences. This ties in with the assert_handshake, in which there
>are multiple outstanding reqs that correspond to different >transactions.
Reviewing the design of my assertion tool, I noticed this
contrast in assertion functionality.
Positive assertions (like the SystemVerilog assertions) are
pipelining - they will track pipelined events and will not
sync on a single event when there is a variable window. One
can specify the degree of pipelining to produce an additional
error when the amount of pipelining exceeds the preset bounds.
E.g. If you can only have 3 outstanding requests, the 4th will
produce an error. If you are using logic that you don't want
pipelining (or retriggering until it completes), you can either
trigger when a signal rises (the positive edge) or turn off the
pipelining (another way is to use a second assertion to prevent
subsequent triggering until the first one completes.)
Negative assertions (like the OVL win_unchange) specify a
window to be checked for the one thing - the absence of change.
My tool treats has a separate keyword for negative assertions
and does not pipeline them. This model most fits the SystemVerilog
assertions.
SystemVerilog and users would benefit from being able to use
the assert statement in their code without the requirement
for extra code to support the statement when dealing with
pipelined events.
> 5. assertion that contains state - These might fall into
>the realm of a protocol type checker, and might also be beyond the >bounds of what the OVL is intended to be. I've written some small >assertions that keep
Dave, could you forward what the OVL 'assert_implication' looks like?
Sugar has the concept of local values (variables?) that allow one
to store state (for that particular thread) to allow comparison
to state in the future. This can be simplified down to a simple
concept - that of a loadable register (loaded based on an assertion
triggering.) Actually, here is a reason that there should be a
'trigger' keyword as part of an assertion. The problem with
if (expression) assert_strobe()
is that to store state (registering some value) it is outside the
assertion and thus is static (not part of the assertion thread.) I.e
if (start_trans)
begin
trans_addr = bus_address;
assert_strobe (; [0:1000]; trans_done
; cache_addr == trans_addr)
else $error("Incorrect cache address %h for corresponding read
request on bus %h.", cache_addr, trans_addr);
end
This code would not work if a design allowed multiple transactions
to start before the first one completed. Now if one could capture
the bus address within the assertion, then you could have the
state local to the thread of the assertion.
assert_strobe (start_trans ; [1:1000]; trans_done
; cache_addr == $captured(bus_addr))
else $error(...);
Adam Krolnik
Verification Mgr.
LSI Logic Corp.
This archive was generated by hypermail 2b28 : Tue May 07 2002 - 10:33:19 PDT