I am formally verifying a block which contains a 10 depth. Few functionalities are used for updating some of its fields based on some of the inputs. It is really difficult to apply abstraction technique in this case, so I am trying to verify this block without using reduction /abstraction.
Here almost all the properties am getting bounded pass, What may be the real cause of bounded pass (inconclusive results) here?
I put that question on perplexity.ai
In SystemVerilog formal verification of a chip design, what is Here almost all the properties am getting bounded pass, What may be the real cause of bounded pass (inconclusive results)
Great reply! (uploaded PDF)
https://www.perplexity.ai/search/in-systemverilkog-formal-s96oQjbQT1SgjHRQK0u.Hw
bounded_pass.pdf (1.1 MB)
Great responses from perplexity.ai. Thanks for sharing, Ben.
Further I would recommend exploring ‘value division’ on your SVA checkers - if applicable. See my article at: 3C's of Formal Property based Verification