Goal: Test for stuck-at faults by generating input patterns that creates output different from the expected output.
D-calculus: 0,1,D,!D,X
1. Justification
2. Pick a variable (decision making)
3. set = 0 / 1
4. implication (reasoning)
5. conflict, not done, or found the test.
SAT solver implementation
- learn thru SCC
- non-local clauses
No comments:
Post a Comment