Subject: [sv-ac] Scheduling semantics and cost of assertions.
From: Adam Krolnik (krolnik@lsil.com)
Date: Thu Feb 27 2003 - 10:21:07 PST
Hello all;
Reading the scheduling semantics paper I have a concern about how properties
are being supported.
I wrote:
"I do not understand how signals in an assertion are able to be scheduled into the
'preponed' block apriori to the clock event. E.g. Once the clock becomes an active
event all blocks awaiting the clock change are added to the active region?
Then we complete the active queue and iterate back to the active region. But
how did we figure out that we should sample the 'sampled data' because the assertions
are now going to be evaluated (in this timestep.)"
Steve wrote:
"The signal values are captured irregardless of whether the clock signal occurs. If
it indeed occurs then we have the sampling condition and the sampled values are
then real and process during assertions."
So here's an example process...
assign clk = #50 ~clk; // Generate the clock.
assign clk1 = #10 ~clk1; // Another clock;
assign clk2 = #12 ~clk2; // YAC.
// Here's my assertion.
always @(posedge clk)
assert (a;b;c;d;e;f;g;h;i;j);
assert (m;n;o;p;q;r;s;t);
...
So a simulator must recognize assertions and for each signal in an assertion, create
a sample for that value that runs in the preponed (prepended?) block. Then when the
clock event occurrs and schedules all processes sensitive to the signal into the active
block we can evaluate the assertion.
So the preponed (prepended) block must execute for EVERY simulation time tick.
This block will consist of a value copy for EVERY signal listed in an assertion.
On a previous project, we benchmarked the assertions in the design to cost about 30%
of the simulation. We had about 1000 assertions. I proposed a metric that their cost
was about the same as 4 registers in the design (We had about 12000 registers in the
design.) Our assertions executed on each clock edge (it was sensitive to.)
So now it seems that assertion cost will be based on the number of signals being used
in the assertions and now many simulation timesteps occur.The number of signals is a
function of the assertions. The number of timesteps is a function of the design, clocks,
external models, etc. It seems to me that this may not be a good computation model for
assertions.
Is this a correct assessment of how assertions/properties are going to work?
Should I ask this question to the other SV groups?
THanks.
Adam Krolnik
Verification Mgr.
LSI Logic Corp.
Plano TX. 75074
This archive was generated by hypermail 2b28 : Thu Feb 27 2003 - 10:22:42 PST