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

Will it be better to rewrite it as "report a violation"?

Thanks,
Dmitry

-----Original Message-----
From: Bresticker, Shalom 
Sent: Monday, December 03, 2007 12:07 PM
To: Korchemny, Dmitry; Thomas.Thatcher@sun.com
Cc: sv-ac@server.eda.org
Subject: RE: [sv-ac] 1900 is reday for review

"can assign" or "may assign"?

What is "fire a violation"?

Shalom

> -----Original Message-----
> From: owner-sv-ac@server.eda.org 
> [mailto:owner-sv-ac@server.eda.org] On Behalf Of Korchemny, Dmitry
> Sent: Monday, December 03, 2007 11:59 AM
> To: Thomas.Thatcher@sun.com
> Cc: sv-ac@server.eda.org
> Subject: RE: [sv-ac] 1900 is reday for review
> 
> 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.
> 
---------------------------------------------------------------------
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.