% \subsection{Initial state}
% How to specify the initial state? Cannot be done inside a hardware
% function, since the initial state is its own state argument for the first
% \subsection{Initial state}
% How to specify the initial state? Cannot be done inside a hardware
% function, since the initial state is its own state argument for the first