Here are the minutes that I took during the meeting: Please feel free to add if I missed some important point that was made in the meeting. Also, I have attached the attendance sheet, if somebody was there but I do not have his/her name on the sheet please let me know. Action Items: 1) Mike Demler (Synopsys) will present some examples of the connectivity checks that were discussed today in the next meeting. 2) Open Item: I would urge other participants to present examples of checks that they are doing currently as well as examples of checks that they would like to be discussed before the committee, so that we have a comprehensive list of examples, before we start narrowing down the focus of the assertions. HA (Himyanshu Anand): Presented the initial problem definition of AMS assertions and its scope. The assertions should target the mixed signal domain (analog-digital boundary). Also assertions should work across the domains so that they can be re-used with different models. The assertions will work in the real (time or frequency) domain. KB (Ken Bakalar): Are we talking about just system level assertions and not block level? KJ (Kevin Jones): If its block level, assertions can still be used with the same semantics. HA: The semantics of assertions does not restrict the application of assertions to just system level. They can be used at block level too. KB: Only block level problem is successfully solved [Tracing] KJ: In a small scale, local. The assertions are not very well done in reality. MD (Mike Demler): Lets go through the examples. HA: The types of assertions can be broadly classified into 1) Safety Checks, 2) Mixed Signal Protocol Checks and 3) Timing Checks. Presented examples of the same. These can be used to verify waveform correctness and validate timing relationships between the signals. SL (Scott Little): Presented more examples. The examples are similar to measurements which analog designers would like to do for the verification of their blocks. Examples include properties from the eye diagram - eye jitter, inner height, outer height, gain-bandwidth product, etc. VS (Venkataramanan Srinivasan): Are the functions for tolerance, gain bandwidth, etc built in? JH (John Havlicek): The examples cover various things designers are interested in verifying. Some are traditional temporal properties and some are relationships (like measurements). When can you reference the measurements inside the properties? Maybe it makes sense to include some of the measurements inside the properties as built-in. MD: It is important to categorize and see what types of properties are missing from the list. HA: What other properties would you like to see being discussed? MD: The properties that were presented today were mostly waveform calculator functions. They mostly exist in one form or another in various tools. Some are like eye diagrams and some like .measure. The language should perform uniform verification from block to system level. Example: Putting a circuit into a power down state and checking for leakage of power through floating gates. HA: Lets discuss the property categories from Mike's blog Connectivity Properties: These are most in power managed designs. People are putting circuits which can't be simulated. Static Electrical Properties: Functional Properties: Most difficult to define in the analog domain. ??: Power down when boundary needs. KJ: Digital assertions, it should also work. MD: You need something. Is it something we can capture from the waveform. KJ: No good way to describe the power supplies via properties. HA: How can you describe connectivity properties using assertions? MD: Properties on devices - wires, etc. Signals are not circuits. There can be cases when the waveform is fine but the circuit does not work. In such a case the verification is broken. SL: Are these properties on devices? ??: How can one have a unified language. The verification tools are different and serve different purposes. MD: There is a point. Either one can focus on higher level properties or point down and go to device level properties. Something like assertions over functions and assertions over structures. KB: Its a matter of model and simulator and these are modeling issues and not concerned with verification. It's a purely static property (power down and connectivity issues of low-voltage to a high-voltage device) MD: How do you check that a low-voltage device is not connected to a high-voltage device? KB: By using electrical disciplines. KJ: You can check whether your switch is bad from the simulation. ??: Whether you impose the condition using disciplines or using assertions. Discussion started with time domain and frequency domain properties. JH: Whether temporal logic is used for assertions or whether simple measurements are done, we should look at all examples. There is nothing wrong with static type property checks. KJ: You can get this with the initial block checks, its already there. MD: Are you suggesting a static collection of an analog model? Or is it something different? How is this information asked. Analog side design is manual. ??: Static assertions are problematic in one way. Different models of time. HA: But you can view static as being a long time (maybe infinite time), where the condition needs to hold throughout. MD: The tools that these types of checks are a command set. Its a long time but not infinite time. If the circuit sits long enough it displays certain bad behavior due to leakage currents. JH: Have a description of what's proper and improper behavior. What is the correctness behavior that the design needs to display? HM (Hillel Miller): We should differentiate the two. One is asking for checking the dynamic behavior the other is asking for static checks which should be done elsewhere. HA: Static checks are like linting checks too. Jasmine: These checks are already there in the tools. Spectre has checks for MOS transistors, min-max so why do we want assertions? HA: Yes, some checks can already be accomplished from what is there in Verilog-AMS, however, there is a class of checks that cannot be done which are temporal in nature. Assertions will be helpful in sort of standardizing those and at the same time including simple checks. MD: Don't constrain ourselves to what can be simulated. The tool that we have is more like static checker or vector-less. End Comments: ----------------------- Intel (Erik Seligman): No comments. Synopsys (MD and VS): Apart from Mike comments above, has the work done for PSL extension at Prosyd and the work done at IIT-KGP been looked at? HA: Yes, we are in touch with both the parties and they are interested in working with us. Cadence (Prabal): No comments Mentor Graphics (KB): We should narrow the scope, might be its my prejudice. We should focus on temporal dense time (real, continuous) assertions that includes, timing, mixed-signal and safety properties and should exclude information about event driven system solvers. Kevin Jones: Participating as individual contributor. We should be clear about the scope. Freescale can lead and provide a document of what needs to be done and we can critique that instead of being asked to be creative on phone. True Circuits (Kevin): It should be more methodology driven and what designers want to verify in real world. Freescale: JH: Would like to see more examples on kinds of properties that need to be verified. Then start collecting requirements. What are the types of categories of these properties can be decided later after going through the examples. Brian Mulvaney: Primitive properties should not be looked at. Those are something that belong to device engineers in the foundries or labs. We should focus on higher level properties. Benjamin Ehlers: Does not see device level checks being done at the verification level. Linda Lin: The examples and discussion was too analog related. Would like to see some digital discussion also. Thanks, Himyanshu Anand 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.
This archive was generated by hypermail 2.1.8 : Wed Sep 24 2008 - 12:28:08 PDT