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
+memory.png
+stream.png
+sum.png
all: formal.pdf
formal.pdf: formal.md states_enable.png states_one.png states_output.png \
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 $@
%.pdf: %.md
pandoc -t beamer $< -o $@
-$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
\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
* 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
# Single register with feedback
self.assertFormal(m, mode="prove", depth=5)
self.assertFormal(m, mode="prove", depth=5)
if __name__ == '__main__':
unittest.main()
```
if __name__ == '__main__':
unittest.main()
```
+# 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)
+
* Discussion: http://lists.libre-soc.org
* Libera IRC \#libre-soc
* http://libre-soc.org/
* 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
* http://nlnet.nl/entrust
* https://libre-soc.org/nlnet_2022_ongoing/
* https://libre-soc.org/nlnet/\#faq