11institutetext: School of Cyber Science and Technology, College of Computer
Science and
Technology, Zhejiang University, China
11email<EMAIL_ADDRESS>11email<EMAIL_ADDRESS>22institutetext: State Key Laboratory of Blockchain and Data Security,
Zhejiang University, China

# K-CIRCT: A Layered, Composable, and Executable Formal Semantics for CIRCT
Hardware IRs

Jianhong Zhao 11 Jinhui Kang 11 Yongwang Zhao 11 2( 2())

###### Abstract

CIRCT, an open-source EDA framework akin to LLVM for software, is a foundation
for various hardware description languages. Despite its crucial role, CIRCT’s
lack of formal semantics challenges necessary rigorous hardware verification.
Thus, this paper introduces K-CIRCT, the first formal semantics in
$\mathbb{K}$ for a substantial CIRCT subset adequate for simulating a RISC-V
processor. Our semantics are structured into multiple layers: (1) MLIR static
semantics, which covers fundamental MLIR concepts across domains; (2) CIRCT
common semantics, featuring a generic hardware model that captures key
hardware features across dialects; and (3) composable and extensible semantics
for specific dialects, formalized individually using a unified approach. This
approach has been applied to formalize CIRCT core dialects. We validated our
semantics through full-rule coverage tests and assessed its practicality using
the popular RISC-V hardware design, riscv-mini.

###### Keywords:

Formal Semantics Hardware Design CIRCT MLIR.

##  1 Introduction

CIRCT [18] (Circuit IR Compilers and Tools) is an open-source compiler
infrastructure for hardware description languages (HDLs), inspired by LLVM’s
[3] success in software. It transforms both traditional HDLs (e.g.,
SystemVerilog [2] and VHDL [6]) and modern languages (e.g., Chisel [1] and
Magma [4]) into formats for simulation, synthesis, and placement. Unlike LLVM,
CIRCT introduces multiple intermediate representations (IRs) for different
purposes. These IRs are defined as dialects in MLIR [17] (Multi-Level
Intermediate Representation), a compiler infrastructure to extend, modify, and
combine dialects across domains.

Unfortunately, CIRCT lacks formal semantics, undermining formal reasoning
about hardware designs. This absence prevents proving the correctness of
CIRCT-based hardware designs, compilers, synthesized circuits, and simulators.
Furthermore, bug-finding tools like symbolic test generators and bounded model
checkers depend on definitive formal semantics to function correctly.

Goal and Challenges. To tackle this pivotal issue, this paper proposes the
first formal semantics for CIRCT, using the $\mathbb{K}$ framework [5] to lay
a rigorous and reliable foundation for modern hardware design. Yet,
formalizing CIRCT semantics is challenging due to the following features:

1\. Composability and Extensibility. A CIRCT/MLIR program often contains
multiple dialects simultaneously. This multi-dialect feature demands the
composability of various dialect semantics. In contrast, current efforts in
formal semantics [11, 16, 15, 9, 12, 10, 13, 7] primarily focus on individual
languages rather than combinations of dialect semantics. Moreover, built on
MLIR, CIRCT enables the creation and modification of dialects. This requires
the extensibility of dialect semantics, which is also less considered by these
existing efforts.

2\. Generic Hardware Features. CIRCT compiles various HDLs into different
outputs to support hardware design. It does this by capturing the features of
HDLs through multiple dialects at various abstraction levels. Each dialect is
designed to capture different hardware features, including combinational and
sequential logic, operation concurrency, and complexities in SystemVerilog.
Therefore, beyond just formalizing these features, there is a need for a
generic hardware model that can formalize key hardware features across diverse
semantics of these dialects. Existing efforts [11, 16, 15, 9, 12] focus on
formalizing one specific HDL and lack a generic model that addresses the
complexities of various dialects.

Insight and Solution. We observe that the CIRCT project can be decomposed into
multiple layers. (1) MLIR, as the top layer, provides a unified compiler
infrastructure across domains, including machine learning [17, 7] and quantum
computing [19]. (2) CIRCT, as the middle layer, introduces multiple dialects
tailored for hardware design. (3) Specific CIRCT dialects, as the bottom
layers, capture different hardware aspects at different abstraction levels.
For example, `hw` deals with hardware module, `comb` focuses on combinational
logic, `seq` addresses digital sequential logic, and `sv` contains
SystemVerilog (SV) features to facilitate translations into SV. Our insight is
that we can systematically formalize this layered structure, from MLIR through
CIRCT to its specific dialects. Each upper layer is well-designed to provide
composability and extensibility for the lower layers. For composability, the
upper layers provide effectful functions as interfaces for individual
semantics of different lower layers. These functions enable lower layers to
access a shared state when they are combined, facilitating their interaction
without creating dependencies in their individual semantics. For
extensibility, the upper layers cover the diversity of lower layers yet are
concrete enough to simplify their formalization. To evaluate our approach, we
present our semantics in $\mathbb{K}$ for executability.

MLIR static semantics (§ 3) provides effectful functions for various domain
semantics (e.g., machine learning and hardware) to access preprocessed and
normalized information. This semantics covers fundamental MLIR concepts across
domains, including generic syntax, preprocessing of type and attribute
aliases, and constructing a symbol table for operations. It eases the
extension of various domain semantics, allowing them to focus on their domain-
specific semantics. CIRCT common semantics (§ 4) enables flexible combinations
of various CIRCT dialect semantics via effectful functions on a generic
hardware model. This model covers key hardware features across dialects to
ease their formalization. Specifically, we present a bit manipulation library
for combinational logic and effectful functions for sequential logic and
operation concurrency.

Using these upper layers, we provide a unified approach to formalize and
combine the semantics of CIRCT dialects (§ 5). This approach further
deconstructs dialect semantics into their minimal semantic units (i.e.,
operations) and provides a step-by-step process to formalize composable
semantics of individual operations. Employing this approach, we have
formalized core CIRCT dialects (i.e., `hw`, `comb`, `seq`, `sv`) that other
dialects can transform into or from.

We provide a simulator and a benchmark to evaluate our semantics (§ 6). The
simulator offers a user-friendly interface for hardware designers, using our
executable semantics defined in $\mathbb{K}$. The benchmark includes two
parts: (1) A full-rule coverage test suite, crucial because official CIRCT
tests do not cover all the semantic rules. (2) A practical test using riscv-
mini, a popular RISC-V design in Chisel. We compile this design into over 1000
lines of CIRCT code to ensure that our semantics are sufficient for complex
designs.

In summary, we make the following main contributions:

  * •

We introduce K-CIRCT, the first semantics for CIRCT capable of simulating
complex hardware designs, e.g., a RISC-V design. It enables the composability
and extensibility of CIRCT dialect semantics through a layered mechanism with
effectful functions. We organize the semantics into layers: starting with
domain-agnostic MLIR static semantics, moving to dialect-agnostic CIRCT common
semantics, and ending in specific dialect semantics. Specifically, CIRCT
common semantics contains a generic hardware model to cover key hardware
features, simplifying hardware-specific dialects’ formalization.

  * •

We implement a simulator and use it to evaluate our semantics through a full-
rule coverage test suite and a popular RISC-V design, mini-riscv.

K-CIRCT, including the formal semantics, a semantics-based simulator, and test
suites, is available at this GitHub repository.

##  2 Overview

This section introduces our formalization target, CIRCT, using a running
example, and presents an overview of our formalization approach.

###  2.1 A Running Example for CIRCT

As mentioned, MLIR is a cross-domain compiler infrastructure, and CIRCT
employs this infrastructure to provide multiple dialects and combine them to
describe the hardware. The dynamic semantics of operations within MLIR and
CIRCT remain undefined until they are explicitly specified within a dialect.
Fig. 1 describes the `Counter` hardware circuit using a combination of
dialects `hw`, `comb`, and `seq` to show this layered semantics. Firstly, the
program (Fig. 1 left side) conforms to the generic MLIR syntax (discussed in §
3), with MLIR itself unaware of the meanings of specific operations.
Similarly, as a hardware compiler framework, CIRCT recognizes the hardware
structure and the internal component connections shown on the right side of
Fig. 1, yet it does not understand these components’ semantic details. Clarity
on the dynamic semantics of an operation emerges only when delving into
specific dialects, e.g., `hw.module` in `hw` dialect, `seq.firreg` in `seq`
dialect, and `comb.add` in `comb` dialect.

Figure 1: An example of CIRCT/MLIR program.

Delving deeper into this hardware description, the circuit is designed to
count the clock, starting at 0 from reset. Line 1 introduces the circuit
module using the `hw.module` operation, with `!hw.modty` specifying its
interface, and `sym_name` identifying its symbol in lines 9-10. A single-block
region starts at line 2, connecting the input port labeled `clk` to `%clk`,
and `reset` to `%reset`. Within this block, `seq.firreg` presents a
synchronous register, equipped with an output port for accessing stored values
and four input ports for control. This synchronous setup ensures that the
register’s content updates only at specific edges of the clock signal. On the
rising edge of the `%clk` port, the register updates to a new value provided
by the `%next` port, and resets by the `%c0` port when the `%reset` port is
triggered. Operation `comb.add` in line 5 constructs a physical net to add the
input ports `%reg_port` and `%c1`. Notably, the input port of `comb.add` is
connected to the output port of the counter register via `%reg_port`. Lines
6-7 present 8-bit constant voltage nets linked to `%c0` and `%c1`,
respectively. Finally, line 8 connects the register’s output port `%reg_port`
to the module’s output interface `res`, completing the circuit’s capability to
start counting from 0 upon reset.

###  2.2 Approach Overview

To address the complexity of MLIR and CIRCT, we introduce two key strategies:
(1) a layered mechanism with effectful functions for extensible and composable
semantics and (2) a generic model to capture key hardware features. Fig. 2
shows a comprehensive overview of our approach, including three basic layers
of semantics. This structure progressively refines from domain-agnostic MLIR
semantics to dialect-agnostic CIRCT semantics, before delving into individual
semantics of various dialects. Utilizing our formalized semantics, we
implement a simulator and a benchmark to evaluate the semantics.

Figure 2: The structure of K-CIRCT.

MLIR static semantics (§ 3) presents generic MLIR syntax to define a program,
alongside an MLIR state $S_{mlir}$ to store the program and preprocessed data.
The MLIR static rules just preprocess the program and store the normalized
information in $S_{mlir}$ to cover the diversity of different domains.
Effectful functions are interfaces for various domain-specific layers to
access data in $S_{mlir}$.

CIRCT common semantics (§ 4) primarily addresses hardware features, omitting
cross-domain generalizations. To house the diversity of various CIRCT
dialects, the CIRCT state $S_{circt}$ contains a generic model to capture key
hardware features. This model is accessible via dialect-agnostic CIRCT
effectful functions, simplifying the formalization of hardware-specific
semantics for dialect-specific layers. Notably, some of these effectful
functions are auto-triggered, thereby eliminating the need for explicit calls
by dialect semantics.

Unified CIRCT dialects formalization (§ 5) presents an approach to formalize
the semantics of individual operations and to combine these into specific
dialect semantics. From our observation, operations like `hw.module` and
`comb.icmp` are the minimal semantic units in CIRCT/MLIR. Each dialect
comprises a set of operations that share a similar purpose and abstraction
level. Other semantic elements within the dialect, including types (e.g.,
`!hw.modty`) and attributes (e.g., `0`), are designed to support the
operations. Therefore, we provide a step-by-step approach to formalizing the
composable semantics of individual operations for various CIRCT dialects. We
then combine these operations’ semantics to construct the semantics of a
specific dialect. Using this method, we have formalized the semantics of core
CIRCT dialects: `hw`, `comb`, `seq`, and `sv`.

By combining the semantics of these core dialects, we can use $\mathbb{K}$’s
kompile tool to generate several tools, including a symbolic executor, a
formal verifier, an interpreter, etc. To evaluate our semantics (§ 6), we
employ the generated interpreter to implement a simulator with a user-friendly
interface, called Kimulator. This simulator is then utilized for full-rule
coverage testing and to check the ability of our semantics by simulating a
complex hardware design `riscv-mini`.

##  3 Formalization of MLIR Static Semantics

This section focuses on formalizing domain-agnostic concepts within MLIR,
enabling its cross-domain extensibility. Thus, we present: (1) a generic MLIR
syntax for program description, (2) a state with effectful functions for
program and information management, and (3) semantic rules for universal
preprocessing.

TopLevel $\displaystyle\text{{{\small{toplevel}}}}\Coloneqq$
(operation$\mid$ta-def$\mid$aa-def)* Operation
$\displaystyle\text{{{\small{operation}}}}\Coloneqq$ (op-results =)? str
((value-uses)?) ([successors])? (<dict-prop>)? ((regions))? ({(dict-attr)?})?
: fun-type (loc-attr)? Region
$\displaystyle\text{{{\small{regions}}}}\Coloneqq$ $\displaystyle\
\text{{{\small{region}}}}\
\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}(}}}\text{{\small{,}}}\
\text{{{\small{region}}}}\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5})*}}}\hskip
51.0pt\text{{{\small{region}}}}\Coloneqq\
\text{{\small{\\{}}}\text{{{\small{operation}}}}^{\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\text{{{\small{block}}}}\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>Block $\displaystyle\text{{{\small{block}}}}\Coloneqq$ $\displaystyle\
\text{{{\small{block-label}}}}\
\text{{{\small{operation}}}}^{\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>16.0pt\text{{{\small{block-label}}}}\Coloneqq\
\text{{\small{\^{}}}}\text{{{\small{id}}}}\
\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}(}}}\text{{\small{(}}}\text{{{\small{block-
args}}}}\text{{\small{)}}}\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5})?}}}\
\text{{\small{:}}}$ Type $\displaystyle\text{{{\small{type}}}}\Coloneqq$
$\displaystyle\ \text{{{\small{type-
alias}}}}\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>type}}}}\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>type}}}}\hskip 8.0pt\text{{{\small{ta-def}}}}\Coloneqq\ \text{{{\small{type-
alias}}}}\ \text{{\small{=}}}\ \text{{{\small{type}}}}$ Attribute
$\displaystyle\text{{{\small{attr-value}}}}\Coloneqq$ $\displaystyle\
\text{{{\small{attr-
alias}}}}\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>attr}}}}\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>attr}}}}\hskip 8.0pt\text{{{\small{aa-def}}}}\Coloneqq\ \text{{{\small{attr-
alias}}}}\ \text{{\small{=}}}\ \text{{{\small{attr-value}}}}$

Figure 3: Syntax for generic MLIR. Note that this figure omits some syntax
definitions due to the limited space. Indeed, our formalization consists of
the complete syntax. Appendix 0.A provides a more detailed version.

Syntax. Fig. 3 shows (a fragment of) the syntax for the generic MLIR. Each
MLIR source file contains a list of operations (operation), type alias
definitions (ta-def), and attribute alias definitions (aa-def). Operations
serve as MLIR’s unified computation unit. Identified by a unique string (str),
an operation can operate on values (value-uses) and potentially produce a
result assigned to variables (op-results). Beyond simple instructions,
operations can contain operations within regions’ blocks (block) for complex
constructs like `hw.module`. Consequently, developers can integrate various
representations into MLIR dialects, comprising a set of types (dialect-type),
attributes (dialect-attr), and operations.

$\left\langle\begin{aligned}
\langle\text{{{\small{toplevel}}}}\rangle_{prog}\hskip
3.0pt\langle\text{{{\small{control}}}}\rangle_{phase}\hskip
3.0pt\langle\text{{{\small{type-
alias}}}}\mapsto\text{{{\small{type}}}}\rangle_{types}\\\
\langle\text{{{\small{attr-alias}}}}\mapsto\text{{{\small{attr-
value}}}}\rangle_{attrs}\hskip
3.0pt\langle\text{{{\small{str}}}}\mapsto\text{{{\small{operation}}}}\rangle_{table}\end{aligned}\right\rangle_{mlir}$
Figure 4: The structure of MLIR state.

State. Fig. 4 depicts the MLIR state structure, where each cell is labeled
with its type inside angle brackets and its name at the bottom right. The MLIR
state <mlir> establishes a generic environment, including <prog> for
preprocessing programs, <phase> for execution control and pattern matching
clarity, <types> and <attrs> for type and attribute aliases, and <table> for
operations indexed by symbol names. Initially, the <prog> contains the MLIR
source program, <phase> is set to `preprocess`, and the other components
within <mlir> are empty, denoted as $S_{init}:=$ <pgm>prog <pre>phase <>types
<>attrs <>table.

Effectful Functions, designed to allow interaction within MLIR, enable easy
access to types, attributes, and operations via aliases or symbols. These are
accessible across all semantic layers through specific function calls:
Rta(type-alias) retrieves types, Raa(attr-alias) fetches attributes, and
Rop(str) accesses operations by symbol, ensuring a unified interface for
cross-layer operations.

Semantic Rules. Starting from the initial state $S_{init}$, the rules here
preprocess programs within <prog> and store normalized details into other
cells of <mlir>, achieving a preprocessed state $S_{ppre}$ that is ready for
effectful functions. These rules are organized into three phases: (1) Assign
Aliases (Rta & Raa): This phase compiles type alias (type-alias-def) and
attribute alias (attr-alias-def) definitions into the <types> and <attrs>
cells, respectively. (2) Normalize Operations: All operations are converted to
their canonical forms, eliminating concrete layers’ need to manage different
operation forms. (3) Construct Symbol Table (Rop): This step decodes nested
operation structures and maps operation symbols to their canonical forms in
<table>. After preprocessing all operations, the phase transitions to
`simulation`, resulting in a preprocessed state $S_{ppre}:=$
<>prog<sim>phase<ta
$\rightarrow$t>types<aa$\rightarrow$a>attrs<sid$\rightarrow$op>table. For
example, after preprocessing for Fig. 1. aliases should be empty <>types and
<>attrs , and the symbol table should be <"Counter"$\mapsto$normalized
line1-10>table.

##  4 Formalization of CIRCT Common Semantics

In this section, we aim to formalize the dialect-agnostic aspects of hardware
features by distilling the essential characteristics inherent to HDLs into
CIRCT common semantics. This semantics is located one layer above specific
dialects, enhancing cross-dialect extensibility and composability in the
hardware domain.

Unlike software languages focusing on computation, CIRCT is designed to
describe hardware structure, rendering the order of operations irrelevant and
enabling complete concurrency. It incorporates combinational logic for
managing logical gates and sequential logic to address dependencies based on
historical states. To tackle these features, we formalize bit manipulation
with constants X and Z for combinational logic, alongside a generic hardware
model that captures circuit architecture and addresses additional hardware-
domain requirements.

$\left\langle\begin{aligned} \langle\text{{{\small{...}}}}\rangle_{mlir}\\\
\langle\text{{{\small{cmd}}}}\rangle_{cmd}\end{aligned}\left\langle\begin{aligned}
\langle\text{{{\small{id*}}}}\rangle_{cid}\mapsto\langle\text{{{\small{K}}}}\rangle^{*}_{exec}\hskip
3.0pt\langle\text{{{\small{id*}}}}\rangle_{pa}\hskip
3.0pt\langle\text{{{\small{\%id}}}}\mapsto\text{{{\small{tv}}}}\rangle_{last}\hskip
3.0pt\langle\text{{{\small{\%id}}}}\mapsto\text{{{\small{tv}}}}\rangle_{curr}\\\
\langle\text{{{\small{str}}}}\rangle_{mod}\hskip
3.0pt\langle\text{{{\small{id}}}}\mapsto\text{{{\small{\%id}}}}\rangle_{out}\hskip
3.0pt\langle\text{{{\small{str}}}}\mapsto\text{{{\small{\%id}}}}\rangle_{reg}\hskip
3.0pt\langle\text{{{\small{str}}}}\mapsto\text{{{\small{\%id}}}}\rangle_{wire}\end{aligned}\right\rangle_{ckt}\right\rangle_{circt}$
Figure 5: The structure of CIRCT common state.

Generic Hardware Model. The common state extends the MLIR state with pending
CIRCT commands <cmd> and circuit layout <ckt>, as shown in Fig. 5. This layout
<ckt> presents a generic hardware model that abstracts the fundamental
structure of hardware without introducing specific dialects. It specifies key
components like the module identifier <mod>, output ports <out>, registers
<reg>, and wires <wire>. It also identifies the circuit’s logical placement
within a larger circuit by specifying its parent circuit module <pa>. To model
ports’ state for sequential logic, we introduce the current state <curr> and
historical state <last>. Additionally, The circuit’s internal components and
their connection are defined in <exec>.

Table 1: Effectful functions for CIRCT common state. function | Effect |  Description | Trigger
---|---|---|---
Ec(cmd) | <circt> |  Execute a CIRCT command |  cmd in <cmd>
Sti(cid, vals) | <ckt> |  Stimulate a circuit with $vals$ | call in <cmd>
Fin | <ckt> |  Finish the simulation circuit | <exec> auto-trigger
Wags(blk,vals) | <ckt> |  Initialize the block arguments | call in <exec>
Rcv(%id*) | <curr> |  Read the variables of current clock | function call
Wcv(%id*, vals) | <curr> |  Write the variables of current clock | function call
Rlv(%id*) | <last> |  Read the variables of lask clock | function call
Rreg(str) | <reg> |  Read the register by the symbol | function call
Wreg(str, %id) | <reg> |  Write the register by the symbol | function call
Rwire(str) | <wire> |  Read the wire by the symbol | function call
Wire(str, val) | <wire> |  Write the wire by the symbol | function call
Wout(id, %id) | <out> |  Mark the output variable | function call
Sop(operation) | <prog> |  Refine $operation$ in hardware domain | <prog> auto-trigger
Mop(operation) | <circt> |  Move unsymboled $op$ to <cmd> | <prog> auto-trigger
Sr(regions) | <exec> |  Standardize $({region})$ to $operations$ | <exec> auto-trigger
Pop(operations) | <exec> |  Parallelize $operations$ | <exec> auto-trigger
Wres(op) | <ckt> |  Assign the operation results | <exec> auto-trigger

Common Hardware Effectful Functions. To enable low-coupling access to this
state across hardware-domain dialect semantics, we introduce 17 effectful
functions as detailed in Table 1. These functions can be activated using three
methods: (1) direct function calls for unrestricted usage within semantic
rules; (2) constrained calls within specific cells; and (3) automatic triggers
through pattern matching when the operation semantics are formalized using the
standard methods (§ 5). With these effectful functions, we decouple dialect
semantics from MLIR semantics, and address sequential logic and operation
concurrency.

1\. Decoupling. For decoupling, the function Ec(cmd) refines MLIR functions
for hardware-specific applications by offering a variety of commands (cmd).
For example, the command CRop utilizes MLIR’s Rop to retrieve operations,
issuing an error for unlisted operations in <table>. The command Debug then
addresses such errors, adjusting <phase> to halt simulation.

2\. Sequential Logic. For sequential logic, we offer functions ranging from
Sti to Wout in Table 1. Specifically, Sti(cid, vals) is designed to stimulate
a dialect-agnostic circuit with specific values within a clock cycle,
extracting operations from <table> based on $cid$ and putting them into
<exec>. For example, we can use Sti("Counter",0,1) to stimulate the counter
and put normalized `hw.module` (lines 1-10 Fig. 1) in <exec>. Following this,
operations may use Wargs(blk, vals) to assign the signals vals to the block
arguments (line 2 Fig.1). With block initialization complete, operations in
the block trigger their dynamic semantic rules in <exec> (lines 3-8 Fig. 1),
using functions like Rcv(%id*) for current circuit state access or Rlv(%id*)
for previous state retrieval. Once no operation contributes to the hardware
module’s structure, Fin is auto-triggered to transition register variables
from <curr> to <last>.

3\. Operation Concurrency and Extensibility. For operation concurrency and
extensibility, we introduce functions positioned below $Sop$ in Table 1
designed to manipulate operations. Initially, operations reside in <prog>,
awaiting static semantic rules for canonicalization. Sop(operation) is an
auto-triggered function that refines the cross-domain normalized operation (by
MLIR static rules) into the hardware domain, simplifying the format. For
example, this function canonicalizes the `comb.add` operation (line 5 Fig. 1)
into the following format:

After canonicalization, an operation with a symbol name is mapped to its
definition in a <table>. For operations that lack a symbol name and are not in
operation with one, a seamless transition from <prog> to <cmd> is facilitated
using $Mop$, allowing dialect semantics to take over. Operations are also
transitioned from <table> to <exec> using $Sti$. Once <prog> is cleared, the
phase transitions from `preprocess` to `simulation`.

$\displaystyle\frac{}{\langle Op\ Ops\rangle_{exec}\Rightarrow\langle
Op\rangle_{exec}\ \langle
Ops\rangle_{exec}}\quad\text{\text{{{\small{Pop}}}}}$ (1)
$\displaystyle\frac{}{\langle OpRes=PureOp\rangle_{exec}\Rightarrow\langle
PureOp\sim>Wcv(OpRes)\rangle_{exec}}\quad\text{\text{{{\small{Wres}}}}}_{0}$
(2) $\displaystyle\frac{}{\langle
Signals\sim>Wcv(OpRes)\rangle_{exec}\Rightarrow\langle\rangle_{exec}\langle
OpRes\mapsto Signals\rangle_{curr}}\quad\text{\text{{{\small{Wres}}}}}_{1}$
(3)

In the <exec> cells, operations are further simplified and parallelized to
streamline the accurate formalization of hardware-specific semantics.
Sr(regions) converts a block region into a sequence of operations (i.e.,
hardware components), which are then split into individual parallelizable
simulation cells <exec> using Pop, obtaining individual hardware components.
Subsequently, Wres is triggered automatically to connect these components.
Specifically, Wres0 sets up the components’ input ports while Wres1 sets the
output ports. For instance, `comb.add` exposes the input ports `%reg_port` and
`%c1` by Wres0 and the output ports `%next` by Wres1 (line 5 Fig. 1).

As a result, CIRCT common semantics simplifies the formalization and
combination of hardware-specific dialect semantics, allowing their
concentration on unique dialect features, disregarding aspects such as
combinational logic, sequential logic, and operation concurrency.

##  5 Unified CIRCT Dialects Formalization

Employing CIRCT common semantics, this section introduces our approach to
define and combine the semantics of various CIRCT dialects. We achieve this
through a unified formalization approach to defining the semantics of
dialects’ minimal semantic units (individual operations) and combining them in
a specific dialect. Utilizing this approach, we formalize the CIRCT core
dialects (`hw`, `comb`, `seq`, `sv`) and combine them to support a CIRCT/MLIR
program (like Fig. 1).

$\displaystyle\frac{\langle pre\rangle_{phase}}{\langle Op\
\dots\rangle_{cmd}\ S_{dss}\Rightarrow\langle\rangle_{cmd}\
S_{dss}^{\prime}}\quad Op_{pre}$ (4) $\displaystyle\frac{\langle
sim\rangle_{phase}}{\langle Op\ \dots\rangle_{exec}\ S_{dss}\Rightarrow\langle
Signals\ \dots\rangle_{exec}\ S_{dss}^{\prime}}\quad Op_{sim}$ (5)

A Unified Formalization Approach for Individual Operations. The key to
formalizing individual operations is to specify their symbolic form in the
pending state (<cmd> or <exec>) and employ effectful functions to access the
upper layers’ state for composability (Fig. 2). The dialect-specific state
$S_{dss}$ is extended on need. $Op_{pre}$ and $Op_{sim}$ are unified
formalizations of various operations of CIRCT dialects. Note that we omit the
transition of states $S_{mlir}$ and $S_{circt}$ in them, because the
transition is triggered by the effectful functions in the upper layers.
Specifically, $Op_{pre}$ represents a unified formalization of the unsymboled
operation outside a block. Because the `=` symbol has different semantics in
different dialects, we leave its definition to their specific semantics,
resulting in empty $S_{cmd}$ ($<>_{cmd}$). Similarly, $Op_{sim}$ is a unified
formalization for other operations that may produce $Signals$ to their output
ports.

Delving into the unified formalization process involves up to 7 steps: (1)
select the phase, (2) retrieving dialect-specific values, (3) compute values
according to the operation, (4) control the simulation flow for operations
with regions, (5) normalize values, (6) update the circuit state if necessary,
and (7) return results. We illustrate this process through the example of
`comb.add` (Fig. 6).

⬇

1rule <phase> simulation </phase> // 1. choose phase

2<exec>

3 // symbolic-specified operation (hardware component) to be formalized

4 "comb.add"(As) : (Ts) -> (To)

5 // 7. return values, e.g., ListItem(TV(X, Y))

6 => ListItem( TV(To, Bit2Int( // 5. normalize values, e.g., Bit2Int(X)

7 add( // 3. operate on values, e.g., add(X, Y, …)

8 // 2. get dialect-specific values, bits(vals, types)

9 bits(Rcv(As), getWidth(Ts))))))

10… </exec>

Figure 6: The $\mathbb{K}$ definition for comb.add.

1\. Phase Selection. The first step is to select a phase based on the
operation’s attributes and location. Top-level operations lacking symbol names
are designated the “preprocess” phase, e.g., `sv.def`. Conversely, operations
like `hw.module`, despite being top-level yet possessing a symbol name, along
with operations like `comb.add`, that lack a symbol name yet are located in a
block, are assigned to the “simulation” phase (line 1).

2\. Retrieving Dialect-Specific Values. This step aims to extract the
operation’s operands and attributes that are unique to its dialect, with
attributes defining the operational logic. For example, in line 9, operand
`As` are read using $Rcv$, and their values are converted to the `comb`
dialect’s bit form using `bits`.

3\. Operating on Values. Operations represent different hardware components.
Specifically, `comb.add` is a logical adder designed to sum signals `As` (line
7).

4\. Simulation Flow Control. Operations, like `hw.module` and `sv.if`, that
involve regions represent specific control circuits. For `sv.if`, which
includes a conditional and a consequent one-block region, evaluating the
condition and then linking to the proper circuit block. Conversely,
`comb.add`, lacking a region, is not this type of circuit (line 4).

5\. Value Normalization. The diversity of types in CIRCT, ranging from built-
in and dialect types to attribute types, introduces complexity. To address
this, we standardize these varying types into a uniform format. For `comb`, we
convert the Bit value to the logical integer (line 6).

6\. State Updates. Operations can have side effects, potentially altering
states following computation. For example, the `hw.output` operation updates
the <out> state of the current instance by triggering the Wout function.

7\. Returning Values. Operations generally produce return values formatted as
a list (line 6). If an operation returns nothing, it yields an empty list
`.List`. These values are then assigned to ports op-results by the prepared
Wres.

Following these steps, we can formalize arbitrary operations by specifying
their name in <exec> or <cmd>. These individual definitions of operations are
composable by the indirect interactions using shared states with effectful
functions. Then, keeping this we can formalize the dialect semantics by
combining proper operation definitions. Without losing this composability, we
are also free to combine the semantics of various dialects.

CIRCT Core Dialects. Utilizing our approach, we formalized CIRCT core
dialects: (1) hw for general hardware representation, (2) comb for
combinational logic, (3) seq for digital sequential logic, and (4) sv for
SystemVerilog-specific constructs in an AST format. Fig. 7 illustrates the
individual declarations of these dialects’ states and their convenient
combination through a top-level state <top>. Each dialect-specific state, such
as <force> for handling `sv.force` in the `seq` dialect, records unique and
independent information on need. Besides the on-need extended state, auxiliary
semantic rules for dialects’ types and attributes are also extended on need,
because they only show their meaning via operations. Additionally, we do not
provide a unified mechanism for types and attributes, because the auxiliary
rules for them are pure and easy to combine.

$\left\langle\begin{aligned}
\langle\text{{{\small{\ldots}}}}\rangle_{log}\hskip
3.0pt\langle\langle\text{{{\small{id*}}}}\rangle_{finst}\mapsto\langle\text{{{\small{\%id}}}}\mapsto
tv\rangle_{fvars}\rangle_{force}\\\
\langle\text{{{\small{str}}}}\mapsto\text{{{\small{str}}}}\rangle_{macro}\hskip
3.0pt\langle\text{{{\small{str*}}}}\rangle_{inited}\hskip
3.0pt\langle\text{{{\small{str}}}}\mapsto\text{{{\small{str}}}}\rangle_{fd}\end{aligned}\right\rangle_{sv}\left\langle\begin{aligned}
\langle\text{{{\small{str}}}}\mapsto\text{{{\small{hw.heir*}}}}\rangle_{hier}\\\
\langle\text{{{\small{hw.heir}}}}\mapsto\text{{{\small{id}}}}\rangle_{h2inst}\end{aligned}\right\rangle_{hw}$

$\langle\langle\text{{{\small{\ldots}}}}\rangle_{mlir}\hskip
3.0pt\langle\text{{{\small{\ldots}}}}\rangle_{circt}\hskip
3.0pt\langle\text{{{\small{\ldots}}}}\rangle_{sv}\hskip
3.0pt\langle\text{{{\small{\ldots}}}}\rangle_{hw}\hskip
3.0pt\dots\rangle_{top}$

Figure 7: The structure of dialect states and their combination.

##  6 Evaluation

###  6.1 Statistics of Semantics

We established the semantics for 98 CIRCT operations, with statistics provided
in Table 2. This table categorizes various metrics such as source lines of
code (SLOC), comment lines of code (CLOC), rule count (N rules) and operation
count (N ops) across its rows. The columns detail the MLIR semantics, CIRCT
common semantics, and the dynamic semantics for hw, comb, seq, and sv
dialects, leading to a summary of the total size. For a complete list of the
formalized operations, please refer to the Appendix 0.B.

Table 2: Statistics for our semantics. | MLIR | CIRCT | HW | COMB | SEQ | SV | Total
---|---|---|---|---|---|---|---
SLOC | 555 | 547 | 582 | 351 | 68 | 1190 | 3969
CLOC | 91 | 31 | 21 | 35 | 13 | 58 | 346
N rules | 61 | 63 | 54 | 44 | 6 | 111 | 461
N ops | - | - | 20 | 20 | 5 | 53 | 98

###  6.2 Kimulator: Formal Semantics-Based Simulation

This section introduces Kimulator, a simulation tool that employs a Python
interface akin to Verilator, enhancing usability with our semantics. Fig. 8
depicts Kimulator’s architecture, illustrating both its usage and structure.

Figure 8: The architecture of Kimulator.

Usage of Kimulator. Kimulator simplifies interaction with CIRCT semantics
through generator.py, a pivotal component for initiating simulation. It parses
CIRCT source files, generating corresponding Python hardware modules to
utilize CIRCT formal semantics within the $\mathbb{K}$ framework. Within these
modules, model.py provides functionalities for manipulating hardware modules
and activating semantics, enabling users to develop simulation scripts in
Python. These scripts can repeatedly stimulate hardware modules, allowing for
simulation result analysis via the generated VCD files with vcd.py. Compared
to the famous open-source simulator Verilator, Kimulator offers a streamlined
simulation experience without increasing the workload, despite employing a
formal framework. For a detailed comparison, please refer to the illustration
in Appendix 0.C.

Structure of Kimulator. Diving into Kimulator’s structure, generator.py
generates instances of the Signal and KimulatorModel classes, along with a
KimulatorContext instance to encapsulate the global simulation information.
context.py provides the Signal class, which structures the hardware module,
and KimulatorContext, which manages the simulation state and interfaces with
the $\mathbb{K}$ framework. model.py introduces the KimulatorModel class,
mirroring hardware modules in Python and leveraging KimulatorContext’s
functions to execute simulations via krun, based on the kompiled circt.k. The
tools krun and kompile, provided by the $\mathbb{K}$ framework, are essential
for the interpretation and tool generation, respectively. To synchronize
changes between the Python twin model and the formal circuit representation,
modifications and data extractions are performed on krun’s output through
Kore, an intermediate representation in $\mathbb{K}$. This approach ensures
that execution can continue seamlessly into the next simulation cycle,
allowing for the dynamic update of the Python model post-simulation. Lastly,
vcd.py serves to store simulation outcomes in a VCD file, streamlining result
analysis and storage.

In conclusion, Kimulator offers a user-friendly simulation platform using our
semantics, reducing the complexity of formal methods and the $\mathbb{K}$
framework.

###  6.3 Validation of Semantics

Using Kimulator, this section provides the approach for building confidence in
our semantics and proposes several findings based on our validation results.

Figure 9: Co-simulation against verilator for semantics validation.

Fig. 9 illustrates our validation strategy by co-simulation with a popular
Verilog simulator, i.e., Verilator. Given the same chisel, firrtl, or other
hardware design source file using CIRCT, we utilize the CIRCT project to
compile them into generic MLIR or Verilog, which can be simulated by Kimulator
and Verilator, respectively. Then, we give the same inputs to stimulate the
same hardware (e.g., Fig. 11). After each simulation cycle, the output is
captured in VCD files, allowing for a detailed comparison. Discrepancies
between the Kimulator and Verilator outputs prompt a thorough error analysis,
potentially attributed to various factors, including documentation ambiguities
or errors in the formal semantics implementation, Kimulator, Verilator, or the
stimulation source files.

Our experiments are divided into two parts: (1) Operation-level validation,
for validating our semantics by testing all the semantic rules and formalized
operations, and (2) Hardware-level validation, for assessing the practicality
of our formalized operations by simulating a popular RISC-V design, `riscv-
mini`.

Operation-Level Validation. The goal here is to validate our semantics through
a full-rule coverage test suite, that contains 86 CIRCT/MLIR programs and
doubled simulation sources for both Kimulator and Verilator. The inputs for
these programs are meticulously designed to ensure full-rule coverage and are
stored in a file to provide the same inputs for co-simulations. The design of
the test suite involves the following steps:

1\. Initial Test Selection: Initially, we considered using existing tests from
Chisel hardware designs, but their complex logic obscured the semantic effects
we sought to observe. We then evaluated the existing tests within the CIRCT
project, which are primarily compilation-oriented and do not adequately cover
all the semantic rules. For example, the test suites of CIRCT don’t cover all
the events of the `sv.alwaysff` like `negedge`. The complexity of CIRCT’s
tests also hindered rapid validation and error identification.

2\. Test Adaptation and Augmentation: We extracted and modified tests from the
CIRCT project, supplementing them with additional tests designed for full-rule
coverage. To aid in rule-coverage determination and accelerate testing, we
designed each program to focus on a minimal set of rules, typically validating
the semantics of one operation per program. 3\. Compiler Compatibility Check:
All programs were checked for compilability via `circt-opt` to align with the
compiler’s expectations and to ensure no errors or ambiguities caused by the
CIRCT documentation.

4\. Handling Operation Interdependencies: Despite efforts to isolate operation
semantics, the inherent interrelations among CIRCT dialect operations (at
compiler level) necessitated their combination for co-simulation. For example,
operations within the `comb` dialect cannot exist outside of `hw.module`, and
`sv.force` continues to override procedural assignments until `sv.release` is
executed. We identified these interrelations and made minimal adjustments to
the programs, such as modifying `comb.add` to `comb.xor` to progressively
cover all the rules.

5\. Input Design: We specifically designed test inputs for operations
sensitive to values, to ensure each rule is invoked. For instance, the
`comb.icmp` operation utilizes the `predicate` attribute to define ten
comparison modes, each formalized by a separate rule. We achieved complete
coverage by assigning ten distinct values to `predicate`, one for each mode.

6\. Simulation Source Adjustments: We simulated multiple clock cycles to
validate rules and operations requiring access to the historical state <last>.

Results. Our semantics successfully passed all operation-level tests,
affirming its correctness. However, several issues were identified, including:

  * •

We have found over 20 flaws in the MLIR documentation, such as missing
definitions and inconsistent syntax. These issues have acknowledged by the
LLVM community, as recorded in GitHub Issues 62489, 62488, 62490.

  * •

Additionally, we have identified numerous flaws in the CIRCT documentation.
The multitude of issues prevents us from formalizing and submitting patches
simultaneously. Even worse, we must repeatedly check the legality of
operations accepted by the CIRCT implementation and compile them into Verilog
to infer their semantics.

  * •

The documentation for CIRCT version changes is lacking. However, dialects
change across CIRCT versions and affect their semantics, such as attributes,
module type notations, and built-in instance unfolding methods. Although our
semantics is extensible, checking these changes requires substantial time.

Hardware-Level Validation. The goal here is to validate the practical
applicability of our formalized operations for complex hardware design, such
as the RISC-V design. We opted for the riscv-mini project, a popular RISC-V
3-stage pipeline in Chisel. Despite its simplicity, it consists of significant
features of a processor, including RV32I from the User-level ISA Version 2.0
and the Machine-level ISA from the Privileged Architecture Version 1.7, as
well as basic instruction and data caches. The riscv-mini, compiled to 1455
lines of CIRCT code, serves as an ideal testbed to determine if our formalized
operations adequately cover the functional requirements of real-world hardware
descriptions. Through multiple input tests on the top module, we validate our
semantics.

Results. (1) This validation phase polished our semantics by revealing
undocumented operation attributes. (2) We observed that certain operations
compiled at the hw-level were underutilized, indicating potential areas for
further capturing the essence of CIRCT.

##  7 Related Work

To the best of our knowledge, our work pioneers the formal semantics for
CIRCT, introducing precision and determinism to the unified hardware compiler
framework. This section compares our contributions with prior efforts in
formal semantics that overlap in scope (i.e., MLIR) or target similar
objectives (i.e., HDLs). Bang et al.’s seminal work on MLIR dialects [7]
encodes memref, linalg, and tensor dialects as a whole in SMT to enable
translation validation for machine learning compilers. While insightful, it
diverges from our scope by concentrating on a different subset of dialects
without addressing the extensibility and composability that our approach
emphasizes. Further, the proposal by Yu [23] acknowledges the challenges of
composability in MLIR formalization, suggesting the adoption of effect
handlers as a novel solution. However, his proposal, merely outlining a simple
idea, underestimates the complexities inherent in real-world projects. Our
methodology leverages insights from their approach but advances further by
employing a layered mechanism in our semantics. This innovation allows for
greater extensibility and composability, addressing the complexities
overlooked in the preliminary proposal.

The exploration of formal semantics within the HDL domain has traditionally
been isolated, benefiting single languages and lacking the cross-language
power found in software formalization efforts like SMACK [8, 14, 10, 21], and
SAW [13]. Specific to HDLs, contributions such as [11, 16, 22, 20] for
Verilog, [15] for VHDL, [9] for BlueSpec, and [12] for Chisel, showcase the
depth of work within individual languages. This fragmented approach may stem
from the lack of a unified intermediate representation (IR) for hardware,
contrasting the cohesive LLVM IR in software. Despite HDLs’ propensity for
generating Verilog to tap into its established ecosystem, Verilog’s primary
orientation towards circuit synthesis limits its efficacy as a unifying IR.
Recognizing this gap, the LLVM community’s introduction of CIRCT seeks to
transpose successful practices from software to hardware. Our contribution
marks a critical step in this transformative journey, offering the first
formal semantics for CIRCT that paves the way for future unified verification
of hardware designs.

##  8 Conclusion

We introduced K-CIRCT, the first formal semantics for CIRCT, capable of
simulating a popular RISC-V design. Through a layered mechanism and effectful
functions, we provide a unified approach to define and combine dialect
semantics. Specifically, the MLIR static semantics simplifies the
formalization of MLIR-based projects across various domains. The CIRCT common
semantics streamlines the formalization of hardware-domain dialects by
introducing a generic hardware model. Utilizing this unified approach, we have
successfully formalized the key dialects—`hw`, `comb`, `seq`, and `sv`. Our
semantics have been tested through a full-rule coverage test suite and the
simulation of the popular RISC-V design, `riscv-mini`, supported by a user-
friendly simulator that we developed.

Leveraging the $\mathbb{K}$ framework, we can derive various formal analysis
tools from our semantics, e.g., a symbolic interpreter and an equivalence
checker. These tools are useful for hardware symbolic execution, formal
verification, equivalence verification, and translation validation,
significantly enhancing the trustworthiness of hardware designs. Future
efforts will focus on collaborating with the CIRCT and $\mathbb{K}$
communities to enhance scalability and further integrate formal methods into
the development of CIRCT tools.

## References

  * [1] Chisel, https://www.chisel-lang.org/
  * [2] IEEE Std 1800-2017 (Revision of IEEE Std 1800-2012) IEEE Standard for SystemVerilog—Unified Hardware Design, Specification, and Verification Language
  * [3] The LLVM Compiler Infrastructure Project, https://llvm.org/
  * [4] Phanrahan/magma: Magma circuits, https://github.com/phanrahan/magma
  * [5] K Framework Tools. Runtime Verification Inc. (Apr 2023), https://github.com/runtimeverification/k
  * [6] Ashenden, P.J.: The Designer’s Guide to VHDL. Morgan Kaufmann (2010)
  * [7] Bang, S., Nam, S., Chun, I., Jhoo, H.Y., Lee, J.: SMT-Based Translation Validation for Machine Learning Compiler. In: Computer Aided Verification. pp. 386–407. Springer, Cham (2022), https://linkspringer.53yu.com/chapter/10.1007/978-3-031-13188-2_19
  * [8] Baranowski, M., He, S., Rakamarić, Z.: Verifying Rust programs with SMACK. In: International Symposium on Automated Technology for Verification and Analysis. pp. 528–535. Springer (2018)
  * [9] Bourgeat, T., Pit-Claudel, C., Chlipala, A., Arvind: The essence of Bluespec: A core language for rule-based hardware design. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 243–257. ACM, London UK (Jun 2020), https://dl.acm.org/doi/10.1145/3385412.3385965
  * [10] Carter, M., He, S., Whitaker, J., Rakamaric, Z., Emmi, M.: SMACK software verification toolchain. In: 2016 IEEE/ACM 38th International Conference on Software Engineering Companion (ICSE-C). pp. 589–592. IEEE (2016)
  * [11] Chen, Q., Zhang, N., Wang, J., Tan, T., Xu, C., Ma, X., Li, Y.: The Essence of Verilog: A Tractable and Tested Operational Semantics for Verilog. Proceedings of the ACM on Programming Languages 7(OOPSLA2), 234–263 (Oct 2023), https://dl.acm.org/doi/10.1145/3622805
  * [12] Dobis, A., Laeufer, K., Damsgaard, H.J., Petersen, T., Rasmussen, K.J.H., Tolotto, E., Andersen, S.T., Lin, R., Schoeberl, M.: Verification of Chisel Hardware Designs with ChiselVerify. Microprocessors and Microsystems 96, 104737 (Feb 2023), https://linkinghub.elsevier.com/retrieve/pii/S0141933122002666
  * [13] Dockins, R., Foltzer, A., Hendrix, J., Huffman, B., McNamee, D., Tomb, A.: Constructing Semantic Models of Programs with the Software Analysis Workbench. In: Blazy, S., Chechik, M. (eds.) Verified Software. Theories, Tools, and Experiments, vol. 9971, pp. 56–72. Springer International Publishing, Cham (2016), http://link.springer.com/10.1007/978-3-319-48869-1_5
  * [14] Kalra, S., Goel, S., Dhawan, M., Sharma, S.: Zeus: Analyzing safety of smart contracts. In: Ndss. pp. 1–12 (2018)
  * [15] Khan, W., Hou, Z., Sanan, D., Nebhen, J., Liu, Y., Tiu, A.: An Executable Formal Model of the VHDL in Isabelle/HOL (Feb 2022), http://arxiv.org/abs/2202.04192
  * [16] Khan, W., Tiu, A., Sanán, D.: VeriFormal: An Executable Formal Model of a Hardware Description Language. In: SG-CRC. pp. 19–36 (2017)
  * [17] Lattner, C., Amini, M., Bondhugula, U., Cohen, A., Davis, A., Pienaar, J., Riddle, R., Shpeisman, T., Vasilache, N., Zinenko, O.: MLIR: Scaling Compiler Infrastructure for Domain Specific Computation. In: 2021 IEEE/ACM International Symposium on Code Generation and Optimization (CGO). pp. 2–14. IEEE, Seoul, Korea (South) (Feb 2021), https://ieeexplore.ieee.org/document/9370308/
  * [18] Lenharth, A., Lattner, C.: CIRCT: Lifting hardware development out of the 20th century (2021)
  * [19] McCaskey, A., Nguyen, T.: A MLIR Dialect for Quantum Assembly Languages. In: 2021 IEEE International Conference on Quantum Computing and Engineering (QCE). pp. 255–264. IEEE, Broomfield, CO, USA (Oct 2021), https://ieeexplore.ieee.org/document/9605269/
  * [20] Meredith, P., Katelman, M., Meseguer, J., Rosu, G.: A formal executable semantics of Verilog. In: Eighth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010). pp. 179–188. IEEE, Grenoble, France (Jul 2010), http://ieeexplore.ieee.org/document/5558634/
  * [21] Rakamarić, Z., Emmi, M.: SMACK: Decoupling source language details from verifier implementations. In: International Conference on Computer Aided Verification. pp. 106–113. Springer (2014)
  * [22] Wolf, C., Glaser, J., Kepler, J.: Yosys-a free Verilog synthesis suite. In: Proceedings of the 21st Austrian Workshop on Microelectronics (Austrochip). p. 97 (2013)
  * [23] Yu, P.: Reasoning about MLIR Semantics through Effects and Handlers. In: Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis. pp. 1552–1554. ACM, Seattle WA USA (Jul 2023), https://dl.acm.org/doi/10.1145/3597926.3605239

##  Appendix 0.A Generic MLIR Syntax

TopLevel $\displaystyle\text{{{\small{toplevel}}}}\Coloneqq$
(operation$\mid$type-alias-def$\mid$attr-alias-def)* Operation
$\displaystyle\text{{{\small{operation}}}}\Coloneqq$ (op-results =)? str
((value-uses)?) ([successors])? (<dict-prop>)? ((regions))? ({(dict-attr)?})?
: fun-type (loc-attr)? $\displaystyle\text{{{\small{op-results}}}}\Coloneqq$
$\displaystyle\ \text{{{\small{op-result}}}}\
\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}(}}}\text{{\small{,}}}\
\text{{{\small{op-
result}}}}\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5})*}}}\hskip
20.0pt\text{{{\small{op-result}}}}\Coloneqq\
\text{{\small{\%}}}\text{{{\small{id}}}}\
\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}(}}}\text{{\small{:}}}\
\text{{{\small{int}}}}\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5})?}}}$
$\displaystyle\text{{{\small{value-uses}}}}\Coloneqq$ $\displaystyle\
\text{{{\small{value-use}}}}\
\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}(}}}\text{{\small{,}}}\
\text{{{\small{value-
use}}}}\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5})*}}}\hskip
14.0pt\text{{{\small{value-use}}}}\Coloneqq\
\text{{\small{\%}}}\text{{{\small{id}}}}\
\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}(}}}\text{{\small{\\#}}}\
\text{{{\small{int}}}}\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5})?}}}$
$\displaystyle\text{{{\small{successors}}}}\Coloneqq$ $\displaystyle\
\text{{{\small{successor}}}}\
\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}(}}}\text{{\small{,}}}\
\text{{{\small{successor}}}}\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5})*}}}\hskip
13.0pt\text{{{\small{successor}}}}\Coloneqq\
\text{{\small{\^{}}}}\text{{{\small{id}}}}\
\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}(}}}\text{{\small{:}}}\
\text{{\small{(}}}\text{{{\small{block-
args}}}}\text{{\small{)}}}\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5})?}}}$
Region $\displaystyle\text{{{\small{regions}}}}\Coloneqq$ $\displaystyle\
\text{{{\small{region}}}}\
\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}(}}}\text{{\small{,}}}\
\text{{{\small{region}}}}\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5})*}}}\hskip
51.0pt\text{{{\small{region}}}}\Coloneqq\
\text{{\small{\\{}}}\text{{{\small{operation}}}}^{\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\text{{{\small{block}}}}\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>Block $\displaystyle\text{{{\small{block}}}}\Coloneqq$ $\displaystyle\
\text{{{\small{block-label}}}}\
\text{{{\small{operation}}}}^{\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>16.0pt\text{{{\small{block-label}}}}\Coloneqq\
\text{{\small{\^{}}}}\text{{{\small{id}}}}\
\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}(}}}\text{{\small{(}}}\text{{{\small{block-
args}}}}\text{{\small{)}}}\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5})?}}}\
\text{{\small{:}}}$ $\displaystyle\text{{{\small{block-args}}}}\Coloneqq$ (%id
: type(, %id : type)*)? Type $\displaystyle\text{{{\small{type-alias-
def}}}}\Coloneqq$ $\displaystyle\ \text{{{\small{type-alias}}}}\
\text{{\small{=}}}\ \text{{{\small{type}}}}\hskip 38.0pt\text{{{\small{type-
alias}}}}\Coloneqq\ \text{{\small{!}}}\text{{{\small{bare-id}}}}$
$\displaystyle\text{{{\small{func-type}}}}\Coloneqq$ $\displaystyle\
\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}(}}}\text{{{\small{type}}}}\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}$\mid$}}}\text{{\small{(}}}\text{{{\small{types}}}}\text{{\small{)}}}\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5})}}}\text{{\small{->}}}\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}(}}}\text{{{\small{type}}}}\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}$\mid$}}}\text{{\small{(}}}\text{{{\small{types}}}}\text{{\small{)}}}\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5})}}}\hskip
4.0pt\text{{{\small{types}}}}\Coloneqq\ \text{{{\small{type}}}}\
\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}(}}}\text{{\small{,}}}\
\text{{{\small{type}}}}\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5})*}}}$
$\displaystyle\text{{{\small{type}}}}\Coloneqq$ type-alias$\mid$dialect-
type$\mid$builtin-type Attribute $\displaystyle\text{{{\small{attr-alias-
def}}}}\Coloneqq$ $\displaystyle\ \text{{{\small{attr-alias}}}}\
\text{{\small{=}}}\ \text{{{\small{attr-value}}}}\hskip
18.0pt\text{{{\small{attr-alias}}}}\Coloneqq\
\text{{\small{\\#}}}\text{{{\small{bare-id}}}}$
$\displaystyle\text{{{\small{dict-attr}}}}\Coloneqq$ $\displaystyle\
\text{{{\small{attr-entry}}}}\
\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}(}}}\text{{\small{,}}}\
\text{{{\small{attr-
entry}}}}\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5})*}}}\hskip
6.0pt\text{{{\small{attr-entry}}}}\Coloneqq\
\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}(}}}\text{{{\small{id}}}}\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}$\mid$}}}\text{{{\small{str}}}}\text{{\small{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5})}}}\
\text{{\small{=}}}\ \text{{{\small{attr-value}}}}$
$\displaystyle\text{{{\small{loc-attr}}}}\Coloneqq$ loc(location)
$\displaystyle\text{{{\small{attr-value}}}}\Coloneqq$ attr-alias$\mid$dialect-
attr$\mid$builtin-attr

Figure 10: Syntax for generic MLIR. Note that this figure omits some syntax
definitions (e.g., builtin-attr — the builtin attributes of MLIR) for clarity.
Indeed, our formalization consists of the complete syntax.

##  Appendix 0.B List of Formalized Operations

Table 3: Operation list of comb dialect No. | Operation Name |  Description
---|---|---
1 | comb.add |  Integer addition for a variadic list of operands together
2 | comb.and |  Logical conjunction for a variadic list of operands together
3 | comb.concat |  Concatenate a variadic list of operands together.
4 | comb.divs |  Signed integer division
5 | comb.divu |  Unsigned interger division
6 | comb.extract |  Extract a range of bits into a smaller value, lowBit specifies the lowest bit included.
7 | comb.icmp |  Compare two integer values
8 | comb.mods |  Signed interger modulo
9 | comb.modu |  Unsigned interger modulo
10 | comb.mul |  Integer multiplication for a variadic list of operands together
11 | comb.mux |  Return one or the other operand depending on a selector bit
12 | comb.or |  Logical disjunction for a variadic list of operands together
13 | comb.parity |  Logical parity operation for an integer
14 | comb.replicate |  Concatenate the operand a constant number of times
15 | comb.shl |  Logical left shifting
16 | comb.shrs |  Logical right shifting for signed intergers
17 | comb.shru |  Logical right shifting for unsigned intergers
18 | comb.sub |  Integer subtraction
19 | comb.truth_table |  Return a true/false based on a lookup table
20 | comb.xor |  Logical XOR operation for a variadic list of operands together
Table 4: Operation list of hw dialect No. | Operation Name |  Description
---|---|---
1 | hw.module |  Represents a Verilog module
2 | hw.hierpath |  Represents a path through the hierarchy
3 | hw.instance |  Create an instance of a module
4 | hw.output |  HW termination operation
5 | hw.bitcast |  Reinterpret one value to another value of the same size and potentially different type
6 | hw.constant |  Produce a constant value
7 | hw.enum.cmp |  Compare two values of an enumeration
8 | hw.enum.constant |  Produce a constant enumeration value
9 | hw.wire |  Assign a name or symbol to an SSA edge
10 | hw.aggregate_constant |  Produce a constant aggregate value
11 | hw.array_concat |  Concatenate some arrays
12 | hw.array_create |  Create an array from values
13 | hw.array_get |  Get the value in an array at the specified index
14 | hw.array_slice |  Get a range of values from an array
15 | hw.struct_create |  Create a struct from constituent parts
16 | hw.struct_explode |  Expand a struct into its constituent parts
17 | hw.struct_extract |  Extract a named field from a struct
18 | hw.struct_inject |  Inject a value into a named field of a struct
19 | hw.union_create |  Create a union with the specified value
20 | hw.union_extract |  Get the value of a union, interpreting it as the type of the specified member field
Table 5: Operation list of seq dialect No. | Operation Name | Description
---|---|---
1 | comb.add | Integer addition for a variadic list of operands together
2 | seq.firmem.read_port | A memory read port
3 | seq.firmem.read_write_port | A memory read-write port
4 | seq.firmem.write_port | A memory write port
5 | seq.firreg | Register with preset and sync or async reset
Table 6: Operation list of sv dialect No. | Operation Name |  Description
---|---|---
1 | sv.always |  `always @` block in SystemVerilog
2 | sv.alwayscomb |  `alwayscomb` block in SystemVerilog
3 | sv.alwaysff |  `alwaysff @` block with optional reset
4 | sv.array_index_inout |  Index an inout memory to produce an inout element
5 | sv.assert |  Immediate assertion statement
6 | sv.assert.concurrent |  Concurrent assertion statement
7 | sv.assign |  Continuous assignment
8 | sv.assume |  Immediate assume statement
9 | sv.assume.concurrent |  Concurrent assume statement
10 | sv.bind |  Indirect instantiation statement
11 | sv.bpassign |  Blocking procedural assignment
12 | sv.case |  `case (cond)` block in SystemVerilog
13 | sv.constantX |  A constant of value `x`
14 | sv.constantZ |  A constant of value `z`
15 | sv.cover |  Immediate cover statement
16 | sv.cover.concurrent |  Concurrent cover statement
17 | sv.error |  "error" severity message task
18 | sv.exit |  "exit" system task
19 | sv.fatal |  "fatal" severity message task
20 | sv.finish |  "finish" system task
21 | sv.for |  for loop in SystemVerilog
22 | sv.force |  Force procedural statement in SystemVerilog
23 | sv.fwrite |  fwrite statement
24 | sv.generate |  A `generate` block
25 | sv.generate.case |  A `case` statement inside of a generate block
26 | sv.if |  `if (cond)` block
27 | sv.ifdef |  `ifdef MACRO` block
28 | sv.ifdef.procedural |  `ifdef MACRO` block for procedural regions
29 | sv.indexed_part_select |  Read several contiguous bits of an int type
30 | sv.indexed_part_select_inout |  Address several contiguous bits of an inout type
31 | sv.info |  "info" severity message task
32 | sv.initial |  `initial` block
33 | sv.logic |  Define a logic
34 | sv.macro.decl |  SystemVerilog macro declaration
35 | sv.macro.def |  SystemVerilog macro definition
36 | sv.macro.ref |  Expression to refer to a SystemVerilog macro
37 | sv.macro.ref.se |  Expression to refer to a SystemVerilog macro
38 | sv.ordered |  A region which guarantees to output statements in order
39 | sv.passign |  Nonblocking procedural assignment
40 | sv.read_inout |  Get the value of from something of inout type as the value itself
41 | sv.readmem |  Load a memory from a file in either binary or hex format
42 | sv.reg |  Define a new register in SystemVerilog
43 | sv.release |  Release procedural statement
44 | sv.stop |  "stop" system task
45 | sv.struct_field_inout |  Create an subfield inout memory to produce an inout element.
46 | sv.warning |  "warning" severity message task
47 | sv.wire |  Define a new wire
48 | sv.xmr |  Encode a reference to a non-local net.
49 | sv.xmr.ref |  Encode a reference to something with a hw.hierpath.
50 | sv.verbatim |  Verbatim opaque text emitted inline.
51 | sv.verbatim.expr |  Expression that expands to a value given SystemVerilog text
52 | sv.verbatim.expr.se |  Expression that expands to a value given SystemVerilog text

##  Appendix 0.C Comparison between Kimulator and Verilator

Figure 11: Comparative simulation illustration for Kimulator and Verilator.