00000000000000010000101111000000000000 Qamar Alam
11111111111111111110101111111011111101 Himyanshu Anand
01111111100111111011101000111111111111 Kenneth Bakalar
11111010101101101110110000111000111010 Prabal Bhattacharya
00000000000000110000101001000010010000 Sri Chandra
01111011111111111101101011111011111000 Eduard Cerny
11101110000101101011101111101111111010 Scott Cranston
00000000000000010000000000000001000000 Dave Cronauer
00000000000011000000000111111001111011 Dejan Nickovic
11011101111001000000000000000000000000 Mike Demler
00000000000000000000000000000000000000 Surrendra Dudani
11100000001111111111110011011111111111 John Havlicek
11100011001000000000000000000000000000 Kevin Jones (RGG Leader)
00000001111111111011101111111111111111 Jim Lear
00000000000011101110000000000000000000 Top Lertpanyavit
11111101101111111111111110111111111111 Scott Little
00000000000001000000000000000000000000 Erik Seligman
10100000000000000000000000000000000000 David Sharrit
00000001000000000000000000000000000000 Murtaza
00000001000000000001011001100000010010 Martin O'Leary


Action Items:


HA: I see that Dejan sent along an e-mail in response to a discussion last meeting. Dejan can you say a few words?

DN: Yes, the note describes the issue with singular intervals. I also talked about defining events in terms of booleans. I went back to look at how to define events using booleans. An event is a boolean that is true now and false in both the right and left neighborhoods. To do this a notion of past operators are needed which aren't present in the semantics presented here. I am starting to believe that having a separate notion of event may be the right thing to do.

SL: Did you find other uses for the past operators?

DN: There are some properties that can be written more succinctly with the past operators. One example that comes to mind is the DDR2 properties where you are looking at setup and hold times. You can define it all in future, but it is more natural to look at both past and future.

KB: To me the DDR2 specs seem like they are specified oddly. Is this a weird type of measurement or is this a standard measurement?

JH: Can you elaborate more on the example you sent out in e-mail?

DN: The first true then concatenation with 'a' then a second true. Then you need to see one unit of time pass and then another 'a'. The idea is that in a sequence you need to find one pair of 'a's with an exact distance of 1. That is fine, but if you take the negation there is a problem. The negation would say that if you have two 'a's they must have a distance = 1. Without a bound on the 'a's you can't forget the occurence of the 'a' until 1 time unit has passed and you can have infinite 'a's before that time unit. That would require an infinite memory. This means that this language isn't closed under complementation. As I said this is a purely mathematical artifact. This issue doesn't show up in a practical simulator.

HA: This example is maybe a general case. What if it isn't a punctual interval?

DN: If you are using intervals with a strictly positive duration some things can be grouped and you don't have to remember every instance of an event and as a result things can be bounded. This is a well know result in timed automata.

JL: I am struggling on the application of this. What is an example of an application of this?

DN: An example is exhaustive verification (model checking). The checking involves negating the property and then intersecting it with the model. Because the property language is not closed under complementation, you cannot do the initial property negation. For the application of monitors, the number of events will be bounded.

JL: What exactly is the property?

DN: The complement of the property is that there does not exist a pair of 'a's that occur 1 time unit apart. This requires infinite memory if the number of events that can occur is unbounded. Think of it as a boolean signal that toggles and you can create a sequence that toggles often and approaches toggling at 1 when the sequence is infinitely long. It would take infinite memory to do this verification.

JH: Does this phenomenon have to do with the exact time? I am tryin to perturb this example. Instead of asking the two 'a's to be exactly 1 unit if I say there separation is 1-\epsilon and 1+\epsilon is that okay?

DN: This becomes fine. Let's say we see an 'a'. We know that this 'a' will be bad for all 'a's in the interval t-\epsilon and t+\epsilon. This allows us to group all of the 'a's in the future in this interval. This allows us to compute a bound on the memory required to check the property. Why do I think this is important to consider? For the application we are considering (monitoring in simulation), I don't think this is a problem. It is still important because using this generalization will allow people to develop theoretical tools using this language in a clean way. I think it is important to have the language clean and understand what we can and can't do with it.

KB: So you are concerned about the difference between lightweight and heavyweight verification?

DN: Yes. I think that when heavyweight verification makes progress then I believe these advances can be pushed back into the lightweight verification space.

KB: I don't think that we have a requirement that the language we are creating be useful for formal methods. It is still a good idea though.

JL: I have a tangential question. There is a large portion of verification that will be based on sampled analog signals. An example would be a signal processing block (FIR, IIR). In that world do we need any extensions to our assertion language other than the real expressions?

DN: I think not.

KB: They went to some effort to exclude reals in SVA. I wonder why?

JH: I can explain why. No one stepped up to define how they would be used. If they are used in expressions with a boolean result it is clear, but no one wanted to go through the other cases and see which ones needed to be excluded. For instance, if I just write a real value then what boolean value should that be?

KB: Is it due to the preponed sampling?

JH: I don't think so.

JL: The purpose of the question is that I have a feeling we will work on the dense time problem for some time. I wonder if we can put forth something simpler much faster.

KB: You almost already have that.

JL: I would just like to see us have the discrete time solution completely figured out in a short period of time. Do we need to tie it into the continuous solution?

KB: Unless someone is going to implement the intermediate solution then I don't think it really matters to have an intermediate solution.

JH: Let's start on the first example on the bottom of page 2 in the semantics document. Our first example, Dejan's example notwithstanding, is a smear of a boolean condition over exactly 10.5 time units. This uses a syntactic shortcut where in a range of a:b if a=b then we only write one. This matches over an interval where (a && b) are continuously true for 10.5 time units.

DN: Actually in the first two examples the exact time doesn't do harmful things.

JH: That is really counterintuitive to me. Why is a followed 9.7 time units by b not as bad as a followed by 1 time unit.

DN: The issue is the universal quantification.

JH: Okay, so this could be used to build a bad example.

DN: Yes.

JH: This second example matches over an interval that is 9.7 units in length. Because of the real booleans on the ends that interval will have to be closed. At the left endpoint a will have to be true and at the right endpoint c will have to be true.

KB: These are sequences that could fit into SVA as it stands?

JH: Yes. These examples all involve constructs not currently in SVA, but they are intended to work within the current SVA.

JH: The third example is described in English. It uses the realtime fusion operator.

KB: The realtime fusion is similar to the digital ##0?

JH: Yes.

JL: What is a[->1]?

JH: It matches over an interval where 'a' is true at the end and at no point previous 'a' is true.

JL: So it is kind of like an 'a' rising?

JH: Yes, but if 'a' is true now it would match.

JL: How is that different from just 'a'?

JH: 'a' only matches if 'a' is only true now. Think of goto 'a' as carrying time forward looking for an 'a'. If you write 'a' or @(posedge a) you could get the same effect. The #0 connects the two other intervals in the sequence.

JH: One final example which shows how to recover the digital ##1 using the realtime operators. There are some additional requirements in the English and both are clocked by 'c'. We should have said that. We have R and then some glue stuff followed by R'. What we have is a smear of true for 0.0+ as a lower bound and $ as an upper bound. We are really just asking the length of the interval to be positive. + means that the inequality on the interval length is strict. The intervals length must be strictly greater than 0 and dollar means there is no upper bound on the interval. That interval is combined without 'c' which means that no 'c' can occur in the interval.

JL: Doesn't this result in an infinite interval? Don't you want to force it on integral length.

JH: Well, R and R' are both clocked on 'c', so they will only match on 'c'.

JL: I see.

JH: With respect to the $, the intervals are bounded in our interval. The length is arbitrarily long, but it is still bounded.

JL: This saying that R is true and then 1 clock cycle later R' is true?

JH: Yes, this is saying that the glue creates ... I hope this gentle introduction will cause some to trek through the rest of the document.

JL: Don't get your hopes. I do think that this introduction and examples are very helpful. I think that the work and the scope are very useful.

JH: We do also show how to get the digital ##0 in the semantics.

SL: It is is simpler, so we didn't show it.

JL: In the paper do you show that all of the digital operators can be derived from the realtime operators?

KB: Yes. The ASVA is a subset of SVA.

JH: Think of choosing basis for vector spaces. There is not a canonical way to to this. We defined a realtime semantics. The first question is if the semantics is consistent with the semantics defined on the discrete traces. The first question is did we define a realtime semantics that is consistent with the discrete semantics. Then we need to determine the primitive and derived operators.

KB: So what you have done is define all of the existing SVA operators as derived?

JH: No, I am not saying that. We assume that we have SVA operators like intersect and or. We are just saying that they can now join more general sequences.

DN: I think these kind of results are very good. It is very good to know that this is possible even if it may not be practical.

SL: Does anyone have any thoughts about remaining work for the rest of the year? Do we need to take a holiday break?

KB: I will be around.

-- ScottLittle - 2009-11-11

Topic revision: r1 - 2009-11-11 - 17:11:15 - ScottLittle
Copyright © 2008-2024 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback