Verification and diagnosis of digital systems by ternary reasoning

Abstract

Ternary vectors {0,1,X} may be used to simulate binary systems more efficiently than binary vectors. It has recently been shown by R.E. Bryant that formal verification by ternary simulation is feasible. In this paper, we demonstrate that complete verification of Finite State Machines is possible by ternary simulation. The verification vectors are derived from AND/OR trees. We also show how design error diagnosis can be performed by utilizing the difference vector set. Algorithms for the diagnosis of single inverter errors, and wrong gate type, are presented, together with illustrative examples.