Attendees:

000000000000000100001011110000000 Qamar Alam
111111111111111111101011111110111 Himyanshu Anand
011111111001111110111010001111111 Kenneth Bakalar
111110101011011011101100001110001 Prabal Bhattacharya
000000000000001100001010010000100 Sri Chandra
011110111111111111011010111110111 Eduard Cerny
111011100001011010111011111011111 Scott Cranston
000000000000000100000000000000010 Dave Cronauer
000000000000110000000001111110011 Dejan Nickovic
110111011110010000000000000000000 Mike Demler
000000000000000000000000000000000 Surrendra Dudani
111000000011111111111100110111111 John Havlicek
111000110010000000000000000000000 Kevin Jones (RGG Leader)
000000011111111110111011111111111 Jim Lear
000000000000111011100000000000000 Top Lertpanyavit
111111011011111111111111101111111 Scott Little
000000000000010000000000000000000 Erik Seligman
101000000000000000000000000000000 David Sharrit
000000010000000000000000000000000 Murtaza
000000010000000000010110011000000 Martin O'Leary

Decisions:

Action Items:

Details:

HA: Next steps beyond the vote to get a move on. I suggest we divide into groups and pick requirements and work on them. How does everyone view this?

KB: They don't correspond to potential features in the future language.

JL: Hesistant to offer services as the syntax requirements is not an expert in the language.

ED: Help in JH and Scott with the real time version of the SVA.

KB: Start off different from requirements. See that validation is against requirements. Extending SVA in a consistent way to the dense time and provide semantics for that. The issue of bind is in the category of the next step. Another issue might be increasing the fidelity of the interface, do we need to types to either language? Checker instantiation in VAMS. Problem is non-port like connections to make checkers work with VAMS.

SL: Two major divisions - 1) What sort of things can we get into checker container? 2) Start looking at the extensions to SVA. There are many facets on those two categories.

SL: What goes into a checker/assertion container? What type of data can go into those. Like, what is in a bind? and where can it be used?

KB: A bind instantiation is no different from a module instantiation. A checker does not a have real number ports. That will have to change.

SC: Reals are allowed in checkers in 2009 LRM.

ED: You have to decide you have to sample your values or not? All integral types are sampled.

KB: I think we need to look at the nature of dense time assertions first. Do you mean clocked when you say sampled?

ED: Preponed region.

KB: I am not sure. We have to define assertions in dense time in asynchronous way. We have to define assertions on real variables in SV, without any reference to analog world.

HA: So, does everyone agree that we need to work on extensions and in parallel work on the interface issues?

PB: Yes, that is fair

SC: No problem with that

JH: I agree with that. I am a firm believer in understanding what you are trying to write before writing it. Are we going to write a document which will describe the changes to other documents? Or are we going to write a self-contained document? Once we understand that, we should start writing it.

KB: I would be tempted to start with the definition of SVA. You are right, the people will have to decide and experiment with various ideas.

JH: It would be useful to look at the previous examples of enhancing an existing language without completely rewriting it. Reference the sections, and we could say, this new section replaces it or say here is the new addition.

KB: John, you have a pretty good idea of how to proceed to dense time of SVA. Also, Dejan said he felt pretty good about the document. That gives me the confidence.

JH: We have gone through many revisions before sending it out to everyone. So, we have confidence on that. What we do not have much confidence is the complexity of implementability. We have gotten some feedback on some of that and that it could be done with some restrictions.

KB: You are concerned about the time it would take to find a solution.

JL: I am not completely sure if current SVA will not be able to handle all analog assertions without modifying it.

KB: That was discussed before, the problem is SVA is clocked.

ED: Other things are @cross, use of local variables, or forbidding events from happenning between two events. You cannot detect the change will not happen.

SL: I do a lot of things like what Jim is talking about. It is very cumbersome that way to have it in the boolean state.

JH: The problem of this approach introduces certain assumptions, that you have a fast enough clock to not miss any of the interesting things.

JL: Clock assertions on analog commit points.

KB: And eliminate the need for dense time.

JL: Not completly.

ED: Maybe good to look at the full real time extension and see if that is sufficient, like John's document, for the first step.

SL: I disagree.

HA: I agree with Scott that it will be inaccurate.

ED: You will be very much limited in what you can express. Multi clock sequences operate only on linear sequences.

KB: The idea of commit clocks is an issue of efficieny. These analog monitors take enormous amount of time. I think the use of commit clock is a proper subset of dense time assertions. The first step is to allow real expressions in the assertions. And then later on top of that we talk about the dense time assertions.

SL: You have to be able to talk about time as first class citizen.

KB: Yes, I agree otherwise there is lot of handwork.

JH: If you deal with commit clock, you have to figure out time too. What ED suggested is that you use local variables to get the passage of time.

JL: Use the vector of times if you wanted access to time values.

JH: I can imagine I can do all my verification in C++. But what kind of analysis can be done with that?

JH: Just give me access to the data, I will form the data structures and do the checks I need. But, it does not open to general purpose programming language that is open to more formal analysis. My vision is to have a formal language that can do other things.

JL: How these checks are going to be translated to checks on lab equipment?

KB: The formal language simplifies the verification effort and the mapping on the simulator time is only a small effort.

JH: Another advantage is that if you have a formal language framework and you can tell much more quickly whether you are designing in the language is marked.

JH: The document that we sent out is - 1) How do we take the existing SVA constructs and extend them in a consistent way for real time extensions? We certainly don't want to break what exists already. We have also added some operators that give us real time temporal operators and that align with the kind of things we have seen in practise. There are about 5 real time operators. There are no more operators. We have not proved everything, but we have laid the groundwork.

-- AnandHimyanshu - 2009-11-03