Attendees:

000000000000000100001011110000000000 Qamar Alam
111111111111111111101011111110111111 Himyanshu Anand
011111111001111110111010001111111111 Kenneth Bakalar
111110101011011011101100001110001110 Prabal Bhattacharya
000000000000001100001010010000100100 Sri Chandra
011110111111111111011010111110111110 Eduard Cerny
111011100001011010111011111011111110 Scott Cranston
000000000000000100000000000000010000 Dave Cronauer
000000000000110000000001111110011110 Dejan Nickovic
110111011110010000000000000000000000 Mike Demler
000000000000000000000000000000000000 Surrendra Dudani
111000000011111111111100110111111111 John Havlicek
111000110010000000000000000000000000 Kevin Jones (RGG Leader)
000000011111111110111011111111111111 Jim Lear
000000000000111011100000000000000000 Top Lertpanyavit
111111011011111111111111101111111111 Scott Little
000000000000010000000000000000000000 Erik Seligman
101000000000000000000000000000000000 David Sharrit
000000010000000000000000000000000000 Murtaza
000000010000000000010110011000000100 Martin O'Leary

---

Decisions:

---

Action Items:

---

Details:

JL: Does it (Digital Monitoring Blocks) need to be defined in VAMS?

KB: Yes, it is better if we investigate it in VAMS.

SL: Accuracy is of utmost importance. Not sure if all the capabilities are
in VAMS today. The infrastructure is there but some key pieces are missing.

HA: We need to start discussing the real time semantics.

JH: Draft version of the introduction to real time semantics. One other
change in the abstract, we did make progress in working on proving the main
conjecture. In the body of the document it is still set as conjecture
instead of a proposition. We are taking the same kind of experience for
digital assertions to analog/mixed signal assertions.

JH: SVA requires sequential constructs to be governed by digital clocking
events. PSL does not require the same requirement, but the semantics require
the same discrete clocks. There has been work from Dejan and other folks in
extending LTL to real time domain or a dense domain.

JH: LTL operators, until, weak until, always, eventually they have been
added to 2009 standard. The vision was clear, but what was not clear is what
is to be done to sequence and regular expressions in real time. We do not
want to have a disjoint set of regular expressions. We can have properties
where sequences are digital and at some point they become real time
sequences. Once we introduce the sampling we get discrete semantics.

KB: Seems ambitious and just the right path to proceed. Do you think we
succeeded?

JH: We have so far. We have excluded some things like local variables and
first_match.

JH: We introduce a realtime boolean. For real time we want to be able to
specify a boolean in real time. And where that point be is dependent upon
the context.

JL: It is time,value pair.

JH: Yes, the state is the set of all such time,value pair. So, at any
particular time, we can ask what value a particular variable. For the
semantics we are assuming the ideal information.

KB: In a programming language, SV, variables always have a value at times,
but between those times, the values are transient. The reason you are
observing on clock edges is that the values are only valid on those edges.

JH: Yes, this is the difference between event and variable. For something
like posedge in digital it happens at the same time. In analog, its close,
don't know how it is done. In future, we might have transients and we treat
them as discrete sequences. We could have a single value with compound
entity. But the framework would allow that. That's what happens in a
glitch.

KB: This is very nice, I see what you are going at.

JH: Trace is on real line.

KB: That is an issue, the variable needs to have a value at every time. Some
booleans will have a value at every time others have garbage values.

JH: What do you mean by garbage values?

KB: The curtains are closed during clock edges.

JH: You can define a value as undefined and say that the boolean has
undefined values at those times. Or you can say they have X or Z values for
that.

KB: X is close, Z has an electrical meaning.

JH: For the purpose of analog assertions don't know what needs to be done
for them. For mathematical purpose we can model it as some undefined value.

JH: The key idea is matching the sequences over bounded interval. Given a
trace and a bounded interval, we can ask the question does the trace match
sequence over a bounded interval.

JH: A sequence without an event. This has come over in various places. We
have seen this come up in Ed's presentation and in the research being done
at IIT, Kharagpur.

KB: How is the negation of an event is not the same as exclusion of event?

JH: Negation of event will include that pattern. So, negation of event will
include a lot more than just the exclusion of the event. The motivation is
to express event ordering.

JH: Boolean smear.

JL: Is this in SVA and PSL already?

JH: This construct is not in SVA.

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.

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.

JL: What is the asterisk doing?

JH: Originally we thought of this as continuous repetition, but we decided not to call it that because repetition implies discrete repetition.

JL: How does this differ from a boolean interval?

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.

JL: I found the lower parts of the paper Greek, so I will stick to this.

JH: We should have summaries of those results in this introduction.

KB: Is this the complete set of operators?

JH: Yes, we believe that these 6 are it, but it should be mentioned that 5 and 6 are derived from the previous 4.

JL: I am a bit worried that without isn't in the current digital. I would like to explore that a bit more.

JH: We can make that case more carefully. In fact, maybe we do need it in digital.

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.

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.

KB: Dejan solved that by just interpolating when a timepoint isn't present.

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.

JH: Yes, that is an interesting point. I think that there is uncertainty in both the values and the time.

JL: It would seem like the tool may have to observe at the endpoints. This may be a performance nightmare.

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.

KB: What sorts of things are alpha and beta? Times?

JH: Yes, think about them as bounds on the time. I am assuming that there are literals that can be used to represent them.

JL: Whether it is an integer or real the properties should work the same way.

KB: Not really because in the digital semantics they represent cycles.

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.

JL: I see.

-- AnandHimyanshu - 2009-11-03