[sv-ac] Review of 3033

From: Thomas J Thatcher <thomas.thatcher@oracle.com>
Date: Fri May 27 2011 - 14:38:49 PDT

Hello Everyone,

This is a review of Dmitry's proposal for 3033. This proposal would
1. Remove checker argument sampling.
2. Make checker non-blocking assignments use the sampled value of their
RHS.
3. Add always_comb always_ff and always_latch
4. Add continuous assignments.

Before I get into a detailed review of this proposal, let me throw out a
radical idea for discussion (since we are changing a bunch of stuff and
breaking backward-compatibility anyway . . .):

Would it make sense to move all checker procedural activity to the
active region set? i.e. move checker non-blocking assignments to the
NBA region and then implement checker continuous assignments in the
active region?

Here's why I'm thinking this:

Many users are still using modules to implement their checking code.
When coding a procedural block in a module, any procedural or continuous
assignments will take place in the active and NBA regions. Signals
defined in these modules work the same way as any other signals. In
assertions, they are sampled according to the same rules as signals in
any other module.

Suppose checkers worked this way: Non-blocking assignments would take
place in the NBA region. Blocking and continuous assignments would take
place in the active region. None of the assignments would use sampled
values. Assertions would use sampled values of input arguments

It seems that this would be much more regular and well behaved. We
would not need all these rules for special cases about what variable s
are sampled and which are not sampled.

Now, on to the proposal.

"-- If an actual argument contains any subexpression that is a const
cast . . ."

        Is more expression needed here to explain that the checker argument
will be used as a const cast? Or is the fact that a checker is
flattened out sufficient?

17.5 Checker procedures

Why not make all procedural assignments use current values, not sampled
values? Then have assertions use the sampled values of all
deterministic checker variables. This would be much more regular. It
would also fix your example: both a (the checker input) and x (the
checker variable assigned in the always_ff) would use the sampled value,
and the assertion would return the same value, no matter whether clk
changes in the Active region (from RTL code) or the Reactive region
(from the test bench). Random checker variables would still be assigned
in the beginning of the Observed region, and assertions would use the
current values of these variables. In the case of Random assignments,
the assume properties that determine the values chosen would use the
sampled values of both the checker inputs, the deterministic checker
variables, and of XMRs that are referenced. So the result would be
consistent, no matter how many times we go around the "big loop" before
we assign the random checker variables. This would also mean that we
wouldn't need to get multiple values for random checker variables, even
if they are solved multiple times in one time-step.

17.7.3
I'm not sure whether we should put this example in or not. There's no
way we could document all the different ways users could cause problems
for themselves.

Tom

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.
Received on Fri May 27 14:39:25 2011

This archive was generated by hypermail 2.1.8 : Fri May 27 2011 - 14:39:40 PDT