SV-ACMinutes2010_11_09 < P1800

P1800 Web>SystemVerilogAssertionCommittee>SVACMeetingMinutes>SV-ACMinutes2010_11_09 (2010-11-19, ErikSeligman) (raw view)EditAttach
Minutes from SV-AC Meeting

Date: 2010-11-09

Time: 16:00 UTC (9:00 PDT)

Duration: 1.5 hours

Dial-in information:

--------------------

Meeting ID:            38198

Phone Number(s):

1-888-813-5316         Toll Free within North America

Live Meeting: [[https://webjoin.intel.com/?passcode=2598352]]

Agenda:

-------

- Reminder of IEEE patent policy.

See: http://standards.ieee.org/board/pat/pat-slideset.ppt

- Minutes approval

- Email ballot results

None

- New issues

None

- Enhancement progress update

Simulation semantics of deferred assertions

Continuous and blocking assignments in checkers

- Issue resolution/discussion

2206: Random simulation of non-deterministic free variables in checkers

- Opens

SV-AC meeting schedule

Attendance Record:

------------------

         Legend:

                 x = attended

                 - = missed

                 r = represented

                 . = not yet a member

                 v = valid voter (2 out of last 3 or 3/4 overall)

                 n = not a valid voter

                 t = chair eligible to vote only to make or break a tie

Attendance re-initialized on 2010-07-06:

  v[xxxxxx-x-xxxxx--xxx] Laurence Bisht (Intel)

  v[xxxx-xxxxxxxxxxxxx-] Eduard Cerny (Synopsys)

  v[xxxxxx-xxxxx-xxxxxx] Ben Cohen

  v[xx-x-xxx-x--xxxxxxx] Surrendra Dudani (Synopsys)

  v[-xx---xxxx---x-xxxx] Dana Fisman (Synopsys)

  v[xxx-xxxx-x-xxxxxxxx] John Havlicek (Freescale)

  v[xx-xxx-xxxxxxxxxxxx] Tapan Kapoor (Cadence)

  t[xx--xxxxxxxxxxxxxxx] Dmitry Korchemny (Intel ¿ Chair)

  v[xx--xxxxxx-xxxxxxxx] Scott Little (Freescale)

  v[x-xxxxxxxxx-xxxxxxx] Manisha Kulshrestha (Mentor Graphics)

  v[xxxxxxxxxxxxxxxxxxx] Anupam Prabhakar (Mentor Graphics)

  v[xxx-xx--xxxxxxx-xxx] Erik Seligman (Intel)

  v[xx--xxxxxx-xxxxxxx.] Samik Sengupta (Synopsys)

  v[x-xxxxxxxxxxxxx-xxx] Tom Thatcher (Oracle ¿ Co-Chair)

    |- attendance on 2010-11-09

  |--- voting eligibility on 2010-11-09

Minutes:

--------

- Reminder of IEEE patent policy.

See: http://standards.ieee.org/board/pat/pat-slideset.ppt

- Minutes approval

Erik: Move to approve minutes

John: Second

     Vote results 12y, 0n, 0a

- Opens

SV-AC Meeting schedule:

Manisha: Can we change the meeting to 8:30

     Because US is now on standard time, her local time is 1 hour later.

Tom:  8:00 would be too early, 8:30 is doable.

Erik: Move to reschedule meeting 1/2 hour ealier

John Second

     vote results; 136, 0n, 0a

Ed:  Will reschedule phone conference

Dmitry:    Will reschedule livemeeting.

- Issue resolution/discussion

2206: Random simulation of non-deterministic free variables in checkers

Dmitry: AC had voted to close as duplicate

     Champions had opposed: "Duplicate of what"

Erik: 17.7.2 seems to describe this operation

John: Move to Change status to "no change required"

     Include a reference to 17.7.2

Erik: Second

     Vote results: 12y, 0n, 0a

(Dana Joined)

- Enhancement progress update

Simulation semantics of deferred assertions:

Discussing 3206 example

     Deferred assertion embedded in an always_ff @(posedge clk)

    References variables a & c

     C is driven from a non-blocking assignment in the same block

     a is driven from a program block through a clocking block with #0

     sampling.

Tom: Seems that this example: assert #0 could be replaced by assert

     property with no loss of function.

Dmitry:    Not for equivalence checking. Concurrent assertions require a clock

     Formal equivalence checking does not define a clock.

John: But this means that assertion is checked all the time.

John:     Is it typical to write assertion on both primary input and internal

     signals? Would prefer to see assertion written only on primary inputs.

Continuous assignments in checkers:

Dmitry:    In his paper, he proposed that continuous assignments would update

     in reactive region.

Anupam:    Does it make sense to synchronize checker inputs in reactive region

     Like clocking block: Any input to the clocking block is only seen

     in the observed region.

     If checker inputs were synchronized similarly, then deferred

     assertions within checkers would not glitch.

Ed:  Random variables: Assigned new values just before observed region

     Shouldn't continuous assignments be similar?

Ed: Given example assertions in LiveMeeting

     (note: We should post the examples on the e-mail reflector)

     If continuous assignments occur in Reactive, then A1 would be bad

     If occurs in Active, then A2 would be bad.

Dmitry:    But if we use Anupam's suggestion of clocking-blok synchronization,

    that would fix A1.

Tom: Isn't this the same as just having sampled values for inputs?

Anupam:    No, it's different.

Lawrence: This would break the rewriting algorithm.

Ed:  This would break symmetry between active & reactive

Dmitry:    One other suggestion would be adding Re-observed region.

Manisha: We can't move the regions. We can only describe how checkers work

     with the given regions.

Dmitry will ask working group about this at next working group meeting.

Dmitry:    Three approaches

     New Re-Observed region

     Move observed region after reactive

     Handle a mix of design and test bench variable correctly

Sampled Value Definition

Dmitry:    Anupam had suggested moving definitions of sampled value to the

     section on the $sampled function.

Samik:     Why is this a big change? It seems to be just copying one section

     to another place tin the LRM.

John: Think it's better to put the definition before, and have the $sampled

     section refer to it.

Meeting adjourned.
Topic revision: r1 - 2010-11-19 - 18:25:56 - ErikSeligman
P1800