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.