Subject: RE: [sv-ac] Scheduling semantics and cost of assertions.
From: Jay Lawrence (lawrence@cadence.com)
Date: Thu Feb 27 2003 - 16:26:45 PST
Adam,
We too (Cadence) believe that having every single signal in an assertion
required to be sampled would be expensive, and it is only necessary when
there are races between the clocking signal and the expressions in the
assertion.
Many folks on the sv-ec have noted that it is not every signal in every
assertion really since most signals are referenced in multiple
asssertions and you only need to sample the value once, but it is still
a big number.
The SystemVerilog 3.1 draft includes the concept of a "clocking domain".
Signals in the clocking domain hold sampled versions of the signals. So
you right something like
module foo (input clk; inout [31:0] bus; input logic grant; output logic
req);
clocking busclk @(posedge clk)
input grant;
output req;
inout bus;
end clocking
endmodule
Now the signals inside the clocking domain are the sampled version of
the signals and they are sampled relative to (posedge clk). There is a
bunch more syntax to specify skews etc.
So... If a user wants to reference sampled values in an assertion, they
can either
- place the assertion in the clocking domain
- reference the sampled signals with a hierarchical path
(Excuse the most probably incorrect assertion syntax below)
module foo (input clk; inout [31:0] bus; input logic grant;
output logic req);
clocking busclk @(posedge clk)
input grant;
output req;
inout bus;
property p = (grant) -> (req) // is in
clocking domain
assert p;
end clocking
property p = (busclk.grant) -> (busclk.req) //
references signals hierarchicaly
assert p;
endmodule
All the reference to 'grant' and 'req' above would be sampled.
Now, if you believe you have properly used non-blocking assignments or
delays such that there are no race conditions between clk and the
signals in the conditions of the assertions then you can avoid all this
and just use an assertion directly on the signals and not incur any
overhead for sampling.
module foo (input clk; inout [31:0] bus; input logic grant;
output logic req);
property p = (grant) -> (req)
assert p;
endmodule
(Here comes the editorial part)
Note, that in Ncsim's implementation of PSL/Sugar we do not have the
concept of a clocking domain and have had no issues with race conditions
of this sort. Most Verilog users are pretty good a de-racing around
latches since there designs break or get different pre-/post- synthesis
results if they don't do it right. None the less, clocking domains have
been added to achieve a guaranteed semantic match for the paranoid or
careless and a user can choose to reference either the sampled or real
signal.
Jay
===================================
Jay Lawrence
Architect - Functional Verification
Cadence Design Systems, Inc.
(978) 262-6294
lawrence@cadence.com
===================================
> -----Original Message-----
> From: Adam Krolnik [mailto:krolnik@lsil.com]
> Sent: Thursday, February 27, 2003 10:21 AM
> To: sv-ac@eda.org
> Subject: [sv-ac] Scheduling semantics and cost of assertions.
>
>
>
>
> 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 - 16:27:33 PST