Parameterized Hardware Verification Through A Term-level Generalized Symbolic Trajectory Evaluation and Its Linkage with Concrete Hardware Verification at Netlist Level

This article proposes a term-level generalized symbolic trajectory evaluation (GSTE) to tackle parameterized hardware verification. We develop a theorem-proving technique for parameterized GSTE verification. In our technique, a constraint is associated with a node in GSTE graphs to specify reachable states. Generalized inductive relations between nodes of GSTE graphs are formulated; instantaneous implications are formalized on the edges of GSTE graphs. Based on this formalization, parameterized GSTE are verified. We moreover formalize our techniques in Isabelle. Furthermore, once a parametrized design is verified at the term level, we can convert the generally parameterized invariants into concrete ones, which can be used to verify a synthesized netlist of an instance of the parameterized design at the Boolean level. We demonstrate the effectiveness of our techniques in case studies. Interestingly, subtleties between different implementations of FIFOs are discovered by our parameterized verification, although these circuits have been extensively studied previously.