I am using IFV for formal property checking and i have some of the assertions/Property explored.How to make them either pass/fail.
I attach an app note that summarizes tool options to improve results. This can not replace review and optimization of your property and environment. If you need more help please contact your local Cadence AE.
Explored is when the time isnt sufficient for the tool and it runs for however long it can. In that time it couldnt find any counter examples. Prove command usually doesn't give explored, just pass/fail.
This explored assertions got pass/failed when i increase effort.It was explained clearly in the document shared by someone for this question.
But sometimes these explored assertions changed to block on increasing the effort.
I think cutpoints are the solution to this. Has anyone overcome this situation?