vlogsl: A Strategy Language for Simulation-based Verification of Hardware Michael Katelman and José Meseguer University of Illinois at Urbana-Champaign Haifa Verification Conference – October 5, 2010 1 / 26 “Implied needs are in: (1) verification, which is a bottleneck that has now reached crisis proportions . . . ” “. . . due to the growing complexity of silicon designs, functional verification is still an unresolved challenge, defeating the enormous effort put forth by armies of verification engineers and academic research efforts.” “Multiple sources report that in current development projects verification engineers outnumber designers, with this ratio reaching two to one for the most complex designs.” [ITRS 09] 2 / 26 language-level approach to mitigating the verification burden: help verification engineers be more productive by providing a better programming language to work in strategy paradigm explore the space of simulations in complex ways vlogsl an EDSL in Haskell supporting the strategy paradigm 3 / 26 Outline: 1 strategy paradigm, motivation and definition 2 vlogsl architecture 3 maze examples 4 I2 C case study 5 concluding remarks 4 / 26 5 / 26 5 / 26 5 / 26 6 / 26 6 / 26 6 / 26 6 / 26 7 / 26 7 / 26 7 / 26 7 / 26 8 / 26 8 / 26 8 / 26 8 / 26 8 / 26 8 / 26 8 / 26 8 / 26 + + 9 / 26 a data type called Config is the linchpin of vlogsl; it provides a first-class representation of a Verilog device event queues: active, non-blocking, future, etc. current and past values of all source-level nodes top-level input, clock, and reset names 10 / 26 + + 11 / 26 + + 12 / 26 + + 12 / 26 + 12 / 26 12 / 26 13 / 26 13 / 26 13 / 26 13 / 26 13 / 26 14 / 26 14 / 26 15 / 26 15 / 26 vlogsl does symbolic simulation synthesizeable and behavioral Verilog time efficient, extra memory required vlogsl function: simulate vlogsl is integrated with an SMT solver integrated with an efficient bit-vector solver (STP) vlogsl function: querySMT 16 / 26 17 / 26 18 / 26 Intel Xeon X5570 (2.93GHz, 8MB L3, Nehalem), 24 GB RAM, Linux kernel 2.6.18, 64-bit. ghc 6.10.4 with -O1. VCS-MX D-2009.12 Full64. vlogsl strategies random 0.070s breadth 0.293s backtrack 0.013s symbolic 0.018s 0.015s mixed vlogsl vs SystemVerilog + script random 0.070s script 7.111s 19 / 26 I2 C serial bus: two serial, open-drain lines: clock (SCL), and data (SDA) multi-master bus (requires arbitration), 7-bit addressing used for low speed peripherals (speakers, cell-phone displays) 20 / 26 I2 C mastering controller from opencores.org (open source): core is roughly 1000 lines of Verilog, FPGA proven capable of multi-mastering uses opencores.org “wishbone” interface 21 / 26 I2 C arbitration process: SCL SDA SDA0 SDA1 22 / 26 multi-mastering very difficult to test opencores.org tested in real-world, no bugs found submitted a potential bug, found via vlogsl, to author 23 / 26 what vlogsl allowed us to do: encapsulate bus transactions within an algebraic data type iteratively insert delays between two conflicting transactions re-use the initialization simulation steps, via backtracking observe correctness, via querying statements potential bug: with just the right delay, slave reads wrong data (all 0s) 24 / 26 Intel Xeon X5570 (2.93GHz, 8MB L3, Nehalem), 24 GB RAM, Linux kernel 2.6.18, 64-bit. ghc 6.10.4 with -O1. VCS-MX D-2009.12 Full64. I2 C write + read ×1 (vlogsl) I2 C write + read ×4 (vlogsl) I2 C write + read ×1 (vcs) I2 C write + read ×4 (vcs) 74.870s 299.06s 0.404s 0.470s 25 / 26 summary and upcoming work: strategy paradigm vlogsl novel use cases I2 C vlogsl large case study 26 / 26