Agenda for next Meeting: Since I failed to ask everyone in the meeting about next meeting's agenda, please email me what you would like to discuss in the next meeting. Attendees: Listed at the end of the summary: Summary: -------------- Dejan Nickovic presented examples from DDR2 case study, followed by Mike Demler's (Synopsys) and Ed Cerny's (Synopsys) presentations. Srini (Synopsys) raised the question of using SV Tasks to check some of the examples presented by Dejan. Dejan answered that assertions were less ad hoc and that procedural AMS was not accurate enough to capture all the properties. Srini wanted to know about the compactness of the property. Dejan mentioned that assertions were more concise than writing in 'C', also assertions are more expressive, they might not be that much more concise than writing them in VAMS equivalent constructs. On one of the examples (Figure 7, Dejan's presentation), with slew rate detection, John mentioned that local variables could be used to verify the variable timing check on the property. Dejan agreed and mentioned that it could be done. It was mentioned that as long as local variable had a value that could be referenced and was evaluated before used, it could be used in an assertion like that. Mike Demler presented the problems that cannot be checked with pure waveform viewing/checking capabilities and presented examples on the problem a circuit might have when low voltage inverted is incorrectly connected to higher voltages. Static checking capability is required in order to detect power budgets, or violations of transistor level properties. Ken Bakalar mentioned such checks could be done at the time of elaboration or if done dynamically at time zero. Kevin Jones added that if the circuit is digitally controlled then it might be interesting to see whether the condition is a problem only under certain circumstances and that it might be dependent on some other property. Dejan had a point that it could be viewed as a general modal logic problem rather than a temporal logic problem. The discussion focused on how to detect a path to power or ground in order to prove correctness of the circuit. Or how would one check dc paths which might created (active/static checks). Ken wanted to separate the two issues - Algorithms (used to do the checks) from Syntax (and how you specify the checks) from each other. The checks could be done on the transient simulations or some other tool - maybe some other kind of simulator which does a different type of analysis. Ed Cerny presented couple of examples and their renderings on the extended System Verilog Assertions. Ken wanted to know whether Ed had tried to write those examples in Verilog AMS. Ed's examples had functions borrowed from the VAMS language like cross and also introduced some new constructs like "restrict" and "simulation time" semantics to the assertions. Sri Chandra mentioned that with the work on the integration of P1800 analog functions should be available within the language to System Verilog Assertions. Dejan mentioned that assertion language should be independent of the implementation like PSL has different syntax flavors for different languages. Himyanshu wanted to know why the restrict operator was used and why time based operator was not used. Ed said that it was due to efficiency (did not want to check at every time step but only at events) and also because events are already available in SVA and ties nicely with other System level constructs. Himyanshu mentioned that "end of time" concept could be used to specify the property passed or failed within a certain duration. John Havlicek wanted to allow for greater flexibility and let the tool worry about the internal implementation and efficiency issues. Ed agreed that time based semantics could be added in addition to event based semantics. Documents: All documents related to Analog assertion released to the committee can be accessed at http://www.eda-stds.org/verilog-ams/htmlpages/public-docs/AMS_Assertions / <http://www.eda-stds.org/verilog-ams/htmlpages/public-docs/AMS_Assertion s/> 1) Dejan Nickovic's presentation is available at - http://www.eda-stds.org/verilog-ams/htmlpages/public-docs/AMS_Assertions /assertions_examples_dejan.zip <http://www.eda-stds.org/verilog-ams/htmlpages/public-docs/AMS_Assertion s/assertions_examples_dejan.zip> 2) Mike Demler's presentation is available at http://www.eda-stds.org/verilog-ams/htmlpages/public-docs/AMS_Assertions /analog_properties_for_100708.ppt <http://www.eda-stds.org/verilog-ams/htmlpages/public-docs/AMS_Assertion s/analog_properties_for_100708.ppt> 3) Eduard Cerny's presentation is available at http://www.eda-stds.org/verilog-ams/htmlpages/public-docs/AMS_Assertions /SVA_analog_simtime.SNPS081005ec.ppt <http://www.eda-stds.org/verilog-ams/htmlpages/public-docs/AMS_Assertion s/SVA_analog_simtime.SNPS081005ec.ppt> 4) We (Scott Little and Himyanshu Anand) have added some more examples to the ones which were presented last week and the document can be accessed at http://www.eda-stds.org/verilog-ams/htmlpages/public-docs/AMS_Assertions /AMSproperties.pdf <http://www.eda-stds.org/verilog-ams/htmlpages/public-docs/AMS_Assertion s/AMSproperties.pdf> Name Company 18-Jun-08 18-Aug-08 23-Sep-08 7-Oct-08 Erik Seligman Intel 1 1 1 1 Thanapoom Lertpanyavit Intel 1 1 1 1 David Smith Synopsys Mike Demler Synopsys 1 1 1 1 Ed Cerny Synopsys 1 1 1 1 Venkataramanan Srinivasan Synopsys 1 1 Dave Cronauer Synopsys 1 1 1 1 Prabal Cadence 1 Scott Cranston Cadence 1 Adam Sherer Cadence 1 Martin O'Leary Cadence 1 1 Dennis Brophy Mentor Graphics 1 1 Kenneth Bakalar Mentor Graphics 1 1 1 Kevin Jones Individual Contributor 1 1 1 Patrick Holloway Tiburon Design Automation 1 1 David Tiburon Design Automation 1 Mark Tiburon Design Automation 1 1 Dejan Nickovic Verimag 1 1 Pallab Dasgupta IIT-KGP Sri Chandra Freescale 1 1 1 Dave Miller Freescale 1 1 John Havlicek Freescale 1 1 1 1 Hillel Miller Freescale 1 1 1 Scott Little Freescale 1 1 1 Himyanshu Anand Freescale 1 1 1 1 Brian Mulvaney Freescale 1 1 Phillip LaPlace Freescale 1 Daniel Christopher Freescale 1 Linda Lin Freescale 1 Saurabh Garg Freescale 1 1 1 Benjamin Ehlers Freescale 1 1 Zhang Yonggang Freescale Bill Read Freescale 1 Fais Yaniv Freescale Mark Kole NXP Jasmine NSC 1 David Tamura NSC Kevin Cameron True Circuits 1 1 David Jonathan Qualcomm 1 Laisne Michael Qualcomm 1 Li Xiang Qualcomm 1 Attendance 19 18 21 20 Himyanshu Anand EDA Strategy, Vendor Relation and Customer Collaboration, Design Technology Organization, Freescale Semiconductor 7700 W. Parmer Lane, Loc/MD: TX32/PL34, Austin, TX - 78729 email: Himyanshu.Anand@freescale.com Ph : +1-512-996-5623 Fax : +1-512-996-7432 -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Tue Oct 7 15:30:57 2008
This archive was generated by hypermail 2.1.8 : Tue Oct 07 2008 - 15:31:07 PDT