From: Cesar Strauss 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/?a=commitdiff_plain;h=1f429eeba125e65ba4649045196d043a4acac31d;p=libreriscv.git 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