System for combinational equivalence checking

Details System for combinational equivalence checking System for combinational equivalence checking

1997-12-23

2000-02-15

Teska, Kevin

39550004, 39550019, G06F 1750

Patent

active

060262222

ABSTRACT:
A computer system, computer program product, and method for solving a combinational logic verification problem with respect to two combinational circuits includes Boolean SAT checking integrated with binary decision diagrams (BDD) use. A fanout partition of a miter circuit formed from the two combinational circuits is reduced to BDD form, while the fanin partition is represented by SAT clauses. As SAT solutions are evaluated, variables in the cutset between the fanout and fanin partitions are assigned values. In a preferred embodiment, each assignment to a cutset variable is checked against an onset of the BDD prior to continuing with SAT solution seeking.

REFERENCES:
patent: 5649165 (1997-07-01), Jain et al.
patent: 5754454 (1998-05-01), Pixley et al.
patent: 5909374 (1999-06-01), Matsunaga
Ashar et al., "Boolean satisfiability and equivalence checking using general binary decision diagrams", Proceedings, 1991 IEEE International Conference on Computer Design: VLSI in Computers and Processors, pp. 259-264, Oct. 14, 1991.
J. P. Billon, et al. "Original concepts of PRIAM, an industrial tool for efficient formal verification Of combinational circuits." In Fusion of Hardware Design and Verification, pp. 487-501, G. J. Milne, ed. North-Holland, Amsterdam, 1988, Jul. 4,1988.
C. Berman et al. Functional comparison of logic design for VLSI circuits. In Proceedings of the IEEE International Conference on Computer-Aided Design, pp. 456-459. EKE Computer Society Press, Los Alamitos, CA, Nov. 1989.
D. Brand. Verification of large synthesized designs. In Proceedings of the IEEE International Conference on Computer-Aided Design, pp. 534-537, Nov. 1993.
F. Brglez et al. Combinational Profiles of Sequential Benchmark Circuits. In Proceedings of the International Symposium on Circuits and Systems, Portland, Oregon, May 1989.
R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677-691, Aug. 1986.
R. E. Bryant. On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication. IEEE Transactions on Computers, 40(2):205-213, Feb. 1991.
E. Cerny et al. Tautology checking using cross-controllability and cross-observability relations. In Proceedings of the IEEE International Conference on Computer-Aided Design, pp. 34-37, IEEE Computer Society Press Los Alamitos, CA, Nov. 1990.
S. Chakradhar et al. A transitive closure algorithm for test generation. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 12(7):1015-1028, Jul. 1993.
M. Fujita et al. Evaluation and improvements of a Boolean comparison program based on Binary Decision Diagrams. In Proceedings of the IEEE International Conference on Computer-Aided Design, pp. 2-5. EKE Computer Society Press, Los Alamitos, CA, 1988.
H. Fujiwara. Fan: A fanout-oriented test pattern generation algorithm. In Proceedings of the 1985 International Symposium on Circuits and Systems, pp. 671-674, Jul. 1985.
P. Goel. An implicit enumeration algorithm to generate tests for combinational logic circuits. In IEEE Transactions on Computers, vol. C-30, pp. 215-222, Mar. 1991.
J. Jain et al. Advanced verification techniques based on learning. In Proceedings of the 32nd ACM/IEEE Design Automation Conference, pp. 420-426. EKE Computer Society Press, Los Alamitos, CA, Jun. 1995.
A. Kuehlmann et al. Equivalence checking using cuts and heaps. In Proceedings of the 34th ACM/IEEE Design Automation Conference, pp. 263-268. EKE Computer Society Press, Los Alamitos, CA, Jun. 1997.
W. Kunz et al. Recursive learning: A new implication technique for efficient solutions to cad problems--test, verifications and optimization.
T. Larrabee. Test pattern generation using boolean satisfiability. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 11(1):4-15, Jan. 1992.
Madre et al., "Autometing the Diagnosis and the Rectification of Design Errors with PRIAM", IEEE, pp. 30-33, Jan. 1989.
S. Malik et al. Logic verification using Binary Decision Diagrams in a logic synthesis environment. In Proceedings of the IEEE International Conference on Computer-Aided Design, pp. 6-9. EKE Computer Society Press, Los Alamitos, CA, 1988.
Y. Matsunaga. An efficient equivalence checker for combinational circuits. In Proceedings of the ACM/IEEE Design Automation Conference, pp. 629-634. IEEE Computer Society Press, Los Alamitos, CA, Jun. 1996.
D. Pradhan et al. Verilat: Verification using logic augmentation and transformations. In Proceedings of the IEEE International Conference on Computer-Aided Design, pp. 88-95. IEEE Computer Society Press, Los Alamitos, CA, Nov. 1996.
M. Schulz et al. Socrates: A highly efficient atpg system. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 7(1): 126-137, Jan. 1988.
E. M. Sentovich et al. Sequential circuit design using synthesis and optimization. In Proceedings of the IEEE International Conference on Computer Design, 1992.
J. P. M. Silva et al. Grasp: A new search algorithm for satisfiability. In Proceedings of the IEEE International Conference on Computer-Aided Design, pp. 220-227. IEEE Computer Society Press, Los Alamitos, CA, Nov. 1996.
Long. BDD Package. Unpublished. School of Computer Science, Carnegie Mellon University, Pittsburgh Prior Art 1993, Jun. 11, 1993.
Kunz et al. A Novel Framework for Logic Verification in a Synthesis Environment. In IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 15, No. 1, Jan. 1996.
P. Stephan et al. Combinational test generation using satisfiability. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 15(9): 1167-1176, Sep. 1996.

Affiliated with

Also associated with

Rating

System for combinational equivalence checking does not yet have a rating. At this time, there are no reviews or comments for this patent.

If you have personal experience with System for combinational equivalence checking, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and System for combinational equivalence checking will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFUS-PAI-O-1912619