Also mine. Thanks, Dmitry ________________________________ From: Fais Yaniv [mailto:yaniv.fais@freescale.com] Sent: Sunday, December 02, 2007 6:36 PM To: Korchemny, Dmitry; sv-ac@eda.org Subject: RE: [sv-ac] 1900 (checkers) and variables types keywords Hi Dmitry, please see my comments below. Yaniv ________________________________ From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com] Sent: Sunday, December 02, 2007 17:17 To: Fais Yaniv; sv-ac@eda.org Subject: RE: [sv-ac] 1900 (checkers) and variables types keywords Hi Yaniv, I understand your concerns, but I am afraid there are also serious arguments against splitting free variables into different entities. I will try to address these issues below. If the name "freevar" itself is confusing, we can consider other suggestions. Thanks, Dmitry ________________________________ From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Behalf Of Fais Yaniv Sent: Wednesday, November 21, 2007 1:05 PM To: sv-ac@server.eda.org Subject: [sv-ac] 1900 (checkers) and variables types keywords Hi, In the current proposal inside checkers all the variables are defined using the keyword "freevar". It seems to me however that those variables can be differentiated into 3 main categories: 1. non deterministic variables 2. (deterministic) state variables 3. (deterministic) continuous assigned variables I think that giving the same keyword for all those types is confusing since it makes it difficult to read and understand which variables are non-deterministic and which aren't (you have to look for all the assignments and check that a variable isn't assigned anywhere) therefore I suggest using different keywords for those different types. The first type (non deterministic state variables) can retain the name "freevar" whereas for the other two I suggest the existing names of "var" for state variables and "wire" for continuous assigned variables. The semantic should remain the same as in the current proposal only that the names of those different types should change. variables of type "wire" can only participate in "assign" only (not always_check assignments). variables of type "var" can have initial value assignment and be assigned inside "always_check" using one nonblocking assignment. variables of type wire or var can be assigned freevars, for example: checker ck(integer inp1); freevar integer f; wire integer d = f + inp1; ... [Korchemny, Dmitry] In SV nets and variables have different types. E.g., variables may be logic, integer, bit, while nets may be wire, wand, tri, etc. I am afraid that the notation "wire integer d" may be confusing, since wire is a type itself, and it is not integer (neither logic, nor bit). Using var for "deterministic free variables" may introduce backward compatibility issues if regular variables become some time legal in checkers. [Fais Yaniv] I don't think it is true that "wire integer d" is confusing as if I read sub clause 6.6 this is legal, it is true that variables and nets have different types (where in common style vars retain a state whereas nets only represent what drives them which is pretty similar to what I'm trying to split here), it is also true that nets have additional types (wor,tri ..), both nets and vars however can have data types so "wire integer d" is legal I think, nets have restrictions that their data types may only be 4 state, I suggested using only "assign" to avoid that if this confuses anyone. [Korchemny, Dmitry] Yes, you are right, I misread the net_declaration production in the LRM. But it is still true that nets may assume only four-value types, therefore wire bit a is illegal (as you mentioned). There is also a backward compatibility issue, in case regular variables and nets are allowed some time in checkers. I think inside checkers you need (as your current proposal suggests) only simple continuous assignments which are represented using common style wire assignment so I suggest using this exact syntax inside checkers or with "assign <var_name> = <expression>" if the keyword "wire" confuses someone. [Korchemny, Dmitry] A bare "assign" is not different from let, since there is no type declaration. This is problematic because of the output arguments of the checker. Consider the following example: checker one; freevar bit a; two mycheck(a); endchecker checker two(x); assign x = 1'b1; endchecker How would you express this with an assign statement only? As for the "var" being problematic for forward compatibility then how about any of "statevar", "detvar" , "nonfreevar" ? [Korchemny, Dmitry] Maybe statevar is a better choice than freevar (I mean keeping only one kind of variables, but call them statevar instead of freevar) "d" is still considered deterministic since it simply has the value of "f" + "inp1", "inp1" in this case can a deterministic signal coming from another module (sampled) or another freevar from another checker,"f" however is free (under assumptions). a freevar therefore doesn't participate in always_check assignments but only in assumptions. There is an issue with uninitialized variables, for example: var [3:0] counter; always_check @clk counter <= counter+1; The above variable has a nondeterministic initial value inside checkers,I think it should be considered "var" and not "freevar" however since its next state function is given. [Korchemny, Dmitry] And how to consider initialized unassigned free variables? Should they be freevar or var? Why should the uninitialized free variables to be considered "deterministic variables" if their value depends on their initial value, which is nondeterministic? Also, if to make "deterministic" and "nondeterministic" free variables different kinds of variables, it will be impossible to mix them in arrays and structures, e.g., freevar bit[2:0] a; freevar bit[2:0] b; assign b = ~a; assign a[2] = a[0] && a[1]; ... [Fais Yaniv] I think initialized unassigned free variables should be considered nondeterministic since their next state function is unknown thus they are determined by assumptions and not any user explicit assignment (except for initial value), generally speaking nondeterministic variables require constraint solver (if there are assumptions) and deterministic variables require only a normal simulator whereas the initial value is somewhat different. I agree that for those "mixed" variables (no initial value with next state assignment and initial value without next state assignment) a strict rule may be confusing for some users but since my suggestion is only syntactical how about allowing those kinds of variables be declared both as deterministic or nondeterministic according to user's view ? (the keyword is suppose only to help the user and if one thinks a state variable with no initial value should be considered nondeterministic there is nothing wrong with that and hopefully it shouldn't cause any problems) [Korchemny, Dmitry] I think it makes things more complicated. As for assumptions is concerned, they may constrain "deterministic" variables as well, e.g., freevar bit a, b; assign a = b; assume property(@clk a); As for the limitation on arrays : do you mean that in your above example a[0] and a[1] are non-deterministic ? if so then I do think that putting this limitation is fair since in my opinion this is bad coding style, it has an easy workaround anyway (freevar bit [1:0] a; assign a_2 = a[0] & a[1]; assign b = ~{a_2,a};) [Korchemny, Dmitry] My example is artificial, of course, but I am not sure that its coding style is that bad. The idea behind this style is to define an entity that looks as an array (or as a struct) towards the external world, but its internal implementation may allow both "deterministic" and "nondeterministic" parts. Thus in the above example a behaves as an array towards the external word represented by b: b considers a as an array and computes its own elements by negating every element of a. But the implementation of a is partially deterministic and partially not. To get a more meaningful example, think about checker(s) modeling a pipeline: the pipeline operates on vectors, but some vectors or their bits may be abstracted by "nondeterministic" variables, while others are not. Another issue is that wires can have only 4 state typed variables in modules, I don't think this is needed inside checkers so if someone finds it confusing to remove this limitation inside checkers I suggest using only "assign" instead of "wire",e.g: "assign integer d = f + inp1; " so the declaration and continuous assignment are in the same line. [Korchemny, Dmitry] See my comment above. [Korchemny, Dmitry] I am recalling the rest of the remaining statement: "The notion of wire is absolutely different here than in Subclause 6.6." What do other people think of this suggested change ? is this worth changing or am I the only one finding the usage of "freevar" for all types confusing ? Yaniv --------------------------------------------------------------------- Intel Israel (74) Limited This e-mail and any attachments may contain confidential material for the sole use of the intended recipient(s). Any review or distribution by others is strictly prohibited. If you are not the intended recipient, please contact the sender and delete all copies. -- This message has been scanned for viruses and dangerous content by MailScanner <http://www.mailscanner.info/> , and is believed to be clean. --------------------------------------------------------------------- Intel Israel (74) Limited This e-mail and any attachments may contain confidential material for the sole use of the intended recipient(s). Any review or distribution by others is strictly prohibited. If you are not the intended recipient, please contact the sender and delete all copies. -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Mon Dec 3 00:22:17 2007
This archive was generated by hypermail 2.1.8 : Mon Dec 03 2007 - 00:22:47 PST