Subject: RE: [sv-ac] Scheduling semantics and cost of assertions.
From: Bassam Tabbara (bassam@novas.com)
Date: Thu Feb 27 2003 - 10:33:13 PST
Adam I don't think you necessarily need to physically copy/duplicate for
assertion purpose....if you do this right. The wording is just to get
the concept across, not implementation.
-Bassam.
-- Dr. Bassam Tabbara Technical Manager, R&D Novas Software, Inc.http://www.novas.com (408) 467-7893
> -----Original Message----- > From: owner-sv-ac@server.eda.org > [mailto:owner-sv-ac@server.eda.org] On Behalf Of Adam Krolnik > Sent: Thursday, February 27, 2003 10:21 AM > To: sv-ac@server.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 - 10:36:19 PST