Subject: accept/reject
From: Erich Marschner (erichm@cadence.com)
Date: Tue Apr 02 2002 - 14:22:47 PST
Tom,
In the last meeting, I agreed to provide some information about how Sugar supports accept/reject semantics. In the following, I've shown how I would express the first four of the accept/reject properties on page 11 in Sugar 2.0, based upon my current understanding of Sugar. The other four properties (assert_strobes) should be symmetrical.
Since Sugar has sequence implication instead of using if statements to express the triggering condition, I've first shown these in sequence implication form (with the antecedent True), and then in a form showing how this might adapted to fit into the DAS/System Verilog context.
1. Assert with Reject on Sychronous input
original: a7: assert reject (!busy) (a;b;c) @@(posedge clk); // busy must be 1
Sugar20: assert {True} |-> (busy[*] && {a; b; c}) @(posedge clk);
adapted: assert (busy[*] && (a; b; c)) @@(posedge clk);
This uses the standard Sugar idiom for distributing a boolean condition over a sequence. The && operator requires sequences of the same length, so the "busy[*]" operand is effectively restricted to being of the same length as the other operand, thus the assertion passes only if busy is high for the duration of the sequence {a; b; c}.
By the way, this idiom is useful for more than just requiring a single signal to be asserted for the duration of another sequence. Sugar also supports regexp qualifies [=...] and [->...], which allow you to specify discontiguous occurrences of a condition. For example,
(busy[=2..] && {a;b;c;d;e})
means that 'busy' is true in 2 or more not-necessarily-contiguous cycles during the occurrence of the sequence {a;b;c;d;e}, and
(busy[->2] && {a;b;c;d;e})
means that 'busy' is true for the 2nd time in the last cycle of of {a;b;c;d;e}, but the first time could be in any of the previous cycles.
2. Assert with Accept on Sychronous input
original: assert accept (sync_reset) (a;b;c) @@(posedge clk);
Sugar20: assert (({True} |-> {a; b; c}) until sync_reset) @(posedge clk);
adapted: assert ((a; b; c) until sync_reset) @@(posedge clk);
This illustrates the use of nested formulae in Sugar. The main formula is (f1 until f2); f1 is then ({True} |-> {a; b; c}), and f2= the boolean sync_reset. In addition to (f1 until f2), Sugar also supports the following variations of 'until':
(f1 until! f2) f2 causes acceptance, and f2 is required to occur
(f1 until_ f2) (f1 && f2) causes acceptance - i.e., f1 must not fail until at least a cycle after f2 is true
(f1 until!_ f2) same as (f1 until_ f2), except that f2 must occur
3. Assert with Reject on Asychronous input
original: a7: assert reject @(negedge busy) (a;b;c) @@(posedge clk); // busy must be 1
Sugar20: assert {True} |-> (busy[*] && ({a; b; c} @(posedge clk)));
adapted: assert (busy[*] && ((a; b; c) @@(posedge clk)));
The primary change required to make the property fail asynchronously is to associate the clock only with the {a;b;c} sequence. The rest of the property is evaluated at every simulation cycle (or, if optimized, just whenever 'busy' changes).
4. Assert with Accept on Asychronous input
original: assert accept @(posedge async_reset) (a;b;c) @@(posedge clk);
Sugar20: assert ((({True} |-> {a; b; c}) @(posedge clk)) until async_reset);
adapted: assert (((a; b; c) @@(posedge clk)) until async_reset);
Same thing here - moving the clock so that it applies only to the synchronous part of the assertion should suffice.
Regards,
Erich
-------------------------------------------
Erich Marschner, Cadence Design Systems
Senior Architect, Advanced Verification
Phone: +1 410 750 6995 Email: erichm@cadence.com
Vmail: +1 410 872 4369 Email: erichm@comcast.net
This archive was generated by hypermail 2b28 : Tue Apr 02 2002 - 14:24:00 PST