Subject: RE: [sv-ac] Scheduling semantics and cost of assertions.
From: Warmke, Doug (doug_warmke@mentorg.com)
Date: Thu Feb 27 2003 - 17:58:42 PST
SV-AC,
We at MTI firmly second Jay's ideas on clocking.
Internally we've been trying to figure out ways
to merge the mainstream SV sampling mechanism
(clocking domains) with what you are doing in AC.
Jay laid out the case very nicely here. Among
other things, simulator implementation will be
much simpler and more efficient if we can agree
to use Jay's proposal.
Regards,
Doug Warmke
> -----Original Message-----
> From: Jay Lawrence [mailto:lawrence@cadence.com]
> Sent: Thursday, February 27, 2003 4:27 PM
> To: Adam Krolnik; sv-ac@server.eda.org
> Subject: RE: [sv-ac] Scheduling semantics and cost of assertions.
>
>
>
>
> 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 - 17:59:32 PST