Performance issue

[Gy-Hu]

For this case, ic3ref can solve <1s, but rIC3 cannot solve in minutes.

I haven't found the reason yet.

wrapper_add_w8.aig.txt

[gipsyh]

The result given by IC3ref is unsafe, but I couldn’t find a bug using BMC. I suspect there might be a bug in IC3ref.

However, at the moment, rIC3 is indeed unable to solve this case, so improvements are definitely needed.

[zhanghongce]

Hi Yuheng, I'm reading the pull request: #25 and try to figure out what it is about.
Is it a change from checking $F_{last} \wedge bad$ to $F_{last} \wedge T \wedge bad_{next}$ ?
And is it related to this issue?

[gipsyh]

Hi Professor Zhang, as you said, #25 changes from "finding bad in the last frame" to "finding a predecessor of bad in the last frame each time." This change is related to this issue, but it still does not resolve this case. Further analysis may be needed.

[gipsyh]

Perhaps unrolling further so that the solver looks for the predecessor of the predecessor of bad instead of the predecessor of bad might be effective. I will try this later.

[zhanghongce]

Hi Yuheng, I suspect that the bug in IC3ref is related to how assumptions are handled. If I use ABC to fold the assumptions and give it to IC3ref aigain, IC3ref will not report any counterexample. I think Guangyu should open an issue in the repo of IC3ref (though I doubt if Aaron will fix it, because the last commit was 10 years ago).

Regarding the performance, in my opinion, this is in general a hard case for IC3, because its inductive invariant seems to be very large if it is expressed just using the latches without additional variables. Additionally, there happens to be no good internal signals to use either 😔

[gipsyh]

Hi Professor Zhang, Lingfeng Zhu @zhfffy once found a bug in IC3ref and provided a detailed description in the attachment. I guess this might be the cause of the issue.

IC3Ref前继泛化方式的Bug及优化(1).pdf

[gipsyh]

Regarding the performance, in my opinion, this is in general a hard case for IC3, because its inductive invariant seems to be very large if it is expressed just using the latches without additional variables. Additionally, there happens to be no good internal signals to use either 😔

Perhaps constructing new signals is necessary to resolve this issue.

[Gy-Hu]

@gipsyh yuheng, thanks for your sharing!! Since this is not the issue related to rIC3, I close this issue now.