Scaling RTL property checking using feasible path analysis and decomposition

Property checking at the Register Transfer Level (RTL) is a critical problem for verifying complex digital design. In this paper, we present a scalable solution for property checking at RTL. We check the properties of the form G(A=>X^=tB), which means that once A is valid, B should be valid t cycles later. We introduce a decomposition strategy to scale high level bounded property checking. This decomposition strategy partitions the monolithic SMT based BMC problem into multiple smaller, independent subproblems. Every path in the RTL program is analyzed for feasibility/relevance using (a) a hybrid of concrete and symbolic execution and (b) property based pruning using the antecedent condition A. The partitions of the RTL source code that correspond to the feasible paths are then checked with respect to the property of interest using an SMT solver. We manage to prune a large percentage of the RTL design paths using feasibility check, such that the decomposed subproblems are small and easily verifiable.