[spec] Specify execution order of side-effect-having statements (#1724)

* Define 'same clock' in a syntactic sense

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

spec/spec.tex

@@ -977,11 +977,17 @@ \subsection{Instances}\label{instances}
 
 To disallow infinitely recursive hardware, modules cannot contain instances of itself, either directly, or indirectly through instances of other modules it instantiates.
 
-\subsection{Stops}
+\subsection{Stops} \label{stop_stmt}
 The stop statement is used to halt simulations of the circuit. Backends are free to generate hardware to stop a running circuit for the purpose of debugging, but this is not required by the FIRRTL specification.
 
 A stop statement requires a clock signal, a halt condition signal that has a single bit unsigned integer type, and an integer exit code.
 
+For clocked statements that have side effects in the environment (stop, print, and verification
+statements), the order of execution of any such statements that are triggered on the same clock edge
+is determined by their syntactic order in the enclosing module. The order of execution of clocked,
+side-effect-having statements in different modules or with different clocks that trigger
+concurrently is undefined.
+
 \begin{lstlisting}
 wire clk:Clock
 wire halt:UInt<1>
@@ -994,6 +1000,9 @@ \subsection{Formatted Prints}
 
 A printf statement requires a clock signal, a print condition signal, a format string, and a variable list of argument signals. The condition signal must be a single bit unsigned integer type, and the argument signals must each have a ground type.
 
+For information about execution ordering of clocked statements with observable environmental side
+effects, see section \ref{stop_stmt}.
+
 \begin{lstlisting}
 wire clk:Clock
 wire condition:UInt<1>
@@ -1030,6 +1039,8 @@ \subsection{Verification}
 
 Backends are free to generate the corresponding model checking constructs in the target language, but this is not required by the FIRRTL specification. Backends that do not generate such constructs should issue a warning. For example, the SystemVerilog emitter produces SystemVerilog assert, assume and cover statements, but the Verilog emitter does not and instead warns the user if any verification statements are encountered.
 
+For information about execution ordering of clocked statements with observable environmental side
+effects, see section \ref{stop_stmt}.
 
 \subsubsection{Assert}