Attendees:

0000000000000001000010111100000000000 Qamar Alam
1111111111111111111010111111101111110 Himyanshu Anand
0111111110011111101110100011111111111 Kenneth Bakalar
1111101010110110111011000011100011101 Prabal Bhattacharya
0000000000000011000010100100001001000 Sri Chandra
0111101111111111110110101111101111100 Eduard Cerny
1110111000010110101110111110111111101 Scott Cranston
0000000000000001000000000000000100000 Dave Cronauer
0000000000001100000000011111100111101 Dejan Nickovic
1101110111100100000000000000000000000 Mike Demler
0000000000000000000000000000000000000 Surrendra Dudani
1110000000111111111111001101111111111 John Havlicek
1110001100100000000000000000000000000 Kevin Jones (RGG Leader)
0000000111111111101110111111111111111 Jim Lear
0000000000001110111000000000000000000 Top Lertpanyavit
1111110110111111111111111011111111111 Scott Little
0000000000000100000000000000000000000 Erik Seligman
1010000000000000000000000000000000000 David Sharrit
0000000100000000000000000000000000000 Murtaza
0000000100000000000101100110000001001 Martin O'Leary

Decisions:

Action Items:

Details:

KB: Dejan, have you read the paper?

DN: I haven't read the most recent version, but the previous version looked quite good to me. What is new in this version?

SL: I believe that we have made the real delay operator a derived operator since you last saw it. We have also proved the main conjecture, but it is not yet typeset.

KB: How do preponed values play into these definitions?

JH: We have thought a bit about this a few months ago, but we haven't explored it thoroughly.

KB: Maybe we need to change the definition of Verilog-AMS and the values we get to ensure that they are preponed values.

JH: We have had internal discussions that led us to believe that the last committed value may be the right thing, but we need to understand the issues more deeply.

JH: Let's start with realtime boolean again. A boolean must be true at a point. The next form is sequence without an event. Ed has mentioned the need for this and the IIT KGP researchers have mentioned it. We haven't seen how to derive it in other forms.

DN: Why can't you express this in terms of booleans?

JH: Booleans and events aren't the same in the languages even though in the formal semantics they are the same.

DN: In my thesis I concluded that events are just booleans that are true at a singular point.

JH: There is a difference at the language level.

DN: I agree, but I still think it would be useful to show that events are equivalent to booleans.

JH: The next form is the boolean smear. Think of this like spreading paint across a wall. The boolean should be true at every point in the interval. The values represent the length of the interval. We used the star because we originally thought of this as repetition but didn't call it repetition because we feel that repetition denotes iteration. This operator isn't really about iteration.

DN: Maybe you should state that beta should be strictly greater than alpha. If they are equal then the problem becomes undecidable. This isn't a problem for monitoring but for cleanliness of the theory this may be useful.

KB: What about open and closed intervals? Is this practical? How do you distinguish this in a simulator?

DN: They are necessary to express some properties. In the implementation some of these details will be abstracted, but they are necessary in the semantics.

JH: We haven't thought about all of the possibilities. Most of the operators match over intervals that are right closed. It is only the smear and operators derived from the smear that result in right open intervals. We thought that local variables might only be assigned on right closed intervals. DN mentioned that these restrictions may be necessary.

DN: Yes, the restrictions would be necessary to avoid degenerate cases.

JH: We started to see that the operators tend to favor right closed intervals with the exception of the smear. We do not generally talk about whether the intervals are closed or open.

DN: I can bring an example for next time. For the monitoring the undecidability isn't that important. It is important to answer the question, Is my property satisfiable? I will try to write a small paragraph on this for next time.

JH: Realtime fusion is a method to concatenate two intervals that abut each other. The real delay operator is derived from the smear. It matches over an interval that is between alpha and beta long. The alpha and the beta are conditions on the length of the gap. The length of the interval doesn't have anything to do with whether the interval is open or closed. I will say that in another way. Let's consider the open interval (0,1). That interval has length one. If my condition is that the gluing interval must have length one then that interval is admissable. I can add the endpoints one by one and the interval is still of length one. If my criteria is that my interval must be strictly greater than one then this interval does not satisfy that criteria.

KB: What are the defaults?

JH: The default is that they (+/-) aren't there.

KB: So you are using them to differentiate between greater than and greater than or equal to?

JH: Yes.

KB: For numerical accuracy this isn't good practice. There is really no difference between greater than and great than or equal to.

SL: This difference may not matter in practice.

JL: Okay, I see. I think that last time JH made the point that this is just a theoretical framework and there may be issues associated with putting it into practice.

JH: The main motivation for the + and the - is say that we match at an event and then the next interval can't match at that point exactly. We need some way to "push off" from the time of the event and start the next matching interval.

KB: There is a similar notion in crossing for VHDL-AMS. It means that we are measurably greater than a value. That type of idea could be applied here.

JH: The last operator is the realtime goto. It matches over an interval that ends at a time when b is true and such that no prior time in the interval b is true.

-- ScottLittle - 2009-11-04