Model Checking

Amit Goel
amitgoel@[Link]

(c) Copyright Apple 2017

Verification complexity
Exponential

Total number of states in an SoC ( 2???????? )

Simulation
States

Emulation
FPGA’s
Formal Verification

Total number of particles in the universe ( 2266 )

2017
Time

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

 Model Checking
Introduction

• Does a given state machine M satisfy a property P?

• Check for all possible behaviors of the state machine
• If not, produce a trace showing the violation

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

Properties

• Safety properties: something bad will never happen

• e.g. we should never write to a full buffer

• Liveness properties: something good will eventually happen

• e.g. all requests to an arbiter will eventually be granted

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

Model Checking

Graph Reachability
Symbolic Model Checking
Proof by Induction

Model Checking

Graph Reachability
Symbolic Model Checking
Proof by Induction
 State Machines

• A state machine M = (S, I, T)

• S is a set of states
• I ⊆ S is the set of initial states
• T ⊆ S × S is a transition relation

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

State Machines
Example

S = {s0, s1, s2, s3}

I = {s2}

T = {(s0,s0), (s0,s1), (s0,s2), (s1,s0), (s1,s1), (s2,s0), (s2,s2), (s3,s0)}

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

 State Machines
Example

S = {s0, s1, s2, s3}

I = {s2} s1 s3

T = {(s0,s0), (s0,s1), (s0,s2), (s1,s0), (s1,s1), (s2,s0), (s2,s2), (s3,s0)}

s0 s2

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

Checking Safety Properties

Examples
Bad = {s1, s3} Bad = {s3}

s1 s3 s1 s3

s0 s2 s0 s2

Can we reach a bad state from an initial state?

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020
 Checking Safety Properties
Examples
Bad = {s1, s3} Bad = {s3}

s1 s3 s1 s3

s0 s2 s0 s2

Yes: Path s2, s0, s1

Can we reach a bad state from an initial state?

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

Checking Safety Properties

Examples
Bad = {s1, s3} Bad = {s3}

s1 s3 s1 s3

s0 s2 s0 s2

Yes: Path s2, s0, s1 No path from s2 to s3

Can we reach a bad state from an initial state?

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020
 Explicit-state Model Checking

CHECK (M, Bad) // M = (S, I, T), Bad ⊆S

if (∃s ∈ I. s ∈ Bad) // Is there a bad initial state?
return Fail

Seen ⟵ I // Mark the Initial states as Seen

while (∃(s,s’) ∈ T. s ∈ Seen and s’ ∉ Seen) // Find a reachable unseen state s’?
if (s’ ∈ Bad) // Is s’ a bad state?
return Fail
Seen ⟵ Seen ⋃ {s’} // Mark s’ as seen
end
return Pass // Cannot reach a bad state

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

Checking Liveness properties Good = {s0, s1, s2}

Example

• Infinite loops (Deadlocks and Livelocks) in state machines s4

S = {s0, s1, s2, s3, s4}

s1 s3
I = {s2}

T = {(s0,s0), (s0,s1), (s0,s2), (s1,s0), (s1,s1), (s1,s4), (s2,s0), (s2,s2), (s3,s0), (s4,s4)}

s0 s2

Can you reach a state where you cannot exit from and return to any good state?
UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020
 State-space Explosion
Example

• The number of reachable states in systems is often too large to enumerate

• Consider a system which orders n things
• e.g. Arbitration, Out-of-order processing, …
• Number of orderings is given by n!

n n!

4 24

8 40,320

16 20,922,789,888,000

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

Model Checking

Graph Reachability
Symbolic Model Checking
Proof by Induction
 Symbolic Representation of States

• States can be encoded using Boolean variables V

State Encoding with V= {x,y}

s0 00

s1 01

s2 10

s3 11

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

Symbolic Representation of States

• States can be encoded using Boolean variables V

• State sets can be represented by Boolean functions over V

Boolean Function State Set

true {00, 01, 10, 11}

false {}

x∙¬y {10}

x∙y {11}

y {01, 11}

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

 Symbolic Representation of States

• States can be encoded using Boolean variables V

• State sets can be represented by Boolean functions over V
• State relations can be encoded by Boolean functions over two sets of variables, V and V’
• V for current state
• V’ for next state

Boolean Function Relation

¬x∙¬y∙x’∙¬y’ {00→10}

¬x∙¬y∙(¬x’ ∣ ¬y’) {00→00, 00→10, 00→01}

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

Symbolic Encoding for FSMs

Example
I = x∙¬y
T = ¬x∙¬x’ ∣ ¬y∙¬y’ ∣ ¬x’∙¬y’
Bad = y Bad = x∙y

01 11 01 11

00 10 00 10

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

 Symbolic Representation for Circuits

module toy (input clock, input reset,

input cx, input cy,
output x, output y);

logic x; logic y;
State Variables:
V = {x, y}
always @(posedge clock)
if (reset) begin
Initial (reset) State:
x <= 1'b1;
I(V) = x∙¬y
y <= 1'b0;
end else begin
x <= !y && cx; Transition Functions:
y <= !x && !cx && cy; x’ = ¬y∙cx
end y’ = ¬x∙¬cx∙cy
// Mutex property
assert property (!(x && y)); Property:
endmodule Bad = x∙y
UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

Synthesized Circuit

module toy (input clock, input reset,

input cx, input cy,
output x, output y);

x
logic x; logic y;
State Variables: NOT
1 AND
V = {x, y}
always @(posedge clock)
reset
if (reset) begin
Initial (reset) State: cy
x <= 1'b1;
I(V) = x∙¬y NOT
AND

y <= 1'b0;
end else begin cx
x <= !y && cx; Transition Functions:
y <= !x && !cx && cy; x’ = ¬y∙cx
y’ = ¬x∙¬cx∙cy y AND
end NOT
0
// Mutex property
reset
assert property (!(x && y)); Property:
endmodule Bad = x∙y
UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020
 Transition Function and Transition Relation
Example

• Transition function: 1
x’ = ¬x ∙ cx
• Transition relation (with input variables): 0,1 1
̃T(x, cx, x’) = (x’ ⟷ ¬x ∙ cx)

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

Transition Function and Transition Relation

Example

• Transition function: 1
x’ = ¬x ∙ cx
• Transition relation (with input variables):
̃T(x, cx, x’) = (x’ ⟷ ¬x ∙ cx)
• Transition Relation (without input variables):
0
T(x, x’) = ∃cx.(x’ ⟷ ¬x ∙ cx)
= (¬x ∣ ¬x’)

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

 Transition Functions and Transition Relation
Example

• Transition function:
x’ = ¬y∙cx
y’ = ¬x∙¬cx∙cy
• Transition relation (with input variables):
̃T(V, cx, cy, V’) = (x’ ⟷ ¬y ∙ cx) ∧ (y’ ⟷ ¬x∙¬cx∙cy)
• Transition Relation:
T(V, V’) = ∃cx, cy. ̃T(V, cx, cy, V’)
= (¬x∙¬x’ ∣ ¬y∙¬y’ ∣ ¬x’∙¬y’)

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

Symbolic Representation V = {x,y}

Verilog, Circuit and FSM I(V) = x∙¬y
T(V,V’) = ¬x∙¬x’ ∣ ¬y∙¬y’ ∣ ¬x’∙¬y’
Bad(V) = x∙y
module toy (input clock, input reset,
input cx, input cy,
output x, output y);

x
NOT
logic x; logic y; 1 AND
01 11
always @(posedge clock)
reset
if (reset) begin
cy
x <= 1'b1; AND
NOT
y <= 1'b0;
end else begin cx
x <= !y && cx;
y <= !x && !cx && cy; 00 10
y AND
end NOT
0
// Mutex property
reset
assert property (!(x && y));
endmodule

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

 Symbolic Set Operations

Symbolic Expression Boolean Formula Corresponding Set Set Expression

true {00, 01,10,11} S

A x {10,11} SA

B y {01,11} SB

A∨B x∣y {01,10,11} SA ∪ SB

A∧B x∙y {11} SA ∩ SB

¬A ¬x {00,01} S ∖ SA

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

Image Computation

• Given states R(V) and transition relation T(V,V’)

• Let F(V’)= ∃V. R(V) ∧ T(V,V’),
• Let F(V) be obtained by renaming V’ to V in F(V’)
• Then F(V) is the set of all states reachable in one step from states in R

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

 Image Computation

• Given states R(V) and transition relation T(V,V’)

• Let F(V’)= ∃V. R(V) ∧ T(V,V’),

• Then F(V) is the set of all states reachable in one step from states in R

R(V) = I(V) = x∙¬y 01 11

T(V,V’) = ¬x∙¬x’ ∣ ¬y∙¬y’ ∣ ¬x’∙¬y’

F(V’) = ¬y’
F(V) = ¬y 00 10

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

Image Computation

• Given states R(V) and transition relation T(V,V’)

• Let F(V’)= ∃V. R(V) ∧ T(V,V’),
• Then F(V) is the set of all states reachable in one step from states in R

R(V) = ¬y 01 11

T(V,V’) = ¬x∙¬x’ ∣ ¬y∙¬y’ ∣ ¬x’∙¬y’

F(V) = ¬x ∣ ¬y

00 10

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

 Image Computation

• Given states R(V) and transition relation T(V,V’)

• Let F(V’)= ∃V. R(V) ∧ T(V,V’),

• Then F(V) is the set of all states reachable in one step from states in R

• We write Img(R,T) for the above image computation

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

Symbolic Model Checking

Forward Reachability Algorithm

CHECK (M, Bad) // M = (S, I, T), Bad ⊆S

Prev ⟵ false // No states have been seen as yet
Seen ⟵ I // Mark Initial States as Seen
while (Seen ≠ Prev) // Have we seen any new states?
if (Seen ∧ Bad ≠false) // Have we seen a bad state?
return Fail
Prev ⟵ Seen // Update previously seen states
Seen ⟵ Prev ∨ Img(Prev,T) // Mark states in the image of Prev as seen
end
return Pass // No Bad state reachable

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

 Satisfiability Solvers

• Given a Boolean formula Q,

• Is there a satisfying assignment to the variables in Q?

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

Satisfiability Solvers
Example

• SAT((x ∣ y) ∙ (x ∣ z) ∙ (¬x ∣ ¬z) ∙ (y ∣ z))?

Yes.
Satisfying assignment: x=1, y=1, z=0
Satisfying assignment: x=0, y=1, z=1
• SAT((x ∣ ¬y) ∙ (¬x ∣ y) ∙ (x ∣ z) ∙ (¬x ∣ ¬z) ∙ (y ∣ ¬z) ∙ (¬y ∣ z))?
No.

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

 Bounded Model Checking

• Bounded Model Checking: Can we reach a bad state in k cycles?

V T(V,V’)

clock

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

Bounded Model Checking

• Bounded Model Checking: Can we reach a bad state in k cycles?

• Unroll the circuit k times

V0 T(V0,V1) V1 T(V1,V2) … Vk-1 T(Vk-1,Vk) Vk

Initial Bad

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

 Bounded Model Checking

• Bounded Model Checking: Can we reach a bad state in k cycles?

• Unroll the circuit k times

V0 T(V0,V1) V1 T(V1,V2) … Vk-1 T(Vk-1,Vk) Vk

Initial Bad
• Badk = I(V0) ∧T(V0,V1) ∧ … ∧ T(Vk-1, Vk) ∧ Bad(Vk)
• Unsatisfiable? No failure in k cycles
• Satisfiable? Satisfying assignment is a k-length counterexample
UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

Bounded Model Checking

Iterative BMC

CHECK (M, Bad) // M = (S, I, T), Bad ⊆S

k ⟵0
while (true)
if SAT(Badk) // k-BMC
return Fail
k ⟵ k+1 // Increment k
end

When does the loop terminate for an N-bit state machine?

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

 Model Checking

Graph Reachability
Symbolic Model Checking
Proof by Induction

Natural Induction

• To Prove:
1 + 2 + … + n = (n * (n+1)) /2
• Base Step:
Show that the equation holds for n = 1
1 = (1 * 2) / 2 = 1
• Induction:
Assume equation holds for n = i,
then show that it holds for n = (i+1)
1+2+…+i = (i*(i+1))/2 // Assumption
1 + 2 + … + i + (i+1) = (i*(i+1))/2 + (i+1)
= (i*(i+1) + 2*(i+1))/2
= ((i+1) * (i+2))/2

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

 Induction for FSM Properties

• Given Bad states, all the other states are Good

Good(V) = ¬Bad(V)
• To show that an FSM never reaches a Bad state
• Prove that the FSM always stays in a Good state
i.e. Good is an invariant for the system

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

Induction for FSM Properties

• Given Bad states, all the other states are Good 01 11

Good(V) = ¬Bad(V)
• To show that an FSM never reaches a Bad state
• Prove that the FSM always stays in a Good state
00 10

• Show that the following are valid:

I(V) Good(V) (Base step)
Good(V) ∧ T(V,V’) Good(V’) (Induction) Bad = x ∙ y
Good = ¬x ∣ ¬y

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

 Induction for FSM Properties
Not all valid properties are inductive

V = {x,y,z}
I = x ∙ ¬y ∙ z
010 110 011 111
T = (x’ ⟷ ¬x) ∙ (y’ ⟷ y) ∙ (z ⟷ (x ∣ z))
Bad = x∙y
Good = ¬(x∙y) Not inductive
000 100 001 101

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

Inductive Invariants

• An inductive invariant for a state machine is any property 𝛷(V) such that:
I(V) 𝛷(V)
𝛷(V) ∧ T(V,V’) 𝛷(V’)

• To prove that FSM always stays in Good:

Find an inductive invariant 𝛷(V)
Show that 𝛷(V) Good(V)

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

 Model Checking and Induction

• The set Reach of all reachable states is, by definition, inductive

• The initial states are in Reach
• From Reach, you can only reach states in Reach

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

Model Checking and Induction

• The set Reach of all reachable states is, by definition, inductive

• The initial states are in Reach
• From Reach, you can only reach states in Reach
• Reach is the strongest invariant for the state machine

• Given any other invariant 𝛷(V),

Reach(V) 𝛷(V)

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

 Model Checking and Induction

• The set Reach of all reachable states is, by definition, inductive

• The initial states are in Reach
• From Reach, you can only reach states in Reach
• Reach is the strongest invariant for the state machine

• Given any invariant 𝛷(V),

Reach(V) 𝛷(V)

• Alternate algorithms attempt to find weaker invariants:

• Interpolation
• Property Directed Reachability (PDR)

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

Model Checking and Induction

The set of reachable states is inductive

V = {x,y,z}
I = x∙¬y∙z
010 110 011 111
T = (x’ ⟷ ¬x) ∙ (y’ ⟷ y) ∙ (z ⟷ (x ∣ z))
Bad = x∙y
Good = ¬(x∙y) Not inductive
Reach = ¬y∙z Inductive 000 100 001 101

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

 Model Checking and Induction
Alternate Inductive Invariant

V = {x,y,z}
I = x∙¬y∙z
010 110 011 111
T = (x’ ⟷ ¬x) ∙ (y’ ⟷ y) ∙ (z ⟷ (x ∣ z))
Bad = x∙y
Good = ¬(x∙y) Not inductive
Reach = ¬y∙z Inductive 000 100 001 101

𝛷 = ¬y Inductive

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

Model Checking and Induction

Invariant Strength

V = {x,y,z}
I = x∙¬y∙z
010 110 011 111
T = (x’ ⟷ ¬x) ∙ (y’ ⟷ y) ∙ (z ⟷ (x ∣ z))
Bad = x∙y
Good = ¬(x∙y) Not inductive
Reach = ¬y∙z Inductive 000 100 001 101

𝛷 = ¬y Inductive

Invariant Strength: Reach 𝛷 Good

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020
 Summary

Summary

• Model Checking is an effective static analysis method for verification

• Enables validation of complex System-on-a-Chip designs (SoC’s), including CPU’s and GPU’s
• Results in robust design micro-architecture specifications and implementations
• Unit-level formal analysis must seamlessly dovetail into product design methodologies
• Core Ideas
• Graph Reachability
• Symbolic representation
• Induction
• Plenty of scope for creative work and careers in hardware verification
• Tools, flows, and methodologies to tackle hard verification “puzzles” in industry

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

 References

References

• Model Checking
• E. A. Emerson and E. M. Clarke, “Characterizing Correctness Properties of Parallel Programs as Fixpoints”, Proceedings
of the Seventh International Colloquium on Automata, Languages, and Programming, LNCS, Vol. 85, 1981.
• E.M. Clarke, E. A. Emerson and A. P. Sistla, “Automatic verification of finite-state concurrent systems using temporal
logic specifications,” ACM Transactions on Programming Languages and Systems, Vol. 8, No. 2, April 1986.
• J-P. Queille and J. Sifakis, “Specification and Verification of Concurrent Systems,” CESAR International Symposium on
Programming, LNCS, Vol. 137, 1982
• BDDs and Symbolic Model Checking
• R.E. Bryant, “Graph-Based Algorithms for Boolean Function Manipulation,” IEEE Transactions on Computers, Vol. C -
35, No. 8, August, 1986
• O. Coudert, C. Berthet and J.C. Madre, “Verification of Synchronous Sequential Machines Based on Symbolic
Execution,” International Workshop on Automatic Verification Methods for Finite State Systems, 1989
• J.R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang, “Symbolic model checking: 1020 states and beyond,”
5th Ann. Symposium on Logic in Computer Science, June 1990
UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020
 References

• Satisfiability and Bounded Model Checking

• Niklas Eén and Niklas Sörensson, “An Extensible SAT-solver,” 6th International Conference on Theory
and Applications of Satisfiability Testing, 2003
• A. Biere, A. Cimatti, E. M. Clarke and Y. Zhu, “Symbolic Model Checking without BDDs,” 5th
International Conference on Tools and Algorithms for Construction and Analysis of Systems, 1999
• Induction and other SAT-based methods
• M. Sheeran, S. Singh and G. Stalmark, “Checking Safety Properties using Induction and a SAT-
solver,” Formal Methods in Computer-Aided Design, 2000
• K.L. McMillan, “Craig Interpolation and Reachability Analysis,” 10th International Symposium on
Static Analysis, 2003
• A.R. Bradley, “SAT-based Model Checking without Unrolling,” 12th International Conference on
Verification, Model Checking, and Abstract Interpretation, 2011
UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020

References

• Textbooks
• E.M. Clarke, O. Grumberg and D.A. Peled, “Model Checking,” MIT Press, 1999
• T. Kropf, “Introduction to Formal Hardware Verification”, Springer-Verlag, 1999

UT Austin College of ECE - [Link] of Digital Systems, 5th March 2020