SAT based property checking

Question 1

Define the SAT problem.

Answer 1

Find a set of assignments for the variables of a formula
f in CNF such that f = 1
or
prove that no such set exists

Question 2

The basic procedure of most modern SAT solvers

Answer 2

Assign step by step values 0 or 1 to the variables in the CNF until all clauses are satisfied (evaluate to 1). If a clause evaluates to 0 it is called violated and backtracks are performed based on a decision tree.

Question 3

Which representation of circuits is used in SAT solvers?

Answer 3

CNF

Question 4

How can the SAT solver be optimized?

Answer 4

…

Question 5

How is SAT-based property checking modelled?

Answer 5

Compute CNF for transition relation of iterative model: “unrolled transition relation”, initial state and property.

Question 6

Why is Interval Property Checking more versitile?

Answer 6

• can prove properties of type: if certain assumptions hold for t≤ti≤t + k
then a certain commitment will hold for t≤tj≤t + k

e.g., if a request is sent to some resource at time t, then an acknowledge will arrive at the latest at time t+k

• can handle much larger blocks than symbolic model
checking.

Question 7

Main problem of Bounded model checking.

Answer 7

• bounded model checking only proves property for k clock cycles, 0≤t≤k
• property is proved for all reachable states if k is chosen large enough, such that k ≥number of cycles to reach every state in the machine at least once (sequential depth of automaton). -> Not always practical

Question 8

What is Interval Property checking (IPC)?

Answer 8

Is a bounded model checking which uses iterative circuit array from i = t to i = t+k.
It means that we prove safety properties by constructing a certain combinational circuit and solve a SAT problem for it.

Question 9

Definition of invariants.

Answer 9

A set of states W in a finite state machine M is called invariant if W contains all states being reachable from W
.

Question 10

How symbolic representation works for model checking.

Answer 10

Using boolean representation of states make the representation of states easier and CNF based SAT-solving easier. Calculate characteristic equation, transition function and property function.

Question 11

Which model is used in bounded model checking?

Answer 11

Iterative circuit model