Alec Stancelescu
Arif Samad
Avinash Mani
Bassam Tabbara
Brad Pierce
Cliff Cummings
David Smith
Dennis Brophy
Doug Warmke
Erich
Marschner
Jay Lawrence
Joao Geada
Karen Pieper
Mehdi Mohtashemi
Neil Korpusik
Nikil Rishiyur
Peter Flake
Ray Ryan
Stu Sutherland
Surrendra Dudani
Swapnajit Mittra
Tarak Parikh
Vassilios Gerousis
Create AI within SV-EC to look at the assume proposal.
Add Errata in SV-EC to deal with implication.
Coordinate issue of $inset vs inside to SV-AC and SV-BC
Review of slides
Review of slides
Review of slides
Review of slides
Erich: Is the lifetime of automatic variables in fork..join being reconciled with the handling of automatic variables within a sequence. This is the same problem.
Jay: It is not clear that this is the same. We should discuss this to see if it is the same.
David: We will look to see if the solutions are consistent (and should be consistent).
VCD API
Jay: Is it really reader for VCD files or a database?
Bassam: It is to a database.
Jay: Then we should not call it a VCD interface. We should call it a data API.
Peter: It is really just a trace interface.
Doug: I would agree with that.
Jay: Let's put it into the database that way.
VPI
Extension
Exported Task
Questions due to lack of precision in slides (mostly from Erich Marschner). David requested that the actual language in the accepted proposal be similarly scrutinized to make sure the language is precise.
Stu raised the issue of limiting the compilation-unit scope to just supporting the import statement.
Dave Rich indicated that once we allowed the import we should just allow the declaration.
David indicated that, after reviewing the usage of both SV 3.0/3.1 and Superlog, the majority uses of $root was for accessing a rooted hierarchical reference and providing a global declarations scope similar to the compilation-unit scope (the actual use of $root as part of a hierarchical reference to items declared in the compilation-unit scope was limited). For backward compatibility it is important to continue to provide this feature in some fashion.
Alec: Difference between assert and assumption is that assumption uses variables used outside scope of circuit being tested?
Surrendra: No difference except assumptions refer to environment. For formal tools the inputs are not connected.
Erich: It is up to the tool creator about using assertions or assumptions. Why is there a need to distinguish between the dist and inside operator? Why not a single operator?
Surrendra: In the property just use a dist. If using as an assertions it is changed to inside.
Nikhil: A question related to assert vs. assume. What in this states that the assume is related to environment?
Erich: There is no semantic requirement to have both but different tools use them.
Jay: In the constraint block we do not allow sequences.
Arturo: This iws what will be provided here.
Jay: We are now adding temporal semantics to the constraints?
Arturo: Yes.
Jay: This will be required by users. Deadend states will be a problem. This makes the implication discussion more important and also using sequences in constraints.
Tarak: You said they are sequential constraints and the become Boolean constraints?
Surrendra: They are transformed. Example on next page.
Jay: for the example of using sequential constraints to be correct the properties pA and pB need to be declared within the class.
Erich: In slide 11 in the class use of constraint are you limited to having only one constraint within the class? Is the example equivalent to having to constraints, one for each property?
Jay: You can have multiple constraints.
Surrendra: The would be the same.
Tarak First time you call randomize the properties advance.
Surrendra: You have to randomize this correctly just like Boolean constraints. You have to make sure that it is done in the correct order at the correct time.
Jay: Is there any provision for overlapping semantics? What happens if X goes hi again? Property pA starts when X goes high (which is randomized). If there is another variable q are we going to handle the overlap?
Joao: Semantically the first call to randomize starts a process. You have to hold the constraints. Until it is complete a call to randomize does not do anything.
Arturo: That is not what he is saying. You call it at the correct time.
Jay: What is the status for this?
Arif: The proposal is under consideration.
Erich: Joao's suggestion makes a lot of sense.
Jay: We need to look at this in the SV-EC as well.
Erich: Slide 14: It looks like this is a deterministic implementation. This means that you do not intend to support overlapping sequential constraints.
Tarak Slide 16: If you say that this is being solved bi-directionally then you cannot set Y to 1 since it violates the constraint.
Jay: Only if you do a full-reachability analysis. We do not want to do this in the language.
Erich: What are the units of the denominator?
Arturo: The denominator is the possible state space.
Doug: Why not use if instead of iff?
Jay: Using if would lead a user to expect to be able to specify an else clause.
Nikhil: The set of values are always integral?
Arturo: Yes.
Erich: Is there an implicit requirement that values are not overlapping?
Arturo: No.
Neil: The slide says multiple bins per value. Is this correct?
Arturo: That is not correct. The slide is wrong.
Doug: If you do not use default then what happens?
Arturo: The values are not counted.
Dave: How do you guarantee that you have not counted something false?
Erich: There does not seem to be a way to prevent overcounting?
Jay: Because of allowing overlap there is no way to restrict.
Arturo: A post-processor can indicate this.
Erich: The {1:8} is a non-deterministic representation of state.
Arturo: It is supposed to be [] in both cases on slide 12.
Erich: This non-determinism shows up in many cases.
Arturo: Why is this non-determinism?
Erich: There is already a syntax for this.
Arturo: We have an operator for this in constraints.
Jay: The same semantics should use the same syntax.
Arturo: Agreed.
Jay: Do you need parenthesis on the bins for t[] on slide 13?
Arturo: Correct.
Nikhil: Can we use assertions to detect transitions and count the result.
Arturo: You would have to define this.
Jay: That was my first thought. The difference is that these are not expressions but little values. You would write a much different thing.
Arturo: You would have to add a lot of syntax.
Jay: With the proposal for triggering on sequences being complete the result could be counted.
Arturo: I do not have a mechanism to access the variables in the sequence.
Jay: Relating the assumptions, assertions, constraint, and coverage stuff is important.
Tarak: How do you define default for expressions? Default sequence means none of the sequences match?
Arturo: Correct. Mostly useful for simple pairs of transitions.
Cliff: If I put [] after bad you can generate a huge number of bins.
Arturo: We can be clever based on knowing the size of the state space.
Erich: The use of wildcard keyword just allows the ? to be interpreted as a wildcard?
Arturo: Correct.
Joao: If the data contains an x then what happens?
Arturo: It is thrown out. It use to be handled that way but we were beat up.
Jay: It might be interesting to allow casez or casex where wildcard as well.
Arturo: This is plausible.
Karen: What about wildcardz and wildcardx?
Arturo: It was considered but not high enough value.
Erich: Can you also control the number of bits in the bin counters?
Arturo: There is a min count not a max count.
Erich: That is a goal. Is there something that says after you get to a specific count that it is enough? You have taken pain to specify the number of bins. You could also specify the size of the counter for the bin.
Arturo: They are currently limited to 32 bits.
Erich: Do they wrap around?
Arturo: Probably. You do have to handle overflow. An upper limit might be a good point.
Page 16:
Erich: What you want is to allow the use to vary the bin size and not have to go to two places (two different statements).
Arturo: Typically the autobinning handles this.
Erich: If you decouple bins from value hits it will adapt better. What you mean is ignore the values. Build an exclusion mechanism as part of the specification.
Arturo: It seems you are suggesting a change in the keyword.
Neil: It is ignoring the set of values not the bin.
Joao: The meaning is not at issue. If there is a bin that includes the value is its specification the ignore_bins will specify that the value will have a count of 0.
Erich: So, the issue is the syntax. exlude_values or something else might be better than ignore_bins.
Page 17:
Erich: Why not use assertions in the cover group?
Joao: Users have always wanted to say never hit this.
Dave: This was because assertions are not available.
Joao: This is much simpler than writing an assertion.
Dave: These coverpoints are available outside of the covergroup.
Arturo: You cannot access the bins. If you will allow for it then the user will have to write lots of code. There is also a syntactical access issue for transitions. And users have not wanted this. Vera had it but no one used it.
Page 21:
Erich: What does intersect mean.
Arturo: It means that it selects only bins that intersect the range specified.
Erich: This is not intersection it is not overlapping.
Arturo: This is to reuse a keyword.
Erich: This is not set intersection.
Arturo: Correct.
Mehdi: Cross only crosses coverpoints so you cannot have a cross of a cross.
Arturo: Correct. You can have an n-dimensional cross. A cross is not a coverpoint. The only operation on a cross is to "print it out".
Page 23:
Doug: Do the arguments have to be elaboration time constants?
Arturo: No.
Nikhil: Why use the ref?
Arturo: Because you want to measure the changing value of ra not the initial value.
Jay: It is pass by value by default.
Dave: So if you pass low as a ref you could change it during run?
Arturo: No. The space is computed at instantiation time.
Jay: We discussed allowing constraints to be parameterized as well. It is almost like the sequence stuff where macro expansion is.
Erich: What is the meaning of commulative count?
Jay: If you do not set per_instance then you cannot call get_inst_coverage.
Arturo: You can but you get 0.
Mehdi: This is common to have in classes and class instances.
Erich: You automatically get commulative coverage. The question is do you get per instance?
Arturo: Correct. You have to turn it on with the option.per_instance.
Erich: These are options you can control outside the cover group?
Mehdi: Not the per_instance. It can only be set once.
Jay: Can you comment on how many times you create multiple instances of a coverage group.
Neil: We did not do it that way but the feedback was that it would be better to use this.
Jay: If you want to have a single coverage group from multiple modules you can put these in a package?
David: There is an action to do this.
Mehdi: Why do we have to call new in a class?
Arturo: Because I hated the way Vera did it and fixed it here to more regular.
Erich: What you seem to be talking about is cummulating to a common point. Aggregate would be better. Some of the options should be available to the manager and no one else.
Erich: What is overall coverage?
Arturo: The bins->coverpoints->crosses->overall.
Erich: A single number does not really say anything.
Arturo: True.
Erich: Is there is a mechanism to tell which cover is hit.
Dave: There is an API that goes with this to access the information.
Karen: Do you have something to merge DBs.
Jay: The name for setting the db_name is the minimum requirement. Having the ability to save different coverage groups in different files will be vendor specific.
Nikhil: Keywords are one of the issues with compatability.
Brad: Correct. But the syntax is a superset.
Peter: Are there any tools that can compare two BNFs or with a YACC.
Brad: The examples in the BNF are not checked by the BNF.
Arturo: The examples are normative.
Brad: Having a reference parser would be very helpful.
Jay: There is a move towards using the UML data model for the VPI and VHPI. It is having problems due to size.
We are basically on track.
Based on email sent to SV-AC and SV-EC reflectors on
Brief overview of the issues associated with the different implication like operators in the language (=>, ->, |=>, |->). The taxonomy presented was:
Concept |
Current |
Prop_1 |
Prop_2 |
Prop_3 |
Overlapping |
|
|
|
|
constraint impl. |
=> |
|-> |
-> |
=> |
sequence impl. |
|-> |
|-> |
|-> |
|=> |
cycle delay |
##0 |
##0 |
##0 |
##0 |
Non-overlapping |
|
|
|
|
transition |
-> |
|=> |
=> |
-> |
sequence impl. |
|=> |
|=> |
|=> |
|-> |
cycle delay |
##1 |
##1 |
##1 |
##1 |
Prop_1 is based on unifying the implication operators down to just two.
Prop_2 is based on making overlapping-like operators consistent and non-overlapping operators consistent.
Prop_3 is based on making the constraint implication consistent with the highest usage found on the web (HTML-4.0, Mathematica Mathworld, Algol-60, Python), the transition operator consistent with Verilog event trigger, and consistency among overlapping-like operators and among non-overlapping operators.
No conclusion in meeting. The SV-EC and SV-AC committees will have to resolve this if there is to be any change.