Re: [sv-ac] Feedback request

Ref: http://www.eda-stds.org/svdb/view.php?id=5063
Dmitry,
[Dmitry]
​
One more thing. I think that the explanation of assume statement should be
modified: assume does not serve to generate input stimuli by formal tools
by to restrict the legal traces. Assumptions may be used to generate input
stimuli for test generation tools.
[Ben] I buy that.

On automatic inferences, I made up the following simple model that brings
up some interesting issues that could be problematic for automatic
inferences.  Code has embedded questions and comments.
*module *dut*(*
        input logic clk, ack,
        output req*);*
  // When dut generates a req, it expects an ack within 4 cycles.
  // also, once req is active (i.e., ==1'b1), it remains hi until ack.
  // req must drop in cycle following ack.

  ap_reqack0:* assert property(@(posedge clk) *
          $rose(req) |=> req[*0:4] ##1 (req && ack) )*; *
  ap_ack_fell:* assert property(@(posedge clk) *
    $rose(ack) |=> $fell(req)*); *
  ap_noack_without_prior_and_hold_req:* assert property(@(posedge clk) *
    ack |-> req && $past(req))*; *
endmodule : dut

module chip( // other stuff
);
  logic clk, req, ack;
  // this module receives req from dut and sends back ack

  dut dut1(.*);
  ap_reqack1: assert property(@(posedge clk)
          $rose(req) |=> req[*0:4] ##1 (req && ack) );
  // For formal verification, we need the following constraints on req input
  // If  the following assume statements are commented out, what kind of
  // automatic inferences can be for req?
  // Also, do we really need an SV interface for automatic inferences?
  mp_reqack1: assume property(@(posedge clk)
          $rose(req) |=> req[*0:4] ##1 (req && ack) );

  // Need to assume constraints on req
  am_ack_fell:* assume property(@(posedge clk) *
    $rose(ack) |=> *$fell*(req))*; *

  am_noack_without_prior_and_hold_req:* assume property(@(posedge clk) *
    ack |-> req && *$past*(req)*); *
endmodule : chip

[Ben] Thus, my concerns are what are the automatic inferences?  If it is
not clear, then there could be bad presumptions about are assertion
statements.  In the above example, I did not us the SV interface, but I
don't think that this would make a difference.


On Thu, Nov 27, 2014 at 12:55 AM, Korchemny, Dmitry <
dmitry.korchemny@intel.com> wrote:

>  Hi all,
>
>
>
> I would like to comment regarding the importance of assertion inference:
>
>
>
> The LRM states the following (16.2 Overview):
>
>
>
> An assertion appears as an assertion statement that states the
> verification function to be performed. The statement shall be of one of the
> following kinds:
>
> — assert, to specify the property as an obligation for the design that is
> to be checked to verify that the property holds.
>
> — assume, to specify the property as an assumption for the environment.
> Simulators check that the property holds, while formal tools use the
> information to generate input stimulus.
>
>
>
> This definition contradicts using assertions as assumptions in formal
> verification. The fact that most FV tools know how to handle this situation
> just means that their behavior contradicts the standard. Because nobody
> wants to make their behavior compliant to the standard, the standard must
> be changed to make such behavior legal, and define the desired degree of
> freedom of assertion inference.
>
>
>
> There may be an entire spectrum of solutions, starting from adding a
> clarification that the formal tools may infer the meaning of assert
> statement freely to introducing a special syntax for assertion inference
> and defying strict rules how to infer assertion meaning in each case. I
> think that the right approach is somewhere in the middle. But in any case
> the problem has to be handle.
>
>
>
> ​​
> One more thing. I think that the explanation of assume statement should be
> modified: assume does not serve to generate input stimuli by formal tools
> by to restrict the legal traces. Assumptions may be used to generate input
> stimuli for test generation tools.
>
>
>
> Thanks,
>
> Dmitry
>
>
>
> *From:* Ben Cohen [mailto:hdlcohen@gmail.com]
> *Sent:* Monday, November 24, 2014 20:01
> *To:* Korchemny, Dmitry
> *Cc:* sv-ac@eda.org
> *Subject:* Re: [sv-ac] Feedback request
>
>
>
> On
>
> ​
>
> 5063: Automatic inference of assertion statement type
>
> I am changing my feedback to *"nice to have*", but I* have concerns about
> usage,* as this will add complications to SVA and possible
> misunderstandings.  Also, isn't this a tool issue rather than a language
> issue? This topic needs discussion at our next meeting.
>
> Thanks,
>
> Ben
>
>
>
> On Fri, Nov 21, 2014 at 3:47 AM, Korchemny, Dmitry <
> dmitry.korchemny@intel.com> wrote:
>
>  Hi,
>
>
>
> You are requested to send your feedback on working on the following Mantis
> items in the next P1800 PAR by 1-Dec-2014, UTC:
>
>
>
> ·        3478: Make drivers of inout ports accessible
>
> ·
>
> ​​
>
> ​​
>
> 5063: Automatic inference of assertion statement type
>
> ·        5064: Create standard package to define constants used in
> assertion-related stuff
>
> ·        5065: Create standard package to define implementation for
> commonly used properties
>
> ·        5067: Allow variables in delays and repeat operators
>
> ·        5068: concurrent assertions in classes
>
>
>
> Your feedback should include one of the following marks for each item:
>
> ·        Important
>
> ·        Nice to have
>
> ·        Not important
>
> ·        No opinion
>
> along with any free text comments.
>
>
>
> You may also suggest additional enhancements not listed above, but they
> need to be filed as Mantis items first.
>
> There is no need to discuss any errata or clarification items.
>
>
>
> 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.
>
>
>
> ---------------------------------------------------------------------
> 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.