1 files changed, 56 insertions, 0 deletions
diff --git a/content/zettel/1c3.md b/content/zettel/1c3.md
new file mode 100644
index 0000000..5436bf5
--- /dev/null
+++ b/content/zettel/1c3.md
@@ -0,0 +1,56 @@
++++
+title = "Dynamic Scheduling"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["1c2", "1c1", "1c"]
+forwardlinks = ["1a2", "3c3", "1c4", "1c3a"]
+zettelid = "1c3"
++++
+
+Dynamic scheduling \[1\] is a really interesting way of generating
+circuits, because one does not have to perform as much static analysis,
+and one does not have to really place operations into specific clock
+cycles.
+
+Dynamic scheduling can be modelled using petri-nets ([\#1a2]), where
+only a few basic components are enough to model any computation which is
+scheduled dynamically, meaning the actual execution times of each
+section are not important to the correctness.
+
+In terms of proving scheduling correct ([\#3c3]), it might actually be
+simpler with dynamic scheduling, assuming that each of the components
+are assumed to be correct. However, if the components need to be proven
+correct as well, then it might be more difficult, as it is not quite
+clear yet if proving components in the Verilog semantics \[2\] is
+feasible, or if a separate translation is needed.
+
+<div id="refs" class="references csl-bib-body" markdown="1">
+
+<div id="ref-carmona09_elast_circuit" class="csl-entry" markdown="1">
+
+<span class="csl-left-margin">\[1\]
+</span><span class="csl-right-inline">J. Carmona, J. Cortadella, M.
+Kishinevsky, and A. Taubin, “Elastic circuits,” *IEEE Transactions on
+Computer-Aided Design of Integrated Circuits and Systems*, vol. 28, no.
+10, pp. 1437–1455, 2009.</span>
+
+</div>
+
+<div id="ref-loeoew19_proof_trans_veril_devel_hol" class="csl-entry"
+markdown="1">
+
+<span class="csl-left-margin">\[2\]
+</span><span class="csl-right-inline">A. Lööw and M. O. Myreen, “A
+proof-producing translator for verilog development in HOL,” in
+*Proceedings of the 7th international workshop on formal methods in
+software engineering*, in FormaliSE ’19. Montreal, Quebec, Canada: IEEE
+Press, 2019, pp. 99–108. doi: [10.1109/FormaliSE.2019.00020].</span>
+
+</div>
+
+</div>
+
+  [\#1a2]: /zettel/1a2
+  [\#3c3]: /zettel/3c3
+  [10.1109/FormaliSE.2019.00020]: https://doi.org/10.1109/FormaliSE.2019.00020