Directed falsification of a circuit

Details Directed falsification of a circuit Directed falsification of a circuit

2004-11-22

2008-11-11

Lamarre, Guy J (Department: 2112)

Error detection/correction and fault detection/recovery

Pulse or data error handling

Digital data error correction

C714S030000, C716S030000, C716S030000, C716S030000

Reexamination Certificate

active

07451375

ABSTRACT:
In one embodiment, a method for directed falsification of a circuit includes selecting a partition of a state space of the circuit. The partition includes only a portion of the state space and is selected according to one or more results of one or more preimage calculations indicating one or more characteristics of the circuit. The characteristics indicate a likelihood that the partition includes one or more errors in the circuit. The method further includes, using one or more partitioned ordered binary decision diagrams (POBDDs), analyzing the partition according to a falsification-based forward-reachability technique to determine whether the partition includes one or more errors in the circuit.

REFERENCES:
patent: 6212669 (2001-04-01), Jain
patent: 7281225 (2007-10-01), Jain et al.
patent: 2004/0093571 (2004-05-01), Jain et al.
Biere et al., “Symbolic Model Checking without BDDs,” Lecture Notes in Computer Science, 1579:193-207, 18 pages, Jan. 4, 1999.
Bloem et al., “Symbolic Guided Search for CTL Model Checking,” In DAC, 6 pages, 2000.
Boppana et al., “Model Checking Based on Sequential ATPG. In ICCAD,” pp. 418-430. Springer-Verlag, 11th International Conference, Jul. 6-10, 1999.
Bryant, “Graph-based Algorithms for Boolean Function Manipulation,” IEEE Transactions Computers, C-35-8, 677-691, 29 pages, 1986.
Clarke et al., “Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic,” In Proc. IBM Workshop on Logics of Programs, vol. 131 of LNCS, pp. 52-71, Springer-Verlag, 1981.
Coudert et al. “Verification of Sequential Machines Based on Symbolic Execution,” In Proc. of the Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France, 1989.
Garavel et al., “Parallel State Space Construction for Model-Checking,” In SPIN workshop on model checking of software, pp. 217-234, Springer-Verlag New York, Inc., 2001.
Heyman et al., “Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits,” In CAV, 19 pages, May 30, 2000.
Jain, “On Analysis of Boolean Functions,” Ph.D Dissertation, Dept. of Electrical and Computer Engineering, The University of Texas at Austin, 1993.
McMillan, “Symbolic Model Checking,” Kluwer Academic Publishers, 1993.
Narayan et al., “Reachability Analysis Using Partitioned-ROBDDs,” In Proc. of the Intl. Conf. on Computer-Aided Design, pp. 383-393, 1997.
Stern et al., “Parallelizing the Murphy Verifier,” in CAV, pp. 1-12, 1997.
Stornetta et al., Implementation of an Efficient Parallel BDD Package,: In DAC, pp. 641-644, 50 pags, 1996.
Yang et al., “Parallel Breadth-First BDD Construction,” In symposium on Principles and practice of parallel programming, pp. 145-146. ACM Press, 12 pages, 1997.
Cabodi et al., “Symbolic Exploration of Large Circuits with Enhanced Forward/Backward Traversals,” In EuroDAC, 6 pages, 1994.
Cabodi et al., “Mixing Forward and Backward Traversals in Guided-Prioritized BDD-Based Verification,” In CAV, pp. 471-484, 2002.
Chauhan et. al., “Non-Linear Quantification Scheduling in Image Computation,” In ICCAD, 6 pages, 2001.
Clarke et al., “Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic,” vol. 131 of LNCS, Unknown.
Govindaraju et al., “Verification by Approximate Forward and Backward Reachability,” In ICCAD, 5 pages, 1998.
Iyer et al., “Improved Symbolic Verification Using Partitioning Techniques,” In Proc. of CHAR ME, vol. 2860 of Lecture Notes in Computer Science, pp. 411-424, 2003.
Jain et. al., “Functional Partitioning for Verification and Related Problems,” Brown/MIT VLSI Conference, 1992 [II] K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
Moon et al., “To Split or to Conjoin: The Question in Image Computation,” In DAC, 6 pages, 2000.
Somenzi., “UDD: CU Decision Diagram Package,” ftp://vlsi.colorado.edulpub, 2001.
VIS. Verilog Benchmarks http://vlsi.colorado.edul- vis/, Unknown.
Wang et al., The Compositional Far Side of Image Computation. In ICCAD, 2003.

Affiliated with

Also associated with

Rating

Directed falsification of a circuit does not yet have a rating. At this time, there are no reviews or comments for this patent.

If you have personal experience with Directed falsification of a circuit, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Directed falsification of a circuit will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFUS-PAI-O-4043634