MeetingMinutes20091028 < VerilogAMS

VerilogAMS Web>AmsAssertions>RequirementsGatheringGroup>MeetingMinutes20091028 (2009-11-03, AnandHimyanshu) (raw view)EditAttach
Attendees:<br /><br />000000000000000100001011110000000000 Qamar Alam<br />111111111111111111101011111110111111 Himyanshu Anand<br />011111111001111110111010001111111111 Kenneth Bakalar<br />111110101011011011101100001110001110 Prabal Bhattacharya<br />000000000000001100001010010000100100 Sri Chandra<br />011110111111111111011010111110111110 Eduard Cerny<br />111011100001011010111011111011111110 Scott Cranston<br />000000000000000100000000000000010000 Dave Cronauer<br />000000000000110000000001111110011110 Dejan Nickovic<br />110111011110010000000000000000000000 Mike Demler<br />000000000000000000000000000000000000 Surrendra Dudani<br />111000000011111111111100110111111111 John Havlicek<br />111000110010000000000000000000000000 Kevin Jones (RGG Leader)<br />000000011111111110111011111111111111 Jim Lear<br />000000000000111011100000000000000000 Top Lertpanyavit<br />111111011011111111111111101111111111 Scott Little<br />000000000000010000000000000000000000 Erik Seligman<br />101000000000000000000000000000000000 David Sharrit<br />000000010000000000000000000000000000 Murtaza<br />000000010000000000010110011000000100 Martin O'Leary
---

Decisions:
---
Action Items:
---
Details:

JL: Does it (Digital Monitoring Blocks) need to be defined in VAMS?<br /><br />KB: Yes, it is better if we investigate it in VAMS.<br /><br />SL: Accuracy is of utmost importance. Not sure if all the capabilities are<br />in VAMS today. The infrastructure is there but some key pieces are missing.<br /><br />HA: We need to start discussing the real time semantics.<br /><br />JH: Draft version of the introduction to real time semantics. One other<br />change in the abstract, we did make progress in working on proving the main<br />conjecture. In the body of the document it is still set as conjecture<br />instead of a proposition. We are taking the same kind of experience for<br />digital assertions to analog/mixed signal assertions.<br /><br />JH: SVA requires sequential constructs to be governed by digital clocking<br />events. PSL does not require the same requirement, but the semantics require<br />the same discrete clocks. There has been work from Dejan and other folks in<br />extending LTL to real time domain or a dense domain. <br /><br />JH: LTL operators, until, weak until, always, eventually they have been<br />added to 2009 standard. The vision was clear, but what was not clear is what<br />is to be done to sequence and regular expressions in real time. We do not<br />want to have a disjoint set of regular expressions. We can have properties<br />where sequences are digital and at some point they become real time<br />sequences. Once we introduce the sampling we get discrete semantics.<br /><br />KB: Seems ambitious and just the right path to proceed. Do you think we<br />succeeded?<br /><br />JH: We have so far. We have excluded some things like local variables and<br />first_match. <br /><br />JH: We introduce a realtime boolean. For real time we want to be able to<br />specify a boolean in real time. And where that point be is dependent upon<br />the context. <br /><br />JL: It is time,value pair.<br /><br />JH: Yes, the state is the set of all such time,value pair. So, at any<br />particular time, we can ask what value a particular variable. For the<br />semantics we are assuming the ideal information.<br /><br />KB: In a programming language, SV, variables always have a value at times,<br />but between those times, the values are transient. The reason you are<br />observing on clock edges is that the values are only valid on those edges. <br /><br />JH: Yes, this is the difference between event and variable. For something<br />like posedge in digital it happens at the same time. In analog, its close,<br />don't know how it is done. In future, we might have transients and we treat<br />them as discrete sequences. We could have a single value with compound<br />entity. But the framework would allow that. That's what happens in a<br />glitch. <br /><br />KB: This is very nice, I see what you are going at.<br /><br />JH: Trace is on real line.<br /><br />KB: That is an issue, the variable needs to have a value at every time. Some<br />booleans will have a value at every time others have garbage values.<br /><br />JH: What do you mean by garbage values?<br /><br />KB: The curtains are closed during clock edges.<br /><br />JH: You can define a value as undefined and say that the boolean has<br />undefined values at those times. Or you can say they have X or Z values for<br />that. <br /><br />KB: X is close, Z has an electrical meaning. <br /><br />JH: For the purpose of analog assertions don't know what needs to be done<br />for them. For mathematical purpose we can model it as some undefined value.<br /><br />JH: The key idea is matching the sequences over bounded interval. Given a<br />trace and a bounded interval, we can ask the question does the trace match<br />sequence over a bounded interval.<br /><br />JH: A sequence without an event. This has come over in various places. We<br />have seen this come up in Ed's presentation and in the research being done<br />at IIT, Kharagpur.<br /><br />KB: How is the negation of an event is not the same as exclusion of event?<br /><br />JH: Negation of event will include that pattern. So, negation of event will<br />include a lot more than just the exclusion of the event. The motivation is<br />to express event ordering. <br /><br />JH: Boolean smear. <br /><br />JL: Is this in SVA and PSL already?<br /><br />JH: This construct is not in SVA.<br /><br />JH: I think you can approximate the without operator Jim, but I don't think you get the exact meaning. We can discuss some examples offline.<br /><br />JH: The smear is taking your paintbrush and creating a horizontal smear across the wall. The items within the brackets describe the length of the interval. The +/- affect whether the inequalities are strict or non-strict. The majority of the operators are flexible with respect to open and closed intervals. The realtime boolean is one exception.<br /><br />JL: What is the asterisk doing?<br /><br />JH: Originally we thought of this as continuous repetition, but we decided not to call it that because repetition implies discrete repetition.<br /><br />JL: How does this differ from a boolean interval?<br /><br />JH: Only that the alpha and beta are reals. Please try not to get hung up on the accidents of the syntax. The meaning is that the boolean has to be true at every point in the interval and meet the length requirement. We also spend some time in the details talking about how some of the digital forms can be derived in terms of the realtime operators.<br /><br />JL: I found the lower parts of the paper Greek, so I will stick to this.<br /><br />JH: We should have summaries of those results in this introduction.<br /><br />KB: Is this the complete set of operators?<br /><br />JH: Yes, we believe that these 6 are it, but it should be mentioned that 5 and 6 are derived from the previous 4.<br /><br />JL: I am a bit worried that without isn't in the current digital. I would like to explore that a bit more.<br /><br />JH: We can make that case more carefully. In fact, maybe we do need it in digital.<br /><br />KB: The problem in the back of my mind is that in a simulation language you will only be looking at the value of a variable at particular times. There is no such thing as continuity. I am going to be looking at that mapping from the real line into the sampled time of a simulator. The simulator is only going to be able to make a test of the value at separated times. When you do an analog simulation you set down a granularity of points.<br /><br />JH: I agree. I have said from the beginning that we should set down a clean semantics and then determine what it means in the face of a finite approximation. I have that in the back of my mind, but I am waiting to do that until we have a clean ideal semantics.<br /><br />KB: Dejan solved that by just interpolating when a timepoint isn't present.<br /><br />JL: What do you do in the case where there is no explicit observation at the endpoints and the value changes between the two closest endpoints.<br /><br />JH: Yes, that is an interesting point. I think that there is uncertainty in both the values and the time.<br /><br />JL: It would seem like the tool may have to observe at the endpoints. This may be a performance nightmare.<br /><br />JH: My advice to everyone is to not let those nightmares complicate pulling together a coherent simple definition. If we can't get this sort of definition work out the ideal semantics then we don't have any business worrying about the other stuff.<br /><br />KB: What sorts of things are alpha and beta? Times?<br /><br />JH: Yes, think about them as bounds on the time. I am assuming that there are literals that can be used to represent them.<br /><br />JL: Whether it is an integer or real the properties should work the same way.<br /><br />KB: Not really because in the digital semantics they represent cycles.<br /><br />JH: Ken has a point. That sort of thing won't work unless you know something about the underlying frequency of the clock. Discrete repetitions are measured from one occurrence of the clocking event to another.<br /><br />JL: I see.<br /> 

-- Main.AnandHimyanshu - 2009-11-03
Topic revision: r1 - 2009-11-03 - 22:06:52 - AnandHimyanshu
VerilogAMS