Introduction to Formal Model Checking Alexander Gnusin SparkEDA Inc

Introduction Importance of formal verification Problem formulation FSMs and Computation Trees Safety vs. liveness property verification Bounded vs. unbounded verification Types of Formal Verification Engines Outcomes of formal verification

Importance of Formal Methods Formal methods are techniques used to model complex systems as mathematical entities. By building a mathematically rigorous model of a complex system, it is possible to verify the system's properties in a more thorough fashion than empirical testing. It is feasible to achieve completeness in property verification.

Formal Model Checking A comparison between the Finite State Machine and Properties Each Design is an FSM Outcomes: True or Counterexample Model Checker Finite State Machine Property True or Counterexample

FSM and Computation Trees Unwind State Graph to obtain Infinite Computation Tree A path of CT is an infinite sequence of states Example : a a b b b c ... Properties (propositions): Atomic : properties of states Temporal Logic Specifications: properties of paths a b c Initial state Finite State System Infinite Computation Tree a a b b c c a a a a b b c

Properties Definition Notes Formal Methods compare Properties with Design To make sense of this comparison, Properties have to not follow design implementation Ideally, Properties have to be independent from design implementation a b c Initial state cond1 Design If cur_state == a and cond1, then next_state == b Property JTAG FSM TDI TMS TCK TRST To save pins, TRST input may be omitted. TMS being high for 5 continuous clock Cycles is the same as TRST Design After 5 TMS==1 in row, JTAG FSM appears in Reset state Property BAD GOOD

Safety Properties “Bad thing” never happens Formula: In simulation, we are dealing with Safety properties only: Assertions/Checkers/Scoreboards verify that bad things don’t happen for all written test scenarios. Directed Test verify Safety property along selected path Safety property verification in simulation is limited by: Time: Each test scenario is bounded in time. Paths: Only user-selected paths are verified. Formal methods allow complete safety properties verification all paths every state on these paths AGp (¬p describes a “bad thing”)

Safety Properties Examples Arbiter outputs always mutually exclusive If posedge(req) , then witihin 10 clocks posedge(ack) Packet A entering the DUT have to exit DUT within 40 cycles Packet B exiting the DUT had to enter DUT within 30 cycles in the past (temporal, implication) Two devices cannot simultaneously write to the same memory address Protocol violation causes system interrupt with meaningful IR status info (max. 5 clocks after violation)

Liveness Properties “Good thing” eventually happens Formula: In Simulation, we are not able to verify Liveness properties: Tests are bounded in time while “eventually” assumes infinite time scale Cannot exhaust all possible paths Approximate Liveness properties with time-bounded safety ones: Replace “eventually” by “within N cycles after initial state” Then, liveness properties may be partially verified in simulation (only for time-bounded parts of selected paths) Formal methods allows complete Liveness properties verification all paths At least one state on these paths AFp (p describes a “good thing”)

Liveness Properties Examples All requests are eventually acknowledged Arbitration Fairness: all requestors eventually able to access the shared resource If External reset is deasserted, them internal reset is eventually deasserted too: POR block Ext rst Int rst Por inputs

Bounded vs. Unbounded Verification Bounded: verifies property in the limited amount of clocks Allow quick but incomplete properties checking Temporal property length must be smaller than the depth ob bounded verification Work well for large designs Unbounded: verifies properties for infinite time frames Allows most complete verification of design properties Runs out of resources for complex properties in large designs Initial state: a Depth: 4 clocks Infinite Depth

Formal Verification Engines Bug-hunters: uncomplete property verification, accept large designs random simulation bounded model checking (BMC) hybrids of the above two (“semi-formal”) Provers : complete propery verification, accept smaller designs or blocks K-step induction, with or without uniqueness constraints BDDs (exact reachability) Interpolation (over-approximate reachability) Property directed reachability (over-approximate reachability) Interval property checking

Outcomes of Formal Verification 3 Outcomes: Success: The property holds in all reachable states Failure: A finite-length counter-example is found Undecided: A limit on resources (such as runtime) is reached The Meaning of Success Bug hunters: no bugs found. Still, there is no guarantee that property holds for all paths. Provers: With unbounded verification, property holds for all times and for all paths. With bounded verification, property holds at limited time but for all paths If Undecided : Formal Attempt failed, need to change design/properties/formal engine

Questions?