diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-04-18 16:23:37 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-04-18 16:23:37 +0100 |
| commit | 5432fc846a60bf6b2567cd5d1f886de052e34940 (patch) | |
| tree | a61db8522fae4e60ece814619c7e15c629bb5b06 /chapters/schedule.tex | |
| parent | dc7d1d5802348356a1c493330f5e290b7bdf7673 (diff) | |
| download | lsr22_fvhls-5432fc846a60bf6b2567cd5d1f886de052e34940.tar.gz lsr22_fvhls-5432fc846a60bf6b2567cd5d1f886de052e34940.zip | |
More work on all chapters
Diffstat (limited to 'chapters/schedule.tex')
| -rw-r--r-- | chapters/schedule.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/chapters/schedule.tex b/chapters/schedule.tex index 49d5251..bf62c59 100644 --- a/chapters/schedule.tex +++ b/chapters/schedule.tex @@ -42,7 +42,7 @@ proof. Vericert to pass through \SSA, as well as GSA, and finally generate dynamic HTL (or some other similar hardware language). During my visit at Inria Rennes, I worked with Sandrine Blazy and Delphine Demange to extend CompCertSSA~\cite[barthe14_formal_verif_ssa_based_middl_end_compc] with -\infull{GSA} (\GSA)~\cite[ottenstein90_progr_depen_web]. Not only should this allow for global +\GSA~\cite[ottenstein90_progr_depen_web]. Not only should this allow for global optimisations of \SSA\ code, but it should also allow for a more straightforward translation to hardware as the GSA code can just be viewed as a \DFG. Instead of working on modulo scheduling, it could therefore be interesting to work on a formally verified dynamic scheduling translation. |