Hi, - 16.18.1 says, "Checker variables differ from regular variables in that they may be both deterministic and nondeterministic. They may have undefined or partially constrained values, while regular variables are always deterministic in the sense that they contain only one specific value at a time." I have not yet finished the proposal, but what does 'undefined' mean here? It seems a little strange. [Korchemny, Dmitry] "Undefined" means that the variable may contain any value of its type, and in formal verification when this variable is used in an assertion, this assertion is checked for all possible values of this variable. This is explained in 16.8.6: "A free variable may assume any value at every point in time, similarly to an input of the design. Formal analysis tools shall take into account all possible values of the free variables imposed by the assumptions and assignments (see 16.18.6.1). Simulators shall assign arbitrary values to the free variables consistent with the assumptions and the assignments." [SB] Thanks, I think this should be clearer. Shalom -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Tue Jan 29 04:08:30 2008
This archive was generated by hypermail 2.1.8 : Tue Jan 29 2008 - 04:08:31 PST