3-Valued Circuit SAT for STE with Automatic Refinement

Abstract. Symbolic Trajectory Evaluation (STE) is a powerful technique for hardware model checking. It is based on a 3-valued symbolic simulation, using 0,1 and X n"), where the X is used to abstract away values of the circuit nodes. Most STE tools are BDD-based and use a dual rail representation for the three possible values of circuit nodes. SAT-based STE tools typically use two variables for each circuit node, to comply with the dual rail representation. In this work we present a novel 3-valued Circuit SAT-based algorithm for STE. The STE problem is translated into a Circuit SAT instance. A solution for this instance implies a contradiction between the circuit and the STE assertion. An unSAT instance either that the assertion holds, or that the model is too abstract to be verified. of a too abstract model, we propose a refinement automatically. We implemented our 3-Valued Circuit SAT-based STE algorithm and applied it successfully to several STE examples.

• Type: Conference
• Year: 2007
• Where: ATVA
• Authors: Orna Grumberg, Assaf Schuster, Avi Yadgar
• Keywords: ATVA 2007, Circuit Node, Hardware, SAT-based STE, STE Tools