Games in Open System Verification Ansuman Banerjee Indian Statistical Institute Outline • The Synthesizability problem for open systems – Game-based analysis – Realizability and Receptiveness • Games in Test Generation – Vacuity Games – Realizability Games • Consistency Issues in 3-party specifications – Game based modeling – Observability based Analysis Formal-V Group, ISI The Validation Problem Specification P Validation Process Does M satisfy P ? Model M • Simulation – Most popular but not exhaustive • Formal verification – mathematically prove that an implementation satisfies its specification Formal-V Group, ISI The Synthesizability Problem Does there at all exist an implementation that can be made to satisfy a given specification ? – For closed systems: Same as the satisfiability problem • Does there exist an assignment of variables that can satisfy the specification? – For Open systems: • Does there exist an implementation that satisfies the specification for all possible environment behaviors? Formal-V Group, ISI Games and Synthesizability of Open system specifications • Can be modeled as a 2-player game – Player 1: The environment (decides the input values) – Player 2: The Open system (decides the output values) • Strategy for Player1: – Depends on nature of the environment – An adversarial environment may try to present inputs to refute the specification • Winning strategy for Player-2 – An implementation that can satisfy the specification against possible moves of Player-1 – Synthesizablity investigates the existence of a strategy for Player-2 Formal-V Group, ISI Games and Property Verification • Whenever x arrives, y is asserted in the next cycle • Strategy of Player-2 (setting y) is a correct labeling of nodes with output variables Formal-V Group, ISI Game Models: Applications • Property Verification of Modules • Synthesis [Church:1962, Rabin, Ramadge/Wonham:1987, Pnueli/Rosner:1989] • Receptiveness [Dill:1989, Abadi/Lamport:1993] • Reasoning about adversarial behavior • Interface-based design [Henzinger:1997] • Modular reasoning [Kupferman:99/Vardi:2000] • Early error detection [deAlfaro/Mang:2001] • Reasoning about security [Raskin et al.] Formal-V Group, ISI Consistency of 2-party specifications • A specification that is satisfiable when interpreted over a closed system may be inconsistent when interpreted over every module (open system) • A consistent specification must meet the following requirements – Realizability: • The module must be able to assign its outputs without knowing its future inputs such that the property is satisfied for all input scenarios – Receptiveness: • The module must have the freedom to choose its outputs as long as it does not refute the specification at that instant Formal-V Group, ISI Realizability • Consider a priority arbiter r g – Property: • Whenever the request r arrives, the grant g must be given exactly in the next cycle – Suppose the designer is tempted to write this as G[ r X(g) ∧ X X(¬ g)] • This property is satisfiable, -- consider input sequences where r is never asserted • It is not realizable for input sequences where r is asserted for two consecutive cycles Formal-V Group, ISI Realizability: Formal Characterization ψ = G(r ( X( g ) ∧ X X( ¬g ))) ψ is satisfiable but not realizable Does there exist a strategy for Player-2 that can guarantee satisfaction of ψ for all possible strategies of Player-1 ? Formal-V Group, ISI Unfolding of LTL formula • An LTL formula L can be unwound to a finite time step(say k) to generate a Boolean formula FL. • Consider the property : (a & X b → XX c) – – – – FL= ¬a ∨ ¬Xb ∨ XX c FL0 = ¬ a0 FL1 = ¬ a0 ∨ ¬b1 FL2 = ¬ a0 ∨ ¬b1 ∨ c2 • Consider the property : G (a) ∧ F (¬a) – FL0 = a0 ∧ ¬a0 – FL1 = (a0 ∧ a1) ∧ (¬a0 ∨ ¬a1 ) – FL2 = (a0 ∧ a1 ∧ a2) ∧ (¬a0 ∨ ¬a1 ∨ ¬a2 ) Formal-V Group, ISI Checking Realizability • L be an LTL formula over set of inputs i and set of outputs o • Let FL be the Boolean formula unfolded for |L| cycles. • L is realizable iff the following QBF is true QL = ∃o0∀i1 ∃o1 … ∀i| L| ∃o| L| (FL) where ik denotes a valuation of the inputs at time step k, and ok denotes a valuation of the outputs at time step k • Theoretical results on the sufficiency of length of L Formal-V Group, ISI Receptiveness • A module must have the freedom of choosing its outputs as long as it does not refute the property • Consider the property: G( o ⇒ X i ) • The arbiter can realize this property by never asserting o. – It cannot assert o because it cannot see its future inputs!! – This is an un-receptive property Formal-V Group, ISI Receptiveness An invalid strategy QBF based characterization for checking receptiveness of specifications has been proposed [ICCAD:2005] Formal-V Group, ISI Outline • The Synthesizability problem for open systems – Game-based analysis – Realizability and Receptiveness • Games in Test Generation – Vacuity Games – Realizability Games • Consistency Issues in 3-party specifications – Game based modeling – Observability based Analysis Formal-V Group, ISI Test Generation for Open Systems • The test-bench attempts to mimic the environment strategies • An intelligent test bench must be online and adaptive – It should avoid generation of vacuous scenarios – Whenever the module makes a wrong move, the test bench must be able to drive the module to a refutation • ATPG based techniques • Methodology for automatically determining the appropriate vector constraints, based on the analysis of both the design and the property being checked • Our contributions – Vacuity Games – Realizability Games Formal-V Group, ISI Intelligent Test-benches Vacuity Games and Test Generation • Strategy of the environment must be to defeat the module by driving it to a refutation of the specification, not satisfy the specification itself • Test-bench must present inputs that are non-vacuous G (x → X y) Formal-V Group, ISI Vacuity Games • Non-vacuous test generation with respect to a specification can be modeled as a game – Strategy for test-bench at every step is to avoid satisfaction of the property due to its own values – Strategy for module is to attempt satisfaction • We have developed an algorithm for non-vacuous test generation – – – – – Simulation based Incrementally unfold the specification Assign inputs that do not satisfy the specification vacuously Simulate the module and sample its outputs Continue till a success or failure is reached Formal-V Group, ISI An example run • Consider the property : (a & X b → XX c) – FL= ¬a ∨ ¬Xb ∨ XX c – Step 0: FL0 = ¬ a0 ∨ ¬b1 ∨ c2 • Substitute module initial values and evaluate • a = 0 satisfies specification vacuously • Simulation done with a = 1 a c b – Step 1: FL1 = ¬b1 ∨ c2 • Substitute value of c in Step 0 and evaluate • b = 0 satisfies specification vacuously • Simulation done with b = 1 – Step 2: FL2 = c2 • Substitute value of c in Step 1 and evaluate • Any random input vector is good. • Simulation done and in the next step c must be true Formal-V Group, ISI Example • P1: Whenever r1 goes high, g1 is asserted in the next cycle : G(r1 → Xg1) • P2: Whenever r2 goes high, g2 is asserted within 3 cycles : G(r2 → (Xg2 ∨ XXg2) • Test sequences that do not drive r2 satisfy P2 vacuously • Test sequences that do not drive r1 satisfy P1 vacuously • Requirement of non-vacuity may span multiple cycles as well • Target P1 and P2 separately and generate non-vacuous tests Formal-V Group, ISI Costly mistakes: Guiding towards disaster X ? 0 X ? X X : Environment 0 : Module 0 1. Unreceptive specifications: Options to realize at the start 2. Module makes a mistake 3. Environment guides the module to disaster !! Formal-V Group, ISI Realizability games • The test-bench can intelligently detect such cases – – – – Aware of realizability Specification was realizable at the beginning Became unrealizable after the first move by module Environment strategy: Drive module to refutation • Crucial move: occupying the central box after module makes the mistake • We have developed an algorithm for intelligent test generation for unreceptive specifications – At the start of every simulation step, check for realizability – If unrealizable, present inputs such that module can’t recover !! Formal-V Group, ISI Outline • The Synthesizability problem for open systems – Game-based analysis – Realizability and Receptiveness • Games in Test Generation – Vacuity Games – Realizability Games • Consistency Issues in 3-party specifications – Game based modeling – Observability based Analysis Formal-V Group, ISI Consistency of 3-party specifications •The module (M): the controlled system •The environment (E): the set of inputs •The controller (C): supplies the control inputs 1. The specification of the system consists of the specification of the module as well as its controller. 2. Neither the module nor the controller can realize the specification alone: Symbiotic strategy 3. We present results of observability based synthesizability analysis of 3-party specifications Formal-V Group, ISI The formal model I = IM ∪ IC IM O C OM IC 1. Verify whether both M and C are realizable 2. Analysis done at the architectural phase of the design, before implementing any of the two 3. Does the controller have adequate observability ? Formal-V Group, ISI An example I = {devicerdy, r0, r1, lock, busfree}, IM = {devicerdy, r0, r1, lock}, IC = {r0, r1, busfree}, C = {valid}, O = {g0, g1, busy}, OM = {busy} Formal-V Group, ISI The Formal Specification P0: G (((r0 ∨ r1 ) ∧ ¬ busy & busfree) → Xvalid) P1: G ((lock ∧ ¬ r0) → X ¬ valid) P2: G ((r0 ∧ valid ∧ devicerdy) → Xg0) P3: G ((r1 ∧ valid ∧ devicerdy) → Xg1) P4: G ((g0 ∨ g1) ↔busy) P5: G (mutex(g0, g1)) P6: G (busy → X ¬ busy) P7: G (mutex(r0, r1)) Formal-V Group, ISI The Observability Spectrum • Zero Observability: The controller has no visibility. Can M alone realize the system specification? • Full Observability: The controller can observe the full set of environment inputs and machine outputs (2-party system) • Partial Observability: – Adequate Observability – Inadequate Observability • For Inadequate Observability, what should be the strategy of the environment ? • Can we bridge the observability gap? Formal-V Group, ISI Zero Observability • Given a machine M and a LTL specification P, we say that the machine is synthesizable under zero observability of the controller, if the machine alone can realize P – Zero Information Game • Both OM and IC are empty, define IMU = I – IM as the set of inputs M cannot see • Solution: Check the truth of QP = ∃o0 ∀iM1 ∀C1 ∃o1 … ∀iM| P| ∀C | P| ∃o| P| (∀iMU1 … ∀iMU| P| ) (FP) • For our example, Zero observability check fails Formal-V Group, ISI Full Observability • OM = O and IC = IM = I • Can M realize P assuming a friendly C? – Perfect Information Game for C • For our example, Full observability check fails !! • Control Strategy: For a given LTL specification P, a control strategy exists if M is able to realize P by choosing appropriate values for its control inputs (assuming the existence of a friendly C) and assigning appropriate values to its outputs Formal-V Group, ISI Control Strategy P0: G (((r0 ∨ r1 ) ∧ ¬ busy & busfree) → Xvalid) P8: G ((r0 & ¬ busy & busfree) → Xvalid ) P9: G (( r1 & ¬ busy & ¬ lock & busfree) → Xvalid ) Formal-V Group, ISI The Formal Specification P0: G (((r0 ∨ r1 ) ∧ ¬ busy & busfree) → Xvalid) P1: G ((lock ∧ ¬ r0) → X ¬ valid) P2: G ((r0 ∧ valid ∧ devicerdy) → Xg0) P3: G ((r1 ∧ valid ∧ devicerdy) → Xg1) P4: G ((g0 ∨ g1) ↔busy) P5: G (mutex(g0, g1)) P6: G (busy → X ¬ busy) P7: G (mutex(r0, r1)) P8: G ((r0 & ¬ busy & busfree) → Xvalid ) P9: G ((r1 & ¬ busy & ¬ lock & busfree) → Xvalid ) Existence of a Control Strategy: Check the truth of QP = ∃o0 ∀i1 ∃C1 ∃o1 … ∀i| P| ∃C| P| ∃o| P| (FP) Formal-V Group, ISI Partial Observability • Can the controller really produce the friendly control which the module wants ? – Incomplete Information Game – Depends on how much it is able to observe. • Existence of a control strategy is not enough – The controller may not be able to provide desired inputs • Inadequate Observability: The controller is not synthesizable for all possible control strategies • Adequate Observability: The controller is synthesizable for all possible control strategies Formal-V Group, ISI Back to our example • • • P1: G((lock & ¬r0) → X ¬ valid) P9: G((r1 & ¬ busy & busfree & ¬ lock) → Xvalid ) Controller cannot see lock Formal-V Group, ISI Back to our example • • P1: G(¬r0 → X ¬ valid) P9: G((r1 & ¬ busy & busfree) → Xvalid ) • Inadequate Observability: Control strategy exists, but the controller is not synthesizable Formal-V Group, ISI Unrealizable Partial Observability: Formal methods • Inadequate Observability: – For all possible control strategies (Synthesizability of M does not imply synthesizability of C) over all time steps • Adequate Observability: – For all possible control strategies (Synthesizability of M should imply synthesizability of C) over all time steps • We have developed a QBF based characterization Formal-V Group, ISI Observability Games • The environment can make use of the observability limitations of the controller • The environment can play its moves such that the system is bound to fail (may span multiple cycles) • We have developed a formal methodology for constructing this malicious environment 1. 2. 3. 4. r0 and lock are raised with devicerdy and busfree, r1 kept low Arbiter is not busy, controller raises valid, Arbiter raises g0 and becomes busy, r0 is lowered and r1 raised Controller lowers valid, arbiter lowers g0 and busy Formal-V Group, ISI Dealing with Inadequate Observability • Transform to a case of adequate observability • Increase observability of the controller – Simple iterative algorithm (guaranteed to be successful since a control strategy exists) – Add the signal lock to the observable set of C • Add more properties that refine the interaction protocol of M and C – Keep busy high till the bus gets unlocked – Solution based on coalition games Formal-V Group, ISI Verification Group @ ISI: Focus Areas • Coverage • Assertion Mining • Semi-formal flows • Efficient implementations • Test versus security Security Protocols in Hardware Modeling and Analysis Formal Methods • Power Intent Analysis Constraint Solvers (AI, Learning, Architecture) Formal-V Group, ISI CAD Tools Research • Cache efficient Algorithms Distributed Computing High Performance Computing Software Verification • • Efficient Procedures Probabilistic verification THANK YOU Formal-V Group, ISI

© Copyright 2018