To ensure a design is deadlock free with formal verification, one approach consists in verifying that it is “always eventually” able to respond to a request. The wording is important. Regardless of the current state and the number of cycles we must wait, in the future the design must respond.
This translates very nicely using a type of SystemVerilog Assertion called “liveness propertie...
» read more
