Novel verification framework combining structural and OBDD methods in a synthesis environment

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Novel verification framework combining structural and OBDD methods in a synthesis environment

Full text

Pdf (188 KB)

Source

Annual ACM IEEE Design Automation Conference archive
Proceedings of the 32nd annual ACM/IEEE Design Automation Conference table of contents

San Francisco, California, United States

Pages: 414 - 419

Year of Publication: 1995

ISBN:0-89791-725-1

Authors

Subdodh M. Reddy	Unisys Corporation and Laboratory for Digital and Computer Systems Research, Department of Computer Science, Texas A&M University, College Station, Texas
Wolfgang Kunz	Fault Tolerant, Computing Laboratory, Max-Planck-Society, University of Potsdam, 14415 Potsdam, Germany
Dhiraj K. Pradhan	Laboratory for Digital and Computer Systems Research, Department of Computer Science, Texas A&M University, College Station, Texas

Sponsors

EDAC : Electronic Design Automation Consortium
SIGDA: ACM Special Interest Group on Design Automation

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 3, Downloads (12 Months): 19, Citation Count: 18

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/217474.328705 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	E. J. Aas, K. Klingsheim, and T. Steen. Quantifying design quality. In Proceedings of EURO ASIC, pages 172-177, 1992.
	2	C. L. Berman and L. H. Trevillyan. Functional comparison of logic designs for vlsi circuits. In Intl. Test Conference, pages 456-459, 1989.
	3	Karl S. Brace , Richard L. Rudell , Randal E. Bryant, Efficient implementation of a BDD package, Proceedings of the 27th ACM/IEEE conference on Design automation, p.40-45, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.123222]
	4	Daniel Brand, Verification of large synthesized designs, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.534-537, November 07-11, 1993, Santa Clara, California, United States
	5	F. Brglez and H. Fujiwara. A neutral netlist of 10 combinational benchmark circuits and a target translator in fortran. In Special Session on the 1985 IEEE Intl. Symposium on Circuits ~ Systems, 1985.
	6	Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
	7	J. Jain et al. Indexed bdds: Algorithmic advances in techniques to represent to represent and verify boolean functions. Technical Report UT-CERC-TR- JAA-93-02, Comp. Eng. Research Center, 1993.
	8	R. Drechsler , A. Sarabi , M. Theobald , B. Becker , M. A. Perkowski, Efficient representation and manipulation of switching functions based on ordered Kronecker functional decision diagrams, Proceedings of the 31st annual conference on Design automation, p.415-419, June 06-10, 1994, San Diego, California, United States [doi>10.1145/196244.196444]
	9	Thomas R. Shiple , Ramin Hojati , Alberto L. Sangiovanni-Vincentelli , Robert K. Brayton, Heuristic minimization of BDDs using don't cares, Proceedings of the 31st annual conference on Design automation, p.225-231, June 06-10, 1994, San Diego, California, United States [doi>10.1145/196244.196360]
	10	H. Fujiwara and T. Shimono. On the acceleration of test generation algorithms. In Intl. Symposium on Fault-tolerant Computing, pages 98-105, 1983.
	11	Wolfgang Kunz, HANNIBAL: an efficient tool for logic verification based on recursive learning, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.538-543, November 07-11, 1993, Santa Clara, California, United States
	12	Wolfgang Kunz , Prem R. Menon, Multi-level logic optimization by implication analysis, Proceedings of the 1994 IEEE/ACM international conference on Computer-aided design, p.6-13, November 06-10, 1994, San Jose, California, United States
	13	W. Kunz and D. K. Pradhan. Recursive learning: A new implication technique for efficient solutions to CAD problems - test, verification, and optimization. In IEEE Trans. on Computer-aided Design of Integrated Circuits and Systems, Vol. 13, No. 9, pages 1143-1157, September, 1994.
	14	S. Malik, A. Wang, R. Brayton, and A. Sangiovanni- Vincentelli. Logic verification using binary decision diagrams in a logic synthesis environment. In Intl. Conference on Computer-aided Design, pages 6-9, Nov. 1988.
	15	M. R. Mercer , R. Kapur , D. E. Ross, Functional approaches to generating orderings for efficient symbolic representations, Proceedings of the 29th ACM/IEEE conference on Design automation, p.624-627, June 08-12, 1992, Anaheim, California, United States
	16	Richard Rudell, Dynamic variable ordering for ordered binary decision diagrams, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.42-47, November 07-11, 1993, Santa Clara, California, United States
	17	Amelia Shen , Srinivas Devadas , Abhijit Ghosh, Probabilistic construction and manipulation of free Boolean diagrams, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.544-583, November 07-11, 1993, Santa Clara, California, United States
	18	D. Stoffel, W. Kunz, S. Gerber. Multi-level Logic Synthesis by And-Or-Graphs. Technical Report, MPI-I-95-602, Max-Planck Fault-Tolerant Computing Group, 1995.
	19	Gert-Jan Tromp , A. J. van de Goor, Logic Synthesis of 100-percent Testable Logic Networks, Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, p.428-431, October 14-16, 1991
	20	R. Wei and A. L. Sangiovanni-Vincentelli. Proteus: A logic verification system for combinational circuits. In Intl. Test Conference, 1986.

CITED BY 18

	Rajarshi Mukherjee , Jawahar Jain , Koichiro Takayama , Masahiro Fujita, Automatic partitioning for efficient combinatorial verification, Proceedings of the 2000 conference on Asia South Pacific design automation, p.67-72, January 2000, Yokohama, Japan
	Amit Narayan , Jawahar Jain , M. Fujita , A. Sangiovanni-Vincentelli, Partitioned ROBDDs—a compact, canonical and efficiently manipulable representation for Boolean functions, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.547-554, November 10-14, 1996, San Jose, California, United States
	Andreas Kuehlmann , Malay K. Ganai , Viresh Paruthi, Circuit-based Boolean Reasoning, Proceedings of the 38th conference on Design automation, p.232-237, June 2001, Las Vegas, Nevada, United States
	Rajarshi Mukherjee , Jawahar Jain , Koichiro Takayama , Jacob A. Abraham , Donald S. Fussell , Masahiro Fujita, Efficient Combinational Verification Using Overlapping Local BDDs and a Hash Table, Formal Methods in System Design, v.21 n.1, p.95-101, July 2002
	Andreas Kuehlmann , Cornelis A. J. van Eijk, Combinational and sequential equivalence checking, Logic Synthesis and Verification, Kluwer Academic Publishers, Norwell, MA, 2001
	Demos Anastasakis , Robert Damiano , Hi-Keung Tony Ma , Ted Stanion, A practical and efficient method for compare-point matching, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA
	Andreas Kuehlmann , Florian Krohm, Equivalence checking using cuts and heaps, Proceedings of the 34th annual conference on Design automation, p.263-268, June 09-13, 1997, Anaheim, California, United States
	Yusuke Matsunaga, An efficient equivalence checker for combinational circuits, Proceedings of the 33rd annual conference on Design automation, p.629-634, June 03-07, 1996, Las Vegas, Nevada, United States
	S. Reda , A. Salem, Combinational equivalence checking using Boolean satisfiability and binary decision diagrams, Proceedings of the conference on Design, automation and test in Europe, p.122-126, March 2001, Munich, Germany
	Shi-Yu Huang , Kuang-Chien Chen , Kwang-Ting Cheng, Error correction based on verification techniques, Proceedings of the 33rd annual conference on Design automation, p.258-261, June 03-07, 1996, Las Vegas, Nevada, United States
	Gagan Hasteer , Anmol Mathur , Prithviraj Banerjee, An efficient assertion checker for combinational properties, Proceedings of the 34th annual conference on Design automation, p.734-739, June 09-13, 1997, Anaheim, California, United States
	Demosthenes Anastasakis , Lisa McIlwain , Slawomir Pilarski, Efficient equivalence checking with partitions and hierarchical cut-points, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA
	Shi-Yu Huang , Kwang-Ting Cheng , Kuang-Chien Chen , Forrest Brewer , Chung-Yang Huang, AQUILA: An Equivalence Checking System for Large Sequential Designs, IEEE Transactions on Computers, v.49 n.5, p.443-464, May 2000
	Ronald P. Lajaunie , Michael S. Hsiao, An effective and efficient ATPG-based combinational equivalence checker, Proceedings of the 15th ACM Great Lakes symposium on VLSI, April 17-19, 2005, Chicago, Illinois, USA
	E. Dubrova , M. Teslenko , A. Martinelli, Kauffman networks: analysis and applications, Proceedings of the 2005 IEEE/ACM International conference on Computer-aided design, p.479-484, November 06-10, 2005, San Jose, CA
	Rajarshi Mukherjee , Jawahar Jain , Koichiro Takayama , Masahiro Fujita , Jacob A. Abraham , Donald S. Fussell, An efficient filter-based approach for combinational verification, Proceedings of the conference on Design, automation and test in Europe, p.31-es, January 1999, Munich, Germany
	João Marques-Silva , Thomas Glass, Combinational equivalence checking using satisfiability and recursive learning, Proceedings of the conference on Design, automation and test in Europe, p.33-es, January 1999, Munich, Germany
	Elena Dubrova , Maxim Teslenko , Hannu Tenhunen, On analysis and synthesis of (n, k)-non-linear feedback shift registers, Proceedings of the conference on Design, automation and test in Europe, March 10-14, 2008, Munich, Germany