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