Generating a test sequence using a satisfiability technique

Details Generating a test sequence using a satisfiability technique Generating a test sequence using a satisfiability technique

2006-07-11

2006-07-11

Ton, David (Department: 2138)

Error detection/correction and fault detection/recovery

Pulse or data error handling

Digital logic testing

C714S741000

Reexamination Certificate

active

07076712

ABSTRACT:
Generating a test sequence includes receiving a circuit representation describing a circuit, and a fault associated with the circuit representation. A miter circuit model associated with a good circuit model and a faulty circuit model is established according to the circuit representation. A satisfiability problem corresponding to the fault as associated with the miter circuit model is also established. Whether the satisfiability problem is satisfiable is determined. If the satisfiability problem is satisfiable, a test sequence is generated for the fault as associated with the miter circuit model.

REFERENCES:
patent: 5345393 (1994-09-01), Ueda
patent: 5410678 (1995-04-01), Takasaki
patent: 5884065 (1999-03-01), Takasaki
patent: 6018813 (2000-01-01), Chakradhar et al.
patent: 6026222 (2000-02-01), Gupta et al.
Abdulla, et al., “Symbolic Reachability Analysis Based on SAT-Solvers,” Uppsala University and Prover Technology, Sweden, Chalmers University of Technology, Sweden (15 pages), unknown.
Agrawal, et al., “Combinational ATPG Theorems for Identifying Untestable Faults in Sequential Circuits, ” © 1995 IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 14, No. 9, Sep. 1995 (pp. 1155-1160).
Clarke, et al., “Bounded Model Checking Using Satisfiability Solving,” Computer Science Dept., CMU, PA: Inst. of Computer Systems, Zürich, BOPS, Inc., TX; Synopsys, Inc., CA, Published in Formal Methods in System Design, vol. 19, Issue 1.(20 pages), Jul. 2001.
Boppana, et al., “Model Checking Based on Sequential ATPG,” Fujitsu Labs. of America, Inc., CA (13 pages), unknown.
Goldberg, et al., “BerkMin: a Fast and Robust Sat-Solver,” Cadence Berkeley Labs, USA; Academy of Sciences (Belarus) (8 pages), unknown.
Hsiao, et al., “Alternating Strategies for Sequential Circuit ATPG,” Univ. of Illinois,European Design&Test Conference, Mar. 1996 (pp. 368-374).
Hsiao, et al., “Sequential Circuit Test Generation Using Dynamic State Traversal,” Univ. of Illinois,European Design&Test Conference, Mar. 1997 (pp. 22-28).
Larrabee, “Test Pattern Generation Using Boolean Satisfiability,” © 1992 IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 11, No. 1, Jan. 1992 (pp. 4-15).
Marques-Silva, et al., “GRASP: A Search Alogorithm for Propositional Satisfiability,” © 1999 IEEE Transactions on Computers, vol. 48, No. 5, May 1999 (pp. 506-521).
Moskewicz, et al., “Chaff: Engineering an Efficient SAT Solver, ” Department of EECS, UC Berkeley, Department of EECS, MIT, Department of Elec. Eng., Princeton University (6 pages), unknown.
Mukherjee, et al., “An Efficient Filter-Based Approach for Combinational Verification,” © 1999IEEE, vol. 18, No. 11, Nov. 1999 (pp. 1542-1557).
Niermann, et al., “HITEC: A Test Generation Package for Sequential Circuits,” © 1991IEEE, European Design Automation Conference (EDAC-91) Amsterdam, The Netherlands (pp. 214-218), Feb.-Mar. 1991.
Goldberg, et al., “Using SAT for Combinational Equivalence Checking,” Cadence, Synopsys and Fujitsu (8 pages), unknown.
Reddy, et al., “New Procedures for Identifying Undetectable and Redundant Faults in Synchronous Sequential Circuits, ” (NSF Grant No. MIP-9387581 and NSF Grant No. MIP-9725053) (7 pages), unknown.
Rudnick, et al., “Combining Deterministic and Genetic Approaches for Sequential Circuit Test Generation,” © 1995ACM0-89791-756-1/95/0006 (6 pages), 1995.
Sheeran, et al., “Checking Safety properties Using Induction and a SAT-Solver,” Prover Tech. AB, Sweden; Chalmers Univ. of Tech., Sweden; Xilinx Inc., CA (18 pages), unknown.
Sheng, et al., “Effective Safety Property Checking Using Simulation-Based Sequential ATPG,” DAC 2002, New Orleans, Louisiana, ACM 1-58113-461-4/02/006 (6 pages), 2002.
Shtrichman, “Tuning SAT Checkers for Bounded Model Checking,” CAV 2000 The Weizmann Institute of Science, Israel; and IBM Haifa Research Lab. (15 pages), 2000.
Shtrichman, “Pruning Techniques for the SAT-Based Bounded Model Checking Problem,” CHARME '01 The Weizmann Institute of Science, Israel; and IBM Haifa Research Lab. (13 pages), 2001.
Stephan, et al., “Combinational Test Generation Using Satisfiability,” © 1996 IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 15, No. 9, Sep. 1996 (pp. 1167-1176).
Zhang, “SATO: An Efficient Propositional Prover,” NSF Grants CCR-9504205 and CCR-9357851 (4 pages), unknown.
Prasad, et al., “An Efficient and Scalable Methodology for Latch Correspondence Using Hybrid Methods&Incremental Reasoning Implemented on a General Purpose Combinational Equivalence Checker,” Mar. 31, 2002, Fujitsu Labs of America and Univ. of British Columbia (9 pages).
Guo, et al., “PROPTEST: A Property Based Test Pattern Generator for Sequential Circutis Using Test Compaction*,” DAC '99, New Orleans, Louisiana, (c) 1999 ACM 1-58113-109-7/99/06, (7 pages).
Konuk, et al., “Explorations of Sequential ATPG Using Boolean Satisfiability,” Board of Studies in Computer Engineering, University of California, Santa Cruz, Santa Cruz, California (6 pages), unknown.
Lin, et al., “Techniques for Improving the Efficiency of Sequential Circuit Test Generation,” 0-7803-5832-X/99 © IEEE, 5 pages.
Wang, et a., “Conflict Driven Techniques for Improving Deterministic Test Pattern Generation,” 0-7803-7607-2/02 © 2002 IEEE (7 pages).
Pomeranz, et al., “Vector Restoration Based Static Compaction of Test Sequences for Synchronous Sequential Circuits,” Proceedings of the 1997 International Conference on Computer Design (ICCD '97), 0-8186-8206-X/97, © 1997, IEEE, (pp. 360-365).
Guo, et al., “Procedures for Static Compaction of Test Sequences for Synchronous Sequential Circuits Based on Vector Restoration,” Electrical and Computer Engineering Department, Unversity of Iowa, Iowa City, Iowa, (5 pages), unknown.
Hsiao, et al., “Fast Static Compaction Algorithms for Sequential Circuit Test Vectors,” IEEE Transactions on Computers, vol. 48, No. 3, 0018-9340/99 © 1999 IEEE, (pp. 311-322), Mar. 1999.
Hsiao, et al., “State Relaxation Based Subsequence Removal for Fast Static Compaction in Sequential Circuits,” Department of Electrical and Computer Engineering, Rutgers University, Piscataway, New Jersey, Computer & Communications Research Lab. NEC USA, Princeton, NJ (6 pages). unknown.
Pomeranz, et al., “On Static Compaction of Test Sequences for Synchronous Sequential Circuits,” 33rdDesign Automation Conference, DAC 96-06/96, Las Vegas, NV, USA, © 1996 ACM, Inc. 0-89791-833-9/96/0006 (6 pages).
Niermann, et al., “Test Compaction for Sequential Circuits,” Short Papers, IEEE Transactions On Computer-Aided Design, vol. 11, No. 2, 0278-0070/92 © 1992 IEEE, (pp. 260-267), Feb. 1992.
Prasad, et al., “Improving Sequential ATPG Using SAT Methods,” Fujitsu Laboratories of America, Sunnyvale, CA, Bradley Department of Electrical and Computer Engineering, Virginia Tech, Blacksburg, VA, (6 pages), presented Jun. 2, 2002.

Affiliated with

Also associated with

Rating

Generating a test sequence using a satisfiability technique does not yet have a rating. At this time, there are no reviews or comments for this patent.

If you have personal experience with Generating a test sequence using a satisfiability technique, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Generating a test sequence using a satisfiability technique will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFUS-PAI-O-3567566