Stats

  • Locked Locked
  • Replies 8
  • Subscribers 65
  • Views 14811
  • Members are here 0
This discussion has been locked.
You can no longer post new replies to this discussion. If you have a question you can start a new discussion

IFV PSL , using VHDL comparison operator

Jentil

Hi ,

  I have an assertion in my PSL file -

 Assert1 : assert always ( { {R_seq} &&  {T /= A and (Z  = '0' ) } }  |=>  { D = ADDBUS }  ) @ (rising_edge(CLK)  ;  

 where  R_Seq is defined as - 

   sequence  R_Seq = { A1 and B1 } ;

 The assertion passed .

 Now , out of curiosity I have written a negative check -

 Assert2: assert always( { {R_seq} && { T/=A and (Z = '0' ) } }   |=>  {  D /= ADDBUS } ) @(rising_edge(CLK) ;

  This assertion also passed !!! .

  From my understanding , since the LHS are same and RHS are contradicting , either Assert1 or Assert2 should surely fail .

  Please explain to me , if my understanding is correct .

  I was using IFV version 8.20 .

 Also , would like to mention that trigger for both Assert1 and Assert2 passed .

 

 

 

Parents

  • Adding the opposite of an assertion (one expected to "fail") is a useful sanity check. It can help uncover problems with a formal verification setup.

     

    In this instance, having both assertions pass is a possible result. An assertion can pass "vacuously" if the prefix of the assertion can never be reached. As an example, the assertion "a |=> b" will pass if 'a' can never occur. If 'a' is impossible, both "a |=> b" and "a |=> not b" will pass because neither can ever reach the failing state.

     

    So the first thing to look for is whether or not IFV says that the "trigger" of these assertions passes. If the trigger check fails, then the prefix of the assertion is impossible and the assertion itself will pass.

Reply

  • Adding the opposite of an assertion (one expected to "fail") is a useful sanity check. It can help uncover problems with a formal verification setup.

     

    In this instance, having both assertions pass is a possible result. An assertion can pass "vacuously" if the prefix of the assertion can never be reached. As an example, the assertion "a |=> b" will pass if 'a' can never occur. If 'a' is impossible, both "a |=> b" and "a |=> not b" will pass because neither can ever reach the failing state.

     

    So the first thing to look for is whether or not IFV says that the "trigger" of these assertions passes. If the trigger check fails, then the prefix of the assertion is impossible and the assertion itself will pass.

Children
No Data

Community Guidelines

The Cadence Design Communities support Cadence users and technologists interacting to exchange ideas, news, technical information, and best practices to solve problems and get the most from Cadence technology. The community is open to everyone, and to provide the most value, we require participants to follow our Community Guidelines that facilitate a quality exchange of ideas and information. By accessing, contributing, using or downloading any materials from the site, you agree to be bound by the full Community Guidelines.