Why Uniqueness Constraints are not used in Yosys' K-Induction script to solve the problem of UNKNOWN due to Unreachable loop of good states?

[shubam7809]

Hello
I have a query related to Yosys implementation of K-Induction Algorithm. I will be grateful if someone (especially Claire Wolf) could help me.
I have been using Yosys for a while to do the Formal Verification of some VHDL designs using PSL assertions. I observed that K-Induction is showing “UNKNOWN” most of the times for my designs. It is probably due to the unreachable loop(s) of good states followed by a reachable bad state in the state space that Claire Wolf have explained in one of her seminars on Yosys. As you must already know, adding addition assertions to break those loops is a strenous process. I wonder why have she has not put any Uniqueness Constraints in Yosys K-Induction script to encounter this problem.

Thanks

[nakengelhardt]

Claire Wolf changed her name in 2019, you'll have a slightly higher chance of getting an answer from her if you edit your message accordingly.

[shubam7809]

Ok Done! Thanks. Hope I'll get a reply soon.

[clairexen]

In most real-world designs there is always some other state somewhere in the design that can change and render simple path constraints useless. There is no option for the smtbmc engine to add simple path constraints. But other engines supported in sby do have such an option. For example the btormc solver that can be used with the btor engine does support a --simple-path option that adds such constraints to the bounded model check.

[shubam7809]

First of all, thank you for your reply. I looked at the documentation of Symbiyosys and one of your paper at CAV 2018 and It seems like there is no provision for K-Induction in Btor engine. It has just two options: BMC and Cover. Can you please confirm it?Also, Can you please elaborate your point on why we can't use simple path constraints? - "In most real-world designs there is always some other state somewhere in the design that can change and render simple path constraints useless. There is no option for the smtbmc engine to add simple path constraints.". As to the best of my knowledge, I see if simple path constraints are added in K-induction, the problem I suggested could be  resolved.