Exploiting state encoding for invariant generation in induction-based property checking

ABSTRACT

This paper focuses on checking safety properties for sequential circuits specified on the RT-level. We study how different state encodings can be used to create a gate-level representation of the circuit that facilitates the computation of effective invariants for induction-based property checking. Our experiments show the strong impact of state encoding on the efficiency of the induction process.

REFERENCES

• 1: Parosh Aziz Abdulla , Per Bjesse , Niklas Eén, Symbolic Reachability Analysis Based on SAT-Solvers, Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems: Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, p.411-425, March 25-April 02, 2000
• 2: Per Bjesse , Koen Claessen, SAT-Based Verification without State Space Traversal, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, p.372-389, November 01-03, 2000
• 3: J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill. Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design, 13(4):401--424, April 1994.
• 4: Andreas Kuehlmann , Jason Baumgartner, Transformation-Based Verification Using Generalized Retiming, Proceedings of the 13th International Conference on Computer Aided Verification, p.104-117, July 18-22, 2001
• 5: Wolfgang Kunz and Dhiraj Pradhan. Recursive learning: A new implication technique for efficient solutions to CAD problems: Test, verification and optimization. IEEE Transactions on Computer-Aided Design, 13:1143--1158, Sep. 1994.
• 6: Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
• 7: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 8: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 9: Mary Sheeran , Satnam Singh , Gunnar Stålmarck, Checking Safety Properties Using Induction and a SAT-Solver, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, p.108-125, November 01-03, 2000
• 10: Dominik Stoffel , Wolfgang Kunz, Record & play: a structural fixed point iteration for sequential circuit verification, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.394-399, November 09-13, 1997, San Jose, California, United States
• 11: C. A. J. van Eijk, Sequential equivalence checking without state space traversal, Proceedings of the conference on Design, automation and test in Europe, p.618-623, February 23-26, 1998, Le Palais des Congrés de Paris, France
• 12: Improving Structural FSM Traversal by Constraint-Satisfying Logic Simulation, Proceedings of the IEEE Computer Society Annual Symposium on VLSI, p.151, April 25-26, 2002