RE: [sv-ac] 1900 is reday for review

Hi Tom,

Some people may object to mention model checking in the LRM, but I
adopted the text you proposed, and uploaded the new version.

Thanks,
Dmitry 

-----Original Message-----
From: Thomas.Thatcher@Sun.COM [mailto:Thomas.Thatcher@Sun.COM] 
Sent: Monday, December 03, 2007 8:27 PM
To: Korchemny, Dmitry
Cc: sv-ac@eda.org
Subject: Re: [sv-ac] 1900 is reday for review

Hi Dmitry,

I think that this text will work.  I agree with Shalom's feedback that
"can" 
should be "may".  You should also add a note similar to the following:

    "(This technique is used by simulators that support model checking
on the
    fly)"

Otherwise, people may have a hard time understanding of what "simulating
all 
possible values" means.

The resulting text would look like:

"Simulation tools may assign random values to the variable flag. They
may use assumptions m1, m2, and m3 to constrain the values generated if
they have the capability to do so. Another option is to perform the
simulation using all possible values of flag constrained by assumptions
m1, m2, and m3 (This technique is used by simulators that support model 
checking on the fly). In case when a simulation tool is unable to
satisfy all
assumptions, it shall report a violation of assumptions that could not
be
satisfied."

Tom

Korchemny, Dmitry wrote:
> Hi Tom,
> 
> My problem here that the simulation tool may not assign random values
at
> all here, but do model checking on the fly and thus check all possible
> combinations, and in some cases this solution may be preferable.
> 
> What about the following text?
> 
> "Simulation tools can assign random values to the variable flag. They
> may use assumptions m1, m2, and m3 to constrain the values generated
if
> they have the capability to do so. Another option is to perform the
> simulation using all possible values of flag constrained by
assumptions
> m1, m2, and m3. In case when a simulation tool is unable to satisfy
all
> assumptions, it shall fire a violation of assumptions that could not
be
> satisfied."
> 
> Thanks,
> Dmitry
> 
> -----Original Message-----
> From: Thomas.Thatcher@Sun.COM [mailto:Thomas.Thatcher@Sun.COM] 
> Sent: Thursday, November 29, 2007 3:13 AM
> To: Korchemny, Dmitry
> Cc: sv-ac@eda.org
> Subject: Re: [sv-ac] 1900 is reday for review
> 
> Hi Dmitry,
> 
> The current wording still sounds like simulators will be required to
> implement
> the constraint solvers necessary to meet assumptions.   How does this
> wording
> sound?
> 
> "Simulation tools shall assign random values to the variable flag.
They
> may
> use assumptions m1, m2, and m3 to constrain the values generated if
they
> have
> the capability to do so.  In case when a simulation tool is unable to
> satisfy
> all assumptions, it shall fire a violation of assumptions that could
not
> be
> satisfied."
> 
> 
> 
> Also I have a question:  are assumptions allowed to constrain a
> non-deterministic free variable indirectly, or only directly?
Consider
> the following example:
> 
>     freevar bit flag;
>     freevar bit flag_d1 = 1'b0;
> 
>     always_check @(posedge clk) begin
> 	flag_d1 <= d1;
>     end
> 
>     m1: assume property (reset |=> !flag_d1);
>     m2: assume property (!reset && flag_d1 |=> flag_d1);
>     m3: assume property (!$rising_gclk(flag_d1) |-> valid);
> 
> The assumptions are written constraining the variable flag_d1, which
is
> a
> deterministic free variable.  Should the constraints be then
propagated
> back
> to constrain the values of the non-deterministic variable flag?
> 
> Thanks,
> 
> Tom
> 
> Korchemny, Dmitry wrote On 11/22/07 04:22 AM,:
> 
> 
>>4.  P. 13:  "In this example the free variable flag behaves as
> 
> follows:"
> 
>>    Change to:  "In formal verification, the free variable flag in
> 
> this
> 
>>		example behaves as follows"
>>
>>[Korchemny, Dmitry] This is not exact. The specification requires that
>>the variable flag behaves as follows, this is not directly related to
>>formal verification. It is written "Formal analysis tools shall take
> 
> all
> 
>>possible legal behaviors of flag into account." and this statement is
>>true for FV of any model: it takes all possible legal behaviors if the
>>model into account.
>>
>>I rewrote this statement as:
>>"In this example the following constraints are imposed on the free
>>variable flag:"
>>
>>    Add:  "In simulation, the free variable flag may take on any value
>>at
>>	  any time, including combinations that could cause the assume
>>	  property statements in this example to fire"
>>
>>[Korchemny, Dmitry] I don't think that in simulation flag values are
>>absolutely random (this might be a case for a "dumb" simulator, but a
>>smart simulator should try to satisfy the constraint or to consider
> 
> all
> 
>>the combinations). Therefore I added the following text:
>>
>>"Simulation tools shall assign values to flag meeting the constraints
>>imposed by assumptions m1, m2, and m3. In case when a simulation tool
> 
> is
> 
>>unable to satisfy all assumptions, it shall fire a violation of
>>assumptions that could not be satisfied."
>>
>>5.  Example, p 21
>>	endchecker : mycheck    should be:   endchecker my_check
>>
>>
>>Tom
>>
>>Korchemny, Dmitry wrote On 11/21/07 04:08 AM,:
>>
>>
>>>Hi all,
>>>
>>>
>>>
>>>I uploaded a new version of the checker proposal
checkers_071120dk.pdf
>>>
>>
>>
>
<http://www.eda-stds.org/mantis/file_download.php?file_id=2813&type=bug>
> 
>>>and I think it is ready for review. This proposal addresses comments
>>
>>of
>>
>>
>>>several people. See the following threads for more information:
>>>
>>>http://www.eda-stds.org/sv-ac/hm/5761.html
>>>
>>>http://www.eda-stds.org/sv-ac/hm/5856.html
>>>
>>>http://www.eda-stds.org/sv-ac/hm/5879.html
>>>
>>>
>>>
>>>Thanks,
>>>
>>>Dmitry
>>>
>>>---------------------------------------------------------------------
>>>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.
>>
>>
> 

-- 
------------------
Thomas J. Thatcher
Sun Microsystems
------------------
---------------------------------------------------------------------
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.