conferences/fosdem2024/fosdem2024_formal/formal.md

   1 ---
   2 title: Introduction to Formal Verification of Digital Circuits
   3 author: Cesar Strauss
   4 theme: Copenhagen
   5 date: FOSDEM 2024
   6 ---
   7 # Why Formal Verification?
   8
   9 * A tool for finding bugs
  10 * Complementary to simulation
  11 * Helps finding corner cases
  12 * ... triggered by specific sequences of events
  13
  14 # Comparison with traditional debugging concepts
  15
  16 | formal                   | traditional       |
  17 |--------------------------|-------------------|
  18 | Cover                    | Simulation        |
  19 | Bounded Model Check      | Unit test         |
  20 | k-Induction              | Test fixture?     |
  21 | Exhaustive search        | random test cases |
  22 | synthesizable test-bench | can be procedural |
  23 | "assume" inputs          | test vectors      |
  24 | "assert" outputs         | "assert" outputs  |
  25
  26 # Workflow
  27
  28 * HDL: includes assertions
  29 * SBY: work plan, drives the process
  30 * Yosys: synthesizes to logic functions:
  31   * state $s$: contents of all registers and inputs
  32   * initial predicate: $I(s)$
  33   * transition relation $T(s_1, s_2)$
  34   * assertions: $P(s)$
  35
  36 * yosys-smtbmc: proves correctness or outputs a trace
  37
  38   * exhaustive search for a path from the initial state to a bad state
  39   * if not found, the design is correct
  40   * if found, output an error trace
  41
  42
  43 # Unbounded inductive proof
  44
  45 * bad trace:
  46
  47 $I(s_0) P(s_0) \wedge T(s_0,s_1)P(s_1)
  48 \wedge\dots\wedge T(s_{k-1},s_k)
  49 \overline{P(s_k)}$
  50
  51 * k $\leftarrow$ 0
  52 * base case: no path from initial state leads to a bad state in k steps
  53 * if base case fails, report the bad trace
  54 * inductive case: no path ending in a bad state can be reached in k+1 steps
  55 * if inductive case fails, $k \leftarrow k + 1$ and repeat
  56 * otherwise, proof is complete, circuit is safe.
  57
  58 # Single register with feedback
  59
  60 ![](states_one.png)
  61
  62 # Registered output with internal state
  63
  64 ![](states_output.png)
  65
  66 # Registered output with enable
  67
  68 ![](states_enable.png)
  69
  70 # Flip-flop with input
  71
  72 ![](states_input.png)
  73
  74 # Verifying a flip-flop
  75
  76 ![](states_verification.png)
  77
  78 # Complete flip-flop with input and enable
  79
  80 ![](states_complete.png)
  81
  82 # Code for simple register with feedback
  83
  84 ```verilog
  85 module simple(input clk);
  86
  87 reg r = 0;
  88
  89 always @(posedge clk)
  90     r <= r;
  91
  92 `ifdef FORMAL
  93 always @*
  94     assert(!r);
  95 `endif
  96 ```
  97
  98 # SBY drive file
  99
 100 ```
 101 [options]
 102 mode prove
 103 depth 1
 104
 105 [engines]
 106 smtbmc yices
 107
 108 [script]
 109 read_verilog -formal simple.v
 110 prep -top simple
 111
 112 [files]
 113 simple.v
 114 ```
 115
 116 # Output (simplified)
 117
 118 ```
 119 $ sby simple.sby
 120
 121 induction: Trying induction in step 1..
 122 induction: Trying induction in step 0..
 123 induction: Temporal induction successful.
 124 basecase: Checking assumptions in step 0..
 125 basecase: Checking assertions in step 0..
 126 basecase: Status: passed
 127 summary: engine_0 (smtbmc yices) returned pass
 128  for induction
 129 summary: engine_0 (smtbmc yices) returned pass
 130  for basecase
 131 summary: successful proof by k-induction.
 132 DONE (PASS, rc=0)
 133
 134 ```
 135
 136 # Flip flop with enable (1/2)
 137
 138 ```
 139 from nmigen.asserts import Assert, Assume, Past
 140 from nmutil.formaltest import FHDLTestCase
 141 from nmigen import Signal, Module
 142 import unittest
 143
 144 class Formal(FHDLTestCase):
 145     def test_enable(self):
 146         m = Module()
 147         r1 = Signal()
 148         r2 = Signal()
 149         s = Signal()
 150         en = Signal()
 151         m.d.sync += [r2.eq(r1), r1.eq(r2)]
 152         with m.If(en):
 153             m.d.sync += s.eq(r1 & r2)
 154 ```
 155 # Flip flop with enable (2/2)
 156
 157 ```
 158         m.d.comb += Assert(~s)
 159         m.d.sync += Assume(Past(en) | en)
 160         m.d.comb += Assert(~r1 & ~r2)
 161         self.assertFormal(m, mode="prove", depth=5)
 162
 163
 164
 165
 166 if __name__ == '__main__':
 167     unittest.main()
 168 ```
 169
 170 # Induction failure example
 171
 172 ```
 173 summary: engine_0 returned pass for basecase
 174 summary: engine_0 returned FAIL for induction
 175 DONE (UNKNOWN, rc=4)
 176 ```
 177
 178 ![](test_enable.png)
 179
 180 # Verifying memories with a "victim address"
 181
 182 ![](memory.png)
 183
 184 # Verifying streams with transaction counters
 185
 186 ![](stream.png)
 187
 188 # Dynamic SIMD
 189
 190 ```
 191 exp-a    : ....0....0....0.... 1x 32-bit
 192 exp-a    : ....0....0....1.... 1x 24-bit plus 1x 8-bit
 193 exp-a    : ....0....1....0.... 2x 16-bit
 194 ...
 195 ...
 196 exp-a    : ....1....1....0.... 2x 8-bit, 1x 16-bit
 197 exp-a    : ....1....1....1.... 4x 8-bit
 198 ```
 199 ![](sum.png)
 200
 201 #
 202
 203 \centering {\Huge
 204
 205 The End
 206
 207 Thank you
 208
 209 Questions?
 210
 211 }
 212
 213 * Discussion: http://lists.libre-soc.org
 214 * Libera IRC \#libre-soc
 215 * http://libre-soc.org/
 216 * https://libre-soc.org/resources/
 217 * http://nlnet.nl/entrust
 218 * https://libre-soc.org/nlnet_2022_ongoing/
 219 * https://libre-soc.org/nlnet/\#faq
 220 * https://git.libre-soc.org/?p=soc.git;a=tree;f=src/soc/experiment/formal;hb=HEAD