Parameterized Hardware Verification Through a Term-Level Generalized Symbolic Trajectory Evaluation

This paper 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 edges of GSTE graphs. Based on these formalization, parameterized GSTE are verified. We moreover formalize our techniques in Isabelle. 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.