‘assume’ and Formal (Static Functional ) Verification

Abstract

This is an interesting operator. ‘assume’ specifies the property as an assumption for the environment. What’s an environment? The most useful ‘environment’ for ‘assume’ is that of static formal verification. Static formal is a method whereby the formal algorithm exercises all possible combinational and sequential possibilities of inputs to exercise all possible ‘logic cones’ of a given logic block and checks to see that the assertion holds. During such verification if you do not specify any constraints (i.e. for a 5 input (a, b, c, d, e) block, if you don’t specify any constraints such as ‘assume’ a=0 and b=1) then the static formal will try to explore all possible combinations of the 5 input both in combinatorial and temporal (if required) domain. Without any constraints provided via ‘assume’, the static formal tool may experience something called ‘state space explosion’. As the description suggests, the tool may give up if too many inputs are unconstrained. This is where the ‘assume’ statement comes into picture.