bug 1220: add a few more slides with examples

[libreriscv.git] / conferences / fosdem2024 / fosdem2024_formal / formal.md

diff --git a/conferences/fosdem2024/fosdem2024_formal/formal.md b/conferences/fosdem2024/fosdem2024_formal/formal.md
index bf26aa07ef278b469ad37f8f31275d5f0e9f5939..f9b32deefbf332767b2e671603736a70038726cf 100644 (file)
--- a/conferences/fosdem2024/fosdem2024_formal/formal.md
+++ b/conferences/fosdem2024/fosdem2024_formal/formal.md
@@ -44,14 +44,16 @@ date: FOSDEM 2024
 
 * 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)}
+$I(s_0) P(s_0) \wedge T(s_0,s_1)P(s_1)
+\wedge\dots\wedge T(s_{k-1},s_k)
 \overline{P(s_k)}$
 
 * k $\leftarrow$ 0
 * base case: no path from initial state leads to a bad state in k steps
+* if base case fails, report the bad trace
 * 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
+* otherwise, proof is complete, circuit is safe.
 
 # Single register with feedback
 
@@ -159,6 +161,8 @@ class Formal(FHDLTestCase):
         self.assertFormal(m, mode="prove", depth=5)
 
 
+
+
 if __name__ == '__main__':
     unittest.main()
 ```
@@ -173,6 +177,27 @@ DONE (UNKNOWN, rc=4)
 
 ![](test_enable.png)
 
+# Verifying memories with a "victim address"
+
+![](memory.png)
+
+# Verifying streams with transaction counters
+
+![](stream.png)
+
+# Dynamic SIMD
+
+```
+exp-a    : ....0....0....0.... 1x 32-bit
+exp-a    : ....0....0....1.... 1x 24-bit plus 1x 8-bit
+exp-a    : ....0....1....0.... 2x 16-bit
+...
+...
+exp-a    : ....1....1....0.... 2x 8-bit, 1x 16-bit
+exp-a    : ....1....1....1.... 4x 8-bit
+```
+![](sum.png)
+
 #
 
 \centering {\Huge
@@ -188,6 +213,7 @@ Questions?
 * Discussion: http://lists.libre-soc.org
 * Libera IRC \#libre-soc
 * http://libre-soc.org/
+* https://libre-soc.org/resources/
 * http://nlnet.nl/entrust
 * https://libre-soc.org/nlnet_2022_ongoing/
 * https://libre-soc.org/nlnet/\#faq