Signal domain based reachability analysis in RTL circuits

Register-transfer level (RTL) verification is a challenging problem for today´s complex circuits. A sub-problem of verification is reachability of basic blocks or branches in the code. This paper proposes a novel analysis based on the domain of signal values in the RTL code to reason about the reachability of all branches without explicit circuit unrolling. This analysis takes into account all assignments, activating and preceding conditions in the code, to derive an assignment table that lists all the possible sequences of branches required to reach a target branch. In the process, it proves unreachable branches as well as provides guidance for reachable branches. This analysis resolves branches more efficiently compared to other methods for the ITC99 [1] benchmarks, especially for larger benchmarks containing previously unresolved branches.