bug 1220: add a few more slides with examples

I did a practice run of the talk, and turns out I still had time to
show some more examples.
Added: verification of memories, streams and partitioned SIMD

diff --git a/conferences/fosdem2024/fosdem2024_formal/.gitignore b/conferences/fosdem2024/fosdem2024_formal/.gitignore
index b43b63175d99b2c496133b46b280b82b440cb5f7..e45fb553a00a6338fe003c3fcd3ed2a329f5d12e 100644 (file)
--- a/conferences/fosdem2024/fosdem2024_formal/.gitignore
+++ b/conferences/fosdem2024/fosdem2024_formal/.gitignore
@@ -1,2 +1,5 @@
 formal.pdf
 states_*.png
+memory.png
+stream.png
+sum.png

diff --git a/conferences/fosdem2024/fosdem2024_formal/Makefile b/conferences/fosdem2024/fosdem2024_formal/Makefile
index f99d01114078db531823e8ed1c88bb1c02d57ee1..9012dc9f023c134914b2ea63b8437fde64b5af48 100644 (file)
--- a/conferences/fosdem2024/fosdem2024_formal/Makefile
+++ b/conferences/fosdem2024/fosdem2024_formal/Makefile
@@ -1,8 +1,8 @@
 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
+            states_input.png states_verification.png states_complete.png \
+            test_enable.png memory.png stream.png sum.png
 
 %.pdf: %.md
        pandoc -t beamer $< -o $@

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

diff --git a/conferences/fosdem2024/fosdem2024_formal/memory.dia b/conferences/fosdem2024/fosdem2024_formal/memory.dia
new file mode 100644 (file)
index 0000000..6f030af
Binary files /dev/null and b/conferences/fosdem2024/fosdem2024_formal/memory.dia differ

diff --git a/conferences/fosdem2024/fosdem2024_formal/states_input.dia b/conferences/fosdem2024/fosdem2024_formal/states_input.dia
index dab3127fafb7528e06ee5e95a36bf42abb8a2c78..43dfac0ee9f33f221f08867cdf78048d0a8f07e5 100644 (file)
Binary files a/conferences/fosdem2024/fosdem2024_formal/states_input.dia and b/conferences/fosdem2024/fosdem2024_formal/states_input.dia differ

diff --git a/conferences/fosdem2024/fosdem2024_formal/stream.dia b/conferences/fosdem2024/fosdem2024_formal/stream.dia
new file mode 100644 (file)
index 0000000..a99d28a
Binary files /dev/null and b/conferences/fosdem2024/fosdem2024_formal/stream.dia differ

diff --git a/conferences/fosdem2024/fosdem2024_formal/sum.dia b/conferences/fosdem2024/fosdem2024_formal/sum.dia
new file mode 100644 (file)
index 0000000..357469b
Binary files /dev/null and b/conferences/fosdem2024/fosdem2024_formal/sum.dia differ