Writing specifications in Sockeye3

Sockeye3 is a toolchain for specifying and analyzing memory addressing of hardware platforms.

The Sockeye3 compiler is written in Rust, and features an accompanying domain-specific language (DSL) for specifying SoCs.

The resulting spec can be fed into the sockeye3 compiler, which can then can then run queries, generate visualization, and so on.

Checking out the source code

Sockeye3 is available open-source. To check out and build the sockeye3 tool, simply clone the repository and run cargo build:

git clone https://gitlab.inf.ethz.ch/project-opensockeye/sockeye3
cd sockeye3
cargo build # add --release for a release build

Alternatively, Sockeye3 is also distributed as part of the Kirsch toolchain.

Organization of the source tree

Note

These instructions were written for sockeye3 commit 9237cca90209cf8bf0d4d2391b5726ecc34c6bb4.

The Sockeye3 source tree contains the Rust-based compiler. Hardware specifications are stored in a separate repository, which is included as a submodule in the subdirectory specs/. Rust enforces a naming scheme for modules, namely that the file src/module.rs contains the export definitions for the source files in sockeye3::module. That said, Sockeye3 contains the following modules:

sockeye3::decoding_net

Contains the definitions of a DecodingNet, and basic tools for manipulating decoding nets: adding address spaces, mappings, and annotating additional information.

sockeye3::specification

Contains the definitions of a Specification, which is a combination of individual modules that form the whole decoding net.

sockeye3::glas

Contains code that derives and exports a global logical address space from a Sockeye3 model.

Reading Sockeye specifications

The folder specs contains all specifications we have written so far. We organize these specifications roughly by vendor and component.

The specification of a platform can be divided into several (sub-)modules, which are then assembled in a top-level .soc file. A SoC-file consists of a list of imports, instantiations, and connections.

A module is a (potentially) reusable component part of an overall specification. A module consists of a number of address spaces, which are connected by mappings. Together, these form a local decoding net, defining how addresses are translated locally by this piece of Sockeye.

In order to interface with other modules, these address spaces can be designated as in- and outports, respectively. An inport receives incoming connections from other modules, while an outport provides directed connections to other modules. Connections between modules are only possible between an originating outport, and a receiving inport.

Below is a screenshot generated from the specification contained in specs/example_vendor/example.soc. This is a fictional, 2-core system with a built-in network interface card, intended to show the basic features of our DSL.

An excerpt of a system specification, showing a Sockeye module for a NIC, consisting of separate address spaces for the NIC core, the NIC’s registers, and a mapped to the main interconnect. Gray arrows denote module-internal mappings, while black arrows denote inter-module connections.

The code that defines the NIC module is shown below. The comments give brief explanations of the individual address spaces and mappings.

specs/example_vendor/example/nic.gls

/// This module describes a fictional network interface card, i.e. a
/// component that issues memory operations,

/// This network interface card has a 32-bit physical address space,
/// therefore we create a 4GiB address space for the execution context.
ctx nic_core 4GiB

/// Part of this context's address space is mapped to the main interconnect,
/// therefore we create an appropriate address space here.
as to_interconnect 4GiB
out to_interconnect

/// The NIC features 64kiB of registers, accessible via the main
/// interconnect. Therefore, we mark the registers as an 'in' address space.
dev registers 64kiB
in registers

/// The upper 3GiB are mapped to the system interconnect.
map nic_core @ 0x4000_0000 -> to_interconnect @ 0x4000_0000 (3GiB)

/// The NIC can also access its registers at 0x0.
map nic_core @ 0x0 -> registers @ 0x0 (64kiB)

The whole system is then described in a top-level .soc file, shown below.

specs/example_vendor/example.soc

/// We can import modules from arbitrary paths, relative to our .soc file.
import example/dram.gls
import example/nic.gls
import example/core.gls
import example/interconnect.gls

/// The imported modules can then be instantiated. Each instantiation has
/// its own address spaces and mappings.
inst xconn interconnect
inst dram dram
inst nic nic
inst core_0 core
inst core_1 core

/// The ports of instances can then be connected, forming the full specification.
conn core_0.core -> xconn.input
conn core_1.core -> xconn.input
conn nic.to_interconnect -> xconn.input
conn xconn.nic_registers -> nic.registers
conn xconn.dram -> dram.dram

The final specification looks like this:

Visualization of the decoding net generated by example.soc

Writing Sockeye specifications

In order to write a new Sockeye specification, we only need to create a new top-level .soc file, and point the sockeye3 tool at it.

# Create the new specification file
touch my_new_spec.soc
# Run sockeye3
sockeye3 my_new_spec.soc
[INFO  sockeye3::cli] Parsed specification from my_new_spec.soc (0 address spaces) [0s]
[INFO  sockeye3::cli] Successful run, terminating [0s]

This specification is not very interesting yet, since we haven’t specified anything. Let us create a new module now:

# Create initial address spaces
cat <<EOF > my_new_module.mod
ctx my_context 128kiB
as my_interconnect 64kiB
mem my_memory 64kiB
EOF

This module defines three address spaces, a context of 128 Kibibytes size, an interconnect of 64 Kibibytes, and finally some memory also 64 Kibibytes in size. In order for this module to show up in our specification, we need to import and instantiate it:

# Import and instantiate the new module
cat <<EOF > my_new_spec.soc
import my_new_module.mod
inst my_instance my_new_module
EOF
# Re-run sockeye3
sockeye3 my_new_spec.soc
[INFO  sockeye3::cli] Parsed specification from my_new_spec.soc (3 address spaces) [0s]
[INFO  sockeye3::cli] Successful run, terminating [0s]

We can visualize these address spaces by outputting a graphviz description.

# Generate a graphviz description of the decoding net, and output it to my_viz.dot
sockeye3 my_new_spec.soc --graphviz my_viz.dot
[INFO  sockeye3::cli] Parsed specification from my_new_spec.soc (3 address spaces) [0s]
[INFO  sockeye3::cli] Dot output to my_viz.dot
[INFO  sockeye3::cli] Successful run, terminating [0s]
# Compile the resulting description to a PNG image
dot -Tpng -o my_viz.png < my_viz.dot

The compiled graphviz description from my_new_spec.soc.

Our address spaces show up now, colored in different colors according to their attribute (context, intermediate, resource). What these attributes mean in detail will be explained later.

Let us add some mappings to our specification, and see how it changes the visualization.

# Add some mappings
cat <<EOF >> my_new_module.mod
map my_context @ 0x0 -> my_interconnect @ 0x0 (64kiB)
map my_interconnect @ 0x0 -> my_memory @ 0x0 (64kiB)
EOF
# Re-run sockeye3
sockeye3 my_new_spec.soc --graphviz my_viz.dot
[INFO  sockeye3::cli] Parsed specification from my_new_spec.soc (3 address spaces) [0s]
[INFO  sockeye3::cli] Dot output to my_viz.dot
[INFO  sockeye3::cli] Successful run, terminating [0s]
# And also re-run dot
dot -Tpng -o my_viz.png < my_viz.dot

Mappings now show up as arrows between address spaces.

Most systems are more complicated than a single module, however. In our case, the context has another 64kiB of address space that are not utilized. It turns out that these are connected to the interconnect of an identical core. In order to represent this in our model, we add another address space to our module, which will be connected to the other interconnect.

# Add a new address space that maps to the other interconnect, and
# add the corresponding mapping to the upper 64KiB of my_context.
cat <<EOF >> my_new_module.mod
as to_other_interconnect 64KiB
map my_context @ 64KiB -> to_other_interconnect @ 0x0 (64KiB)
EOF

This by itself is insufficient, however, as we haven’t declared our interconnect as a valid connection point. Therefore, we additionally have to declare the address space to_other_interconnect as valid outport, and the address space my_interconnect as valid inport.

# Add the in- and outport declarations
cat <<EOF >> my_new_module.mod
out to_other_interconnect
in my_interconnect
EOF

Now we can instantiate another module, and connect up the address spaces. Note that this specification only connects the instances one way, namely from my_instance to other_instance. If we want the reverse connection to appear as well, we need another conn statement.

# Create a second instance of my_new_module, and connect the
# corresponding address spaces.
cat <<EOF >> my_new_spec.soc
inst other_instance my_new_module
conn my_instace.to_other_interconnect -> other_instance.my_interconnect
# All address spaces show up twice now, once for each instance
sockeye3 my_new_spec.soc --graphviz my_viz.dot
[INFO  sockeye3::cli] Parsed specification from my_new_spec.soc (8 address spaces) [0s]
[INFO  sockeye3::cli] Dot output to my_viz.dot
[INFO  sockeye3::cli] Successful run, terminating [0s]

There are multiple instances of my_new_module now.

Now you know the basics to start specifying your own SoCs. The next section contains a brief summary of the Sockeye syntax.

The Sockeye syntax

The code block below shows a brief summary of expressions in sockeye.

// Comments are written using two slashes, and continue to the end of the line.
/// Doc-comments use triple slashes.

///////////////////////////////////////////////////////////////////////////////
// A SoC file consists of import, inst, and conn statements.

// Imports
// import <path>
import some/path/to/some/module.mod

// Instantiation
// inst <instance_name> <module_name>
inst my_instance my_module

// Connections
// conn <instance>.<address_space> -> <instance>.<address_space>
conn inst0.core -> inst1.interconnect

///////////////////////////////////////////////////////////////////////////////
// A module file consists of address space declarations, mappings, and port
// declarations.

// Address spaces
// <address_space_type> <name> <size>

// Generic address spaces are declared using 'as'
as generic_address_space 1024B

// Contexts
// Things that issue memory requests are declared using 'ctx'.
ctx context 1KiB
ctx my_dma_engine 16MiB

// Resources
// Things that answer memory requests are declared either to be
// memory (mem), device registers (dev), or generic/unknown (res).
res my_generic_resource 3KiB
mem my_large_dram 5PiB
dev my_dma_engine_configuration 16KiB

// Mappings
// map <source_address_space> @ <offset> -> <target_address_space> @ <offset> (<size>)
map core @ 0x0 -> interconnect @ 0x0 (4GiB)
map interconnect @ 0x123_0000 -> dev1 @ 0x0 (16KiB)
map interconnect @ 0x126_0000 -> dev2 @ 0x0 (16KiB)
map interconnect @ 0x800_0000 -> ram @ 0x0 (5GiB)

// Ports
// <port_type> <address_space>

// Address spaces are declared as ports using 'in' or 'out', depending on
// the port type.
out core
in interconnect
in dram

Using Sockeye models in practice

Now that we know how to define Sockeye models, we need to know how to visualize and use them. The Sockeye toolchain provides a command-line interface for processing specifications.

The --help flag prints a list of arguments with their descriptions.

$ sockeye3 --help
Usage: sockeye3 [OPTIONS] <SPEC_PATH>

Arguments:
  <SPEC_PATH>

Options:
      --derive-glas                    Derive a global logical address space
      --load-glas <LOAD_GLAS>          Path to deserialize the GLAS from
      --save-glas <FILE>               Path to serialize the GLAS to
      --glas-out <FILE>                Path to output GLAS to
      --glas-constraints <FILE>        Additional constraints for GLAS derivation
      --glas-try-optimal               Attempt to derive an optimal GLAS, minimizing the number of non-zero offsets.
      --glas-format <GLAS_FORMAT>      [possible values: json]
      --matrix-out <MATRIX_OUT>        Path to output the hardware matrix to
      --matrix-format <MATRIX_FORMAT>  [default: text] [possible values: json, text]
      --graphviz <FILE>                File path to output a graphviz visualization to
      --focus <ADDRESS_SPACE>          Address space to focus (e.g. for visualizations)
  -v, --verbose                        Enable verbose output
  -h, --help                           Print help
  -V, --version                        Print version

Generating visualizations

You can output a graphviz descriptions of a specification via the --graphviz commands. They will output a dot description of the requested graph to the given path, which can then be further processed with dot, as we have seen before. Using the --focus argument, we can zoom in on a target address space.

This output is useful for getting an overview of the components present on a given platform, as well as debugging specifications as you write them.

Deriving a Global Logical Address Space

The --derive-glas flag attempts to derive a GLAS for the current decoding net. The --glas-out flag defines where to output the computed GLAS to. Additionally, a GLAS can be serialized using the --save-glas flag, which can later be loaded using --load-glas.

Using --glas-out, we can select the output format for the GLAS. The JSON format suitable for ingestion into e.g. our patched version of microkit.

Sockeye allows the user to specify additional constraints that must be satisfied of the GLAS. The constraints can be given in two forms:

ctx_constraint ctx @ local_addr, len -> glas_addr
res_constraint res @ res_addr, len -> glas_addr

A ctx_constraint forces the resource that appears at local_addr of context ctx to appear at address glas_addr in the GLAS. Similarly, a resource constraint forces the resource to be placed at glas_addr for all contexts. Note that the latter can easily lead to an unsatisfiable GLAS configuration, so use it with care.