diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-04-16 09:13:30 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-04-16 09:13:40 +0100 |
| commit | 84fc88390e37b82a8dbdd54889736b03ea00f0ef (patch) | |
| tree | 32b1b71535576d1032b989958c631ca62796e04e /proof.tex | |
| parent | 92d7fcff745a33083336d42828d1ad9853269b03 (diff) | |
| download | oopsla21_fvhls-84fc88390e37b82a8dbdd54889736b03ea00f0ef.tar.gz oopsla21_fvhls-84fc88390e37b82a8dbdd54889736b03ea00f0ef.zip | |
Add proof
Diffstat (limited to 'proof.tex')
| -rw-r--r-- | proof.tex | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -109,7 +109,7 @@ We can now define the simulation diagram for the translation. The 3AC state can \subsection{Forward simulation of RAM insertion}\label{sec:proof:ram_insertion} -HTL can only represent a single state machine, it is therefore necessary to model +HTL can only represent a single state machine, it is therefore necessary to model the RAM abstractly to reason about the correctness of replacing the direct read and writes to the array to load and stores to a RAM. The abstract specification used for the RAM is shown in Figure~\ref{fig_htl_ram_spec}, which defines how the RAM $r$ will behave with all the possible combinations of the input signals. \begin{figure} \centering |