TWiki> VerilogAMS Web>AmsAssertions>RequirementsGatheringGroup>MeetingMinutes20091028 (2009-11-03, AnandHimyanshu)EditAttach

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

Action Items:

Details:

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

Edit | Attach | Print version | History: r1 | Backlinks | Raw View | Raw edit | More topic actions

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

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

Ideas, requests, problems regarding TWiki? Send feedback