[sv-ac] Minutes from SV-AC meeting 11/9/2010

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.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.