From 5a89fca6090948d0a99c217a09c692e58a20d1df Mon Sep 17 00:00:00 2001
From: Kevin Laeufer
Date: Wed, 17 Feb 2021 12:16:52 -0800
Subject: Allow Side Effecting Statement to have Names (#2057)

* firrtl: add optional statement labels for stop, printf, assert, assume and cover

* test: parsing of statement labels

* ir: ensure that name is properly retained

* SymbolTable: add support for labled statements

* test: parsing statement labels

* test: lower types name collisions with named statements

* ignore empty names

* Inline: deal with named and unnamed statements

* RemoveWires: treat stop, printf and verification statements as "others"

* test: fix InlineInstance tests

* DeadCodeEliminations: statements are now als declarations

* CheckHighForm: ensure that statement names are not used as references

* CheckSpec: throw error if statement name collides

* add pass to automatically add missing statement names

* check: make sure that two statements cannot have the same name

* stmtLabel -> stmtName

* scalafmt

* add statement names to spec

* spec: meta data -> metadata

* EnsureStatementNames: explain naming algorithm

* remove returns

* better namespace use

* ir: add CanBeReferenced trait

* ir: add newline as jack requested---
 spec/spec.pdf | Bin 338200 -> 338944 bytes
 spec/spec.tex |  29 ++++++++++++++++++++++-------
 2 files changed, 22 insertions(+), 7 deletions(-)

(limited to 'spec')

diff --git a/spec/spec.pdf b/spec/spec.pdf
index 45dd4879..e392dec6 100644
Binary files a/spec/spec.pdf and b/spec/spec.pdf differ
diff --git a/spec/spec.tex b/spec/spec.tex
index 41de5d5e..8201b32e 100644
--- a/spec/spec.tex
+++ b/spec/spec.tex
@@ -989,10 +989,15 @@ is determined by their syntactic order in the enclosing module. The order of exe
 side-effect-having statements in different modules or with different clocks that trigger
 concurrently is undefined.
 
+The stop statement has an optional name attribute which can be used to
+attach metadata to the statement. The name is part of the module level
+namespace. However it can never be used in a reference since it is not of
+any valid type.
+
 \begin{lstlisting}
 wire clk:Clock
 wire halt:UInt<1>
-stop(clk,halt,42)
+stop(clk,halt,42) : optional_name
 ...
 \end{lstlisting}
 
@@ -1004,12 +1009,17 @@ A printf statement requires a clock signal, a print condition signal, a format s
 For information about execution ordering of clocked statements with observable environmental side
 effects, see section \ref{stop_stmt}.
 
+The printf statement has an optional name attribute which can be used to
+attach metadata to the statement. The name is part of the module level
+namespace. However it can never be used in a reference since it is not of
+any valid type.
+
 \begin{lstlisting}
 wire clk:Clock
 wire condition:UInt<1>
 wire a:UInt
 wire b:UInt
-printf(clk, condition, "a in hex: %x, b in decimal:%d.\n", a, b)
+printf(clk, condition, "a in hex: %x, b in decimal:%d.\n", a, b) : optional_name
 ...
 \end{lstlisting}
 
@@ -1043,6 +1053,11 @@ Backends are free to generate the corresponding model checking constructs in the
 For information about execution ordering of clocked statements with observable environmental side
 effects, see section \ref{stop_stmt}.
 
+Any verification statement has an optional name attribute which can be used to
+attach metadata to the statement. The name is part of the module level
+namespace. However it can never be used in a reference since it is not of
+any valid type.
+
 \subsubsection{Assert}
 
 The assert statement verifies that the predicate is true on the rising edge of any clock cycle when the enable is true. In other words, it verifies that enable implies predicate.
@@ -1053,7 +1068,7 @@ wire pred:UInt<1>
 wire en:UInt<1>
 pred <= eq(X, Y)
 en <= Z_valid
-assert(clk, pred, en, "X equals Y when Z is valid")
+assert(clk, pred, en, "X equals Y when Z is valid") : optional_name
 \end{lstlisting}
 
 \subsubsection{Assume}
@@ -1066,7 +1081,7 @@ wire pred:UInt<1>
 wire en:UInt<1>
 pred <= eq(X, Y)
 en <= Z_valid
-assume(clk, pred, en, "X equals Y when Z is valid")
+assume(clk, pred, en, "X equals Y when Z is valid") : optional_name
 \end{lstlisting}
 
 \subsubsection{Cover}
@@ -1079,7 +1094,7 @@ wire pred:UInt<1>
 wire en:UInt<1>
 pred <= eq(X, Y)
 en <= Z_valid
-cover(clk, pred, en, "X equals Y when Z is valid")
+cover(clk, pred, en, "X equals Y when Z is valid") : optional_name
 \end{lstlisting}
 
 \section{Expressions}
@@ -2108,8 +2123,8 @@ The concrete syntax of FIRRTL is defined in section \ref{syntax_tree}. Productio
                 &\pipe &\pd{exp} \vv{is invalid} \opt{\pd{info}}                                               &\text{Invalidate}\\
                 &\pipe &\vv{attach}\vv{(}\rpt{\pd{exp}}\vv{)} \opt{\pd{info}}                                  &\text{Attach}\\
                 &\pipe &\vv{when} \pd{exp} \vv{:} \opt{\pd{info}} \pd{stmt} \opt{\vv{else} \vv{:} \pd{stmt}}   &\text{Conditional}\\
-                &\pipe &\vv{stop(}\pd{exp}, \pd{exp}, \pd{int})\opt{\pd{info}}                                 &\text{Stop}\\
-                &\pipe &\vv{printf(}\pd{exp}, \pd{exp}, \pd{string}, \rpt{\pd{exp}}\vv{)} \opt{\pd{info}}      &\text{Printf}\\
+                &\pipe &\vv{stop(}\pd{exp}, \pd{exp}, \pd{int}) \opt{\vv{:}\pd{id}} \opt{\pd{info}}            &\text{Stop}\\
+                &\pipe &\vv{printf(}\pd{exp}, \pd{exp}, \pd{string}, \rpt{\pd{exp}}\vv{)} \opt{\vv{:}\pd{id}} \opt{\pd{info}}  &\text{Printf}\\
                 &\pipe &\vv{skip} \opt{\pd{info}}                                                              &\text{Empty}\\
                 &\pipe &\vv{(}\rpt{\pd{stmt}}\vv{)}                                                            &\text{Statement Group}\\
 \pd{ruw}        &=     &\vv{old} \pipe \vv{ new} \pipe \vv{ undefined}                                         &\text{Read Under Write Flag}\\
-- 
cgit v1.2.3