path: root/spec/spec.tex

% SPDX-License-Identifier: Apache-2.0

%Useful Macros
\newcommand{\id}{\text{id }}
\newcommand{\idst}{\text{id*}}
\newcommand{\ids}{\text{id}}
\newcommand{\ints}{\text{int}}
\newcommand{\intsp}{\text{int }}
\newcommand{\strings}{\text{string}}
\newcommand{\stringsp}{\text{string }}
\newcommand{\kw}[1]{\text{\bf #1\ }}
\newcommand{\kws}[1]{\text{\bf #1}}
\newcommand{\pds}[1]{\text{\em #1\ }}
\newcommand{\pd}[1]{\text{\em #1}}
\newcommand{\bundleT}[1]{\{#1\}}
\newcommand{\info}{[\pds{info}]\ }
\newcommand{\version}{0.2.0}

\renewcommand{\arraystretch}{1.15}

\title{Specification for the FIRRTL Language}
\author{Patrick S. Li \\ \href{mailto:psli@eecs.berkeley.edu}{psli@eecs.berkeley.edu}
   \and Adam M. Izraelevitz \\ \href{mailto:adamiz@eecs.berkeley.edu}{adamiz@eecs.berkeley.edu}
   \and Jonathan Bachrach \\ \href{mailto:jrb@eecs.berkeley.edu}{jrb@eecs.berkeley.edu} }
\documentclass[12pt]{article}
\usepackage{listings}
\usepackage{amsmath}
\usepackage{proof}
\usepackage{amsfonts}
\usepackage{enumitem}
\usepackage{multirow}
\usepackage{hyperref}
\hypersetup{
    colorlinks=true,
    linkcolor=blue,
    filecolor=magenta,
    urlcolor=cyan,
}
\usepackage[pdftex]{graphicx}
\usepackage{fancyhdr}
\usepackage{fixltx2e}
\usepackage{float}
\usepackage{stmaryrd}

\pagestyle{fancy}
\lhead{Specification for the FIRRTL Language}
\rhead{Version \version}
\renewcommand{\headrulewidth}{0.4pt}
\renewcommand{\footrulewidth}{0.4pt}
\lstset{
    basicstyle=\footnotesize\ttfamily,
    breaklines=true,
    numberstyle=\tiny,
    captionpos=b,
    caption=\lstname,
    morekeywords={circuit,module,input,output,flip,wire,reg,is,invalid,when,else,skip},
    keywordstyle=\color{blue}
}

\begin{document}
\maketitle
\tableofcontents
\newpage


\section{Introduction}

\subsection{Background}
The ideas for FIRRTL (Flexible Intermediate Representation for RTL) originated from work on Chisel, a hardware description language (HDL) embedded in Scala used for writing highly-parameterized circuit design generators. Chisel designers manipulate circuit components using Scala functions, encode their interfaces in Scala types, and use Scala's object-orientation features to write their own circuit libraries. This form of meta-programming enables expressive, reliable and type-safe generators that improve RTL design productivity and robustness.

The computer architecture research group at U.C. Berkeley relies critically on Chisel to allow small teams of graduate students to design sophisticated RTL circuits. Over a three year period with under twelve graduate students, the architecture group has taped-out over ten different designs.

Internally, the investment in developing and learning Chisel was rewarded with huge gains in productivity. However, Chisel's external rate of adoption was slow for the following reasons.
\begin{enumerate}[topsep=3pt,itemsep=-0.5ex,partopsep=1ex,parsep=1ex]
\item Writing custom circuit transformers requires intimate knowledge about the internals of the Chisel compiler.
\item Chisel semantics are under-specified and thus impossible to target from other languages.
\item Error checking is unprincipled due to under-specified semantics resulting in incomprehensible error messages.
\item Learning a functional programming language (Scala) is difficult for RTL designers with limited programming language experience.
\item Confounding the previous point, conceptually separating the embedded Chisel HDL from the host language is difficult for new users.
\item The output of Chisel (Verilog) is unreadable and slow to simulate.
\end{enumerate}

As a consequence, Chisel needed to be redesigned from the ground up to standardize its semantics, modularize its compilation process, and cleanly separate its front-end, intermediate representation, and backends. A well defined intermediate representation (IR) allows the system to be targeted by other HDLs embedded in other host programming languages, making it possible for RTL designers to work within a language they are already comfortable with. A clearly defined IR with a concrete syntax also allows for inspection of the output of circuit generators and transformers thus making clear the distinction between the host language and the constructed circuit. Clearly defined semantics allows users without knowledge of the compiler implementation to write circuit transformers; examples include optimization of circuits for simulation speed, and automatic insertion of signal activity counters. An additional benefit of a well defined IR is the structural invariants that can be enforced before and after each compilation stage, resulting in a more robust compiler and structured mechanism for error checking.

\subsection{Design Philosophy}
FIRRTL represents the standardized elaborated circuit that the Chisel HDL produces. FIRRTL represents the circuit immediately after Chisel's elaboration but before any circuit simplification. It is designed to resemble the Chisel HDL after all meta-programming has executed. Thus, a user program that makes little use of meta-programming facilities should look almost identical to the generated FIRRTL.

For this reason, FIRRTL has first-class support for high-level constructs such as vector types, bundle types, conditional statements, partial connects, and modules. These high-level constructs are then gradually removed by a sequence of {\em lowering} transformations. During each lowering transformation, the circuit is rewritten into an equivalent circuit using simpler, lower-level constructs. Eventually the circuit is simplified to its most restricted form, resembling a structured netlist, which allows for easy translation to an output language (e.g. Verilog). This form is given the name {\em lowered FIRRTL} (LoFIRRTL) and is a strict subset of the full FIRRTL language.

Because the host language is now used solely for its meta-programming facilities, the frontend can be very light-weight, and additional HDLs written in other languages can target FIRRTL and reuse the majority of the compiler toolchain.

\section{Acknowledgments}
The FIRRTL language could not have been developed without the help of many of the faculty and students in the ASPIRE lab, and the University of California, Berkeley.

This project originated from discussions with the authors' advisor, Jonathan Bachrach, who indicated the need for a structural redesign of the Chisel system around a well-defined intermediate representation. Patrick Li designed and implemented the first prototype of the FIRRTL language, wrote the initial specification for the language, and presented it to the Chisel group consisting of Adam Izraelevitz, Scott Beamer, David Biancolin, Christopher Celio, Henry Cook, Palmer Dabbelt, Donggyu Kim, Jack Koenig, Martin Maas, Albert Magyar, Colin Schmidt, Andrew Waterman, Yunsup Lee, Richard Lin, Eric Love, Albert Ou, Stephen Twigg, John Bachan, David Donofrio, Farzad Fatollahi-Fard, Jim Lawson, Brian Richards, Krste Asanovi\'c, and John Wawrzynek.

Adam Izraelevitz then reworked the design and re-implemented FIRRTL, and after many discussions with Patrick Li and the Chisel group, refined the design to its present version.

The authors would like to thank the following individuals in particular for their contributions to the FIRRTL project:
\begin{itemize}
\item Andrew Waterman: for his many contributions to the design of FIRRTL's constructs, for his work on Chisel 3.0, and for porting architecture research infrastructure
\item Richard Lin: for improving the Chisel 3.0 code base for release quality
\item Jack Koenig: for implementing the FIRRTL parser in Scala
\item Henry Cook: for porting and cleaning up many aspects of Chisel 3.0, including the testing infrastructure and the parameterization library
\item Chick Markley: for creating the new testing harness and porting the Chisel tutorial
\item Stephen Twigg: for his expertise in hardware intermediate representations and for providing many corner cases to consider
\item Palmer Dabbelt, Eric Love, Martin Maas, Christopher Celio, and Scott Beamer: for their feedback on previous drafts of the FIRRTL specification
\end{itemize}

And finally this project would not have been possible without the continuous feedback and encouragement of Jonathan Bachrach, and his leadership on and implementation of Chisel.

This research was partially funded by DARPA Award Number HR0011-12-2-0016, the Center for Future Architecture Research, a member of STARnet, a Semiconductor Research Corporation program sponsored by MARCO and DARPA, and ASPIRE Lab industrial sponsors and affiliates Intel, Google, Huawei, Nokia, NVIDIA, Oracle, and Samsung. Any opinions, findings, conclusions, or recommendations in this paper are solely those of the authors and does not necessarily reflect the position or the policy of the sponsors.

\section{Circuits and Modules}

\subsection{Circuits}
All FIRRTL circuits consist of a list of modules, each representing a hardware block that can be instantiated. The circuit must specify the name of the top-level module.

\begin{lstlisting}
circuit MyTop :
   module MyTop :
      ...
   module MyModule :
      ...
\end{lstlisting}

\subsection{Modules}
Each module has a given name, a list of ports, and a statement representing the circuit connections within the module. A module port is specified by its \pd{direction}, which may be input or output, a name, and the data type of the port.

The following example declares a module with one input port, one output port, and one statement connecting the input port to the output port. See section \ref{connects} for details on the connect statement.

\begin{lstlisting}
module MyModule :
   input foo: UInt
   output bar: UInt
   bar <= foo
\end{lstlisting}

Note that a module definition does {\em not} indicate that the module will be physically present in the final circuit. Refer to the description of the instance statement for details on how to instantiate a module (section \ref{instances}).

\subsection{Externally Defined Modules}
Externally defined modules are modules whose implementation is not provided in the current circuit.
Only the ports and name of the externally defined module are specified in the circuit.
An externally defined module may include, in order, an optional \emph{defname} which sets the name of the external module in the resulting Verilog and zero or more name--value \emph{parameter} statements.
Each name--value parameter statement will result in a value being passed to the named parameter in the resulting Verilog.

An example of an externally defined module is:

\begin{lstlisting}
extmodule MyExternalModule :
   input foo: UInt<2>
   output bar: UInt<4>
   output baz: SInt<8>
   defname = VerilogName
   parameter x = "hello"
   parameter y = 42
\end{lstlisting}

The widths of all externally defined module ports must be specified.
Width inference, described in section \ref{width_inference}, is not supported for module ports.

A common use of an externally defined module is to represent a Verilog module that will be written separately and provided together with FIRRTL-generated Verilog to downstream tools.

% The following example is the port declaration of a module that spans two clock domains.

% \[
% \begin{aligned}
% &\kw{module} TwoClock : \\
% &\quad \kw{input} clk1 : \kw{Clock}\\
% &\quad \kw{input} clk2 : \kw{Clock}\\
% &\quad ... \\
% \end{aligned}
% \]

\section{Types}

Types are used to specify the structure of the data held by each circuit component. All types in FIRRTL are either one of the fundamental ground types or are built up from aggregating other types.

\subsection{Ground Types}

There are five ground types in FIRRTL: an unsigned integer type, a signed integer type, a fixed-point number type, a clock type, and an analog type.

\subsubsection{Integer Types}

Both unsigned and signed integer types may optionally be given a known non-negative integer bit width.

\begin{lstlisting}
UInt<10>
SInt<32>
\end{lstlisting}

Alternatively, if the bit width is omitted, it will be automatically inferred by FIRRTL's width inferencer, as detailed in section \ref{width_inference}.

\begin{lstlisting}
UInt
SInt
\end{lstlisting}

\subsubsection{Fixed-Point Number Type}

In general, a fixed-point binary number type represents a range of values corresponding with the
range of some integral type scaled by a fixed power of two. In the FIRRTL language, the number
represented by a signal of fixed-point type may expressed in terms of a base integer \emph{value}
term and a \emph{binary point}, which represents an inverse power of two.

The range of the value term is governed by a \emph{width} an a manner analogous to integral types,
with the additional restriction that all fixed-point number types are inherently signed in FIRRTL.
Whenever an operation such as a \verb|cat| operates on the ``bits'' of a fixed-point number, it
operates on the string of bits that is the signed representation of the integer value term. The
\emph{width} of a fixed-point typed signal is the width of this string of bits.

\begin{align*}
  \text{fixed-point quantity} &= \left( \text{integer value} \right) \times 2^{-\left(\text{binary point}\right)}\\
  \text{integer value} &\in \left[ -2^{(\text{width})-1}, 2^{(\text{width})-1} \right)\\
  \text{binary point} &\in \mathbb{Z}
\end{align*}

In the above equation, the range of possible fixed-point quantities is governed by two parameters
beyond a the particular ``value'' assigned to a signal: the width and the binary point. Note that
when the binary point is positive, it is equivalent to the number of bits that would fall after the
binary point. Just as width is a parameter of integer types in FIRRTL, width and binary point are
both parameters of the fixed-point type.

When declaring a component with fixed-point number type, it is possible to leave the width and/or
the binary point unspecified. The unspecified parameters will be inferred to be sufficient to hold
the results of all expressions that may drive the component. Similar to how width inference for
integer types depends on width-propagation rules for each FIRRTL expression and each kind of
primitive operator, fixed-point parameter inference depends on a set of rules outlined throughout
this spec.

Included below are examples of the syntax for all possible combinations of specified and inferred
fixed-point type parameters.
\begin{lstlisting}
Fixed<3><<2>>    ; 3-bit width, 2 bits after binary point
Fixed<10>        ; 10-bit width, inferred binary point
Fixed<<-4>>      ; Inferred width, binary point of -4
Fixed            ; Inferred width and binary point
\end{lstlisting}

\subsubsection{Clock Type}

The clock type is used to describe wires and ports meant for carrying clock signals. The usage of components with clock types are restricted. Clock signals cannot be used in most primitive operations, and clock signals can only be connected to components that have been declared with the clock type.

The clock type is specified as follows:
\begin{lstlisting}
Clock
\end{lstlisting}

\subsubsection{Analog Type}

The analog type specifies that a wire or port can be attached to multiple drivers. \verb|Analog|
cannot be used as the type of a node or register, nor can it be used as the datatype of a memory. In
this respect, it is similar to how \verb|inout| ports are used in Verilog, and FIRRTL analog signals
are often used to interface with external Verilog or VHDL IP.

In contrast with all other ground types, analog signals cannot appear on either side of a connection
statement. Instead, analog signals are attached to each other with the commutative \verb|attach|
statement. An analog signal may appear in any number of attach statements, and a legal circuit may
also contain analog signals that are never attached. The only primitive operations that may be
applied to analog signals are casts to other signal types.

When an analog signal appears as a field of an aggregate type, the aggregate cannot appear in a
standard connection statement; however, the partial connection statement will \verb|attach|
corresponding analog fields of its operands according to the partial connection algorithm described
in Section \ref{partial_connection_algorithm}.

As with integer types, an analog type can represent a multi-bit signal. When analog signals are not
given a concrete width, their widths are inferred according to a highly restrictive width inference
rule, which requires that the widths of all arguments to a given attach operation be identical.

\begin{lstlisting}
Analog<1>  ; 1-bit analog type
Analog<32> ; 32-bit analog type
Analog     ; analog type with inferred width
\end{lstlisting}

\subsection{Vector Types}

A vector type is used to express an ordered sequence of elements of a given type. The length of the sequence must be non-negative and known.

The following example specifies a ten element vector of 16-bit unsigned integers.
\begin{lstlisting}
UInt<16>[10]
\end{lstlisting}

The next example specifies a ten element vector of unsigned integers of omitted but identical bit widths.
\begin{lstlisting}
UInt[10]
\end{lstlisting}

Note that any type, including other aggregate types, may be used as the element type of the vector. The following example specifies a twenty element vector, each of which is a ten element vector of 16-bit unsigned integers.
\begin{lstlisting}
UInt<16>[10][20]
\end{lstlisting}

\subsection{Bundle Types}

A bundle type is used to express a collection of nested and named types. All fields in a bundle type must have a given name, and type.

The following is an example of a possible type for representing a complex number. It has two fields, \verb|real|, and \verb|imag|, both 10-bit signed integers.
\begin{lstlisting}
{real:SInt<10>, imag:SInt<10>}
\end{lstlisting}

Additionally, a field may optionally be declared with a {\em flipped} orientation.
\begin{lstlisting}
{word:UInt<32>, valid:UInt<1>, flip ready:UInt<1>}
\end{lstlisting}
In a connection between circuit components with bundle types, the data carried by the flipped fields flow in the opposite direction as the data carried by the non-flipped fields.

As an example, consider a module output port declared with the following type:
\begin{lstlisting}
output a: {word:UInt<32>, valid:UInt<1>, flip ready:UInt<1>}
\end{lstlisting}
In a connection to the \verb|a| port, the data carried by the \verb|word| and \verb|valid| sub-fields will flow out of the module, while data carried by the \verb|ready| sub-field will flow into the module. More details about how the bundle field orientation affects connections are explained in section \ref{connects}.

As in the case of vector types, a bundle field may be declared with any type, including other aggregate types.
\begin{lstlisting}
{real: {word:UInt<32>, valid:UInt<1>, flip ready:UInt<1>}
 imag: {word:UInt<32>, valid:UInt<1>, flip ready:UInt<1>}}
\end{lstlisting}

When calculating the final direction of data flow, the orientation of a field is applied recursively to all nested types in the field. As an example, consider the following module port declared with a bundle type containing a nested bundle type.
\begin{lstlisting}
output myport: {a: UInt, flip b: {c: UInt, flip d:UInt}}
\end{lstlisting}
In a connection to \verb|myport|, the \verb|a| sub-field flows out of the module. The \verb|c| sub-field contained in the \verb|b| sub-field flows into the module, and the \verb|d| sub-field contained in the \verb|b| sub-field flows out of the module.

\subsection{Passive Types} \label{passive_types}

It is inappropriate for some circuit components to be declared with a type that allows for data to flow in both directions. For example, all sub-elements in a memory should flow in the same direction. These components are restricted to only have a passive type.

Intuitively, a passive type is a type where all data flows in the same direction, and is defined to be a type that recursively contains no fields with flipped orientations. Thus all ground types are passive types. Vector types are passive if their element type is passive. And bundle types are passive if no fields are flipped and if all field types are passive.

\subsection{Type Equivalence} \label{type_equivalence}

The type equivalence relation is used to determine whether a connection between two components is legal. See section \ref{connects} for further details about connect statements.

An unsigned integer type is always equivalent to another unsigned integer type regardless of bit width, and is not equivalent to any other type. Similarly, a signed integer type is always equivalent to another signed integer type regardless of bit width, and is not equivalent to any other type.

A fixed-point number type is always equivalent to another fixed-point number type, regardless of width or binary point. It is not equivalent to any other type.

Clock types are equivalent to clock types, and are not equivalent to any other type.

Two vector types are equivalent if they have the same length, and if their element types are equivalent.

Two bundle types are equivalent if they have the same number of fields, and both the bundles' i'th fields have matching names and orientations, as well as equivalent types. Consequently, \verb|{a:UInt, b:UInt}| is not equivalent to \verb|{b:UInt, a:UInt}|, and \verb|{a: {flip b:UInt}}| is not equivalent to \verb|{flip a: {b: UInt}}|.

\subsection{Weak Type Equivalence} \label{weak_type_equivalence}

The weak type equivalence relation is used to determine whether a partial connection between two components is legal. See section \ref{partial_connects} for further details about partial connect statements.

Two types are weakly equivalent if their corresponding oriented types are equivalent.

\subsubsection{Oriented Types}
The weak type equivalence relation requires first a definition of {\em oriented types}. Intuitively, an oriented type is a type where all orientation information is collated and coupled with the leaf ground types instead of in bundle fields.

An oriented ground type is an orientation coupled with a ground type. An oriented vector type is an ordered sequence of positive length of elements of a given oriented type. An oriented bundle type is a collection of oriented fields, each containing a name and an oriented type, but no orientation.

Applying a flip orientation to an oriented type recursively reverses the orientation of every oriented ground type contained within. Applying a non-flip orientation to an oriented type does nothing.

\subsubsection{Conversion to Oriented Types}
To convert a ground type to an oriented ground type, attach a non-flip orientation to the ground type.

To convert a vector type to an oriented vector type, convert its element type to an oriented type, and retain its length.

To convert a bundle field to an oriented field, convert its type to an oriented type, apply the field orientation, and combine this with the original field's name to create the oriented field. To convert a bundle type to an oriented bundle type, convert each field to an oriented field.

\subsubsection{Oriented Type Equivalence}
Two oriented ground types are equivalent if their orientations match and their types are equivalent.

Two oriented vector types are equivalent if their element types are equivalent.

Two oriented bundle types are not equivalent if there exists two fields, one from each oriented bundle type, that have identical names but whose oriented types are not equivalent. Otherwise, the oriented bundle types are equivalent.

As stated earlier, two types are weakly equivalent if their corresponding oriented types are equivalent.


\section{Statements} \label{statements}

Statements are used to describe the components within a module and how they interact.

\subsection{Connects}\label{connects}
The connect statement is used to specify a physically wired connection between two circuit components.

The following example demonstrates connecting a module's input port to its output port, where port \verb|myinput| is connected to port \verb|myoutput|.
\begin{lstlisting}
module MyModule :
   input myinput: UInt
   output myoutput: UInt
   myoutput <= myinput
\end{lstlisting}

In order for a connection to be legal the following conditions must hold:
\begin{enumerate}
\item The types of the left-hand and right-hand side expressions must be equivalent (see section \ref{type_equivalence} for details).
\item The bit widths of the two expressions must allow for data to always flow from a smaller bit width to an equal size or larger bit width.
\item The flow of the left-hand side expression must be sink or duplex (see section \ref{flows} for an explanation of flow).
\item Either the flow of the right-hand side expression is source or duplex, or the right-hand side expression has a passive type.
\end{enumerate}

Connect statements from a narrower ground type component to a wider ground type component will have its value automatically sign-extended or zero-extended to the larger bit width. The behaviour of connect statements between two circuit components with aggregate types is defined by the connection algorithm in section \ref{connection_algorithm}.

\subsubsection{The Connection Algorithm} \label{connection_algorithm}
Connect statements between ground types cannot be expanded further.

Connect statements between two vector typed components recursively connects each sub-element in the right-hand side expression to the corresponding sub-element in the left-hand side expression.

Connect statements between two bundle typed components connects the i'th field of the right-hand side expression and the i'th field of the left-hand side expression. If the i'th field is not flipped, then the right-hand side field is connected to the left-hand side field. Conversely, if the i'th field is flipped, then the left-hand side field is connected to the right-hand side field.

\subsection{Partial Connects}\label{partial_connects}
Like the connect statement, the partial connect statement is also used to specify a physically wired connection between two circuit components. However, it enforces fewer restrictions on the types and widths of the circuit components it connects.

In order for a partial connect to be legal the following conditions must hold:
\begin{enumerate}
\item The types of the left-hand and right-hand side expressions must be weakly equivalent (see section \ref{weak_type_equivalence} for details).
\item The flow of the left-hand side expression must be sink or duplex (see section \ref{flow} for an explanation of flow).
\item Either the flow of the right-hand side expression is source or duplex, or the right-hand side expression has a passive type.
\end{enumerate}

Partial connect statements from a narrower ground type component to a wider ground type component will have its value automatically sign-extended to the larger bit width. Partial connect statements from a wider ground type component to a narrower ground type component will have its value automatically truncated to fit the smaller bit width.

Intuitively, bundle fields with matching names will be connected appropriately, while bundle fields not present in both types will be ignored. Similarly, vectors with mismatched lengths will be connected up to the shorter length, and the remaining sub-elements are ignored. The full algorithm is detailed in section \ref{partial_connection_algorithm}.

The following example demonstrates partially connecting a module's input port to its output port, where port \verb|myinput| is connected to port \verb|myoutput|.
\begin{lstlisting}
module MyModule :
   input myinput: {flip a:UInt, b:UInt[2]}
   output myoutput: {flip a:UInt, b:UInt[3], c:UInt}
   myoutput <- myinput
\end{lstlisting}

The above example is equivalent to the following:
\begin{lstlisting}
module MyModule :
   input myinput: {flip a:UInt, b:UInt[2]}
   output myoutput: {flip a:UInt, b:UInt[3], c:UInt}
   myinput.a <- myoutput.a
   myoutput.b[0] <- myinput.b[0]
   myoutput.b[1] <- myinput.b[1]
\end{lstlisting}
For details on the syntax and semantics of the sub-field expression, sub-index expression, and statement groups, see sections \ref{subfields}, \ref{subindices}, and \ref{statement_groups}.

\subsubsection{The Partial Connection Algorithm} \label{partial_connection_algorithm}

A partial connect statement between two non-analog ground type components connects the right-hand side expression to the left-hand side expression. Conversely, a {\em reverse} partial connect statement between two non-analog ground type components connects the left-hand side expression to the right-hand side expression. A partial connect statement between two analog-typed components performs an attach between the two signals.

A partial (or reverse partial) connect statement between two vector typed components applies a partial (or reverse partial) connect from the first n sub-elements in the right-hand side expression to the first n corresponding sub-elements in the left-hand side expression, where n is the length of the shorter vector.

A partial (or reverse partial) connect statement between two bundle typed components considers any pair of fields, one from the first bundle type and one from the second, with matching names. If the first field in the pair is not flipped, then we apply a partial (or reverse partial) connect from the right-hand side field to the left-hand side field. However, if the first field is flipped, then we apply a reverse partial (or partial) connect from the right-hand side field to the left-hand side field.

\subsection{Statement Groups} \label{statement_groups}

An ordered sequence of one or more statements can be grouped into a single statement, called a statement group. The following example demonstrates a statement group composed of three connect statements.

\begin{lstlisting}
module MyModule :
   input a: UInt
   input b: UInt
   output myport1: UInt
   output myport2: UInt
   myport1 <= a
   myport1 <= b
   myport2 <= a
\end{lstlisting}

\subsubsection{Last Connect Semantics}\label{last_connect}
Ordering of statements is significant in a statement group. Intuitively, during elaboration, statements execute in order, and the effects of later statements take precedence over earlier ones. In the previous example, in the resultant circuit, port \verb|b| will be connected to \verb|myport1|, and port \verb|a| will be connected to \verb|myport2|.

Note that connect and partial connect statements have equal priority, and later connect or partial connect statements always take priority over earlier connect or partial connect statements. Conditional statements are also affected by last connect semantics, and for details see section \ref{conditional_last_connect}.

In the case where a connection to a circuit component with an aggregate type is followed by a connection to a sub-element of that component, only the connection to the sub-element is overwritten. Connections to the other sub-elements remain unaffected. In the following example, in the resultant circuit, the \verb|c| sub-element of port \verb|portx| will be connected to the \verb|c| sub-element of \verb|myport|, and port \verb|porty| will be connected to the \verb|b| sub-element of \verb|myport|.
\begin{lstlisting}
module MyModule :
   input portx: {b:UInt, c:UInt}
   input porty: UInt
   output myport: {b:UInt, c:UInt}
   myport <= portx
   myport.b <= porty
\end{lstlisting}
The above circuit can be rewritten equivalently as follows.
\begin{lstlisting}
module MyModule :
   input portx: {b:UInt, c:UInt}
   input porty: UInt
   output myport: {b:UInt, c:UInt}
   myport.b <= porty
   myport.c <= portx.c
\end{lstlisting}

In the case where a connection to a sub-element of an aggregate circuit component is followed by a connection to the entire circuit component, the later connection overwrites the earlier connections completely.

\begin{lstlisting}
module MyModule :
   input portx: {b:UInt, c:UInt}
   input porty: UInt
   output myport: {b:UInt, c:UInt}
   myport.b <= porty
   myport <= portx
\end{lstlisting}
The above circuit can be rewritten equivalently as follows.
\begin{lstlisting}
module MyModule :
   input portx: {b:UInt, c:UInt}
   input porty: UInt
   output myport: {b:UInt, c:UInt}
   myport <= portx
\end{lstlisting}

See section \ref{subfields} for more details about sub-field expressions.

\subsection{Empty}
The empty statement does nothing and is used simply as a placeholder where a statement is expected. It is specified using the \verb|skip| keyword.

The following example:
\begin{lstlisting}
a <= b
skip
c <= d
\end{lstlisting}
can be equivalently expressed as:
\begin{lstlisting}
a <= b
c <= d
\end{lstlisting}

The empty statement is most often used as the \verb|else| branch in a conditional statement, or as a convenient placeholder for removed components during transformational passes. See section \ref{conditionals} for details on the conditional statement.

\subsection{Wires}
A wire is a named combinational circuit component that can be connected to and from using connect and partial connect statements.

The following example demonstrates instantiating a wire with the given name \verb|mywire| and type \verb|UInt|.

\begin{lstlisting}
wire mywire : UInt
\end{lstlisting}

\subsection{Registers}
A register is a named stateful circuit component.

The following example demonstrates instantiating a register with the given name \verb|myreg|, type \verb|SInt|, and is driven by the clock signal \verb|myclock|.

\begin{lstlisting}
wire myclock: Clock
reg myreg: SInt, myclock
...
\end{lstlisting}

Optionally, for the purposes of circuit initialization, a register can be declared with a reset signal and value. In the following example, \verb|myreg| is assigned the value \verb|myinit| when the signal \verb|myreset| is high.

\begin{lstlisting}
wire myclock: Clock
wire myreset: UInt<1>
wire myinit: SInt
reg myreg: SInt, myclock with: (reset => (myreset, myinit))
...
\end{lstlisting}

Note that the clock signal for a register must be of type \verb|clock|, the reset signal must be a single bit \verb|UInt|, and the type of initialization value must match the declared type of the register.

\subsection{Invalidates}
An invalidate statement is used to indicate that a circuit component contains indeterminate values. It is specified as follows:

\begin{lstlisting}
wire w:UInt
w is invalid
\end{lstlisting}

Invalidate statements can be applied to any circuit component of any type. However, if the circuit component cannot be connected to, then the statement has no effect on the component. This allows the invalidate statement to be applied to any component, to explicitly ignore initialization coverage errors.

The following example demonstrates the effect of invalidating a variety of circuit components with aggregate types. See section \ref{invalidate_algorithm} for details on the algorithm for determining what is invalidated.

\begin{lstlisting}
module MyModule :
   input in: {flip a:UInt, b:UInt}
   output out: {flip a:UInt, b:UInt}
   wire w: {flip a:UInt, b:UInt}
   in is invalid
   out is invalid
   w is invalid
\end{lstlisting}
is equivalent to the following:
\begin{lstlisting}
module MyModule :
   input in: {flip a:UInt, b:UInt}
   output out: {flip a:UInt, b:UInt}
   wire w: {flip a:UInt, b:UInt}
   in.a is invalid
   out.b is invalid
   w.a is invalid
   w.b is invalid
\end{lstlisting}

For the purposes of simulation, invalidated components are initialized to random values, and operations involving indeterminate values produce undefined behaviour. This is useful for early detection of errors in simulation.

\subsubsection{The Invalidate Algorithm}\label{invalidate_algorithm}
Invalidating a component with a ground type indicates that the component's value is undetermined if the component has sink or duplex flow (see section \ref{flows}). Otherwise, the component is unaffected.

Invalidating a component with a vector type recursively invalidates each sub-element in the vector.

Invalidating a component with a bundle type recursively invalidates each sub-element in the bundle.

\subsection{Attaches}

The \verb|attach| statement is used to attach two or more analog signals, defining that their
values be the same in a commutative fashion that lacks the directionality of a regular connection.
It can only be applied to signals with analog type, and each analog signal may be attached zero or
more times.

\begin{lstlisting}
wire x: Analog<2>
wire y: Analog<2>
wire z: Analog<2>
attach(x, y)      ; binary attach
attach(z, y, x)   ; attach all three signals
\end{lstlisting}

When signals of aggregate types that contain analog-typed fields are used as operators of a partial
connection, corresponding fields of analog type are attached, rather than connected.

\subsection{Nodes}
A node is simply a named intermediate value in a circuit. The node must be initialized to a value with a passive type and cannot be connected to. Nodes are often used to split a complicated compound expression into named sub-expressions.

The following example demonstrates instantiating a node with the given name \verb|mynode| initialized with the output of a multiplexer (see section \ref{multiplexers}).

\begin{lstlisting}
wire pred: UInt<1>
wire a: SInt
wire b: SInt
node mynode = mux(pred, a, b)
...
\end{lstlisting}

\subsection{Conditionals}\label{conditionals}
Connections within a conditional statement that connect to previously declared components hold only when the given condition is high. The condition must have a 1-bit unsigned integer type.

In the following example, the wire \verb|x| is connected to the input \verb|a| only when the \verb|en| signal is high. Otherwise, the wire \verb|x| is connected to the input \verb|b|.

\begin{lstlisting}
module MyModule :
   input a: UInt
   input b: UInt
   input en: UInt<1>
   wire x: UInt
   when en :
      x <= a
   else :
      x <= b
\end{lstlisting}

\subsubsection{Syntactic Shorthands}
The \verb|else| branch of a conditional statement may be omitted, in which case a default \verb|else| branch is supplied consisting of the empty statement.

Thus the following example:

\begin{lstlisting}
module MyModule :
   input a: UInt
   input b: UInt
   input en: UInt<1>
   wire x: UInt
   when en :
      x <= a
\end{lstlisting}

can be equivalently expressed as:

\begin{lstlisting}
module MyModule :
   input a: UInt
   input b: UInt
   input en: UInt<1>
   wire x: UInt
   when en :
      x <= a
   else :
      skip
\end{lstlisting}

To aid readability of long chains of conditional statements, the colon following the \verb|else| keyword may be omitted if the \verb|else| branch consists of a single conditional statement.

Thus the following example:

\begin{lstlisting}
module MyModule :
   input a: UInt
   input b: UInt
   input c: UInt
   input d: UInt
   input c1: UInt<1>
   input c2: UInt<1>
   input c3: UInt<1>
   wire x: UInt
   when c1 :
      x <= a
   else :
      when c2 :
         x <= b
      else :
         when c3 :
            x <= c
         else :
            x <= d
\end{lstlisting}

can be equivalently written as:

\begin{lstlisting}
module MyModule :
   input a: UInt
   input b: UInt
   input c: UInt
   input d: UInt
   input c1: UInt<1>
   input c2: UInt<1>
   input c3: UInt<1>
   wire x: UInt
   when c1 :
      x <= a
   else when c2 :
      x <= b
   else when c3 :
      x <= c
   else :
      x <= d
\end{lstlisting}

To additionally aid readability, a conditional statement where the contents of the \verb|when| branch consist of a single line may be combined into a single line.
If an \verb|else| branch exists, then the \verb|else| keyword must be included on the same line.

The following statement:
\begin{lstlisting}
when c :
   a <= b
else :
   e <= f
\end{lstlisting}

can have the \verb|when| keyword, the \verb|when| branch, and the \verb|else| keyword expressed as a single line:

\begin{lstlisting}
when c : a <= b else :
  e <= f
\end{lstlisting}

The \verb|else| branch may also be added to the single line:

\begin{lstlisting}
when c : a <= b else : e <= f
\end{lstlisting}

\subsubsection{Nested Declarations}
If a component is declared within a conditional statement, connections to the component are unaffected by the condition. In the following example, register \verb|myreg1| is always connected to \verb|a|, and register \verb|myreg2| is always connected to \verb|b|.

\begin{lstlisting}
module MyModule :
   input a: UInt
   input b: UInt
   input en: UInt<1>
   input clk : Clock
   when en :
      reg myreg1 : UInt, clk
      myreg1 <= a
   else :
      reg myreg2 : UInt, clk
      myreg2 <= b
\end{lstlisting}

Intuitively, a line can be drawn between a connection (or partial connection) to a component and that component's declaration. All conditional statements that are crossed by the line apply to that connection (or partial connection).

\subsubsection{Initialization Coverage}
Because of the conditional statement, it is possible to syntactically express circuits containing wires that have not been connected to under all conditions.

In the following example, the wire \verb|a| is connected to the wire \verb|w| when \verb|en| is high, but it is not specified what is connected to \verb|w| when \verb|en| is low.

\begin{lstlisting}
module MyModule :
   input en: UInt<1>
   input a: UInt
   wire w: UInt
   when en :
      w <= a
\end{lstlisting}

This is an illegal FIRRTL circuit and an error will be thrown during compilation. All wires, memory ports, instance ports, and module ports that can be connected to must be connected to under all conditions. Registers do not need to be connected to under all conditions, as it will keep its previous value if unconnected.

\subsubsection{Scoping}
The conditional statement creates a new {\em scope} within each of its \verb|when| and \verb|else| branches. It is an error to refer to any component declared within a branch after the branch has ended. As mention in section~\ref{namespaces}, circuit component declarations in a module must be unique within the module's flat namespace; this means that shadowing a component in an enclosing scope with a component of the same name inside a conditional statement is not allowed.

\subsubsection{Conditional Last Connect Semantics}\label{conditional_last_connect}
In the case where a connection to a circuit component is followed by a conditional statement containing a connection to the same component, the connection is overwritten only when the condition holds. Intuitively, a multiplexer is generated such that when the condition is low, the multiplexer returns the old value, and otherwise returns the new value. For details about the multiplexer, see section \ref{multiplexers}.

The following example:
\begin{lstlisting}
wire a: UInt
wire b: UInt
wire c: UInt<1>
wire w: UInt
w <= a
when c :
   w <= b
...
\end{lstlisting}
can be rewritten equivalently using a multiplexer as follows:
\begin{lstlisting}
wire a: UInt
wire b: UInt
wire c: UInt<1>
wire w: UInt
w <= mux(c, b, a)
...
\end{lstlisting}

In the case where an invalid statement is followed by a conditional statement containing a connect to the invalidated component, the resulting connection to the component can be expressed using a conditionally valid expression. See section \ref{conditionally_valids} for more details about the conditionally valid expression.
\begin{lstlisting}
wire a: UInt
wire c: UInt<1>
wire w: UInt
w is invalid
when c :
   w <= a
...
\end{lstlisting}
can be rewritten equivalently as follows:
\begin{lstlisting}
wire a: UInt
wire c: UInt<1>
wire w: UInt
w <= validif(c, a)
...
\end{lstlisting}

The behaviour of conditional connections to circuit components with aggregate types can be modeled by first expanding each connect into individual connect statements on its ground elements (see section \ref{connection_algorithm} and \ref{partial_connection_algorithm} for the connection and partial connection algorithms) and then applying the conditional last connect semantics.

For example, the following snippet:
\begin{lstlisting}
wire x: {a:UInt, b:UInt}
wire y: {a:UInt, b:UInt}
wire c: UInt<1>
wire w: {a:UInt, b:UInt}
w <= x
when c :
   w <= y
...
\end{lstlisting}
can be rewritten equivalently as follows:
\begin{lstlisting}
wire x: {a:UInt, b:UInt}
wire y: {a:UInt, b:UInt}
wire c: UInt<1>
wire w: {a:UInt, b:UInt}
w.a <= mux(c, y.a, x.a)
w.b <= mux(c, y.b, x.b)
...
\end{lstlisting}

Similar to the behavior of aggregate types under last connect semantics (see section \ref{last_connect}), the conditional connects to a sub-element of an aggregate component only generates a multiplexer for the sub-element that is overwritten.

For example, the following snippet:
\begin{lstlisting}
wire x: {a:UInt, b:UInt}
wire y: UInt
wire c: UInt<1>
wire w: {a:UInt, b:UInt}
w <= x
when c :
   w.a <= y
...
\end{lstlisting}
can be rewritten equivalently as follows:
\begin{lstlisting}
wire x: {a:UInt, b:UInt}
wire y: UInt
wire c: UInt<1>
wire w: {a:UInt, b:UInt}
w.a <= mux(c, y, x.a)
w.b <= x.b
...
\end{lstlisting}

\subsection{Memories}
A memory is an abstract representation of a hardware memory. It is characterized by the following parameters.
\begin{enumerate}
\item A passive type representing the type of each element in the memory.
\item A positive integer representing the number of elements in the memory.
\item A variable number of named ports, each being a read port, a write port, or readwrite port.
\item A non-negative integer indicating the read latency, which is the number of cycles after setting the port's read address before the corresponding element's value can be read from the port's data field.
\item A positive integer indicating the write latency, which is the number of cycles after setting the port's write address and data before the corresponding element within the memory holds the new value.
\item A read-under-write flag indicating the behaviour when a memory location is written to while a read to that location is in progress.
\end{enumerate}

The following example demonstrates instantiating a memory containing 256 complex numbers, each with 16-bit signed integer fields for its real and imaginary components. It has two read ports, \verb|r1| and \verb|r2|, and one write port, \verb|w|. It is combinationally read (read latency is zero cycles) and has a write latency of one cycle. Finally, its read-under-write behavior is undefined.
\begin{lstlisting}
mem mymem :
  data-type => {real:SInt<16>, imag:SInt<16>}
  depth => 256
  reader => r1
  reader => r2
  writer => w
  read-latency => 0
  write-latency => 1
  read-under-write => undefined
\end{lstlisting}

In the example above, the type of \verb|mymem| is:
\begin{lstlisting}
{flip r1: {addr: UInt<8>,
           en: UInt<1>,
           clk: Clock,
           flip data: {real:SInt<16>, imag:SInt<16>}}
 flip r2: {addr: UInt<8>,
           en: UInt<1>,
           clk: Clock,
           flip data: {real:SInt<16>, imag:SInt<16>}}
 flip w: {addr: UInt<8>,
          en: UInt<1>,
          clk: Clock,
          data: {real:SInt<16>, imag:SInt<16>},
          mask: {real:UInt<1>, imag:UInt<1>}}}
\end{lstlisting}

The following sections describe how a memory's field types are calculated and the behavior of each type of memory port.

\subsubsection{Read Ports}
If a memory is declared with element type \verb|T|, has a size less than or equal to $2^N$, then its read ports have type:
\begin{lstlisting}
{addr:UInt<N>, en:UInt<1>, clk:Clock, flip data:T}
\end{lstlisting}

If the \verb|en| field is high, then the element value associated with the address in the \verb|addr| field can be retrieved by reading from the \verb|data| field after the appropriate read latency. If the \verb|en| field is low, then the value in the \verb|data| field, after the appropriate read latency, is undefined. The port is driven by the clock signal in the \verb|clk| field.

\subsubsection{Write Ports}
If a memory is declared with element type \verb|T|, has a size less than or equal to $2^N$, then its write ports have type:
\begin{lstlisting}
{addr:UInt<N>, en:UInt<1>, clk:Clock, data:T, mask:M}
\end{lstlisting}
where \verb|M| is the mask type calculated from the element type \verb|T|. Intuitively, the mask type mirrors the aggregate structure of the element type except with all ground types replaced with a single bit unsigned integer type. The {\em non-masked portion} of the data value is defined as the set of data value leaf sub-elements where the corresponding mask leaf sub-element is high.

If the \verb|en| field is high, then the non-masked portion of the \verb|data| field value is written, after the appropriate write latency, to the location indicated by the \verb|addr| field. If the \verb|en| field is low, then no value is written after the appropriate write latency. The port is driven by the clock signal in the \verb|clk| field.

\subsubsection{Readwrite Ports}
Finally, the readwrite ports have type:
\begin{lstlisting}
{addr:UInt<N>, en:UInt<1>, clk:Clock, flip rdata:T, wmode:UInt<1>, wdata:T, wmask:M}
\end{lstlisting}
A readwrite port is a single port that, on a given cycle, can be used either as a read or a write port. If the readwrite port is not in write mode (the \verb|wmode| field is low), then the \verb|rdata|, \verb|addr|, \verb|en|, and \verb|clk| fields constitute its read port fields, and should be used accordingly. If the readwrite port is in write mode (the \verb|wmode| field is high), then the \verb|wdata|, \verb|wmask|, \verb|addr|, \verb|en|, and \verb|clk| fields constitute its write port fields, and should be used accordingly.

\subsubsection{Read Under Write Behaviour}

The read-under-write flag indicates the value held on a read port's \verb|data| field if its memory location is written to while it is reading. The flag may take on three settings: \verb|old|, \verb|new|, and \verb|undefined|.

If the read-under-write flag is set to \verb|old|, then a read port always returns the value existing in the memory on the same cycle that the read was requested.

Assuming that a combinational read always returns the value stored in the memory (no write forwarding), then intuitively, this is modeled as a combinational read from the memory that is then delayed by the appropriate read latency.

If the read-under-write flag is set to \verb|new|, then a read port always returns the value existing in the memory on the same cycle that the read was made available. Intuitively, this is modeled as a combinational read from the memory after delaying the read address by the appropriate read latency.

If the read-under-write flag is set to \verb|undefined|, then the value held by the read port after the appropriate read latency is undefined.


For the purpose of defining such collisions, an ``active write port'' is a write port or a readwrite port that is used to initiate a write operation on a given clock edge, where \verb|en| is set and, for a readwriter, \verb|wmode| is set.
An ``active read port'' is a read port or a readwrite port that is used to initiate a read operation on a given clock edge, where \verb|en| is set and, for a readwriter, \verb|wmode| is not set.
Each operation is defined to be ``active'' for the number of cycles set by its corresponding latency, starting from the cycle where its inputs were provided to its associated port.
Note that this excludes combinational reads, which are simply modeled as combinationally selecting from stored values

For memories with independently clocked ports, a collision between a read operation and a write operation with independent clocks is defined to occur when the address of an active write port and the address of an active read port are the same for overlapping clock periods, or when any portion of a read operation overlaps part of a write operation with a matching addresses.
In such cases, the data that is read out of the read port is undefined.

\subsubsection{Write Under Write Behaviour}

In all cases, if a memory location is written to by more than one port on the same cycle, the stored value is undefined.

\subsection{Instances}\label{instances}
FIRRTL modules are instantiated with the instance statement. The following example demonstrates creating an instance named \verb|myinstance| of the \verb|MyModule| module within the top level module \verb|Top|.

\begin{lstlisting}
circuit Top :
   module MyModule :
      input a: UInt
      output b: UInt
      b <= a
   module Top :
      inst myinstance of MyModule
\end{lstlisting}

The resulting instance has a bundle type. Each port of the instantiated module is represented by a field in the bundle with the same name and type as the port. The fields corresponding to input ports are flipped to indicate their data flows in the opposite direction as the output ports. The \verb|myinstance| instance in the example above has type \verb|{flip a:UInt, b:UInt}|.

Modules have the property that instances can always be {\em inlined} into the parent module without affecting the semantics of the circuit.

To disallow infinitely recursive hardware, modules cannot contain instances of itself, either directly, or indirectly through instances of other modules it instantiates.

\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.

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) : optional_name
...
\end{lstlisting}

\subsection{Formatted Prints}
The formatted print statement is used to print a formatted string during simulations of the circuit. Backends are free to generate hardware that relays this information to a hardware test harness, but this is not required by the FIRRTL specification.

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}.

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) : optional_name
...
\end{lstlisting}

On each positive clock edge, when the condition signal is high, the printf statement prints out the format string where its argument placeholders are substituted with the value of the corresponding argument.

\subsubsection{Format Strings}

Format strings support the following argument placeholders:
\begin{itemize}
\item \verb|%b| : Prints the argument in binary
\item \verb|%d| : Prints the argument in decimal
\item \verb|%x| : Prints the argument in hexadecimal
\item \verb|%%| : Prints a single \verb|%| character
\end{itemize}

Format strings support the following escape characters:
\begin{itemize}
\item \verb|\n| : New line
\item \verb|\t| : Tab
\item \verb|\\| : Back slash
\item \verb|\"| : Double quote
\item \verb|\'| : Single quote
\end{itemize}

\subsection{Verification}

To facilitate simulation, model checking and formal methods, there are three non-synthesizable verification statements available: assert, assume and cover. Each type of verification statement requires a clock signal, a predicate signal, an enable signal and an explanatory message string literal. The predicate and enable signals must have single bit unsigned integer type. When an assert is violated the explanatory message may be issued as guidance. The explanatory message may be phrased as if prefixed by the words ``Verifies that...''.

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}.

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.

\begin{lstlisting}
wire clk:Clock
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") : optional_name
\end{lstlisting}

\subsubsection{Assume}

The assume statement directs the model checker to disregard any states where the enable is true and the predicate is not true at the rising edge of the clock cycle. In other words, it reduces the states to be checked to only those where enable implies predicate is true by definition. In simulation, assume is treated as an assert.

\begin{lstlisting}
wire clk:Clock
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") : optional_name
\end{lstlisting}

\subsubsection{Cover}

The cover statement verifies that the predicate is true on the rising edge of some clock cycle when the enable is true. In other words, it directs the model checker to find some way to make enable implies predicate true at some time step.

\begin{lstlisting}
wire clk:Clock
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") : optional_name
\end{lstlisting}

\section{Expressions}

FIRRTL expressions are used for creating literal unsigned and signed integers, for referring to a declared circuit component, for statically and dynamically accessing a nested element within a component, for creating multiplexers and conditionally valid signals, and for performing primitive operations.

\subsection{Unsigned Integers}

A literal unsigned integer can be created given a non-negative integer value and an optional positive bit width. The following example creates a 10-bit unsigned integer representing the number 42.
\begin{lstlisting}
UInt<10>(42)
\end{lstlisting}

Note that it is an error to supply a bit width that is not large enough to fit the given value. If the bit width is omitted, then the minimum number of bits necessary to fit the given value will be inferred.
\begin{lstlisting}
UInt(42)
\end{lstlisting}

\subsection{Unsigned Integers from Literal Bits}

A literal unsigned integer can alternatively be created given a string representing its bit representation and an optional bit width.

The following radices are supported:
\begin{enumerate}
\item \verb|b| : For representing binary numbers.
\item \verb|o| : For representing octal numbers.
\item \verb|h| : For representing hexadecimal numbers.
\end{enumerate}

If a bit width is not given, the number of bits in the bit representation is directly represented by the string. The following examples create a 8-bit integer representing the number 13.
\begin{lstlisting}
UInt("b00001101")
UInt("h0D")
\end{lstlisting}

If the provided bit width is larger than the number of bits required to represent the string's value, then the resulting value is equivalent to the string zero-extended up to the provided bit width. If the provided bit width is smaller than the number of bits represented by the string, then the resulting value is equivalent to the string truncated down to the provided bit width. All truncated bits must be zero.

The following examples create a 7-bit integer representing the number 13.
\begin{lstlisting}
UInt<7>("b00001101")
UInt<7>("o015")
UInt<7>("hD")
\end{lstlisting}

\subsection{Signed Integers}

Similar to unsigned integers, a literal signed integer can be created given an integer value and an optional positive bit width. The following example creates a 10-bit unsigned integer representing the number -42.
\begin{lstlisting}
SInt<10>(-42)
\end{lstlisting}

Note that it is an error to supply a bit width that is not large enough to fit the given value using two's complement representation. If the bit width is omitted, then the minimum number of bits necessary to fit the given value will be inferred.
\begin{lstlisting}
SInt(-42)
\end{lstlisting}

\subsection{Signed Integers from Literal Bits}

Similar to unsigned integers, a literal signed integer can alternatively be created given a string representing its bit representation and an optional bit width.

The bit representation contains a binary, octal or hex indicator, followed by an optional sign, followed by the value.

If a bit width is not given, the number of bits in the bit representation is the minimal bitwidth to represent the value represented by the string. The following examples create a 8-bit integer representing the number -13. For all bases, a negative sign acts as if it were a unary negation; in other words, a negative literal produces the additive inverse of the unsigned interpretation of the digit pattern.
\begin{lstlisting}
SInt("b-1101")
SInt("h-d")
\end{lstlisting}

If the provided bit width is larger than the number of bits represented by the string, then the resulting value is unchanged.
It is an error to provide a bit width smaller than the number of bits required to represent the string's value.

\subsection{References}
A reference is simply a name that refers to a previously declared circuit component. It may refer to a module port, node, wire, register, instance, or memory.

The following example connects a reference expression \verb|in|, referring to the previously declared port \verb|in|, to the reference expression \verb|out|, referring to the previously declared port \verb|out|.

\begin{lstlisting}
module MyModule :
   input in: UInt
   output out: UInt
   out <= in
\end{lstlisting}

In the rest of the document, for brevity, the names of components will be used to refer to a reference expression to that component. Thus, the above example will be rewritten as ``the port \verb|in| is connected to the port \verb|out|''.

\subsection{Sub-fields}\label{subfields}
The sub-field expression refers to a sub-element of an expression with a bundle type.

The following example connects the \verb|in| port to the \verb|a| sub-element of the \verb|out| port.
\begin{lstlisting}
module MyModule :
   input in: UInt
   output out: {a:UInt, b:UInt}
   out.a <= in
\end{lstlisting}

\subsection{Sub-indices}\label{subindices}
The sub-index expression statically refers, by index, to a sub-element of an expression with a vector type. The index must be a non-negative integer and cannot be equal to or exceed the length of the vector it indexes.

The following example connects the \verb|in| port to the fifth sub-element of the \verb|out| port.
\begin{lstlisting}
module MyModule :
   input in: UInt
   output out: UInt[10]
   out[4] <= in
\end{lstlisting}

\subsection{Sub-accesses}
The sub-access expression dynamically refers to a sub-element of a vector-typed expression using a calculated index. The index must be an expression with an unsigned integer type.

The following example connects the n'th sub-element of the \verb|in| port to the \verb|out| port.
\begin{lstlisting}
module MyModule :
   input in: UInt[3]
   input n: UInt<2>
   output out: UInt
   out <= in[n]
\end{lstlisting}

A connection from a sub-access expression can be modeled by conditionally connecting from every sub-element in the vector, where the condition holds when the dynamic index is equal to the sub-element's static index.
\begin{lstlisting}
module MyModule :
   input in: UInt[3]
   input n: UInt<2>
   output out: UInt
   when eq(n, UInt(0)) :
      out <= in[0]
   else when eq(n, UInt(1)) :
      out <= in[1]
   else when eq(n, UInt(2)) :
      out <= in[2]
   else :
      out is invalid
\end{lstlisting}

The following example connects the \verb|in| port to the n'th sub-element of the \verb|out| port. All other sub-elements of the \verb|out| port are connected from the corresponding sub-elements of the \verb|default| port.
\begin{lstlisting}
module MyModule :
   input in: UInt
   input default: UInt[3]
   input n: UInt<2>
   output out: UInt[3]
   out <= default
   out[n] <= in
\end{lstlisting}

A connection to a sub-access expression can be modeled by conditionally connecting to every sub-element in the vector, where the condition holds when the dynamic index is equal to the sub-element's static index.
\begin{lstlisting}
module MyModule :
   input in: UInt
   input default: UInt[3]
   input n: UInt<2>
   output out: UInt[3]
   out <= default
   when eq(n, UInt(0)) :
      out[0] <= in
   else when eq(n, UInt(1)) :
      out[1] <= in
   else when eq(n, UInt(2)) :
      out[2] <= in
\end{lstlisting}

The following example connects the \verb|in| port to the m'th \verb|UInt| sub-element of the n'th vector-typed sub-element of the \verb|out| port. All other sub-elements of the \verb|out| port are connected from the corresponding sub-elements of the \verb|default| port.
\begin{lstlisting}
module MyModule :
   input in: UInt
   input default: UInt[2][2]
   input n: UInt<1>
   input m: UInt<1>
   output out: UInt[2][2]
   out <= default
   out[n][m] <= in
\end{lstlisting}

A connection to an expression containing multiple nested sub-access expressions can also be modeled by conditionally connecting to every sub-element in the expression. However the condition holds only when all dynamic indices are equal to all of the sub-element's static indices.
\begin{lstlisting}
module MyModule :
   input in: UInt
   input default: UInt[2][2]
   input n: UInt<1>
   input m: UInt<1>
   output out: UInt[2][2]
   out <= default
   when and(eq(n, UInt(0)), eq(m, UInt(0))) :
      out[0][0] <= in
   else when and(eq(n, UInt(0)), eq(m, UInt(1))) :
      out[0][1] <= in
   else when and(eq(n, UInt(1)), eq(m, UInt(0))) :
      out[1][0] <= in
   else when and(eq(n, UInt(1)), eq(m, UInt(1))) :
      out[1][1] <= in
\end{lstlisting}

\subsection{Multiplexers}\label{multiplexers}

A multiplexer outputs one of two input expressions depending on the value of an unsigned selection signal.

The following example connects to the \verb|c| port the result of selecting between the \verb|a| and \verb|b| ports. The \verb|a| port is selected when the \verb|sel| signal is high, otherwise the \verb|b| port is selected.
\begin{lstlisting}
module MyModule :
   input a: UInt
   input b: UInt
   input sel: UInt<1>
   output c: UInt
   c <= mux(sel, a, b)
\end{lstlisting}

A multiplexer expression is legal only if the following holds.
\begin{enumerate}
\item The type of the selection signal is an unsigned integer.
\item The width of the selection signal is any of:
  \begin{enumerate}
  \item One-bit
  \item Unspecified, but will infer to one-bit
  \end{enumerate}
\item The types of the two input expressions are equivalent.
\item The types of the two input expressions are passive (see section \ref{passive_types}).
\end{enumerate}

\subsection{Conditionally Valids} \label{conditionally_valids}

A conditionally valid expression is expressed as an input expression guarded with an unsigned single bit valid signal. It outputs the input expression when the valid signal is high, otherwise the result is undefined.

The following example connects the \verb|a| port to the \verb|c| port when the \verb|valid| signal is high. Otherwise, the value of the \verb|c| port is undefined.
\begin{lstlisting}
module MyModule :
   input a: UInt
   input valid: UInt<1>
   output c: UInt
   c <= validif(valid, a)
\end{lstlisting}

A conditionally valid expression is legal only if the following holds.
\begin{enumerate}
\item The type of the valid signal is a single bit unsigned integer.
\item The type of the input expression is passive (see section \ref{passive_types}).
\end{enumerate}

Conditional statements can be equivalently expressed as multiplexers and conditionally valid expressions. See section \ref{conditionals} for details.

\subsection{Primitive Operations}

All fundamental operations on ground types are expressed as a FIRRTL primitive operation. In general, each operation takes some number of argument expressions, along with some number of static integer literal parameters.

The general form of a primitive operation is expressed as follows:
\begin{lstlisting}
op(arg0, arg1, ..., argn, int0, int1, ..., intm)
\end{lstlisting}

The following examples of primitive operations demonstrate adding two expressions, \verb|a| and \verb|b|, shifting expression \verb|a| left by 3 bits, selecting the fourth bit through and including the seventh bit in the \verb|a| expression, and interpreting the expression \verb|x| as a Clock typed signal.
\begin{lstlisting}
add(a, b)
shl(a, 3)
bits(a, 7, 4)
asClock(x)
\end{lstlisting}

Section \ref{primitives} will describe the format and semantics of each primitive operation.

\section{Primitive Operations} \label{primitives}

%====Macros======
\newcommand{\vv}[1]{{\ttfamily #1}}
\newcommand{\ts}[1]{\textsubscript{#1}}
\newcommand{\nf}[1]{\normalfont{\textbf{#1}}}
\newcommand{\nit}[1]{\normalfont{\textit{#1}}}
\newcommand{\mrow}[2]{\multirow{#1}{*}{#2}}
\newcommand{\mcol}[3]{\multicolumn{#1}{#2}{#3}}
\newcommand{\opheader}{
  \hline
  \mrow{2}{\nf{Name}} & \mrow{2}{\nf{Arguments}} & \mrow{2}{\nf{Parameters}} & \mrow{2}{\nf{Arg Types}} & \multicolumn{2}{c|}{\nf{Result}} \\
                      &                          &                           &                          & \mcol{1}{c}{\nit{Type}} & \mcol{1}{c|}{\nit{Width}} \\
  \hline
}

The arguments of all primitive operations must be expressions with ground types, while their parameters are static integer literals. Each specific operation can place additional restrictions on the number and types of their arguments and parameters.

Notationally, the width of an argument \vv{e} is represented as \vv{w}\ts{e}.

\subsection{Add Operation}

\begin{figure}[H]
{ \fontsize{10pt}{1.10em}\selectfont
{\ttfamily
\begin{tabular}{ |c|c|c|c|c|c| }
  \opheader
  \mrow{3}{add} & \mrow{3}{(e1,e2)} & \mrow{3}{()} & (UInt,UInt)   & UInt  & max(w\ts{e1},w\ts{e2})+1\\
                &                   &              & (SInt,SInt)   & SInt  & max(w\ts{e1},w\ts{e2})+1\\
                &                   &              & (Fixed,Fixed) & Fixed & \nit{see section \ref{fixed_rules}}\\
 \hline
\end{tabular}
}}
\end{figure}
The add operation result is the sum of \vv{e1} and \vv{e2} without loss of precision.

\subsection{Subtract Operation}

\begin{figure}[H]
{ \fontsize{10pt}{1.10em}\selectfont
{\ttfamily
\begin{tabular}{ |c|c|c|c|c|c| }
  \opheader
  \mrow{3}{sub} & \mrow{3}{(e1,e2)} & \mrow{3}{()} & (UInt,UInt)   & UInt  & max(w\ts{e1},w\ts{e2})+1\\
                &                   &              & (SInt,SInt)   & SInt  & max(w\ts{e1},w\ts{e2})+1\\
                &                   &              & (Fixed,Fixed) & Fixed & \nit{see section \ref{fixed_rules}}\\
 \hline
\end{tabular}
}}
\end{figure}
The subtract operation result is \vv{e2} subtracted from \vv{e1}, without loss of precision.

\subsection{Multiply Operation}

\begin{figure}[H]
{ \fontsize{10pt}{1.10em}\selectfont
{\ttfamily
\begin{tabular}{ |c|c|c|c|c|c| }
  \opheader
  \mrow{3}{mul} & \mrow{3}{(e1,e2)} & \mrow{3}{()} & (UInt,UInt)   & UInt  & w\ts{e1}+w\ts{e2}\\
                &                   &              & (SInt,SInt)   & SInt  & w\ts{e1}+w\ts{e2}\\
                &                   &              & (Fixed,Fixed) & Fixed & \nit{see section \ref{fixed_rules}}\\
 \hline
\end{tabular}
}}
\end{figure}
The multiply operation result is the product of \vv{e1} and \vv{e2}, without loss of precision.

\subsection{Divide Operation}

\begin{figure}[H]
{ \fontsize{10pt}{1.10em}\selectfont
{\ttfamily
\begin{tabular}{ |c|c|c|c|c|c| }
  \opheader
  \mrow{2}{div} & \mrow{2}{(num,den)} & \mrow{2}{()} & (UInt,UInt) & UInt & w\ts{num}\\
                &                     &              & (SInt,SInt) & SInt & w\ts{num}+1\\
 \hline
\end{tabular}
}}
\end{figure}
The divide operation divides \vv{num} by \vv{den}, truncating the fractional portion of the result. This is equivalent to rounding the result towards zero. The result of a division where \vv{den} is zero is undefined.

\subsection{Modulus Operation}

\begin{figure}[H]
{ \fontsize{10pt}{1.10em}\selectfont
{\ttfamily
\begin{tabular}{ |c|c|c|c|c|c| }
  \opheader
  \mrow{2}{rem} & \mrow{2}{(num,den)} & \mrow{2}{()} & (UInt,UInt) & UInt & min(w\ts{num},w\ts{den})\\
                &                     &              & (SInt,SInt) & SInt & min(w\ts{num},w\ts{den})\\
 \hline
\end{tabular}
}}
\end{figure}
The modulus operation yields the remainder from dividing \vv{num} by \vv{den}, keeping the sign of the numerator. Together with the divide operator, the modulus operator satisfies the relationship below:
\begin{lstlisting}
num = add(mul(den,div(num,den)),rem(num,den))}
\end{lstlisting}

\subsection{Comparison Operations}

\begin{figure}[H]
{ \fontsize{10pt}{1.10em}\selectfont
{\ttfamily
\begin{tabular}{ |c|c|c|c|c|c| }
  \opheader
  lt,leq &         &    & (UInt,UInt)   & UInt & 1\\
  gt,geq & (e1,e2) & () & (SInt,SInt)   & UInt & 1\\
  eq,neq &         &    & (Fixed,Fixed) & UInt & 1\\
 \hline
\end{tabular}
}}
\end{figure}
The comparison operations return an unsigned 1 bit signal with value one if \vv{e1} is less than (\vv{lt}), less than or equal to (\vv{leq}), greater than (\vv{gt}), greater than or equal to (\vv{geq}), equal to (\vv{eq}), or not equal to (\vv{neq}) \vv{e2}. The operation returns a value of zero otherwise.

\subsection{Padding Operations}

\begin{figure}[H]
{ \fontsize{10pt}{1.10em}\selectfont
{\ttfamily
\begin{tabular}{ |c|c|c|c|c|c| }
  \opheader
  \mrow{3}{pad} & \mrow{3}{(e)} & \mrow{3}{(n)} & (UInt)  & UInt  & max(w\ts{e},n)\\
                &               &               & (SInt)  & SInt  & max(w\ts{e},n)\\
                &               &               & (Fixed) & Fixed & \nit{see section \ref{fixed_rules}}\\
 \hline
\end{tabular}
}}
\end{figure}

If \vv{e}'s bit width is smaller than \vv{n}, then the pad operation zero-extends or sign-extends \vv{e} up to the given width \vv{n}. Otherwise, the result is simply \vv{e}. \vv{n} must be non-negative. The binary point of fixed-point values is not affected by padding.

\subsection{Interpret As UInt}

\begin{figure}[H]
{ \fontsize{10pt}{1.10em}\selectfont
{\ttfamily
\begin{tabular}{ |c|c|c|c|c|c| }
  \opheader
  \mrow{4}{asUInt} & \mrow{4}{(e)} & \mrow{4}{()} & (UInt)  & UInt & w\ts{e}\\
                   &               &              & (SInt)  & UInt & w\ts{e}\\
                   &               &              & (Fixed) & UInt & w\ts{e}\\
                   &               &              & (Clock) & UInt & 1\\
 \hline
\end{tabular}
}}
\end{figure}

The interpret as UInt operation reinterprets \vv{e}'s bits as an unsigned integer.

\subsection{Interpret As SInt}

\begin{figure}[H]
{ \fontsize{10pt}{1.10em}\selectfont
{\ttfamily
\begin{tabular}{ |c|c|c|c|c|c| }
  \opheader
  \mrow{4}{asSInt} & \mrow{4}{(e)} & \mrow{4}{()} & (UInt)  & SInt & w\ts{e}\\
                   &               &              & (SInt)  & SInt & w\ts{e}\\
                   &               &              & (Fixed) & SInt & w\ts{e}\\
                   &               &              & (Clock) & SInt & 1\\
 \hline
\end{tabular}
}}
\end{figure}

The interpret as SInt operation reinterprets \vv{e}'s bits as a signed integer according to two's complement representation.

\subsection{Interpret As Fixed-Point Number}

\begin{figure}[H]
{ \fontsize{10pt}{1.10em}\selectfont
{\ttfamily
\begin{tabular}{ |c|c|c|c|c|c|c| }
  \hline
  \mrow{2}{\nf{Name}} & \mrow{2}{\nf{Arguments}} & \mrow{2}{\nf{Parameters}} & \mrow{2}{\nf{Arg Types}} & \multicolumn{3}{c|}{\nf{Result}} \\
                      &                          &                           &                          & \mcol{1}{c}{\nit{Type}} & \mcol{1}{c}{\nit{Width}} & \mcol{1}{c|}{\nit{Binary Point}} \\
  \hline
  \mrow{4}{asFixed} & \mrow{4}{(e)} & \mrow{4}{(p)} & (UInt)  & Fixed & w\ts{e} & p\\
                    &               &               & (SInt)  & Fixed & w\ts{e} & p\\
                    &               &               & (Fixed) & Fixed & w\ts{e} & p\\
                    &               &               & (Clock) & Fixed & 1       & p\\
  \hline
\end{tabular}
}}
\end{figure}

The interpret as fixed-point operation reinterprets \vv{e}'s bits as a fixed-point number of identical width. Since all fixed-point number in FIRRTL are signed, the bits are taken to mean a signed value according to two's complement representation. They are scaled by the provided binary point \vv{p}, and the result type has binary point \vv{p}.

\subsection{Interpret as Clock}

\begin{figure}[H]
{ \fontsize{10pt}{1.10em}\selectfont
{\ttfamily
\begin{tabular}{ |c|c|c|c|c|c| }
  \opheader
  \mrow{4}{asClock} & \mrow{4}{(e)} & \mrow{4}{()} & (UInt)  & Clock & n/a\\
                    &               &              & (SInt)  & Clock & n/a\\
                    &               &              & (Fixed) & Clock & n/a\\
                    &               &              & (Clock) & Clock & n/a\\
 \hline
\end{tabular}
}}
\end{figure}

The result of the interpret as clock operation is the Clock typed signal obtained from interpreting a single bit integer as a clock signal.

\subsection{Shift Left Operation}

\begin{figure}[H]
{ \fontsize{10pt}{1.10em}\selectfont
{\ttfamily
\begin{tabular}{ |c|c|c|c|c|c| }
  \opheader
  \mrow{3}{shl} & \mrow{3}{(e)} & \mrow{3}{(n)} & (UInt)  & UInt  & w\ts{e}+n\\
                &               &               & (SInt)  & SInt  & w\ts{e}+n\\
                &               &               & (Fixed) & Fixed & \nit{see section \ref{fixed_rules}}\\
 \hline
\end{tabular}
}}
\end{figure}

The shift left operation concatenates \vv{n} zero bits to the least significant end of \vv{e}. \vv{n} must be non-negative.

\subsection{Shift Right Operation}

\begin{figure}[H]
{ \fontsize{10pt}{1.10em}\selectfont
{\ttfamily
\begin{tabular}{ |c|c|c|c|c|c| }
  \opheader
  \mrow{3}{shr} & \mrow{3}{(e)} & \mrow{3}{(n)} & (UInt)  & UInt  & max(w\ts{e}-n, 1)\\
                &               &               & (SInt)  & SInt  & max(w\ts{e}-n, 1)\\
                &               &               & (Fixed) & Fixed & \nit{see section \ref{fixed_rules}}\\
  \hline
\end{tabular}
}}
\end{figure}

The shift right operation truncates the least significant \vv{n} bits from \vv{e}.
If \vv{n} is greater than or equal to the bit-width of \vv{e}, the resulting value will be zero for unsigned types and the sign bit for signed types.
\vv{n} must be non-negative.

\subsection{Dynamic Shift Left Operation}

\begin{figure}[H]
{ \fontsize{10pt}{1.10em}\selectfont
{\ttfamily
\begin{tabular}{ |c|c|c|c|c|c| }
  \opheader
  \mrow{3}{dshl} & \mrow{3}{(e1, e2)} & \mrow{3}{()} & (UInt, UInt)  & UInt  & w\ts{e1} + 2\verb|^|w\ts{e2} - 1\\
                 &                  &              & (SInt, UInt)  & SInt  & w\ts{e1} + 2\verb|^|w\ts{e2} - 1\\
                 &                  &              & (Fixed, UInt) & Fixed & \nit{see section \ref{fixed_rules}}\\
  \hline
\end{tabular}
}}
\end{figure}

The dynamic shift left operation shifts the bits in \vv{e1} \vv{e2} places towards the most significant bit. \vv{e2} zeroes are shifted in to the least significant bits.

\subsection{Dynamic Shift Right Operation}

\begin{figure}[H]
{ \fontsize{10pt}{1.10em}\selectfont
{\ttfamily
\begin{tabular}{ |c|c|c|c|c|c| }
  \opheader
  \mrow{3}{dshr} & \mrow{3}{(e1, e2)} & \mrow{3}{()} & (UInt, UInt)  & UInt  & w\ts{e1}\\
                 &                  &                & (SInt, UInt)  & SInt  & w\ts{e1}\\
                 &                  &                & (Fixed, UInt) & Fixed & \nit{see section \ref{fixed_rules}}\\
 \hline
\end{tabular}
}}
\end{figure}

The dynamic shift right operation shifts the bits in \vv{e1} \vv{e2} places towards the least significant bit. \vv{e2} signed or zeroed bits are shifted in to the most significant bits, and the \vv{e2} least significant bits are truncated.

\subsection{Arithmetic Convert to Signed Operation}

\begin{figure}[H]
{ \fontsize{10pt}{1.10em}\selectfont
{\ttfamily
\begin{tabular}{ |c|c|c|c|c|c| }
  \opheader
  \mrow{2}{cvt} & \mrow{2}{(e)} & \mrow{2}{()} & (UInt) & SInt & w\ts{e}+1\\
                &               &              & (SInt) & SInt & w\ts{e}\\
 \hline
\end{tabular}
}}
\end{figure}

The result of the arithmetic convert to signed operation is a signed integer representing the same numerical value as \vv{e}.

\subsection{Negate Operation}

\begin{figure}[H]
{ \fontsize{10pt}{1.10em}\selectfont
{\ttfamily
\begin{tabular}{ |c|c|c|c|c|c| }
  \opheader
  \mrow{2}{neg} & \mrow{2}{(e)} & \mrow{2}{()} & (UInt) & SInt & w\ts{e}+1\\
                &               &              & (SInt) & SInt & w\ts{e}+1\\
 \hline
\end{tabular}
}}
\end{figure}

The result of the negate operation is a signed integer representing the negated numerical value of \vv{e}.

\subsection{Bitwise Complement Operation}

\begin{figure}[H]
{ \fontsize{10pt}{1.10em}\selectfont
{\ttfamily
\begin{tabular}{ |c|c|c|c|c|c| }
  \opheader
  \mrow{2}{not} & \mrow{2}{(e)} & \mrow{2}{()} & (UInt) & UInt & w\ts{e}\\
                &               &              & (SInt) & UInt & w\ts{e}\\
 \hline
\end{tabular}
}}
\end{figure}

The bitwise complement operation performs a logical not on each bit in \vv{e}.

\subsection{Binary Bitwise Operations}

\begin{figure}[H]
{ \fontsize{10pt}{1.10em}\selectfont
{\ttfamily
\begin{tabular}{ |c|c|c|c|c|c| }
  \opheader
  \mrow{2}{and,or,xor} & \mrow{2}{(e1, e2)} & \mrow{2}{()} & (UInt,UInt) & UInt & max(w\ts{e1},w\ts{e2})\\
                       &                    &              & (SInt,SInt) & UInt & max(w\ts{e1},w\ts{e2})\\
 \hline
\end{tabular}
}}
\end{figure}

The above bitwise operations perform a bitwise and, or, or exclusive or on \vv{e1} and \vv{e2}. The result has the same width as its widest argument, and any narrower arguments are automatically zero-extended or sign-extended to match the width of the result before performing the operation.

\subsection{Bitwise Reduction Operations}

\begin{figure}[H]
{ \fontsize{10pt}{1.10em}\selectfont
{\ttfamily
\begin{tabular}{ |c|c|c|c|c|c| }
  \opheader
  \mrow{2}{andr,orr,xorr} & \mrow{2}{(e)} & \mrow{2}{()} & (UInt) & UInt & 1\\
                          &               &              & (SInt) & UInt & 1\\
 \hline
\end{tabular}
}}
\end{figure}

The bitwise reduction operations correspond to a bitwise and, or, and exclusive or operation, reduced over every bit in \vv{e}.

In all cases, the reduction incorporates as an inductive base case the ``identity value'' associated with each operator. This is defined as the value that preserves the value of the other argument: one for \vv{and} (as $x \wedge 1 = x$), zero for \vv{or} (as $x \vee 0 = x$), and zero for \vv{xor} (as $x \oplus 0 = x$). Note that the logical consequence is that the and-reduction of a zero-width expression returns a one, while the or- and xor-reductions of a zero-width expression both return zero.

\subsection{Concatenate Operation}

\begin{figure}[H]
{ \fontsize{10pt}{1.10em}\selectfont
{\ttfamily
\begin{tabular}{ |c|c|c|c|c|c| }
  \opheader
  \mrow{3}{cat} & \mrow{2}{(e1,e2)} & \mrow{3}{()} & (UInt, UInt)   & UInt & w\ts{e1}+w\ts{e2}\\
                &                   &              & (SInt, SInt)   & UInt & w\ts{e1}+w\ts{e2}\\
                &                   &              & (Fixed, Fixed) & UInt & w\ts{e1}+w\ts{e2}\\
 \hline
\end{tabular}
}}
\end{figure}

The result of the concatenate operation is the bits of \vv{e1} concatenated to the most significant end of the bits of \vv{e2}.

\subsection{Bit Extraction Operation}

\begin{figure}[H]
{ \fontsize{10pt}{1.10em}\selectfont
{\ttfamily
\begin{tabular}{ |c|c|c|c|c|c| }
  \opheader
  \mrow{3}{bits} & \mrow{3}{(e)} & \mrow{3}{(hi,lo)} & (UInt)  & UInt & hi-lo+1\\
                 &               &                   & (SInt)  & UInt & hi-lo+1\\
                 &               &                   & (Fixed) & UInt & hi-lo+1\\
 \hline
\end{tabular}
}}
\end{figure}

The result of the bit extraction operation are the bits of \vv{e} between \vv{lo} (inclusive) and \vv{hi} (inclusive). \vv{hi} must be greater than or equal to \vv{lo}. Both \vv{hi} and \vv{lo} must be non-negative and strictly less than the bit width of \vv{e}.

\subsection{Head}

\begin{figure}[H]
{ \fontsize{10pt}{1.10em}\selectfont
{\ttfamily
\begin{tabular}{ |c|c|c|c|c|c| }
  \opheader
  \mrow{3}{head} & \mrow{3}{(e)} & \mrow{3}{(n)} & (UInt)  & UInt & n\\
                 &               &               & (SInt)  & UInt & n\\
                 &               &               & (Fixed) & UInt & n\\
 \hline
\end{tabular}
}}
\end{figure}

The result of the head operation are the \vv{n} most significant bits of \vv{e}. \vv{n} must be non-negative and less than or equal to the bit width of \vv{e}.

\subsection{Tail}

\begin{figure}[H]
{ \fontsize{10pt}{1.10em}\selectfont
{\ttfamily
\begin{tabular}{ |c|c|c|c|c|c| }
  \opheader
  \mrow{3}{tail} & \mrow{3}{(e)} & \mrow{3}{(n)} & (UInt)  & UInt & w\ts{e}-n\\
                 &               &               & (SInt)  & UInt & w\ts{e}-n\\
                 &               &               & (Fixed) & UInt & w\ts{e}-n\\
 \hline
\end{tabular}
}}
\end{figure}

The tail operation truncates the \vv{n} most significant bits from \vv{e}. \vv{n} must be non-negative and less than or equal to the bit width of \vv{e}.

\subsection{Fixed-Point Precision Modification Operations}

\begin{figure}[H]
{ \fontsize{10pt}{1.10em}\selectfont
{\ttfamily
\begin{tabular}{ |c|c|c|c|c|c| }
  \opheader
  incp & \mrow{3}{(e)} & \mrow{3}{(n)} & \mrow{3}{(Fixed)} & \mrow{3}{Fixed} & \mrow{3}{\nit{see section \ref{fixed_rules}}}\\
  decp &               &               &                   &                 &\\
  setp &               &               &                   &                 &\\
 \hline
\end{tabular}
}}
\end{figure}

The increase precision, decrease precision, and set precision operations are used to alter the
number of bits that appear after the binary point in a fixed-point number. This will cause the
binary point and consequently the total width of the fixed-point result type to differ from those of
the fixed-point argument type. See section \ref{fixed_rules} for more detail.

\section{Flows}\label{flows}

An expression's flow partially determines the legality of connecting to and from the expression. Every expression is classified as either {\em source}, {\em sink}, or {\em duplex}. For details on connection rules refer back to sections \ref{connects} and \ref{partial_connects}.

The flow of a reference to a declared circuit component depends on the kind of circuit component. A reference to an input port, an instance, a memory, and a node, is a source. A reference to an output port is a sink. A reference to a wire or register is duplex.

The flow of a sub-index or sub-access expression is the flow of the vector-typed expression it indexes or accesses.

The flow of a sub-field expression depends upon the orientation of the field. If the field is not flipped, its flow is the same flow as the bundle-typed expression it selects its field from. If the field is flipped, then its flow is the reverse of the flow of the bundle-typed expression it selects its field from. The reverse of source is sink, and vice-versa. The reverse of duplex remains duplex.

The flow of all other expressions are source.

\section{Width Inference}\label{width_inference}

For all circuit components declared with unspecified widths, the FIRRTL compiler will infer the minimum possible width that maintains the legality of all its incoming connections. If a component has no incoming connections, and the width is unspecified, then an error is thrown to indicate that the width could not be inferred.

For module input ports with unspecified widths, the inferred width is the minimum possible width that maintains the legality of all incoming connections to all instantiations of the module.

The width of a ground-typed multiplexer expression is the maximum of its two corresponding input widths. For multiplexing aggregate-typed expressions, the resulting widths of each leaf sub-element is the maximum of its corresponding two input leaf sub-element widths.

The width of a conditionally valid expression is the width of its input expression.

The width of each primitive operation is detailed in section \ref{primitives}.

The width of the integer literal expressions is detailed in their respective sections.

\section{Fixed-Point Math}\label{fixed_rules}

\begin{figure}[H]
  \bgroup
  \newcommand{\pt}[1]{p\ts{#1}}
  \newcommand{\w}[1]{w\ts{#1}}
  \newcommand{\prebits}[1]{\w{#1}-\pt{#1}}
  \centering
      { \fontsize{10pt}{1.10em}\selectfont
        {\ttfamily
          \begin{tabular}{|c|c|c|}
            \hline
            \multicolumn{1}{|c|}{\multirow{2}{*}{\nf{Operator}}} & \multicolumn{2}{c|}{\nf{Result}}\\
            \multicolumn{1}{|c|}{} & \multicolumn{1}{c}{\nit{Width}} & \multicolumn{1}{c|}{\nit{Binary Point}}\\ \hline
            add(e1, e2) & max(\prebits{e1}, \prebits{e2}) + max(\pt{e1}, \pt{e2}) + 1 & max(\pt{e1}, \pt{e2}) \\ \hline
            sub(e1, e2) & max(\prebits{e1}, \prebits{e2}) + max(\pt{e1}, \pt{e2}) + 1 & max(\pt{e1}, \pt{e2}) \\ \hline
            mul(e1, e2) & \w{1} + \w{2}                                               & \pt{1} + \pt{2} \\ \hline
          \end{tabular}
        }
      }
      \caption{Propagation rules for binary primitive operators that operate on two fixed-point
        numbers. Here, \texttt{\w{e1}} and \texttt{\pt{e1}} are used to indicate the width and
        binary point of the first operand, while \texttt{\w{e2}} and \texttt{\pt{e2}} are used to
        indicate the width and binary point of the second operand.}
      \label{fixed_binary_rules}
  \egroup
\end{figure}

\begin{figure}[H]
  \bgroup
  \newcommand{\pt}[1]{p\ts{#1}}
  \newcommand{\w}[1]{w\ts{#1}}
  \centering
      { \fontsize{10pt}{1.10em}\selectfont
        {\ttfamily
          \begin{tabular}{|c|c|c|}
            \hline
            \multicolumn{1}{|c|}{\multirow{2}{*}{\nf{Operator}}} & \multicolumn{2}{c|}{\nf{Result}}\\
            \multicolumn{1}{|c|}{} & \multicolumn{1}{c}{\nit{Width}} & \multicolumn{1}{c|}{\nit{Binary Point}}\\ \hline
            pad(e, n)  & max(\w{e}, n)                  & \pt{e} \\ \hline
            shl(e, n)  & \w{e} + n                      & \pt{e} \\ \hline
            shr(e, n)  & max(\w{e} - n, max(1, \pt{e})) & \pt{e} \\ \hline
            incp(e, n) & \w{e} + n                      & \pt{e} + n \\ \hline
            decp(e, n) & \w{e} - n                      & \pt{e} - n \\ \hline
            setp(e, n) & \w{e} - \pt{e} + n             & n \\ \hline
          \end{tabular}
        }
      }
      \caption{Propagation rules for binary primitive operators that modify the width and/or
        precision of a single fixed-point number using a constant integer literal parameter. Here,
        \texttt{\w{e}} and \texttt{\pt{e}} are used to indicate the width and binary point of the
        fixed-point operand, while \texttt{n} is used to represent the value of the constant
        parameter.}
      \label{fixed_and_const_rules}
  \egroup
\end{figure}

\begin{figure}[H]
  \bgroup
  \newcommand{\pt}[1]{p\ts{#1}}
  \newcommand{\w}[1]{w\ts{#1}}
  \newcommand{\prebits}[1]{\wd{#1}-\pt{#1}}
  \centering
      { \fontsize{10pt}{1.10em}\selectfont
        {\ttfamily
          \begin{tabular}{|c|c|c|}
            \hline
            \multicolumn{1}{|c|}{\multirow{2}{*}{\nf{Operator}}} & \multicolumn{2}{c|}{\nf{Result}}\\
            \multicolumn{1}{|c|}{} & \multicolumn{1}{c}{\nit{Width}} & \multicolumn{1}{c|}{\nit{Binary Point}}\\ \hline
            dshl(e1, e1) & \w{e1} + 2\verb|^|\w{e2} - 1 & \pt{e} \\ \hline
            dshr(e1, e2) & \w{e1}                         & \pt{e} \\ \hline
          \end{tabular}
        }
      }
      \caption{Propagation rules for dynamic shifts on fixed-point numbers. These take a fixed-point
        argument and an UInt argument. Here, \texttt{\w{e1}} and \texttt{\pt{e1}} are used to
        indicate the width and binary point of the fixed-point operand, while \texttt{\w{e2}} is
        used to represent the width of the unsigned integer operand. Note that the actual shift
        amount will be the dynamic value of the \texttt{e2} argument.}
      \label{fixed_dynamic_shifts}
  \egroup
\end{figure}

\section{Namespaces} \label{namespaces}

All modules in a circuit exist in the same module namespace, and thus must all have a unique name.

Each module has an identifier namespace containing the names of all port and circuit component declarations. Thus, all declarations within a module must have unique names. Furthermore, the set of component declarations within a module must be {\em prefix unique}. Please see section \ref{prefix_unique} for the definition of prefix uniqueness.

Within a bundle type declaration, all field names must be unique.

Within a memory declaration, all port names must be unique.

During the lowering transformation, all circuit component declarations with aggregate types are rewritten as a group of component declarations, each with a ground type. The name expansion algorithm in section \ref{expansion_algorithm} calculates the names of all replacement components derived from the original aggregate-typed component.

After the lowering transformation, the names of the lowered circuit components are guaranteed by the name expansion algorithm and thus can be reliably referenced by users to pair meta-data or other annotations with named circuit components.

\subsection{Name Expansion Algorithm} \label{expansion_algorithm}

Given a component with a ground type, the name of the component is returned.

Given a component with a vector type, the suffix \verb|$|{\em i} is appended to the expanded names of each sub-element, where {\em i} is the index of each sub-element.

Given a component with a bundle type, the suffix \verb|$|{\em f} is appended to the expanded names of each sub-element, where {\em f} is the field name of each sub-element.

\subsection{Prefix Uniqueness} \label{prefix_unique}

The {\em symbol sequence} of a name is the ordered list of strings that results from splitting the name at each occurrence of the `\$' character.

A symbol sequence $a$ is a {\em prefix} of another symbol sequence $b$ if the strings in $a$ occur in the beginning of $b$.

A set of names are defined to be {\em prefix unique} if there exists no two names such that the symbol sequence of one is a prefix of the symbol sequence of the other.

As an example \verb|firetruck$y$z| shares a prefix with \verb|firetruck$y| and \verb|firetruck|, but does not share a prefix with \verb|fire|.

\section{The Lowered FIRRTL Forms}

The lowered FIRRTL forms, MidFIRRTL and LoFIRRTL, are increasingly restrictive subsets of the FIRRTL language that omit many of the higher level constructs. All conforming FIRRTL compilers must provide a {\em lowering transformation} that transforms arbitrary FIRRTL circuits into equivalent LoFIRRTL circuits. However, there are no additional requirements related to accepting or producing MidFIRRTL, as the LoFIRRTL output of the lowering transformation will already be a legal subset of MidFIRRTL.

\subsection{MidFIRRTL}

A FIRRTL circuit is defined to be a valid MidFIRRTL circuit if it obeys the following restrictions:
\begin{itemize}
\item All widths must be explicitly defined.
\item The conditional statement is not used.
\item The dynamic sub-access expression is not used.
\item All components are connected to exactly once.
\end{itemize}

\subsection{LoFIRRTL}

A FIRRTL circuit is defined to be a valid LoFIRRTL circuit if it obeys the following restrictions:
\begin{itemize}
\item All widths must be explicitly defined.
\item The conditional statement is not used.
\item All components are connected to exactly once.
\item All components must be declared with a ground type.
\item The partial connect statement is not used.
\end{itemize}

The first three restrictions follow from the fact that any LoFIRRTL circuit is also a legal MidFIRRTL circuit. The additional restrictions give LoFIRRTL a direct correspondence to a circuit netlist.

Low level circuit transformations can be conveniently written by first lowering a circuit to its LoFIRRTL form, then operating on the restricted (and thus simpler) subset of constructs. Note that circuit transformations are still free to generate high level constructs as they can simply be lowered again.

The following module:
\begin{lstlisting}
module MyModule :
   input in: {a:UInt<1>, b:UInt<2>[3]}
   input clk: Clock
   output out: UInt
   wire c: UInt
   c <= in.a
   reg r: UInt[3], clk
   r <= in.b
   when c :
      r[1] <= in.a
   out <= r[0]
\end{lstlisting}
is rewritten as the following equivalent LoFIRRTL circuit by the lowering transform.
\begin{lstlisting}
module MyModule :
   input in$a: UInt<1>
   input in$b$0: UInt<2>
   input in$b$1: UInt<2>
   input in$b$2: UInt<2>
   input clk: Clock
   output out: UInt<2>
   wire c: UInt<1>
   c <= in$a
   reg r$0: UInt<2>, clk
   reg r$1: UInt<2>, clk
   reg r$2: UInt<2>, clk
   r$0 <= in$b$0
   r$1 <= mux(c, in$a, in$b$1)
   r$2 <= in$b$2
   out <= r$0
\end{lstlisting}

\section{Details about Syntax}

FIRRTL's syntax is designed to be human-readable but easily algorithmically parsed.

The following characters are allowed in identifiers: upper and lower case letters, digits, and \verb|_|. Identifiers cannot begin with a digit.

An integer literal in FIRRTL begins with one of the following, where `\#' represents a digit between 0 and 9.
\begin{itemize}
\item `h' : For indicating a hexadecimal number, followed by an optional sign. The rest of the literal must consist of either digits or a letter between `A' and `F'.
\item `o' : For indicating an octal number, followed by an optional sign. The rest of the literal must consist of digits between 0 and 7.
\item `b' : For indicating a binary number, followed by an optional sign. The rest of the literal must consist of digits that are either 0 or 1.
\item `-\#' : For indicating a negative decimal number. The rest of the literal must consist of digits between 0 and 9.
\item `\#' : For indicating a positive decimal number. The rest of the literal must consist of digits between 0 and 9.
\end{itemize}

Comments begin with a semicolon and extend until the end of the line. Commas are treated as whitespace, and may be used by the user for clarity if desired.

In FIRRTL, indentation is significant.
Indentation must consist of spaces only---tabs are illegal characters.
The number of spaces appearing before a FIRRTL IR statement is used to establish its \emph{indent level}.
Statements with the same indent level have the same context.
The indent level of the \verb|circuit| declaration must be zero.

Certain constructs (\verb|circuit|, \verb|module|, \verb|when|, and \verb|else|) create a new sub-context.
The indent used on the first line of the sub-context establishes the indent level.
The indent level of a sub-context is one higher than the parent.
All statements in the sub-context must be indented by the same number of spaces.
To end the sub-context, a line must return to the indent level of the parent.

Since conditional statements (\verb|when| and \verb|else|) may be nested, it is possible to create a hierarchy of indent levels, each with its own number of preceding spaces that must be larger than its parent’s and consistent among all direct child statements (those that are not children of an even deeper conditional statement).

As a concrete guide, a few consequences of these rules are summarized below:

\begin{itemize}
\item The \verb|circuit| keyword must not be indented.
\item All \verb|module| keywords must be indented by the same number of spaces.
\item In a module, all port declarations and all statements (that are not children of other statements) must be indented by the same number of spaces.
\item The number of spaces comprising the indent level of a module is specific to each module.
\item The statements comprising a conditional statement's branch must be indented by the same number of spaces.
\item The statements of nested conditional statements establish their own, deeper indent level.
\item Each \verb|when| and each \verb|else| context may have a different number of non-zero spaces in its indent level.
\end{itemize}

As an example illustrating some of these points, the following is a legal FIRRTL circuit:

\begin{lstlisting}
circuit Foo :
    module Foo :
      skip
    module Bar :
     input a: UInt<1>
     output b: UInt<1>
     when a:
         b <= a
     else:
       b <= not(a)
\end{lstlisting}

All circuits, modules, ports and statements can optionally be followed with the info token \verb|@[fileinfo]|
where fileinfo is a string containing the source file information from where it was generated.
The following characters need to be escaped with a leading `\verb|\|':
`\verb|\n|' (new line), `\verb|\t|' (tab), `\verb|]|' and `\verb|\|' itself.

The following example shows the info tokens included:

\begin{lstlisting}
circuit Top : @[myfile.txt 14:8]
   module Top : @[myfile.txt 15:2]
     output out:UInt @[myfile.txt 16:3]
     input b:UInt<32> @[myfile.txt 17:3]
     input c:UInt<1> @[myfile.txt 18:3]
     input d:UInt<16> @[myfile.txt 19:3]
     wire a:UInt @[myfile.txt 21:8]
     when c : @[myfile.txt 24:8]
       a <= b @[myfile.txt 27:16]
     else :
       a <= d @[myfile.txt 29:17]
     out <= add(a,a) @[myfile.txt 34:4]
\end{lstlisting}

\section{FIRRTL Language Definition}
\newcommand{\pipe}{\textbar}
\newcommand{\opt}[1]{$\llbracket$#1$\rrbracket_?$}
\newcommand{\rpt}[1]{$\llbracket$#1$\rrbracket_{...}$}
\subsection{Notation}
The concrete syntax of FIRRTL is defined in section \ref{syntax_tree}. Productions in the syntax tree are {\em italicized} and keywords are written in \verb|monospaced| font. The special productions \pd{id}, \pd{int}, and \pd{string}, indicates an identifier, an integer literal, and a string respectively. The notation \rpt{\pd{e}} is used to indicate that \pd{e} is repeated zero or more times, and the notation \opt{\pd{e}} is used to indicate that including \pd{e} is optional.

\subsection{Concrete Syntax Tree} \label{syntax_tree}

\begin{tabular}{rrll}
\pd{circuit}    &=     &\vv{circuit} \pd{id} \vv{:} \opt{\pd{info}} \vv{(}\rpt{\pd{module}}\vv{)}              &\text{Circuit}\\
\pd{module}     &=     &\vv{module} \pd{id} \vv{:} \opt{\pd{info}} \vv{(}\rpt{\pd{port}} \pd{stmt}\vv{)}       &\text{Module}\\
                       &\pipe &\vv{extmodule} \pd{id} \vv{:} \opt{\pd{info}} \vv{(}\rpt{\pd{port}}\vv{)}
                        \vv{(}\pd{defname}\vv{)}
                        \vv{(}\rpt{\pd{parameter}}\vv{)}
                                                                                                               &\text{External Module}\\
\pd{port}       &=     &\pd{dir} \pd{id} \vv{:} \pd{type} \opt{\pd{info}}                                      &\text{Port}\\
\pd{dir}        &=     &\vv{input} \pipe \vv{ output}                                                          &\text{Port Direction}\\
\pd{type}       &=     &\vv{UInt}\opt{\vv{<}\pd{int}\vv{>}}                                                    &\text{Unsigned Integer}\\
                &\pipe &\vv{SInt}\opt{\vv{<}\pd{int}\vv{>}}                                                    &\text{Signed Integer}\\
                &\pipe &\vv{Fixed}\opt{\vv{<}\pd{int}\vv{>}}\opt{\vv{<<}\pd{int}\vv{>>}}                       &\text{Fixed-Point Number}\\
                &\pipe &\vv{Clock}                                                                             &\text{Clock}\\
                &\pipe &\vv{Analog}\opt{\vv{<}\pd{int}\vv{>}}                                                  &\text{Analog}\\
                &\pipe &\verb|{|\rpt{\pd{field}}\verb|}|                                                       &\text{Bundle}\\
                &\pipe &\pd{type}\vv{[}\pd{int}\vv{]}                                                          &\text{Vector}\\
\pd{field}      &=     &\opt{\vv{flip}} \pd{id} \vv{:} \pd{type}                                               &\text{Bundle Field}\\
\pd{stmt}       &=     &\vv{wire} \pd{id} \vv{:} \pd{type} \opt{\pd{info}}                                     &\text{Wire}\\
                &\pipe &\vv{reg} \pd{id} \vv{:} \pd{type} \pd{exp} \opt{\vv{(with:} \vv{\{reset => (}\pd{exp}, \pd{exp}\vv{)\})}} \opt{\pd{info}}   &\text{Register}\\
                &\pipe &\vv{mem} \pd{id} \vv{:} \opt{\pd{info}} \vv{(}                                         &\text{Memory}\\
                && \verb|       |\vv{data-type =>} \pd{type}\\
                && \verb|       |\vv{depth =>} \pd{int}\\
                && \verb|       |\vv{read-latency =>} \pd{int}\\
                && \verb|       |\vv{write-latency =>} \pd{int}\\
                && \verb|       |\vv{read-under-write =>} \pd{ruw}\\
                && \verb|       |\rpt{\vv{reader =>} \pd{id}}\\
                && \verb|       |\rpt{\vv{writer =>} \pd{id}}\\
                && \verb|       |\rpt{\vv{readwriter =>} \pd{id}}\vv{)}                                \\
                &\pipe &\vv{inst} \pd{id} \vv{of} \pd{id} \opt{\pd{info}}                                      &\text{Instance}\\
                &\pipe &\vv{node} \pd{id} \vv{=} \pd{exp} \opt{\pd{info}}                                      &\text{Node}\\
                &\pipe &\pd{exp} \vv{<=} \pd{exp} \opt{\pd{info}}                                              &\text{Connect}\\
                &\pipe &\pd{exp} \vv{<-} \pd{exp} \opt{\pd{info}}                                              &\text{Partial Connect}\\
                &\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{\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}\\
\pd{info}       &=     &\vv{@[}\pd{string}\vv{]}                                                               &\text{File Information Token}\\
\pd{defname}    &=     &\vv{defname} \vv{=} \pd{string}                                                        &\text{External Module Defname}\\
\pd{parameter}  &=     &\vv{parameter} \vv{=} \vv{(} \pd{string} \pipe~\pd{int} \vv{)}
\end{tabular}

\begin{tabular}{rrll}
\pd{exp}        &=     &\vv{UInt}\opt{\vv{<}\pd{int}\vv{>}}\vv{(}\pd{int}\vv{)}                                &\text{Literal Unsigned Integer}\\
                &\pipe &\vv{UInt}\opt{\vv{<}\pd{int}\vv{>}}\vv{(}\pd{string}\vv{)}                             &\text{Literal Unsigned Integer From Bits}\\
                &\pipe &\vv{SInt}\opt{\vv{<}\pd{int}\vv{>}}\vv{(}\pd{int}\vv{)}                                &\text{Literal Signed Integer}\\
                &\pipe &\vv{SInt}\opt{\vv{<}\pd{int}\vv{>}}\vv{(}\pd{string}\vv{)}                             &\text{Literal Signed Integer From Bits}\\
                &\pipe &\pd{id}                                                                                &\text{Reference}\\
                &\pipe &\pd{exp}\vv{.}\pd{id}                                                                  &\text{Sub-field}\\
                &\pipe &\pd{exp}\vv{[}\pd{int}\vv{]}                                                           &\text{Sub-index}\\
                &\pipe &\pd{exp}\vv{[}\pd{exp}\vv{]}                                                           &\text{Sub-access}\\
                &\pipe &\vv{mux}\vv{(}\pd{exp}, \pd{exp}, \pd{exp}\vv{)}                                       &\text{Multiplexer}\\
                &\pipe &\vv{validif}\vv{(}\pd{exp}, \pd{exp}\vv{)}                                             &\text{Conditionally Valid}\\
                &\pipe &\pd{primop}\vv{(}\rpt{\pd{exp}}, \rpt{\pd{int}}\vv{)}                                  &\text{Primitive Operation}\\
\end{tabular}

\begin{tabular}{rrll}
\pd{primop}   &=               &\vv{add}            &\text{Add}\\
              &\pipe           &\vv{sub}            &\text{Subtract}\\
              &\pipe           &\vv{mul}            &\text{Multiply}\\
              &\pipe           &\vv{div}            &\text{Divide}\\
              &\pipe           &\vv{mod}            &\text{Modulo}\\
              &\pipe           &\vv{lt}             &\text{Less Than}\\
              &\pipe           &\vv{leq}            &\text{Less or Equal}\\
              &\pipe           &\vv{gt}             &\text{Greater Than}\\
              &\pipe           &\vv{geq}            &\text{Greater or Equal}\\
              &\pipe           &\vv{eq}             &\text{Equal}\\
              &\pipe           &\vv{neq}            &\text{Not-Equal}\\
              &\pipe           &\vv{pad}            &\text{Pad}\\
              &\pipe           &\vv{asUInt}         &\text{Interpret Bits as UInt}\\
              &\pipe           &\vv{asSInt}         &\text{Interpret Bits as SInt}\\
              &\pipe           &\vv{asClock}        &\text{Interpret as Clock}\\
              &\pipe           &\vv{shl}            &\text{Shift Left}\\
              &\pipe           &\vv{shr}            &\text{Shift Right}\\
              &\pipe           &\vv{dshl}           &\text{Dynamic Shift Left}\\
              &\pipe           &\vv{dshr}           &\text{Dynamic Shift Right}\\
              &\pipe           &\vv{cvt}            &\text{Arithmetic Convert to Signed}\\
              &\pipe           &\vv{neg}            &\text{Negate}\\
              &\pipe           &\vv{not}            &\text{Not}\\
              &\pipe           &\vv{and}            &\text{And}\\
              &\pipe           &\vv{or}             &\text{Or}\\
              &\pipe           &\vv{xor}            &\text{Xor}\\
              &\pipe           &\vv{andr}           &\text{And Reduce}\\
              &\pipe           &\vv{orr}            &\text{Or Reduce}\\
              &\pipe           &\vv{xorr}           &\text{Xor Reduce}\\
              &\pipe           &\vv{cat}            &\text{Concatenation}\\
              &\pipe           &\vv{bits}           &\text{Bit Extraction}\\
              &\pipe           &\vv{head}           &\text{Head}\\
              &\pipe           &\vv{tail}           &\text{Tail}\\
\end{tabular}

%\section{TODO}
%
%- FIRRTL implementation
%   - Add partial connect algorithm     ;
%   - Add oriented types to type checker
%   - Add memory read-under-write flag  ; probably overengineering, but could be a wash

\end{document}