Bedrock-RTL

High quality and composable RTL libraries in SystemVerilog

Dependencies

At minimum, you need to have the following tools installed in your environment.

• Bazel == 9.1.0 (recommended to manage this using Bazelisk)

• System Python interpreter >= 3.12

Additionally, several tools are needed to build and run all of the tests:

• Open source

  • Linting

    • Verible

  • Simulation

    • Icarus Verilog

    • Verilator

  • RTL wrapper generation

    • TopStitch

  • Additional tools included in the Docker image

    • Yosys, EQY, and Yices

    • Slang

    • XLS support libraries

• Proprietary (not provided - purchase your own installation and licenses)

  • Elaboration

    • Verific tclmain

  • Linting

    • RealIntent AscentLint

  • Simulation

    • Synopsys VCS

  • Formal

    • Cadence JasperGold

    • Synopsys VCF

Note	We no longer support Altair DSim in CI. Nevertheless, the build system should continue to support it if you wish to use it for your own tests.

The provided Dockerfile can be used to build an image with the minimum dependencies and open source tools listed above. The Dockerfile uses RockyLinux 8 on x86-64 as the base image. If you want to run tests that leverage proprietary tools, you need to provide your own installations and licenses (which are typically compatible with RockyLinux 8 on x86-64).

If you bring your own EDA tools, you may need to provide a bit of your own Python code that implements the plugin API for verilog_runner.py. If you want to use a tool that isn’t already supported, update //bazel:verilog.bzl, implement a new verilog runner plugin, and reference your new tool in the appropriate Bazel test targets. Not all tests necessarily work with every tool. Refer to the BUILD.bazel files for specifics.

Using the Published Docker Image

Prebuilt linux/amd64 images are published to the Bedrock-RTL package on GitHub Container Registry. Each image has an immutable tag of the form YYYY-MM-DD-<full-git-sha>, where the date is the commit date in UTC. We intentionally do not publish a moving latest tag.

To use the latest image, open the package page linked above, copy the tag from the most recently published version, and run:

docker pull ghcr.io/xlsynth/bedrock-rtl:<tag>
docker run --rm -it -v "$(pwd)":/src -w /src ghcr.io/xlsynth/bedrock-rtl:<tag> /bin/bash

The package is public, so pulling it does not require GitHub Container Registry authentication. Using an immutable tag makes local and CI environments reproducible; pull a newer tag from the package page when you want to update the toolchain.

Building the Docker Image Locally

To build the image from the checked-out Dockerfile instead:

docker build --platform=linux/amd64 --tag=bedrock-rtl:${USER} .
docker run --rm -it -v "$(pwd)":/src -w /src bedrock-rtl:${USER} /bin/bash

Then once inside the container, try bazel build //…​ && bazel test //fifo/sim/…​ --test_tag_filters=iverilog.

Deploying Docker Images

The docker-image-build job in .github/workflows/ci.yml builds the image for every pull request, push to main, and manual CI run. After that build succeeds, the docker-image-publish job deploys the image to ghcr.io/xlsynth/bedrock-rtl for pushes to main and manually dispatched CI runs. Pull requests build the image but do not publish it.

The publish job generates the immutable YYYY-MM-DD-<full-git-sha> tag, pushes the linux/amd64 image, attaches BuildKit provenance, and publishes a signed GitHub artifact attestation for the image digest. Repository maintainers can deploy an image manually by opening the CI workflow, selecting Run workflow, and choosing the Git ref to publish.

Pre-Commit Hooks

We use pre-commit hooks to enforce basic coding style. To install the hooks, run:

pre-commit install

This installs both the pre-commit and pre-push hooks configured by .pre-commit-config.yaml. They should automatically run on every commit and push. You can also run them manually via:

pre-commit run

We’ve tested with pre-commit version 4.0.1.

Building and Testing

We use the powerful Bazel build system to assemble filelists and to run all tests (elaboration, lint, simulation, and formal).

A one-step command builds and runs all tests:

bazel test //...

Important

Action required for tests to pass! The repository includes an Icarus Verilog plugin for open-source simulation tests, but most EDA tool plugins are intentionally not provided. Many Bazel tests will fail unless your local or CI environment provides plugins for the proprietary tools used by those tests. We keep those plugins outside the repository because: We want to keep test definitions as vendor-agnostic as possible. Certain vendors may have non-disclosure agreements that protect usage of their APIs or licensing agreements that restrict where and how the tools can be run. For additional tools, implement the plugin API by subclassing //python/verilog_runner/eda_tool.py and point to the plugin module search directories with the VERILOG_RUNNER_PLUGIN_PATH environment variable. You can set this environment variable in user.bazelrc so that it is used in all Bazel test invocations.

The Bazel test rule implementations at //bazel:verilog.bzl shell out the //python/verilog_runner/verilog_runner.py tool that presents a generic tool-agnostic API that actually implements the test.

Continuous Integration

We run continuous integration tests with GitHub Actions. The main CI workflow currently covers pre-commit, build, Python/ecc codegen tests, Stardoc, Verific, AscentLint, VCS, and Icarus. Sampled JasperGold formal tests run in the nightly workflow. See .github/workflows/ci.yml and .github/workflows/nightly.yml for details.

Style Guide

We follow the xlsynth Verilog Style Guide, which is a fork of the lowRISC style guide with some minor differences.

Bazel Rules for Verilog

This repository defines several generally-helpful Bazel Verilog rules that you can use in your own projects.

verilog_library (external)

The verilog_library rule is used to collect Verilog source and header files and track their dependencies. The original definition of the verilog_library rule can be found here. We pick up that rule dependency transitively (see the top-level MODULE.bazel).

Using verilog_library

load("@rules_hdl//verilog:providers.bzl", "verilog_library")

verilog_library(
    name = "bar",
    srcs = ["bar.sv"],
    hdrs = ["baz.svh"]
)

verilog_library(
    name = "foo",
    srcs = ["foo.sv"],
    deps = [":bar"],
)

Other rules

Please see bazel/verilog_rules.md for documentation on rules defined in this repository.

Using Bedrock

Usage is best illustrated with an example using the bzlmod dependency management system in Bazel.

Tip	You are not required to use Bazel to depend on Bedrock-RTL. You can also use the Verilog files directly in your own projects (e.g., with git submodule, git subtree, or some other method).

In your project’s MODULE.bazel:

MODULE.bazel

module(name = "your-project")

bazel_dep(name = "bedrock-rtl", version = "0.0.1")
git_override(
    module_name = "bedrock-rtl",
    commit = <fill_in_git_commit_sha>,
    remote = "https://github.com/xlsynth/bedrock-rtl",
)

rules_hdl_extension = use_extension("@bedrock-rtl//dependency_support/rules_hdl:extension.bzl", "rules_hdl_extension")
use_repo(rules_hdl_extension, "rules_hdl")

If you need to redirect the rules_hdl wrapper module in a larger Bazel dependency graph, load the extension through a root-module rules_hdl dependency instead:

bazel_dep(name = "rules_hdl", version = "0.0.0", repo_name = "rules_hdl_wrapper_module")

# Use an override only if your root module needs to provide the rules_hdl wrapper
# from a local checkout or another non-registry source.
local_path_override(
    module_name = "rules_hdl",
    path = "<path-to-rules-hdl-wrapper>",
)

rules_hdl_extension = use_extension("@rules_hdl_wrapper_module//:extension.bzl", "rules_hdl_extension")
use_repo(rules_hdl_extension, "rules_hdl")

Note

Bazel only applies module overrides from the root module. If rules_hdl is available from your configured Bazel registries, no override is needed. Otherwise, your root MODULE.bazel must provide the rules_hdl module with an override such as local_path_override, archive_override, or git_override. The direct @bedrock-rtl//dependency_support/rules_hdl:extension.bzl load shown in the main example keeps @rules_hdl//…​ labels available, but root-module overrides for rules_hdl will not affect that direct extension load.

Then suppose you have the following SystemVerilog module called datapath_join.sv:

datapath_join.sv

// An example design using two Bedrock-RTL modules: br_flow_reg_fwd and br_flow_join.
//
// Joins two or more equal-width datapaths into a single output datapath.
// Uses ready/valid protocol on all flows.
// Push-side is registered.

`include "br_asserts.svh"

module datapath_join #(
    parameter int NumFlows = 2,  // must be at least 2
    parameter int WidthPerFlow = 32  // must be at least 1
) (
    input logic clk,
    input logic rst,
    output logic [NumFlows-1:0] push_ready,
    input logic [NumFlows-1:0] push_valid,
    input logic [NumFlows-1:0][WidthPerFlow-1:0] push_data,
    input logic pop_ready,
    output logic pop_valid,
    output logic [(NumFlows*WidthPerFlow)-1:0] pop_data
);

  `BR_ASSERT_STATIC(numflows_gte_2_a, NumFlows >= 2)
  `BR_ASSERT_STATIC(widthperflow_gte_1_a, WidthPerFlow >= 1)

  logic [NumFlows-1:0] inter_ready;
  logic [NumFlows-1:0] inter_valid;
  logic [NumFlows-1:0][WidthPerFlow-1:0] inter_data;

  for (genvar i = 0; i < NumFlows; i++) begin : gen_regs
    br_flow_reg_fwd #(
        .Width(WidthPerFlow)
    ) br_flow_reg_fwd (
        .clk,
        .rst,
        .push_ready(push_ready[i]),
        .push_valid(push_valid[i]),
        .push_data (push_data[i]),
        .pop_ready (inter_ready[i]),
        .pop_valid (inter_valid[i]),
        .pop_data  (inter_data[i])
    );
  end

  br_flow_join #(
      .NumFlows(NumFlows)
  ) br_flow_join (
      .clk,
      .rst,
      .push_ready(inter_ready),
      .push_valid(inter_valid),
      .pop_ready (pop_ready),
      .pop_valid (pop_valid)
  );

  assign pop_data = inter_data;  // direct concat

endmodule : datapath_join

Your BUILD.bazel file could then do this:

BUILD.bazel

load("@bedrock-rtl//bazel:verilog.bzl", "verilog_elab_and_lint_test_suite", "verilog_elab_test", "verilog_lint_test")
load("@rules_hdl//verilog:providers.bzl", "verilog_library")

package(default_visibility = ["//visibility:private"])

verilog_library(
    name = "datapath_join",
    srcs = ["datapath_join.sv"],
    deps = [
        "@bedrock-rtl//flow/rtl:br_flow_join",
        "@bedrock-rtl//flow/rtl:br_flow_reg_fwd",
        "@bedrock-rtl//macros:br_asserts",
    ],
)

verilog_elab_test(
    name = "datapath_join_elab_test",
    deps = [":datapath_join"],
)

verilog_lint_test(
    name = "datapath_join_lint_test",
    deps = [":datapath_join"],
)

verilog_elab_and_lint_test_suite(
    name = "datapath_join_test_suite",
    params = {
        "NumFlows": [
            "2",
            "3",
        ],
        "WidthPerFlow": [
            "1",
            "64",
        ],
    },
    deps = [":datapath_join"],
)

macros: Macros and Defines

br_registers.svh: Flip-Flop Inference Macros

These macros conveniently wrap always_ff blocks, improving readability and helping to structure user code into sequential and combinational portions. The macros are named according to the following suffix convention.

• A: Asynchronous reset (if absent, then synchronous)

• I: Initial value given (if absent, then 0)

• L: Conditional load enable (if absent, then unconditional)

• N: No reset (if absent, then reset)

• X: Given explicit clock and reset names (if absent, then clk and either rst if synchronous or arst if asynchronous)

Important

Clocks are always positive-edge triggered. Resets are always active-high.

Note

The order of the suffices generally matches the order of the arguments to the macro. The suffices are also listed in alphabetical order, with the exception of L before I. The table below groups macros that share the same clock/reset behavior; the suffix convention above describes the load-enable and initial-value variants.

Macro/define	Description
BR_REG, BR_REGL, BR_REGI, BR_REGLI	Synchronous active-high reset named rst, positive-edge clock named clk; optional load enable and initial value.
BR_REGX, BR_REGLX, BR_REGIX, BR_REGLIX	Synchronous active-high reset and positive-edge clock are explicit macro arguments; optional load enable and initial value.
BR_REGA, BR_REGAL, BR_REGAI, BR_REGALI	Asynchronous active-high reset named arst, positive-edge clock named clk; optional load enable and initial value.
BR_REGAX, BR_REGALX, BR_REGAIX, BR_REGALIX	Asynchronous active-high reset and positive-edge clock are explicit macro arguments; optional load enable and initial value.
BR_REGN, BR_REGLN	No reset, positive-edge clock named clk; optional load enable.
BR_REGNX, BR_REGLNX	No reset, positive-edge clock is an explicit macro argument; optional load enable.

br_asserts.svh: Public Assertions

These assertion macros are intended for use by the user in their own designs. They are guarded (enabled) by the following defines:

• BR_ASSERT_ON — if not defined, then all macros other than BR_ASSERT_STATIC* are no-ops.

• BR_ENABLE_FPV — if not defined, then all BR_*_FPV macros are no-ops.

• BR_DISABLE_ASSERT_IMM — if defined, then all BR_ASSERT_IMM*, BR_COVER_IMM*, BR_ASSERT_COMB*, and BR_COVER_COMB* macros are no-ops.

• BR_DISABLE_FINAL_CHECKS — if defined, then all BR_ASSERT_FINAL* macros are no-ops.

Tip	It is recommended that users simply define BR_ASSERT_ON when integrating Bedrock modules into their designs. The other guards will typically not be necessary.

Important

Clocks are always positive-edge triggered. Resets are always active-high.

Macro/define	Description
BR_ASSERT_STATIC	Static (elaboration-time) assertion for use within modules
BR_ASSERT_STATIC_IN_PACKAGE	Static (elaboration-time) assertion for use within packages
BR_ASSERT_FINAL	Immediate assertion evaluated at the end of simulation (e.g., when $finish is called). Disable by defining BR_DISABLE_FINAL_CHECKS.
BR_ASSERT	Concurrent assertion with implicit clk and rst names.
BR_ASSERT_CR	Concurrent assertion with explicit clock and reset names.
BR_ASSERT_KNOWN	Concurrent assertion that an expression is known, with implicit clk and rst names.
BR_ASSERT_KNOWN_VALID	Concurrent assertion that an expression is known when a valid condition is true, with implicit clk and rst names.
BR_ASSERT_KNOWN_CR	Concurrent known-value assertion with explicit clock and reset names.
BR_ASSERT_KNOWN_VALID_CR	Concurrent known-value assertion with explicit clock and reset names and an explicit valid condition.
BR_ASSERT_IMM	Immediate assertion. Also passes if the expression is unknown. Disable by defining BR_DISABLE_ASSERT_IMM.
BR_ASSERT_COMB	Immediate assertion wrapped inside of an always_comb block. Also passes if the expression is unknown. Disable by defining BR_DISABLE_ASSERT_IMM.
BR_COVER	Concurrent cover with implicit clk and rst names.
BR_COVER_CR	Concurrent cover with explicit clock and reset names.
BR_COVER_INCL_RST	Concurrent cover that is active both in reset and out of reset, with implicit clk name.
BR_COVER_IMM	Immediate cover. Disable by defining BR_DISABLE_ASSERT_IMM.
BR_COVER_COMB	Immediate cover wrapped inside of an always_comb block. Disable by defining BR_DISABLE_ASSERT_IMM.
BR_ASSUME	Concurrent assumption with implicit clk and rst names.
BR_ASSUME_CR	Concurrent assumption with explicit clock and reset names.
BR_ASSERT_INCL_RST	Concurrent assertion that is active in reset and out of reset (but specifically intended for checking the former), with implicit clk name.
BR_ASSERT_INCL_RST_C	Concurrent assertion that is active in reset and out of reset (but specifically intended for checking the former), with explicit clock name.

FPV-only Wrappers

These assertion macros are intended for use in formal verification monitors that might be integrated into a simulation environment, but where not all formal assertions should be used in simulation. They are guarded (enabled) by the following defines:

• BR_ENABLE_FPV — if not defined, then all BR_*_FPV macros are no-ops.

Macro/define	Description
BR_ASSERT_FPV	Wraps BR_ASSERT.
BR_ASSERT_CR_FPV	Wraps BR_ASSERT_CR.
BR_ASSERT_COMB_FPV	Wraps BR_ASSERT_COMB.
BR_COVER_FPV	Wraps BR_COVER.
BR_COVER_CR_FPV	Wraps BR_COVER_CR.
BR_COVER_COMB_FPV	Wraps BR_COVER_COMB.
BR_ASSUME_FPV	Wraps BR_ASSUME.
BR_ASSUME_CR_FPV	Wraps BR_ASSUME_CR.

br_asserts_internal.svh: Bedrock-internal Assertions

These assertion macros wrap the public assertions. They are intended only for internal use inside Bedrock libraries, but the user needs to know about them. They are guarded (enabled) by the following defines:

The macros in this file are guarded with the following defines. * BR_DISABLE_INTG_CHECKS — if defined, then all the BR_*INTG checks are no-ops. * BR_ENABLE_IMPL_CHECKS — if not defined, then all the BR*_IMPL checks are no-ops.

The intent is that users should not need to do anything, so that by default they will get only the integration checks but not the implementation checks.

Tip	All of these macros wrap the public macros in br_asserts.svh, so they are also subject to the same global defines such as BR_ASSERT_ON.

Integration Checks

These checks are meant for checking the integration of a library module into an end user’s design. Disable them globally by defining BR_DISABLE_INTG_CHECKS.

Macro/define	Description
BR_ASSERT_INTG	Wraps BR_ASSERT.
BR_ASSERT_CR_INTG	Wraps BR_ASSERT_CR.
BR_ASSERT_KNOWN_INTG	Wraps BR_ASSERT_KNOWN.
BR_ASSERT_KNOWN_VALID_INTG	Wraps BR_ASSERT_KNOWN_VALID.
BR_ASSERT_KNOWN_CR_INTG	Wraps BR_ASSERT_KNOWN_CR.
BR_ASSERT_KNOWN_VALID_CR_INTG	Wraps BR_ASSERT_KNOWN_VALID_CR.
BR_ASSERT_COMB_INTG	Wraps BR_ASSERT_COMB.
BR_ASSERT_INCL_RST_INTG	Wraps BR_ASSERT_INCL_RST.
BR_ASSERT_INCL_RST_C_INTG	Wraps BR_ASSERT_INCL_RST_C.
BR_ASSERT_IMM_INTG	Wraps BR_ASSERT_IMM.
BR_COVER_INTG	Wraps BR_COVER.
BR_COVER_INCL_RST_INTG	Wraps BR_COVER_INCL_RST.
BR_COVER_CR_INTG	Wraps BR_COVER_CR.
BR_COVER_IMM_INTG	Wraps BR_COVER_IMM.
BR_COVER_COMB_INTG	Wraps BR_COVER_COMB.

Implementation Checks

These checks are meant for checking the implementation of a library module. Enable them globally by defining BR_ENABLE_IMPL_CHECKS.

Macro/define	Description
BR_ASSERT_IMPL	Wraps BR_ASSERT.
BR_ASSERT_CR_IMPL	Wraps BR_ASSERT_CR.
BR_ASSERT_KNOWN_IMPL	Wraps BR_ASSERT_KNOWN.
BR_ASSERT_KNOWN_VALID_IMPL	Wraps BR_ASSERT_KNOWN_VALID.
BR_ASSERT_KNOWN_CR_IMPL	Wraps BR_ASSERT_KNOWN_CR.
BR_ASSERT_KNOWN_VALID_CR_IMPL	Wraps BR_ASSERT_KNOWN_VALID_CR.
BR_ASSERT_COMB_IMPL	Wraps BR_ASSERT_COMB.
BR_ASSERT_INCL_RST_IMPL	Wraps BR_ASSERT_INCL_RST.
BR_ASSERT_INCL_RST_C_IMPL	Wraps BR_ASSERT_INCL_RST_C.
BR_ASSERT_IMM_IMPL	Wraps BR_ASSERT_IMM.
BR_COVER_IMPL	Wraps BR_COVER.
BR_COVER_INCL_RST_IMPL	Wraps BR_COVER_INCL_RST.
BR_COVER_CR_IMPL	Wraps BR_COVER_CR.
BR_COVER_IMM_IMPL	Wraps BR_COVER_IMM.
BR_COVER_COMB_IMPL	Wraps BR_COVER_COMB.

br_gates.svh: Gate Convenience Wrappers

These macros conveniently wrap module instantiations from the gate category.

Macro/define	Description
BR_GATE_BUF	Instantiates br_gate_buf.
BR_GATE_CLK_BUF	Instantiates br_gate_clk_buf.
BR_GATE_CLK_INV	Instantiates br_gate_clk_inv.
BR_GATE_INV	Instantiates br_gate_inv.
BR_GATE_AND2	Instantiates br_gate_and2.
BR_GATE_OR2	Instantiates br_gate_or2.
BR_GATE_XOR2	Instantiates br_gate_xor2.
BR_GATE_MUX2	Instantiates br_gate_mux2.
BR_GATE_CLK_MUX2	Instantiates br_gate_clk_mux2.
BR_GATE_ICG	Instantiates br_gate_icg.
BR_GATE_ICG_RST	Instantiates br_gate_icg_rst.
BR_GATE_CDC_SYNC	Instantiates br_gate_cdc_sync.
BR_GATE_CDC_SYNC_STAGES	Instantiates br_gate_cdc_sync with an explicit number of synchronizer stages.
BR_GATE_CDC_SYNC_ARST	Instantiates br_gate_cdc_sync_arst.
BR_GATE_CDC_SYNC_ARST_STAGES	Instantiates br_gate_cdc_sync_arst with an explicit number of synchronizer stages.
BR_GATE_CDC_RST_SYNC	Instantiates br_cdc_rst_sync as an asynchronous-reset to synchronous-reset synchronizer.
BR_GATE_CDC_RST_SYNC_STAGES	Instantiates the reset synchronizer with an explicit number of synchronizer stages.
BR_GATE_CDC_PSEUDOSTATIC, BR_GATE_CDC_PSEUDOSTATIC_BUS	Instantiates br_gate_cdc_pseudostatic for scalar or bus pseudo-static CDC nets.
BR_GATE_CDC_MAXDEL, BR_GATE_CDC_MAXDEL_BUS	Instantiates br_gate_cdc_maxdel for scalar or bus CDC nets that should be checked for max delay.

br_assign.svh: Assignment Helpers

These macros provide size-aware assignment helpers for common bit slicing and extension operations.

Macro/define	Description
BR_ZERO_EXT	Zero-extend a smaller expression into a larger destination.
BR_ASSIGN_MAYBE_ZERO_EXT	Zero-extend when the destination is wider than the source, otherwise assign directly.
BR_TRUNCATE_FROM_LSB, BR_TRUNCATE_FROM_MSB	Assign the least-significant or most-significant bits of a wider expression into a narrower destination.
BR_INSERT_TO_LSB, BR_INSERT_TO_MSB	Insert a narrower expression into the least-significant or most-significant bits of a wider destination.

br_fv.svh: Formal Verification Helpers

These macros provide small helper patterns used by formal monitors.

Macro/define	Description
BR_FV_2RAND_IDX	Constrains two symbolic indices to be stable, in range, and unique.
BR_FV_IDX	Computes the selected index for a one-hot vector.

br_tieoff.svh: Tie-off Convenience Wrappers

These macros conveniently wrap br_misc_tieoff* module instantiations.

Macro/define	Description
BR_TIEOFF_ZERO_NAMED	Instantiates br_misc_tieoff_zero with a given submodule instance suffix.
BR_TIEOFF_ONE_NAMED	Instantiates br_misc_tieoff_one with a given submodule instance suffix.
BR_TIEOFF_ZERO	Instantiates br_misc_tieoff_zero with a derived submodule instance suffix.
BR_TIEOFF_ONE	Instantiates br_misc_tieoff_one with a derived submodule instance suffix.
BR_TIEOFF_ZERO_TODO	Provided for convenience of the user grepping for TODO in the codebase, to help prevent accidental tie-offs that result in bugs. Instantiates br_misc_tieoff_zero with a derived submodule instance suffix.
BR_TIEOFF_ONE_TODO	Provided for convenience of the user grepping for TODO in the codebase, to help prevent accidental tie-offs that result in bugs. Instantiates br_misc_tieoff_one with a derived submodule instance suffix.

br_unused.svh: Unused Signal Convenience Wrappers

These macros conveniently wrap br_misc_unused module instantiations.

Macro/define	Description
BR_UNUSED_NAMED	Instantiates br_misc_unused with a given submodule instance suffix.
BR_UNUSED	Instantiates br_misc_unused with a derived submodule instance suffix.
BR_UNUSED_TODO	Provided for convenience of the user grepping for TODO in the codebase, to help prevent accidental unused signals that result in bugs. Instantiates br_misc_unused with a derived submodule instance suffix.

Modules

This section inventories public RTL modules under top-level /rtl directories. Internal implementation modules under /rtl/internal are intentionally omitted. The verification-artifact column reports repository evidence, not a promise that the tests pass in every local environment. Elab/lint means the module has Bazel elaboration/lint targets; Sim means there is a simulation testbench or generated simulation test; FPV means there is formal monitor or formal test collateral.

amba: AMBA Protocol Components

Module	Description	Verification artifacts
br_amba_apb_timing_slice	Inserts timing isolation on an APB channel.	Elab/lint, FPV.
br_amba_atb_funnel	Funnels multiple AMBA Trace Bus streams into one downstream stream.	Elab/lint, FPV.
br_amba_axi2axil	Converts an AXI subordinate interface into an AXI-Lite manager interface.	Elab/lint, FPV.
br_amba_axi_default_target	Terminates AXI requests with default target responses.	Elab/lint, FPV.
br_amba_axi_demux	Routes AXI transactions from one upstream interface to selected downstream interfaces.	Elab/lint, Sim, FPV.
br_amba_axi_isolate_mgr	Isolates the manager side of an AXI interface during reset or shutdown sequencing.	Elab/lint, Sim, FPV.
br_amba_axi_isolate_sub	Isolates the subordinate side of an AXI interface during reset or shutdown sequencing.	Elab/lint, Sim, FPV.
br_amba_axi_shrinker	Shrinks AXI data width while preserving AXI transaction semantics.	Elab/lint, Sim, FPV.
br_amba_axi_timing_slice	Inserts timing isolation on AXI channels.	Elab/lint, FPV.
br_amba_axil2apb	Bridges AXI-Lite transactions to APB.	Elab/lint, FPV.
br_amba_axil_default_target	Terminates AXI-Lite requests with default target responses.	Elab/lint, FPV.
br_amba_axil_msi	Generates AXI-Lite write transactions for message-signaled interrupts.	Elab/lint, FPV.
br_amba_axil_split	Splits AXI-Lite traffic across multiple downstream interfaces.	Elab/lint, FPV.
br_amba_axil_timing_slice	Inserts timing isolation on AXI-Lite channels.	Elab/lint, FPV.

arb: Arbiters

Module	Description	Verification artifacts
br_arb_fixed	Grants the first eligible requester according to fixed priority.	Elab/lint, Sim, FPV.
br_arb_grant_hold	Holds an arbitration grant stable until the selected requester releases it.	Elab/lint, Sim, FPV.
br_arb_lru	Grants using least-recently-used priority state.	Elab/lint, Sim, FPV.
br_arb_multi_rr	Produces multiple round-robin grants per arbitration cycle.	Elab/lint, FPV.
br_arb_pri_rr	Combines fixed-priority and round-robin arbitration behavior.	Elab/lint, FPV.
br_arb_rr	Grants using round-robin priority state.	Elab/lint, Sim, FPV.
br_arb_weighted_lru	Grants using weighted least-recently-used priority state.	Elab/lint, Sim, FPV.
br_arb_weighted_rr	Grants using weighted round-robin priority state.	Elab/lint, FPV.

cdc: Clock Domain Crossings

Module	Description	Verification artifacts
br_cdc_bit_pulse	Transfers a single-cycle pulse between clock domains.	Elab/lint, Sim.
br_cdc_bit_toggle	Synchronizes a single-bit level signal between clock domains.	Elab/lint.
br_cdc_fifo_ctrl_1r1w	Controls a dual-clock 1R1W external RAM FIFO with ready/valid push and pop flow control.	Elab/lint, FPV.
br_cdc_fifo_ctrl_1r1w_push_credit	Controls a dual-clock 1R1W external RAM FIFO with credit/valid push and ready/valid pop flow control.	Elab/lint, FPV.
br_cdc_fifo_ctrl_pop_1r1w	Provides the pop-side controller for a split dual-clock 1R1W FIFO controller.	FPV through combined FIFO controller collateral.
br_cdc_fifo_ctrl_push_1r1w	Provides the ready/valid push-side controller for a split dual-clock 1R1W FIFO controller.	FPV through combined FIFO controller collateral.
br_cdc_fifo_ctrl_push_1r1w_push_credit	Provides the credit/valid push-side controller for a split dual-clock 1R1W FIFO controller.	FPV through combined FIFO controller collateral.
br_cdc_fifo_flops	Implements a dual-clock FIFO using internal flop storage and ready/valid flow control.	Elab/lint, Sim, FPV.
br_cdc_fifo_flops_push_credit	Implements a dual-clock FIFO using internal flop storage with credit/valid push flow control.	Elab/lint, Sim, FPV.
br_cdc_reg	Transfers a register-like value between clock domains.	Elab/lint, Sim.
br_cdc_rst_sync	Synchronizes an asynchronous reset into a destination clock domain.	Elab/lint.
br_cdc_stable_data	Transfers data that is stable while sampled across a clock-domain boundary.	Elab/lint, Sim.
br_cdc_stable_data_autoupdate	Transfers stable CDC data with automatic update handling.	Elab/lint, Sim.

counter: Wrapping and Saturating Counters

Module	Description	Verification artifacts
br_counter	Counts up and down with wrapping or saturation behavior.	Elab/lint, Sim, FPV.
br_counter_decr	Counts down with wrapping or saturation behavior.	Elab/lint, Sim, FPV.
br_counter_incr	Counts up with wrapping or saturation behavior.	Elab/lint, Sim, FPV.

credit: Credit/Valid Flow Control

Module	Description	Verification artifacts
br_credit_counter	Tracks available credits for credit/valid flow control.	Elab/lint, FPV.
br_credit_receiver	Manages the receiver side of credit/valid flow control without adding datapath buffering.	Elab/lint, Sim, FPV.
br_credit_sender	Converts ready/valid sender traffic into credit/valid receiver traffic.	Elab/lint, FPV.
br_credit_sender_vc	Sends credit/valid traffic across multiple virtual channels.	Elab/lint, Sim.

csr: Control and Status Registers

Module	Description	Verification artifacts
br_csr_axil_widget	Presents a CSR memory interface through an AXI-Lite subordinate port.	Elab/lint, Sim, FPV.
br_csr_cdc	Bridges CSR requests and responses across a clock-domain boundary.	Elab/lint, FPV.
br_csr_demux	Routes CSR requests to one of multiple downstream CSR interfaces.	Elab/lint, Sim, FPV.
br_csr_mem_interface	Adapts CSR requests to a simple memory-like interface.	Elab/lint, Sim.

delay: Fixed-Delay Pipelines

Module	Description	Verification artifacts
br_delay	Delays a signal by a fixed number of stages with reset.	Elab/lint, FPV.
br_delay_deskew	Applies per-lane delay to deskew multiple related signals.	Elab/lint.
br_delay_nr	Delays a signal by a fixed number of stages without reset.	Elab/lint, FPV.
br_delay_shift_reg	Implements a loadable shift register.	Elab/lint.
br_delay_skew	Applies per-lane delay to intentionally skew multiple related signals.	Elab/lint.
br_delay_valid	Delays data using valid-based self-gating.	Elab/lint, FPV.
br_delay_valid_next	Delays data using valid-next self-gating.	Elab/lint, FPV.
br_delay_valid_next_nr	Delays data using valid-next self-gating without reset.	Elab/lint, FPV.
br_delay_valid_nr	Delays data using valid-based self-gating without reset.	Elab/lint.

demux: Simple Demultiplexers

Module	Description	Verification artifacts
br_demux_bin	Routes input data to one output selected by a binary index.	Elab/lint.
br_demux_onehot	Routes input data to outputs selected by a one-hot mask.	Elab/lint.

ecc: Error Correcting Codes

Module	Description	Verification artifacts
br_ecc_secded_decoder	Decodes SECDED-protected data and reports/corrects errors.	Elab/lint, Sim, FPV.
br_ecc_secded_encoder	Encodes data with single-error-correcting, double-error-detecting parity.	Elab/lint, Sim, FPV.
br_ecc_sed_decoder	Decodes single-error-detecting protected data and reports errors.	Elab/lint, Sim, FPV.
br_ecc_sed_encoder	Encodes data with single-error-detecting parity.	Elab/lint, Sim, FPV.

enc: Combinational Encoders

Module	Description	Verification artifacts
br_enc_bin2gray	Converts a binary value to Gray code.	Elab/lint, Sim.
br_enc_bin2onehot	Converts a binary index to a one-hot vector.	Elab/lint, Sim.
br_enc_countones	Counts the number of asserted bits in a vector.	Elab/lint, Sim.
br_enc_gray2bin	Converts a Gray-code value to binary.	Elab/lint, Sim.
br_enc_onehot2bin	Converts a one-hot vector to a binary index.	Elab/lint, Sim.
br_enc_priority_dynamic	Selects priority winners with a dynamic priority input.	Elab/lint, Sim.
br_enc_priority_encoder	Selects priority winners from a request vector.	Elab/lint, Sim.

fifo: First-In-First-Out Queues

Module	Description	Verification artifacts
br_fifo_ctrl_1r1w	Controls a 1R1W external RAM FIFO with ready/valid push and pop flow control.	Elab/lint, FPV.
br_fifo_ctrl_1r1w_push_credit	Controls a 1R1W external RAM FIFO with credit/valid push and ready/valid pop flow control.	Elab/lint, FPV.
br_fifo_flops	Implements a FIFO using internal flop storage and ready/valid flow control.	Elab/lint, Sim, FPV.
br_fifo_flops_push_credit	Implements a FIFO using internal flop storage with credit/valid push flow control.	Elab/lint, Sim, FPV.
br_fifo_shared_dynamic_ctrl	Dynamically shares FIFO storage across multiple logical FIFOs.	Elab/lint, FPV.
br_fifo_shared_dynamic_ctrl_ext_arbiter	Dynamically shares FIFO storage using an externally supplied arbiter.	Elab/lint, FPV.
br_fifo_shared_dynamic_ctrl_push_credit	Dynamically shares FIFO storage with credit/valid push flow control.	Elab/lint, FPV.
br_fifo_shared_dynamic_ctrl_push_credit_ext_arbiter	Dynamically shares FIFO storage with credit/valid push flow control and an external arbiter.	Elab/lint, FPV.
br_fifo_shared_dynamic_ctrl_push_credit_pop_credit	Dynamically shares FIFO storage with credit/valid flow control on both push and pop sides.	Elab/lint.
br_fifo_shared_dynamic_ctrl_push_credit_pop_credit_ext_arbiter	Dynamically shares FIFO storage with push/pop credits and an external arbiter.	Elab/lint.
br_fifo_shared_dynamic_flops	Implements dynamically shared FIFO storage using internal flops.	Elab/lint, Sim, FPV.
br_fifo_shared_dynamic_flops_push_credit	Implements dynamically shared flop FIFOs with credit/valid push flow control.	Elab/lint, Sim, FPV.
br_fifo_shared_dynamic_flops_push_credit_pop_credit	Implements dynamically shared flop FIFOs with credit/valid push and pop flow control.	Elab/lint, Sim.
br_fifo_shared_pop_ctrl	Arbitrates pop access for shared FIFO storage.	Elab/lint.
br_fifo_shared_pop_ctrl_credit	Arbitrates pop access for shared FIFO storage with credit flow control.	Elab/lint.
br_fifo_shared_pop_ctrl_credit_ext_arbiter	Arbitrates credit-based pop access using an external arbiter.	Elab/lint.
br_fifo_shared_pop_ctrl_ext_arbiter	Arbitrates pop access using an external arbiter.	Elab/lint.
br_fifo_shared_pstatic_ctrl	Statically partitions shared FIFO storage across logical FIFOs.	Elab/lint, FPV.
br_fifo_shared_pstatic_ctrl_push_credit	Statically partitions shared FIFO storage with credit/valid push flow control.	Elab/lint, FPV.
br_fifo_shared_pstatic_flops	Implements statically partitioned shared FIFO storage using internal flops.	Elab/lint, Sim, FPV.
br_fifo_shared_pstatic_flops_push_credit	Implements statically partitioned shared flop FIFOs with credit/valid push flow control.	Elab/lint, Sim, FPV.

flow: Ready/Valid Flow Control

Module	Description	Verification artifacts
br_flow_arb_fixed	Arbitrates ready/valid flows with fixed priority.	Elab/lint, FPV.
br_flow_arb_lru	Arbitrates ready/valid flows with least-recently-used priority.	Elab/lint, FPV.
br_flow_arb_rr	Arbitrates ready/valid flows with round-robin priority.	Elab/lint, FPV.
br_flow_burst_mux_fixed	Multiplexes bursty ready/valid flows with fixed-priority arbitration.	Elab/lint, FPV.
br_flow_burst_mux_fixed_stable	Multiplexes bursty stable-data ready/valid flows with fixed-priority arbitration.	Elab/lint, FPV.
br_flow_burst_mux_lru	Multiplexes bursty ready/valid flows with least-recently-used arbitration.	Elab/lint, FPV.
br_flow_burst_mux_lru_stable	Multiplexes bursty stable-data ready/valid flows with least-recently-used arbitration.	Elab/lint, FPV.
br_flow_burst_mux_rr	Multiplexes bursty ready/valid flows with round-robin arbitration.	Elab/lint, FPV.
br_flow_burst_mux_rr_stable	Multiplexes bursty stable-data ready/valid flows with round-robin arbitration.	Elab/lint, FPV.
br_flow_demux_select	Demultiplexes a ready/valid flow to a registered selected output.	Elab/lint, FPV.
br_flow_demux_select_unstable	Demultiplexes a ready/valid flow to a combinational selected output.	Elab/lint, FPV.
br_flow_deserializer	Converts multiple narrow ready/valid flits into fewer wider flits.	Elab/lint, FPV.
br_flow_fork	Forks one ready/valid flow to multiple downstream consumers.	Elab/lint, FPV.
br_flow_fork_select_multihot	Forks one ready/valid flow to a multihot-selected subset of consumers.	Elab/lint, FPV.
br_flow_join	Joins multiple ready/valid control flows into one output flow.	Elab/lint.
br_flow_mux_fixed	Multiplexes ready/valid flows with fixed-priority arbitration.	Elab/lint, FPV.
br_flow_mux_fixed_stable	Multiplexes stable-data ready/valid flows with fixed-priority arbitration.	Elab/lint, FPV.
br_flow_mux_lru	Multiplexes ready/valid flows with least-recently-used arbitration.	Elab/lint, FPV.
br_flow_mux_lru_stable	Multiplexes stable-data ready/valid flows with least-recently-used arbitration.	Elab/lint, FPV.
br_flow_mux_rr	Multiplexes ready/valid flows with round-robin arbitration.	Elab/lint, FPV.
br_flow_mux_rr_stable	Multiplexes stable-data ready/valid flows with round-robin arbitration.	Elab/lint, FPV.
br_flow_mux_select	Multiplexes ready/valid flows using an explicit external select and registered pop outputs.	Elab/lint, FPV.
br_flow_mux_select_unstable	Multiplexes ready/valid flows using a combinational external select.	Elab/lint, FPV.
br_flow_reg_both	Registers both forward and reverse sides of a ready/valid flow.	Elab/lint, FPV.
br_flow_reg_fwd	Registers the forward valid/data side of a ready/valid flow.	Elab/lint, FPV.
br_flow_reg_none	Passes a ready/valid flow through without registering it.	Elab/lint, FPV.
br_flow_reg_rev	Registers the reverse ready side of a ready/valid flow.	Elab/lint, FPV.
br_flow_serializer	Converts fewer wide ready/valid flits into multiple narrower flits.	Elab/lint, FPV.
br_flow_xbar_fixed	Crossbars ready/valid flows with fixed-priority arbitration.	Elab/lint, FPV.
br_flow_xbar_lru	Crossbars ready/valid flows with least-recently-used arbitration.	Elab/lint, FPV.
br_flow_xbar_rr	Crossbars ready/valid flows with round-robin arbitration.	Elab/lint, FPV.

gate: Behavioral Gate Primitives

Module	Description	Verification artifacts
br_gate_buf	Buffers a scalar signal.	Elab/lint through gate macro tests.
br_gate_clk_buf	Buffers a clock signal.	Elab/lint through gate macro tests.
br_gate_inv	Inverts a scalar signal.	Elab/lint through gate macro tests.
br_gate_clk_inv	Inverts a clock signal.	Elab/lint through gate macro tests.
br_gate_and2	Computes a two-input AND.	Elab/lint through gate macro tests.
br_gate_or2	Computes a two-input OR.	Elab/lint through gate macro tests.
br_gate_xor2	Computes a two-input XOR.	Elab/lint through gate macro tests.
br_gate_mux2	Selects between two data inputs.	Elab/lint through gate macro tests.
br_gate_clk_mux2	Selects between two clock inputs.	Elab/lint through gate macro tests.
br_gate_icg	Models an integrated clock gate.	Elab/lint through gate macro tests.
br_gate_icg_rst	Models an integrated clock gate with synchronous reset behavior.	Elab/lint through gate macro tests.
br_gate_cdc_sync	Models a CDC synchronizer cell.	Elab/lint through gate macro tests.
br_gate_cdc_sync_arst	Models a CDC synchronizer cell with asynchronous reset.	Elab/lint through gate macro tests.
br_gate_cdc_pseudostatic	Marks a pseudo-static CDC crossing.	Elab/lint through gate macro tests.
br_gate_cdc_maxdel	Marks a CDC crossing that should receive max-delay checking.	Elab/lint through gate macro tests.

lfsr: Linear Feedback Shift Registers

Module	Description	Verification artifacts
br_lfsr	Implements a configurable linear feedback shift register.	Elab/lint, Sim.

misc: Miscellaneous

Module	Description	Verification artifacts
br_misc_tieoff_one	Drives an expression to constant ones and waives related lint warnings internally.	Elab/lint.
br_misc_tieoff_zero	Drives an expression to constant zeros and waives related lint warnings internally.	Elab/lint.
br_misc_unused	Sinks an unused expression and waives related lint warnings internally.	Elab/lint.

multi_xfer: Multiple-Transfer Flow Control

Module	Description	Verification artifacts
br_multi_xfer_distributor_rr	Distributes multi-transfer work using round-robin selection.	Elab/lint, FPV.
br_multi_xfer_reg_fwd	Registers the forward side of a multi-transfer interface.	Elab/lint, Sim, FPV.

mux: Simple Multiplexers

Module	Description	Verification artifacts
br_mux_bin	Selects one input using a binary index.	Elab/lint, Sim.
br_mux_bin_array	Selects one element from an unpacked input array using a binary index.	Elab/lint.
br_mux_bin_structured_gates	Builds a binary-select mux from structured gate primitives.	Elab/lint, Sim.
br_mux_onehot	Selects inputs using a one-hot select vector.	Elab/lint, Sim.

ram: Memories

Module	Description	Verification artifacts
br_ram_addr_decoder	Decodes RAM addresses and optionally steers write data for tiled RAMs.	Elab/lint, FPV.
br_ram_data_rd_pipe	Pipelines read data returned from tiled RAMs.	Elab/lint, FPV.
br_ram_flops	Implements a tiled flop RAM with configurable read and write ports.	Elab/lint, FPV.
br_ram_flops_1r1w_mock	Provides a simplified one-read, one-write flop RAM mock that should not be synthesized.	Elab/lint, Sim collateral.
br_ram_flops_tile	Implements one physical tile of a flop RAM with configurable read and write ports.	Elab/lint, FPV.
br_ram_initializer	Initializes RAM contents through a write port after reset.	Elab/lint, Sim collateral, FPV.

shift: Shifters

Module	Description	Verification artifacts
br_shift_left	Shifts an input value left by a selected amount.	Elab/lint, Sim.
br_shift_right	Shifts an input value right by a selected amount.	Elab/lint, Sim.
br_shift_rotate	Rotates an input value by a selected amount.	Elab/lint, Sim.

tracker: Tracking Data Structures

Module	Description	Verification artifacts
br_tracker_freelist	Manages allocation and deallocation of free identifiers or tags.	Elab/lint, Sim, FPV.
br_tracker_linked_list_ctrl	Manages linked-list pointers for tracker-style data structures.	Elab/lint, Sim, FPV.
br_tracker_reorder	Reorders completed operations back into sequence order.	Elab/lint, FPV.
br_tracker_reorder_buffer_ctrl_1r1w	Controls a reorder buffer backed by a one-read, one-write memory.	Elab/lint, FPV.
br_tracker_reorder_buffer_flops	Implements a flop-backed reorder buffer.	Elab/lint, Sim, FPV.
br_tracker_sequence	Tracks sequence numbers and wraparound ordering.	Elab/lint, FPV.

Packages and Formal Libraries

RTL Packages

Package	Public helpers	Verification artifacts
br_amba	AMBA protocol constants, typedefs, and helpers used by amba/rtl.	Elab/lint via AMBA module users.
br_cdc_pkg	CDC helper declarations used by CDC FIFO and register modules.	Elab/lint via CDC module users.
br_ecc_secded	_get_max_message_width, get_message_width, get_parity_width	Package elaboration test.
br_lfsr_taps	LFSR tap helper package used by br_lfsr.	Package elaboration test; Sim through br_lfsr_tb.
br_math	floor_div, ceil_div, align_down, align_up, is_power_of_2, is_even, clogb, clamped_clog2, min2, max2, exp2, round_up_to_power_of_2	Package elaboration test.

fpv/lib: Reusable Formal Monitors

Module	Description
fv_4phase_handshake	Formal monitor for four-phase handshake behavior.
fv_delay	Formal monitor for delay-line behavior.
fv_fifo	Formal monitor for FIFO ordering and occupancy behavior.
fv_ram	Formal monitor for RAM behavior.
fv_valid_ready_check	Formal monitor for valid/ready protocol behavior.
fv_wolper_coloring	Formal helper for Wolper-style coloring arguments.