1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
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
|
