Protocols

Protocols is a DSL for specifying & testing hardware communication protocols at the cycle-level register-transfer level (RTL). A protocol is described using an prot definition containing a sequence of statements:

• symbol := RHS assigns the value of the RHS expression to the DUT input port symbol. The right-hand side expression may be an arbitrary value, represented by X ("don't care").
• step(n) advances the clock by n cycles (n > 0)
• fork() allows for concurrent protocol execution.
• assert_eq(e1, e2) tests equality between e1 and e2.
• while and if/else blocks allow for control flow
• repeat num_iters iterations { ... } is a loop that executes for num_iters iterations exactly, where num_iters must be an input parameter supplied to the prot

This repository contains:

• An interpreter for the DSL
• A backwards interpreter (BI) tool, which given a specification of a hardware module's communication behavior (written in our DSL) and a .fst waveform file, infers a transaction-level trace that is consistent with the waveform data
• Common infrastructure shared between the interpreter & the BI, such as a parser, type-checker and pretty-printer for our DSL These tools are all implemented in Rust, with some auxiliary benchmarking scripts written in Python.

Installation + Build Instructions

Installation script: Run ./install.sh to install all dependencies required for macOS / Linux. If you want, you can also manually install dependencies, as described below.

Manually installing dependencies: Note: the instructions below assume a macOS environment.

• Ensure you have Homebrew and uv installed
  • If not, follow these instructions to install Homebrew and uv
• (Optional) Run brew install hyperfine to install Hyperfine, a command-line benchmarking tool
• Run brew install just to install Just, a command runner
• Run cargo install --git https://github.com/Nikil-Shyamsunder/runt.git to install our fork of Runt, a command-line tool we use for snapshot tests. Runt compares the output of our tools to expected outputs stored in dedicated files.
• Run uv sync to install the Python dependencies specified in pyproject.toml
• Some of the benchmarks correspond to real-world bugs taken from the artifact for Debugging in the Brave New World of Reconfigurable Hardware (Ma et al. ASPLOS '22) -- these can be found in the tests/fpga-debugging sub-directory (more details in the README of the sub-directories corresponding to each bug)

Interpreter-specific dependencies:

• Run brew install yosys to install Yosys

Building the source code:

• Run cargo build to build the Rust code
• Run just test to execute all unit tests (cargo test) + snapshot tests (via Runt)
• To generate HTML documentation, run just doc (this opens Cargo-generated docs in your browser)

Backwards Interpreter CLI

The CLI for the BI can be used as follows:

$ cargo bi --help
analyze signal traces to extract transactions

Usage: bi [OPTIONS] --wave <WAVE_FILE>

Options:
  -p, --protocol <PROTOCOLS_FILE>
          One or several protocol files.
  -w, --wave <WAVE_FILE>
          Path to a waveform trace (.fst, .vcd, .ghw) file
  -i, --instances <INSTANCES>...
          A mapping of DUT struct in the protocol file to an instance in the signal trace. Can be used multiple times. Format is: `${instance_name}:${dut_struct_name}
  -v, --verbose...
          Increase logging verbosity
  -q, --quiet...
          Decrease logging verbosity
      --sample-posedge <SIGNAL_TO_SAMPLE_ON_RISING_EDGE>
          Optional argument which specifies the name of the signal to sample on a rising edge (posedge). If enabled, this flag acts as the "clock" signal for the monitor. Note: the full path to the signal should be passed as this argument, e.g. `uut_rx.clk`, where `uut_rx` is an instance in the signal trace
      --include-idle
          Optional flag: if enabled, always prints out idle transcations regardless of whether the protocol has been annotated with `#[idle]`
      --show-steps
          If enabled, displays the start & end step for each inferred transaction
      --include-in-progress
          This flag will make the bi append any in-progress transactions to the trace
      --show-waveform-time

      --time-unit <TIME_UNIT>

      --max-traces <MAX_TRACES>
          Limit the number of traces written to stdout
      --color <COLOR_CHOICE>
          To suppress colors in error messages, pass in `--color never`. Otherwise, by default, error messages are displayed with colors [default: auto] [possible values: auto, always, never]
  -d, --display-hex
          If enabled, displays integer literals using hexadecimal notation
  -r, --rename <RENAME>...
          Rename pins of the DUT. &{field name in the struct} = ${verilog name}
  -h, --help
          Print help

Example usage:

$ cd tests
$ cargo bi -p adders/add_d1.prot --wave adders/add_d1.fst --instances add_d1:Adder

Interpreter CLI

The interpreter has a CLI, which can be invoked as follows:

$ cargo interp --help

Usage: protocols-interp [OPTIONS] --protocol <PROTOCOLS_FILE> --transactions <TRANSACTIONS_FILE>

Options:
      --verilog <VERILOG_FILES>...
          Paths to one or more Verilog (.v) files
  -p, --protocol <PROTOCOLS_FILE>
          Path to a Protocol (.prot) file
  -t, --transactions <TRANSACTIONS_FILE>
          Path to a Transactions (.tx) file
  -m, --module <MODULE_NAME>
          Name of the top-level module (if one exists)
  -f, --fst <WAVEFORM_FILE>
          (Optional) Name of the waveform file (.fst) in which to save results
  -v, --verbose...
          Increase logging verbosity
  -q, --quiet...
          Decrease logging verbosity
      --color <COLOR_CHOICE>
          Pass in `--color never` to suppress colored error messages. (By default, error messages are displayed w/ ANSI colors.) [default: auto] [possible values: auto, always, never]
  -n, --no-error-locations
          Whether to suppress location info (source file and label) in error messages
      --max-steps <MAX_STEPS>
          Stop the interpreter if it ever reaches the maximum number of cycles specified with this option
  -h, --help
          Print help

Example usage:

$ cargo interp --verilog tests/adders/adder_d1/add_d1.v \
        --protocol tests/adders/adder_d1/add_d1.prot \
        -t tests/adders/adder_d1/both_threads_pass.tx \
        --verbose

Syntax highlighting

This repository contains a TextMate Bundle, which provides syntax highlighting for .prot and .tx files (the .tx file format is used to supply a list of transactions to be executed for the interpreter).

VS Code Installation: Add a link to the Protocols VS Code extension directory to your VS Code extensions directory as follows:

$ cd $HOME/.vscode/extensions
$ ln -s <path to protocols root directory>/tools/protocols-textmate protocols.protocols-0.0.1

Then, restart VS Code.

RustRover Installation: Go to Settings -> Editor -> TextMate Bundles. Click the + and navigate to <path to protocols root directory>/tools/protocols-textmate in your file explorer.

One confirmed, protocols should appear as an entry in the TextMate Bundles table.

If the syntax highlighting does not immediately load, restart RustRover.