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
------------------

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.