2010-02-17
Attendees:

000000000000000100001011110000000000000000 Qamar Alam
111111111111111111101011111110111111011111 Himyanshu Anand
011111111001111110111010001111111111111011 Kenneth Bakalar
111110101011011011101100001110001110101000 Prabal Bhattacharya
000000000000001100001010010000100100000010 Sri Chandra
011110111111111111011010111110111110001111 Eduard Cerny
111011100001011010111011111011111110101000 Scott Cranston
000000000000000100000000000000010000001000 Dave Cronauer
000000000000110000000001111110011110111001 Dejan Nickovic
110111011110010000000000000000000000000000 Mike Demler
000000000000000000000000000000000000000000 Surrendra Dudani
111000000011111111111100110111111111111111 John Havlicek
111000110010000000000000000000000000000000 Kevin Jones
000000011111111110111011111111111111111111 Jim Lear
000000000000111011100000000000000000001110 Top Lertpanyavit
111111011011111111111111101111111111111111 Scott Little
000000000000010000000000000000000000000000 Erik Seligman
101000000000000000000000000000000000000000 David Sharrit
000000010000000000000000000000000000000000 Murtaza
000000010000000000010110011000000100100000 Martin O'Leary

SUMMARY:

-P1800 presentation was discussed and finalized.  Ken has already sent the final version to the asva mailing list.
-Discussion of synchronizaton needs for ASVA.  Dejan has begun investigating algorithms that dynamically determine sample points required to guarantee property correctness in the face of a finitely sampled signal.
-No meeting next week.

ACTION ITEMS:

-Scott will send instructions for the P1800 call to the list.

DETAILS:

KB: Let's get these slides out of the way.

JL: Slides are short and sweet if it conveys everything it needs that is good.  I made a comment regarding just limiting to voltages and currents, but that is just decoration.  Do we have enough here to entice the P1800 committee to action?

KB: I really feel a bit uncomfortable going in front of these guys.  If you look at the dialogue there are a lot of big arguments going on.  I don't want to claim that we are too important here.  I just want to say what we are doing and get their reaction.

SL:  I agree.  We just sort of want to fit in and make them aware of the work.

KB: I want to make sure that I understand where we are headed.  We are proposing to extend the language for properties.

SL: When you say properties do you mean SVA?

KB:  Well, I mean properties.  This isn't necessarily all of SVA.  If we are going to embed ASVA within SVA then we would need to bring all of this stuff over into Verilog-AMS.  All of the stuff we talked about with cross instantiation we always talk about instantiating SV within VAMS.  We aren't talking about instantiating VAMS in SV.  The difference being that the latter deals with boundary connections.  We can instantiate SV in VAMS and the connect logic of VAMS will serve to make the mixed connections.  If we instantiate VAMS in SV then the connect problem becomes visible in SV.

SL: That is fine.  My concern is a specific use case.  Let me describe it and see if it fits into your ideas.  I have a SV testbench that contains SV testbench constructs, SV design code, and VAMS models.  The VAMS models are instantiated within SV blocks.  The ASVA module binds to a mixture of SV and VAMS signals.  Does this sort of design fit within the framework you are describing?

KB: You don't really have SV on top.  You have VAMS on top.

SL: Okay, well that isn't a big deal I guess.  I could feasible wrap my top-level SV in VAMS.

JH: Can I try to streamline some of this.  I want to talk about one of my peeves.  I understand not wanting to raise red flags.  I don't want to emphasize "eventually SV."  Can this just be removed.  For this discussion the real question is this PAR going to include AMS features.  If we want to work on this in SV then it needs to be in the PAR.

SL: I think AMS needs to make it into the PAR.

EC: I think we should drop eventually AMS.

KB: Ok.

JH: Metric time?  What does it mean?

KB: It means that you can measure time.  You have a notion that you can measure time.  I would say that.

DN: Personally, I don't have anything against the word metric.  We simply need to distinguish from logical time.  In digital you are counting samples or clock edges.

KB: The reason I want to get away from talking about analog time is that the ASVA language is a digital event driven language.  We can now talk about intervals of time and relations that include real numbers (boolean expressions that include real numbers).  I want to emphasize the fact that there isn't any analog magic going on.  We want to map the problem onto the event driven simulator.  I want to provoke that thought by using the word metric time.

JH: What about continuous time?

KB: We could call it continuous time.  I am not really concerned about continuity.

DN: Continous on one hand is clearer, but when we are moving from the purely theoretical framework when we assume that we have our waveforms defined all over the real axis to the reality where you are provided a finite number of sample maybe the continuous is a bit misleading?

JH: In what way is metric time less misleading?

KB: You can measure the interval between samples?

JH: There are many metrics that you can induce that have the same topology.

KB: We can use the words continuous time.  The point is to show that it is really a digital problem.

DN: Maybe you can use continuous time and then expound about looking at intervals during the presentation.

SL: What about the SV-AC on the last slide?

KB: I am going to embed ASVA in VAMS and SV without eventually.  Change from SV-AC to P1800 and change metric to continuous.

HA: Can we discuss the examples.  In the last example it says stays there.

KB: We could change it back and remove stays there.

HA: What is the motivation for the example?

KB: It is that there is some mysterious synchronization there.  We have to solve the interval colliding with the clocks.

HA: If we want to convey that the crossing isn't being checked at the clock boundary then shouldn't we be more specific and emphasize that it isn't being sampled at the clock boundary?

DN: Maybe a good question to JH, SL, and HA is in the mixed language what would be the semantics of this property?  If the crossing happens between two digital clocks what would be the meaning of the assertion.

JH: I can't assign a meaning b/c I don't know what stays there means.

DN: Assume that stays there is removed.

JH: I would say that s1 rising is in respect to some other clocking event then it could be concurrent with the crossing.

KB: The s1 that is in the assertion or the real s1?

HA: I was thinking about saying stays there for x ns.

KB: I didn't want to check assertions on a glitch.

HA: Yeah, that is why I think emphasizing a time would be good.

JL: Can we attend this meeting?

SL: Yes, I believe so.  I should send out the web page with the meeting information.  I presume that the agenda will be up on that page prior to the meeting.

KB:  All IEEE meetings are open to the public so you can attend.

SL: In the meeting a few weeks ago we divided the requirements into 3 primary areas.  In light of Ken's more careful analysis of the requirements for his slides, Ken do you think these three categories still make sense?

KB: I am not sure about the synchronization category.

DN: There is some relation to assertion language.

KB: That is the more abstract view.  How and to what degree is the analog solver controleld by assertions.

DN: I have recently started looking at the problem.  Basically the problem is that you have some language defined in terms of perfect signals.  We just have boolean continuous time signals.  In all of these logics we assume that you know the values of your signal at any point in time, but the analog solver sends you discrete points but you can control it.  What I am trying to do now is show that given an arbitrary assertion and a perfect signal what is a sufficient number and position of samples that I need to preserve the correctness.  I want to do this online.  Given a prefix of a trace and the structure of the formula what are the next samples that I need.  This becomes verification with partial steering.  I assume that I will have the two steering functions.  I don't observe the model...only its output and then only sampled versions.  Steering means that I want the value of variable x in y ns.  This corresponds to turning on and off @cross and @timer constructs in VAMS.

KB: It would be reassuring to have this.

DN: I will do it in a more abstract framework.  This will give us some foundation.

JL: I am a bit lost.  Are you saying that you will be able to imply what the synchronization requirements are from the assertion?

DN: My ultimate goal is to have  a dynamic algorithm that given a prefix of the trace and the formula that I will know what samples I need next to continue evaluating the formula.  From a perfect trace I only need a finite number of samples to evaluate the property.  I want an algorithm to identify these points.

JL: I am having trouble seeing how that would be implemented.  I would love to see this on paper.

DN: Sure.  I started thinking about this recently so it is at the level of an idea.  I would like to push it because I think it would be very interesting for this committee.

KB: That is automated way.  I really like that.  If you can formulate this it should cover Jim's requirements.

JL: Maybe.  What about tolerances?

DN: I don't want to cover tolerances.  I think that is an orthogonal issue.

SL: I am not sure this covers Jim's requirements.  I thought Jim wanted to adjust sampling and collect data.  I didn't think that he wanted that tied to a property.

JL: I had envisioned that at predicates it would evaluate and then at some previous points then maybe you could imply what the synchronization needs to be in the future.  For example, when a signal crosses an upper threshold look at the preceding 10 ns of time to ensure that the slew rate never exceeded some limit.  Wouldn't that maybe be able to derive this information.

DN: That is exactly what I want to do.

KB: Looking back in time is complicated.

JL: I think if you specify it properly it can be done.

DN: Probably, but it would have to be very conservative.

EC: This sort of sampling is already done with $past.  It would be much more costly in the analog engine.

JL: Much of the work I have done with propagation delays the standard sampling has been adequate.

KB: Are we meeting next week.

SL: I will not be able to make the meeting.

KB: I will be at DVCON.

JH: Let's cancel the meeting for next week.

-- ScottLittle - 2010-02-17