Minutes from SV-AC Committee Meeting
Date: 2016-04-06
Time: 16.00:00 UTC (9:00 PDT)
Duration: 1 hour
Agenda
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 2016-03-09:
v[.x-] Mehbub Ali (Intel)
v[.xx] Ang Boon Chong (Intel)
v[x-x] Shalom Bresticker (Accellera)
v[.x-] Dennis Brophy (Mentor Graphics)
v[xxx] Eduard Cerny (Synopsys)
v[xx-] Ben Cohen (Accellera)
t[x-x] Dmitry Korchemny (Synopsys - Chair)
v[xxx] Manisha Kulshrestha (Mentor Graphics)
v[xxx] Anupam Prabhakar (Mentor Graphics)
v[xxx] Erik Seligman (Intel – Co-chair)
v[x-x] Samik Sengupta (Synopsys)
|- attendance on 2016-04-06
|--- voting eligibility on 2016-03-09
Minutes
IEEE patent policy reminder
Minutes approval
Erik: Move to approve the minutes from SV-AC meeting 2016-03-23.
Manisha: Second
Vote: 6y/0n/1a (Samik abstained as he was absent at the last meeting)
Meeting minutes have been approved.
Email ballot results
Issue 3117 failed: 6y/1n/0a (+1 late yes)
Issue 5476 passed: 7y/0n/0a (+1 late yes)
Issue 5517 passed: 7y/0n/0a
Dmitry: Since Mehbub was not in the list of the voters, though he was a valid voter, I suggest to confirm the email ballot results by voice vote.
Ed: Move to revote to accept issues 5476 and 5517.
Anupam: Second.
Issues 5476 and 5517 reapproved: 7y/0n/0a
Mantis 3117: make it clear that rewriting algorithm (F.4.1) applies to checker and let
Manisha: Got comments from Shalom that let is not covered in this proposal. Modify this proposal or to create a new one for let?
Shalom, Ed: Better to create a separate proposal for let rewriting.
Dmitry: This proposal does not cover checker output arguments. Need to mention how they are handled in rewriting.
Manisha: Will update the proposal and send a notification.
Mantis 4750: Allow immediate assertions in checker body
Anupam: Need to modify Mantis title and description. Immediate assertions are not allowed in a checker body. The proposal is about checker always procedures. Need also indicate the subclause where the changes are to be done, in the proposal.
Dmitry to fix and call to vote.
Mantis 4037: Define false vacuity and contributions to pass/fail counters in simulation
Ben: The reason to handle this proposal in this PAR is the undefined behavior for coverage counting in presence of vacuity in some cases.
Ed, Dmitry: This is, indeed, a conceptual problem. However, it does not happen in practice.
Ed: E.g., a property with double negation will behave differently.
Dmitry: Need more discussion for this item.
Mantis 5548: Non-degeneracy: limitations and references
Ben: The industrial simulators not always impose the non-degeneracy rule.
Dmitry: The existing non-degeneracy condition prevents several rewriting rules. Followed-by with a degenerate sequence cannot succeed.
Manisha: However, according to current definition, followed-by should require a non-degenerate antecedent. Need to make this requirement explicit.
Mantis 5372: Need to clearly define the term "tick" before using
Dmitry: Suggest to define clock tick as a time step where the clocking event occurs
Shalom: This will require to change the wording in many cases.
Ed, Samik: Why not occurrence of the event?
Dmitry: This is not exact. E.g., assertions are evaluated in the Observed region, but clocking events usually occur in the Active or the Reactive region.
Shalom: Tick is sometimes used as a verb. Also, what about a tick of the global clock?
Erik: Looks like the definition based on the time step will do the work in most cases.
Opens
Anupam: In the LRM on p.346 it is written that $ stands for the end of simulation. This is wrong. Will fill a Mantis.
--
Erik Seligman - 2016-04-20
Comments