From: Cesar Strauss Date: Tue, 30 Jan 2024 22:25:03 +0000 (-0300) Subject: fosdem2024_formal: add slides and diagrams X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b2a917b33ec26d7178bdf4b85e518a6bbafc3d95;p=libreriscv.git fosdem2024_formal: add slides and diagrams See Bug #1220: An introduction to Formal Verification of Digital Circuits --- diff --git a/conferences/fosdem2024/fosdem2024_formal/.gitignore b/conferences/fosdem2024/fosdem2024_formal/.gitignore new file mode 100644 index 000000000..b43b63175 --- /dev/null +++ b/conferences/fosdem2024/fosdem2024_formal/.gitignore @@ -0,0 +1,2 @@ +formal.pdf +states_*.png diff --git a/conferences/fosdem2024/fosdem2024_formal/Makefile b/conferences/fosdem2024/fosdem2024_formal/Makefile new file mode 100644 index 000000000..f99d01114 --- /dev/null +++ b/conferences/fosdem2024/fosdem2024_formal/Makefile @@ -0,0 +1,14 @@ +all: formal.pdf + +formal.pdf: formal.md states_enable.png states_one.png states_output.png \ + states_input.png states_verification.png states_complete.png \ + test_enable.png + +%.pdf: %.md + pandoc -t beamer $< -o $@ + +%.svg: %.dia + dia -e $*.svg $< + +%.png: %.svg + inkscape -w 800 -e $@ $*.svg diff --git a/conferences/fosdem2024/fosdem2024_formal/enable.dia b/conferences/fosdem2024/fosdem2024_formal/enable.dia new file mode 100644 index 000000000..6ea793740 Binary files /dev/null and b/conferences/fosdem2024/fosdem2024_formal/enable.dia differ diff --git a/conferences/fosdem2024/fosdem2024_formal/formal.md b/conferences/fosdem2024/fosdem2024_formal/formal.md new file mode 100644 index 000000000..bf26aa07e --- /dev/null +++ b/conferences/fosdem2024/fosdem2024_formal/formal.md @@ -0,0 +1,194 @@ +--- +title: Introduction to Formal Verification of Digital Circuits +author: Cesar Strauss +theme: Copenhagen +date: FOSDEM 2024 +--- +# Why Formal Verification? + +* A tool for finding bugs +* Complementary to simulation +* Helps finding corner cases +* ... triggered by specific sequences of events + +# Comparison with traditional debugging concepts + +| formal | traditional | +|--------------------------|-------------------| +| Cover | Simulation | +| Bounded Model Check | Unit test | +| k-Induction | Test fixture? | +| Exhaustive search | random test cases | +| synthesizable test-bench | can be procedural | +| "assume" inputs | test vectors | +| "assert" outputs | "assert" outputs | + +# Workflow + +* HDL: includes assertions +* SBY: work plan, drives the process +* Yosys: synthesizes to logic functions: + * state $s$: contents of all registers and inputs + * initial predicate: $I(s)$ + * transition relation $T(s_1, s_2)$ + * assertions: $P(s)$ + +* yosys-smtbmc: proves correctness or outputs a trace + + * exhaustive search for a path from the initial state to a bad state + * if not found, the design is correct + * if found, output an error trace + + +# Unbounded inductive proof + +* bad trace: + +$I(s_0) P(s_0) \wedge T(s_0,s_1)\overline{I(s_1)}P(s_1) +\wedge\dots\wedge T(s_{k-1},s_k)\overline{I(s_k)} +\overline{P(s_k)}$ + +* k $\leftarrow$ 0 +* base case: no path from initial state leads to a bad state in k steps +* inductive case: no path ending in a bad state can be reached in k+1 steps +* if inductive case fails, $k \leftarrow k + 1$ and repeat + +# Single register with feedback + +![](states_one.png) + +# Registered output with internal state + +![](states_output.png) + +# Registered output with enable + +![](states_enable.png) + +# Flip-flop with input + +![](states_input.png) + +# Verifying a flip-flop + +![](states_verification.png) + +# Complete flip-flop with input and enable + +![](states_complete.png) + +# Code for simple register with feedback + +```verilog +module simple(input clk); + +reg r = 0; + +always @(posedge clk) + r <= r; + +`ifdef FORMAL +always @* + assert(!r); +`endif +``` + +# SBY drive file + +``` +[options] +mode prove +depth 1 + +[engines] +smtbmc yices + +[script] +read_verilog -formal simple.v +prep -top simple + +[files] +simple.v +``` + +# Output (simplified) + +``` +$ sby simple.sby + +induction: Trying induction in step 1.. +induction: Trying induction in step 0.. +induction: Temporal induction successful. +basecase: Checking assumptions in step 0.. +basecase: Checking assertions in step 0.. +basecase: Status: passed +summary: engine_0 (smtbmc yices) returned pass + for induction +summary: engine_0 (smtbmc yices) returned pass + for basecase +summary: successful proof by k-induction. +DONE (PASS, rc=0) + +``` + +# Flip flop with enable (1/2) + +``` +from nmigen.asserts import Assert, Assume, Past +from nmutil.formaltest import FHDLTestCase +from nmigen import Signal, Module +import unittest + +class Formal(FHDLTestCase): + def test_enable(self): + m = Module() + r1 = Signal() + r2 = Signal() + s = Signal() + en = Signal() + m.d.sync += [r2.eq(r1), r1.eq(r2)] + with m.If(en): + m.d.sync += s.eq(r1 & r2) +``` +# Flip flop with enable (2/2) + +``` + m.d.comb += Assert(~s) + m.d.sync += Assume(Past(en) | en) + m.d.comb += Assert(~r1 & ~r2) + self.assertFormal(m, mode="prove", depth=5) + + +if __name__ == '__main__': + unittest.main() +``` + +# Induction failure example + +``` +summary: engine_0 returned pass for basecase +summary: engine_0 returned FAIL for induction +DONE (UNKNOWN, rc=4) +``` + +![](test_enable.png) + +# + +\centering {\Huge + +The End + +Thank you + +Questions? + +} + +* Discussion: http://lists.libre-soc.org +* Libera IRC \#libre-soc +* http://libre-soc.org/ +* http://nlnet.nl/entrust +* https://libre-soc.org/nlnet_2022_ongoing/ +* https://libre-soc.org/nlnet/\#faq +* https://git.libre-soc.org/?p=soc.git;a=tree;f=src/soc/experiment/formal;hb=HEAD diff --git a/conferences/fosdem2024/fosdem2024_formal/states_complete.dia b/conferences/fosdem2024/fosdem2024_formal/states_complete.dia new file mode 100644 index 000000000..a4556ed5f Binary files /dev/null and b/conferences/fosdem2024/fosdem2024_formal/states_complete.dia differ diff --git a/conferences/fosdem2024/fosdem2024_formal/states_enable.dia b/conferences/fosdem2024/fosdem2024_formal/states_enable.dia new file mode 100644 index 000000000..6c0583cba Binary files /dev/null and b/conferences/fosdem2024/fosdem2024_formal/states_enable.dia differ diff --git a/conferences/fosdem2024/fosdem2024_formal/states_input.dia b/conferences/fosdem2024/fosdem2024_formal/states_input.dia new file mode 100644 index 000000000..dab3127fa Binary files /dev/null and b/conferences/fosdem2024/fosdem2024_formal/states_input.dia differ diff --git a/conferences/fosdem2024/fosdem2024_formal/states_one.dia b/conferences/fosdem2024/fosdem2024_formal/states_one.dia new file mode 100644 index 000000000..bb3d5f466 Binary files /dev/null and b/conferences/fosdem2024/fosdem2024_formal/states_one.dia differ diff --git a/conferences/fosdem2024/fosdem2024_formal/states_output.dia b/conferences/fosdem2024/fosdem2024_formal/states_output.dia new file mode 100644 index 000000000..881dd21e5 Binary files /dev/null and b/conferences/fosdem2024/fosdem2024_formal/states_output.dia differ diff --git a/conferences/fosdem2024/fosdem2024_formal/states_verification.dia b/conferences/fosdem2024/fosdem2024_formal/states_verification.dia new file mode 100644 index 000000000..74cb75129 Binary files /dev/null and b/conferences/fosdem2024/fosdem2024_formal/states_verification.dia differ diff --git a/conferences/fosdem2024/fosdem2024_formal/test_enable.png b/conferences/fosdem2024/fosdem2024_formal/test_enable.png new file mode 100644 index 000000000..5a8acfa87 Binary files /dev/null and b/conferences/fosdem2024/fosdem2024_formal/test_enable.png differ