Subject: Re: Assertion Committee Meeting Minutes
From: Adam Krolnik (krolnik@lsil.com)
Date: Mon Mar 11 2002 - 11:09:50 PST
Hello Rajeev;
I like this example to illustrate my question about if the accept/reject
statements must be at the front of the assertion.
always @(posedge clk)
if (fifoFsmState == READ)
assert accept(ack) (dataValid * [0:15]);
Your design statment, reads like:
"Once the fifo goes to READ state, the dataValid must be held high for
15
cycles or when the ack goes high, whichever comes first."
The language I have refers to this accept clause as an 'until' clause.
It allows for dynamic closing of the checking time window. Since the
english statement has this closing statement after the testing
condition,
it would also be nice to have the assertion language be able to
specify this acceptance/until clause later too.
E.g. I would write
assert (fifoFsmState == READ -> dataValid {0:15} until ack);
If one could write an assertion like:
assert (fifoFsmState == READ triggers (dataValid * [0:15] accept (ack));
or
assert (fifoFsmState == READ triggers (dataValid * [0:15] until (ack));
It would fit more closely with the english statements we which to
translate
into this code.
Choosing the below list reminds me of the necessary operation we call
delay().
This function like operation provides for previous cycle values of
signals.
It is tedious to have to write code to register signals (or find a
different
stage signal) to write an assertion with. This operation keeps track
of the previous value requested for a signal. Here is a simple (and
common)
usage of this idea:
"When a request(req_valid) is asserted, the address(addr)
must be driven for 2 clocks."
assert (req_valid triggers (1; delay(addr, 1) == addr)
$error("Request did not provide stable 2 cycle address.");
"When the queue becomes full, it must become unfilled within 50 cycles."
assert (posedge(cq1s_sa_full) triggers negedge(cq1s_sa_full) {1:50})
This second example is a derivative of the delay() function - posedge
is defined as posedge(sig) :== ~delay(sig, 1) && sig. Negedge is
the opposite. In fact, the first example actually would use the function
stable() which implements the example test expression.
These example only show usage of delay() to obtain the value the
previous cycle.
We have used the delay() functionality for several cycles in the past.
One example is to check for past implication.
"A request_done assertion must have been preceeded by a request_valid
assertion
within the last 50 cycles."
assert:hadReq (request_done triggers delay(request_valid, 50) * [0:49]
$error("Extra request_done asserted without corresponding request
valid.");
In fact, the larger example of this is where a need for controlling the
retriggering
of the assertions comes into play. Ideally one would like to be able to
check
for this kind of correctness given 0, 1, N pipelined transactions, but
this
is a larger topic for discussion.
Looking at previous assertion examples, here is a very common set:
[$atmost1 returns true if 0 or 1 bits are set; $posedge/$negedge is
explained
above; $in() can accept ? as a don't care specification.]
assert ($atmost1({sq2s_actl_load[2], sq2s_actl_shift[2]}))
$error("mux failed on lowmux selects: %b",
{sq2s_actl_load[2], sq2s_actl_shift[2]});
assert ($exactly1(sq1s_actl_nfull[10:0]))
$error("trashed nfull counter: %b",sq1s_actl_nfull[10:0]);
assert:ie_sel_s4_b (en2 triggers $atmost1(leie_sel_s4,aeie_sel_s4,
seie_sel_s4,beie_sel_s4)
$error("stage 4 intermediate exponent select must be one-hot");
assert ($posedge(mq2q_ldq_valid[0] & ~`RQ_SCHED_CTL.rq2q_cqaq_stop)
triggers ($negedge(mq2q_ldq_valid[0])
| `RQ_SCHED_CTL.rq2q_cqaq_stop) * [1:1500])
$error("MQ LDQ req in entry 0 did not get completed in 1500
cycles.");
assert:legal (rq1s_apsh triggers
$in({rq1s_dst, rq1s_apr, rq1s_coh, rq1s_wr, rq1s_brst,
rq1s_tt, rq1s_lock, rq1s_gart, rq1s_iowp},
`attr_single_read, `attr_single_write,
`attr_dcache_read, `attr_dcache_write,
`attr_io_read, `attr_io_write,
`attr_msr_read, `attr_msr_write))
$error("Adam, what is this command? %0h",
{rq1s_dst, rq1s_apr, rq1s_coh, rq1s_wr, rq1s_brst,
rq1s_tt, rq1s_lock, rq1s_gart, rq1s_iowp});
assert:badACaccess ($delay(ac2s_adctl_acvalid, 1) && !lq1f_use_ma1_ars)
->
$in($delay({rf1s_ars_prefetch,rf1s_ars_nullreq,rf1s_ars_invlpg,
rf1s_ars_pa,rf1s_ars_special,rf1s_ars_io,rf1s_ars_lock,
rf1s_ars_write,
rf1s_ars_read,rf1s_ars_user,rf1s_ars_imm,
rf1s_ars_fp,rf1s_ars_noex},1),
13'b100000001?00?, //prefetch
13'b010000????0??, //nullreq
13'b0010?00??010?, //invlpg
13'b0001000???00?, //pa_in_smi
13'b000010001?00?, //MSR read
13'b00?010010?00?, //MSR write
13'b00?010011?00?, //MSR RMW
... ))
$error("illegal AC access.
rf1s_ars_prefetch,rf1s_ars_nullreq,rf1s_ars_invl
pg,rf1s_ars_pa,rf1s_ars_special,rf1s_ars_io,rf1s_ars_lock,rf1s_ars_write,rf1s_ar
s_read,rf1s_ars_user,rf1s_ars_imm,rf1s_ars_fp, rf1s_ars_noex =
%1b%1b%1b%1b%1b%1
b%1b%1b%1b%1b%1b%1b%1b\n",
rf1s_ars_prefetch,rf1s_ars_nullreq,rf1s_ars_invlpg,rf
1s_ars_pa,rf1s_ars_special,rf1s_ars_io,rf1s_ars_lock,rf1s_ars_write,rf1s_ars_rea
d,rf1s_ars_user,rf1s_ars_imm,rf1s_ars_fp, rf1s_ars_noex);
Adam Krolnik
Verification Mgr.
LSI Logic Corp.
Plano TX. 75074
This archive was generated by hypermail 2b28 : Mon Mar 11 2002 - 11:11:13 PST