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)\overline{I(s_1)}P(s_1)
  48 \wedge\dots\wedge T(s_{k-1},s_k)\overline{I(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 * inductive case: no path ending in a bad state can be reached in k+1 steps
  54 * if inductive case fails, $k \leftarrow k + 1$ and repeat
  55
  56 # Single register with feedback
  57
  58 ![](states_one.png)
  59
  60 # Registered output with internal state
  61
  62 ![](states_output.png)
  63
  64 # Registered output with enable
  65
  66 ![](states_enable.png)
  67
  68 # Flip-flop with input
  69
  70 ![](states_input.png)
  71
  72 # Verifying a flip-flop
  73
  74 ![](states_verification.png)
  75
  76 # Complete flip-flop with input and enable
  77
  78 ![](states_complete.png)
  79
  80 # Code for simple register with feedback
  81
  82 ```verilog
  83 module simple(input clk);
  84
  85 reg r = 0;
  86
  87 always @(posedge clk)
  88     r <= r;
  89
  90 `ifdef FORMAL
  91 always @*
  92     assert(!r);
  93 `endif
  94 ```
  95
  96 # SBY drive file
  97
  98 ```
  99 [options]
 100 mode prove
 101 depth 1
 102
 103 [engines]
 104 smtbmc yices
 105
 106 [script]
 107 read_verilog -formal simple.v
 108 prep -top simple
 109
 110 [files]
 111 simple.v
 112 ```
 113
 114 # Output (simplified)
 115
 116 ```
 117 $ sby simple.sby
 118
 119 induction: Trying induction in step 1..
 120 induction: Trying induction in step 0..
 121 induction: Temporal induction successful.
 122 basecase: Checking assumptions in step 0..
 123 basecase: Checking assertions in step 0..
 124 basecase: Status: passed
 125 summary: engine_0 (smtbmc yices) returned pass
 126  for induction
 127 summary: engine_0 (smtbmc yices) returned pass
 128  for basecase
 129 summary: successful proof by k-induction.
 130 DONE (PASS, rc=0)
 131
 132 ```
 133
 134 # Flip flop with enable (1/2)
 135
 136 ```
 137 from nmigen.asserts import Assert, Assume, Past
 138 from nmutil.formaltest import FHDLTestCase
 139 from nmigen import Signal, Module
 140 import unittest
 141
 142 class Formal(FHDLTestCase):
 143     def test_enable(self):
 144         m = Module()
 145         r1 = Signal()
 146         r2 = Signal()
 147         s = Signal()
 148         en = Signal()
 149         m.d.sync += [r2.eq(r1), r1.eq(r2)]
 150         with m.If(en):
 151             m.d.sync += s.eq(r1 & r2)
 152 ```
 153 # Flip flop with enable (2/2)
 154
 155 ```
 156         m.d.comb += Assert(~s)
 157         m.d.sync += Assume(Past(en) | en)
 158         m.d.comb += Assert(~r1 & ~r2)
 159         self.assertFormal(m, mode="prove", depth=5)
 160
 161
 162 if __name__ == '__main__':
 163     unittest.main()
 164 ```
 165
 166 # Induction failure example
 167
 168 ```
 169 summary: engine_0 returned pass for basecase
 170 summary: engine_0 returned FAIL for induction
 171 DONE (UNKNOWN, rc=4)
 172 ```
 173
 174 ![](test_enable.png)
 175
 176 #
 177
 178 \centering {\Huge
 179
 180 The End
 181
 182 Thank you
 183
 184 Questions?
 185
 186 }
 187
 188 * Discussion: http://lists.libre-soc.org
 189 * Libera IRC \#libre-soc
 190 * http://libre-soc.org/
 191 * http://nlnet.nl/entrust
 192 * https://libre-soc.org/nlnet_2022_ongoing/
 193 * https://libre-soc.org/nlnet/\#faq
 194 * https://git.libre-soc.org/?p=soc.git;a=tree;f=src/soc/experiment/formal;hb=HEAD