Subject: RE: [sv-ac] Scheduling semantics and cost of assertions.
From: Stephen Meier (Stephen.Meier@synopsys.com)
Date: Tue Mar 04 2003 - 11:40:35 PST
Doug, Jay, Adam et al:
The sampling mechanism defined by SV is the same for both SV-EC and SV-AC,
the only difference is that the clocking domain provides additional
parameters to control skew values, where AC uses only the default skew.
All concurrent assertions use sampled variables in order to support a clean
and consistent cycle based semantic that can achieve the same results
between simulation and formal and hw accelerators.
WRT simulation performance our experience indicates that there are
optimizations which enable a much lower overhead on simulation. Variables
can be updated only when they change and thus there is only small overhead
of having a second copy of variables. As you indicate there may also be
opportunities
to recognize when a signal is race free with respect to the clock and thus
no shadow
copy is required.
So the key points are that the semantic is well defined and robust and the
simulation
overhead is not too high.
Opening the door to non-sampled signals would bring out a whole bunch of issues
and scope that we have carefully avoided. There are problems with false
and multiple firings and
event ordering. All of these issues are avoided with the sampling semantic.
Lastly I do not understand why the task of implementation in simulator
would be simplified in that in Jay's proposal the sampling would need to be
supported and in addition the simulator would need to support accessing
current variable values. In addition, what is the reference point for
passing time in a sequence when there is no clock defined.
Steve
---------
At 05:58 PM 2/27/2003 -0800, Warmke, Doug wrote:
>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
> > >
> > >
> > >
> > >
> > >
> > >
> > >
> >
Steve Meier (stephen.meier@synopsys.com) W: 650-584-4476, Cell: 408-393-8246
This archive was generated by hypermail 2b28 : Tue Mar 04 2003 - 11:42:30 PST