What to do after Inconclusive Assertion in Assertion Based Formal Verification?

SystemVerilog
, ,
1

In Assertion Based Formal Verification, if I get an Inconclusive Assertion, then what are the various approached to handle that assertion or to converge it?

Also, Is it a right approach to develop a reference rtl and write assertions to compare reference rtl output with DUT output? Will it increase the valid State Spaces and hence complexity, run time also?

2

n Assertion Based Formal Verification, if I get an Inconclusive Assertion, then what are the various approached to handle that assertion or to converge it?

You say “inconclusive”, by that you mean could not find a pattern to make it pass?

  • Did you use the “strong” or the s_eventually"?
  • Did you write necessary “assume” statements? From my 4th Edition of SVA Handbook:

4.5.1.2.2 Same inputs in antecedent and consequent
Inputs are sometimes used in both the antecedent and consequent of a property. They are often useful in simulation to ensure compliance to protocol by either the higher-level design or by the testbench. For example, the property pACK_START_VALID_DONE states that both the trigger condition (the antecedent) and the EFFECT sequence (consequent) rely on the

input ack_in. // /ch4/4.5/orig_slave_handshake.sv
sequence qACTIVE_REQUEST; req && !ack_in;
property pACK_START_VALID_DONE;
@ (posedge clk) disable iff (!reset_n)
qACTIVE_REQUEST ##1 ack_in |=>
start && !ack_in && valid ##1
(!start && !ack_in && valid)[*3] ##1
(!start && !valid && done);
endproperty : pACK_START_VALID_DONE
apACK_START_VALID_DONE : assert property (pACK_START_VALID_DONE);

When the same input signals are used in the antecedent and consequent side of a property, false negative errors in formal verification can be created because the formal verification tool can assume inputs to have any value at any cycle. This is not a design fault, but rather an error in the definition of the constraints on the inputs. An example of a constraint for the above case would be:

mpCONSTRAINT_ACK_START_VALID_DONE : assume property(@ (posedge clk)
qACTIVE_REQUEST ##1 ack_in |=> !ack_in[*1:$] ##1 (!start && !valid && done));

The mpCONSTRAINT_ACK_START_VALID_DONE assumption states that one clock after state qACTIVE_REQUEST, if ack_in ==1, then it must be zero starting from the next cycle until (!start && !valid && done).

  • Can you break your assertion into smaller ones? That might help determine where the issues are.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

  • SystemVerilog Assertions Handbook 4th Edition, 2016 ISBN 978-1518681448
  • A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
  • Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
  • Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
  • Component Design by Example ", 2001 ISBN 0-9705394-0-1
  • VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
  • VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
3

In reply to ben@SystemVerilog.us:

Actually, I have written simple enough constraints for APB protocol. And I have created a reference model to mimick DUT.

So my assertions are just to compare reference model output with DUT output on every active clock edge.

In this scenario, can you give me any approaches for Inconclusive Assertions? Also, it would be helpful, if you can give me any paper/article related to Assertion Based Formal Verification, as I am not able to find much on this topic.

4

In reply to Karan:

In reply to ben@SystemVerilog.us:
Actually, I have written simple enough constraints for APB protocol. And I have created a reference model to mimick DUT.
So my assertions are just to compare reference model output with DUT output on every active clock edge.

In his book on formal verification (see reference below), Erik Seligman addresses the topic of shadow modeling, and it is a good technique, for complex models (e.g., ALUs) to generate the expected results based on the inputs.

In this scenario, can you give me any approaches for Inconclusive Assertions? Also, it would be helpful, if you can give me any paper/article related to Assertion Based Formal Verification, as I am not able to find much on this topic.

In his book, Erik addresses the topic of inconclusive proofs Formal Verification: An Essential Toolkit for Modern VLSI Design - Erik Seligman, Tom Schubert, M. V. Achutha Kiran Kumar - Google Books
Unfortunately, I am not an expert on formal verification. However, in his book, Erik does an excellent job on covering the topic and on addressing guidelines and tips to achieve the desired goals. My guess in addressing this topic of inconclusive proofs is to isolate that piece of hardware and to add more constraints or more restrict SVA statements.
Erik’s book: Formal Verification: An Essential Toolkit for Modern VLSI Design 1st Edition by Erik Seligman (Author), Tom Schubert (Author), M V Achutha Kiran Kumar (Author) http://goo.gl/u20Om2
Also, read the reviews at Amazon.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

  • SystemVerilog Assertions Handbook 4th Edition, 2016 ISBN 978-1518681448