diff options
| -rw-r--r-- | algorithm.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/algorithm.tex b/algorithm.tex index 8323cfb..fb70bee 100644 --- a/algorithm.tex +++ b/algorithm.tex @@ -189,7 +189,7 @@ endmodule \end{minted} \caption{Verilog always block describing the control logic of the module.}\label{fig:accumulator_v_2} \end{subfigure} - \caption{Accumulator example using \vericert{} to translate the 3AC to a state machine expressed in Verilog.}\label{fig:accumulator_v} + \caption{Accumulator example using \vericert{} to translate the 3AC to a state machine expressed in Verilog. \JW{If space permits, it would probably be preferable to have this code in a single column, as splitting a single module across two subfigures is a bit jarring.}}\label{fig:accumulator_v} \end{figure} To check that the initial state of the Verilog is the same as the HTL code, we therefore have to run the module once, assuming the state is undefined and the reset is set to high. We then have to compare the abstract starting state stored in the HTL module to the bitvector value we obtain from running the module for one clock cycle and prove that they are the same. As the value for the state is undefined, the case statements will evaluate to the default state and therefore not perform any computations. |