Subject: [sv-ec] RE: [sv-ac] Scheduling semantics and cost of assertions.
From: Jay Lawrence (lawrence@cadence.com)
Date: Mon Mar 10 2003 - 07:14:24 PST
Stephen,
I think we will have to take this issue to a larger group than just the
sv-ac. The simulation semantics working group and sv-ec have agreed on
the clocking domain as the way of indicating a sampled signal. Yes, it
allows for skews etc, but in the simplest form acts like the implicit
sampling as specified for assertions. We should look at ways of unifying
the assertion sampling and clocking domains so that the semantics are
only explained once.
Some suggestions would be:
- allow implicit declarations in clocking domains
Today there is a bunch of repetitive syntax to get #1 step
sampling. If we just allow any variable/net used in clocking domain
without a declaration to have the #1 step then the syntax is greatly
reduced and typos are eliminated.
- allow the use of a clocking domain name in an event control to
indicate sampling should be used.
I think this work is a natural extension of having the other committees
review each others work during the integration of everyones
contributions into the final draft LRM. Assumptions by one committee
(such as the sv-ec's use of clocking domains) must be validated and
discussed with the others.
A few more comments are interspersed below.
Jay
> -----Original Message-----
> From: Stephen Meier [mailto:Stephen.Meier@synopsys.com]
> Sent: Tuesday, March 04, 2003 2:41 PM
> To: sv-ac@eda.org
> Subject: RE: [sv-ac] Scheduling semantics and cost of assertions.
>
>
> 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.
>
The LRM needs one consistent place to describe this (I suggest the
clocking domain) and then the other places should refer to it (i.e.
describe the equivalent clocking domain implied, if any).
> 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.
>
You left out synthesis as another tool that typically looks at the
cycle-accurate view of the design. Our experience is that the vast
majority of design styles in use already de-race values around clocks so
that pre-/post- synthesis results match. If the user still has these
kinds of races many years after the introduction of NBA assignments then
they have much bigger problems than figuring out how to get simulation
and formal to agree.
> 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.
Yes, we agree these optimizations exist, we already implement them for
VHDL `delayed signals (which is really all a clocking domain input
provides), however, no matter how much you optimize them the performance
degredate is non-zero which means it is slower than using non-sampled
values.
>
> So the key points are that the semantic is well defined and
> robust and the
> simulation
> overhead is not too high.
After delivering commercial HDL simulators for the last 15 years it is
my opinion that any overhead that can be avoided is too high. The user
should be given the option. Put them in clocking domain (or otherwise
indicate a sampled value) and you pay the price. Don't do it and you get
some non-determism with the benefit of more speed. This is Verilog.
>
> 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.
>
The are also avoided by good synthesis coding practices adopted by
virtually all Verilog users. We also believe that there is a place for
completely asynchronous invariant assertions for checking conditions
that should be preserved even between clock edges.
> 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.
I don't think I proposed that this would be a simplification for
implementation. As noted above, we already do this for VHDL and the
Verilog equivalent is pretty trivial.
One your second point in this paragraph, sampling variables and having a
clock are not equivalent. You can have an assertion sensitive to a clock
and reference non-sampled values as long as they are stable at that
clock. The "reference point for passing time in a sequence" is exactly
the same.
>
> 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 : Mon Mar 10 2003 - 07:16:41 PST