Transaction Interaction Properties and Modeling in Hardware Verification

www.gigascale.org Specification and Encoding of Transaction Interaction Properties Divjyot Sethi Yogesh Mahajan Sharad Malik Princeton University Hardware Verification Workshop Edinburgh July 15, 2010 1

Gap Between Specification and Implementation Specification Objects are units of data Concurrent computation on these objects Instr Op Rs Rt Consequences for Verification Need humans to translate correctness conditions between them Incomplete, expensive, error prone Significant barrier to automation in verification. Frame l1 Immediate Packet ln H T Mapping of concurrent functions onto concurrent hardware blocks is captured by humans Implementation Objects are functional logic blocks Concurrent communication between these objects Drives efforts to move design and verification to levels above RTL. M1 M2 M3 Pipeline

Modeling Concurrent Computation Using Transactions Time Read Transaction is a unit of work Transactions can be concurrent Transaction sequences Permits reasoning about Individual transactions Interactions between transactions e.g. pipeline hazards End Fetch Decode T1 End Read Address Write Read End Fetch Decode T2 End Read Address Write Read End Fetch Decode T3 Transaction End Read Address Shared Resource Write Sequence Order 3

Transaction Interaction Properties Examples Contention Mutual exclusion Sequencing Ordering of packets in a router Pipeline hazards Priority Choosing among concurrent processes Generally deal with ordering of individual transaction instances. 4

Transaction Interaction Properties in RTL Lack high-level information Where are the instructions? Need to instrument the design to capture high-level objects Instructions in flight Need to state the property in terms of instrumented variables Human intervention limits automation Example: RAW Pipeline Hazard Easier with a transaction-level model with explicit ordering information. 5

Big Picture Automated Transaction- LevelModel Transaction Interaction Property Finite Model + Temporal Logic Property + Encoding Model Check This Verified Synthesis This Work Previous Work (CODES+ISSS 09) Synthesized RTL

Talk Outline Motivation Modeling Transactions and Interaction Properties Encoding for Model Checking Experiments Related Work Summary 7

Transaction-Level Model Start Step Guarded Transitions Individual Transaction Explicit start and end steps Guarded transitions Model as a Kripke structure Infinite array of transactions Index value refers to specific transaction State Local Transaction state present step & local variables Local variables constant after a transaction ends Global shared state End Step T1 T2 Parametric, but not symmetric in i M1 i Ti Global State Local State Of Ti Modeled as an infinite Kripke structure 8

Property Specification using Indexed Temporal Logic Indexed transaction local variables Example: RAW hazard property i, j are transaction indices i,j j>i G~( readj & ~writei & F(writei)) [L(I),g] I, P(I) Indexed Temporal Logic Formula General Form of property: I: Set of index variables, one for each interacting transaction P(I): Predicate on the set of indices I capturing relationship among interacting transactions [L(I),g]: Temporal logic formula on transaction local indexed variables and global variables 9

Talk Outline Motivation Modeling Transactions and Interaction Properties Encoding for Model Checking Experiments Related Work Summary 10

Encoding for Model Checking Infinite State Model + I, P(I) [v(I),g] T1 Encode T2 M1 LTL/CTL Formula + Global State i Finite State Model Ti Encode Model Check This Indexed State 11

Handling Infinite State Infinite State Model + I, P(I) [v(I),g] T1 Observation 1: Only a finite number of active transactions possible due to finite resources Finite state for active transactions T2 M1 S1 Global State S2 i State of active transactions Ti SK User specified upper bound Independently verified Indexed State 12

Handling Infinite State Infinite State Model + I, P(I) [v(I),g] T1 But, properties may refer to local variables of transactions that have ended. T2 M1 Observation 2: Can exploit non-determinism. Non-deterministically select |I| transactions for tracking past history. The model checker will implicitly consider all possible values. Global State i Ti E1 Number of interacting transactions E2 Local variables of selected transactions Indexed State E|I| 13

Encoding the Predicate Infinite State Model + I, P(I) [v(I),g] T1 But, predicate evaluation needs the potentially infinite index value of the interacting transactions. Observation 3: Can handle several (all?) useful predicates without explicit index value storage. Ordering Constraints P(i, j) : i > j Separation Constraints P(i, j) : i j > m P(i, j) : i j < m Equality Constraints: P(i, j) i = j + m Inequality constraints P(i, j) : i j + m T2 M1 ND_Selecti Global State Predicate FSM i Ti ND_Selectj I = {i,j} Indexed State 14

Encoding for Model Checking Infinite State Model + I, P(I) [v(I),g] T1 Key Components T2 E1 S1 M1 E2 S2 Global State E|I| i Ti SK Local variables of ended transactions State of active transactions ND_Selecti Predicate FSM Indexed State ND_Selectj 15

Talk Outline Motivation Modeling Transactions and Interaction Properties Encoding for Model Checking Experiments Related Work Summary 16

Experiments Design examples Simple router Property: Flits are processed in order Simple processor Property: Absence of RAW hazard Input: Designs specified using a transaction-level model Properties specified using indexed temporal logic Output: Synthesized SMV for finite model and LTL property Model checked using Cadence SMV 17

Model Checking Results System Time (s) BDD Size (Number of Nodes) No. of State Variables Property Result Lines of Code K (Finite Bound) Router 43324 397 3 <0.1 30 True Processor 3152542 382 6 17 50 False All experiments done on Intel Core 2 Duo 2.5GHz 3 GB RAM Machine with Windows XP 18

Talk Outline Motivation Modeling Transactions and Interaction Properties Encoding for Model Checking Experiments Related Work Summary 19

Related Work Summary Transaction Based System Unbounded/ Infinite State Indexed Properties Finite Encoding Encoding Generation Automated Parameterized Synchronous Systems [Emerson, Namjoshi] Indexed CTL* Logic [Clarke, Grumberg, Brown] NA NA NA Hazard Checking using Transaction Models [Malik, Mahajan] This Work 20

Talk Outline Motivation Modeling Transactions and Interaction Properties Encoding for Model Checking Experiments Related Work Summary 21

Summary Transaction-based higher-level models enable reasoning without resorting to design instrumentation Main Contributions: Infinite Kripke structure model for transactions with explicit indices Indexed temporal logic for specifying transactions interactions properties Finite encoding of design and property exploiting Finiteness of hardware resources Non-determinism in model checkers Specific ordering relationships of interacting transactions Initial prototype demonstration 22

Related Papers Y. Mahajan, C. Chan, A. Bayazit, S. Malik, and W. Qin, Verification driven formal architecture and microarchitecture modeling, in MEMOCODE 07: Proceedings of the 5th IEEE/ACM International Conference on Formal Methods and Models for Codesign. Washington, DC, USA: IEEE Computer Society, 2007, pp. 123 132. Y. Mahajan and S. Malik, Automating hazard checking in transaction-level microarchitecture models, in FMCAD 07: Proceedings of the Formal Methods in Computer Aided Design. Washington, DC, USA: IEEE Computer Society, 2007, pp. 62 65. D. Schwartz-Narbonne, C. Chan, Y. Mahajan, and S. Malik, Supporting RTL flow compatibility in a microarchitecture-level design framework, in CODES+ISSS 09: Proceedings of the 7th IEEE/ACM international conference on Hardware/software codesign and system synthesis. New York, NY, USA: ACM, 2009, pp. 343 352. 23