[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>

2 files changed, 12 insertions, 1 deletions

diff --git a/spec/spec.pdf b/spec/spec.pdf
index 15916d6c..26be49e6 100644
--- a/spec/spec.pdf
+++ b/spec/spec.pdf
diff --git a/spec/spec.tex b/spec/spec.tex
index 64965539..d65078bc 100644
--- a/spec/spec.tex
+++ b/spec/spec.tex
@@ -977,11 +977,17 @@ Modules have the property that instances can always be {\em inlined} into the pa
 
 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 @@ The formatted print statement is used to print a formatted string during simulat
 
 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 @@ To facilitate simulation, model checking and formal methods, there are three non
 
 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}