From: Cesar Strauss <cestrauss@gmail.com>
Date: Tue, 13 Feb 2024 13:43:27 +0000 (-0300)
Subject: bug 1220: add a few more slides with examples
X-Git-Url: https://git.libre-soc.org/?p=libreriscv.git;a=commitdiff_plain;h=1f429eeba125e65ba4649045196d043a4acac31d

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 b43b63175..e45fb553a 100644
--- 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 f99d01114..9012dc9f0 100644
--- 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 bf26aa07e..f9b32deef 100644
--- 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
index 000000000..6f030afc7
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 dab3127fa..43dfac0ee 100644
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
index 000000000..a99d28a2b
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
index 000000000..357469b82
Binary files /dev/null and b/conferences/fosdem2024/fosdem2024_formal/sum.dia differ