Getting Started with OpenForge EDA

This guide walks you through creating your first OpenForge project — a simplified ML-KEM accelerator module — from initialization through simulation, formal verification, and cryptographic security analysis. By the end, you will have a working verification environment with full crypto-specific analysis coverage.

Quick Overview #

OpenForge organizes work into projects. Each project contains your RTL design files, testbenches, constraint files, and an openforge.yaml configuration that defines your verification and analysis flows. The platform orchestrates open-source and Dyber-proprietary tools across four verification domains:

The typical workflow follows this sequence: initialize a project, add design files, configure verification targets, run the verification pipeline, and review results either via the CLI or the Web UI dashboard.

Your First Project #

We'll create a project that verifies a simple NTT butterfly unit — the core building block of ML-KEM and ML-DSA lattice operations. This is representative of what you'd verify when developing post-quantum cryptographic hardware with OpenForge.

Initialize the Project

# Create a new OpenForge project using the crypto-accelerator template
$ openforge init ntt-butterfly --template crypto-accelerator

✓ Created project: ntt-butterfly
✓ Template: crypto-accelerator
✓ Generated openforge.yaml
✓ Created directory structure:

  ntt-butterfly/
  ├── openforge.yaml
  ├── src/
  │   └── rtl/
  │       └── ntt_butterfly.v      # Example Cooley-Tukey butterfly
  ├── tb/
  │   └── test_ntt_butterfly.py    # Cocotb testbench
  ├── formal/
  │   └── ntt_properties.sv        # Formal assertions
  ├── constraints/
  │   └── timing.sdc               # Timing constraints
  └── reports/                      # Output reports directory

$ cd ntt-butterfly

The crypto-accelerator template pre-populates a working NTT butterfly design with testbenches, formal properties, and an openforge.yaml configured for all verification domains including the Dyber crypto security analysis suite.

Available Templates

Project Structure #

Every OpenForge project follows a consistent directory layout. The openforge.yaml at the root is the single source of truth for all configuration.

ntt-butterfly/
├── openforge.yaml              # Project configuration (required)
├── src/
│   ├── rtl/                    # RTL design files (.v, .sv, .vhd)
│   │   ├── ntt_butterfly.v     # Cooley-Tukey butterfly unit
│   │   ├── mod_reduce.v        # Barrett/Montgomery reduction
│   │   └── twiddle_rom.v       # Pre-computed twiddle factor ROM
│   └── include/                # Header/parameter files
│       └── ntt_params.vh       # ML-KEM constants (q=3329, n=256)
├── tb/
│   ├── test_ntt_butterfly.py   # Cocotb testbench
│   ├── test_mod_reduce.py      # Modular reduction tests
│   └── nist_vectors/           # NIST ACVP test vectors
│       └── ML-KEM-768.json
├── formal/
│   ├── ntt_properties.sv       # NTT-specific formal properties
│   ├── crypto_properties.sv    # OpenForge crypto property library
│   └── fsm_properties.sv       # State machine integrity assertions
├── constraints/
│   └── timing.sdc              # SDC timing constraints
├── reports/                    # Generated reports (HTML, JUnit, SARIF)
└── .openforge/                 # Cache and intermediate files

Adding Design Files #

The template includes a working Cooley-Tukey butterfly unit. Here's the core design — this is what OpenForge will verify across all four domains:

// src/rtl/ntt_butterfly.v — Cooley-Tukey butterfly for ML-KEM
module ntt_butterfly #(
    parameter Q = 3329,          // ML-KEM prime modulus
    parameter DATA_W = 12         // ceil(log2(Q))
)(
    input  wire              clk,
    input  wire              rst_n,
    input  wire              valid_in,
    input  wire [DATA_W-1:0]  a_in,       // First operand
    input  wire [DATA_W-1:0]  b_in,       // Second operand
    input  wire [DATA_W-1:0]  twiddle,    // Twiddle factor ζ
    output reg              valid_out,
    output reg  [DATA_W-1:0]  a_out,      // a + ζ·b mod q
    output reg  [DATA_W-1:0]  b_out       // a - ζ·b mod q
);
    // Pipeline stage 1: multiply
    reg [2*DATA_W-1:0] product;
    reg [DATA_W-1:0]   a_d1;
    reg                valid_d1;

    always @(posedge clk or negedge rst_n) begin
        if (!rst_n) begin
            product  <= 0;
            a_d1     <= 0;
            valid_d1 <= 0;
        end else begin
            product  <= twiddle * b_in;       // ζ · b
            a_d1     <= a_in;
            valid_d1 <= valid_in;
        end
    end

    // Pipeline stage 2: Barrett reduction + add/sub
    wire [DATA_W-1:0] t = product % Q;   // Replace with Barrett in production

    always @(posedge clk or negedge rst_n) begin
        if (!rst_n) begin
            a_out     <= 0;
            b_out     <= 0;
            valid_out <= 0;
        end else begin
            a_out     <= (a_d1 + t < Q) ? (a_d1 + t) : (a_d1 + t - Q);
            b_out     <= (a_d1 >= t)    ? (a_d1 - t) : (a_d1 - t + Q);
            valid_out <= valid_d1;
        end
    end

endmodule

The corresponding testbench uses Cocotb with OpenForge's NIST test vector integration to verify functional correctness against the FIPS 203 reference implementation:

# tb/test_ntt_butterfly.py — Cocotb testbench with NIST vector integration
import cocotb
from cocotb.clock import Clock
from cocotb.triggers import RisingEdge, Timer
from openforge.cocotb import NistVectorLoader, ReferenceNTT

Q = 3329

# Reference butterfly computation
def ref_butterfly(a, b, w):
    t = (w * b) % Q
    return (a + t) % Q, (a - t + Q) % Q

@cocotb.test()
async def test_butterfly_exhaustive(dut):
    """Test butterfly against reference for random inputs."""
    clock = Clock(dut.clk, 10, units="ns")
    cocotb.start_soon(clock.start())

    # Reset
    dut.rst_n.value = 0
    await RisingEdge(dut.clk)
    dut.rst_n.value = 1
    await RisingEdge(dut.clk)

    # Test 10000 random inputs
    import random
    for _ in range(10000):
        a = random.randint(0, Q - 1)
        b = random.randint(0, Q - 1)
        w = random.randint(0, Q - 1)

        dut.a_in.value = a
        dut.b_in.value = b
        dut.twiddle.value = w
        dut.valid_in.value = 1
        await RisingEdge(dut.clk)

        dut.valid_in.value = 0
        # Wait for 2-stage pipeline
        await RisingEdge(dut.clk)
        await RisingEdge(dut.clk)

        exp_a, exp_b = ref_butterfly(a, b, w)
        assert dut.a_out.value == exp_a, \
            f"a_out mismatch: got {dut.a_out.value}, expected {exp_a}"
        assert dut.b_out.value == exp_b, \
            f"b_out mismatch: got {dut.b_out.value}, expected {exp_b}"

@cocotb.test()
async def test_nist_vectors(dut):
    """Validate against NIST ACVP ML-KEM test vectors."""
    loader = NistVectorLoader("tb/nist_vectors/ML-KEM-768.json")
    ref = ReferenceNTT(q=Q, n=256)

    for vector in loader.butterfly_vectors():
        dut.a_in.value = vector.a
        dut.b_in.value = vector.b
        dut.twiddle.value = vector.twiddle
        dut.valid_in.value = 1
        await RisingEdge(dut.clk)
        dut.valid_in.value = 0
        await RisingEdge(dut.clk)
        await RisingEdge(dut.clk)

        assert dut.a_out.value == vector.expected_a
        assert dut.b_out.value == vector.expected_b

Running Simulation #

With the project initialized and design files in place, run the simulation pipeline:

# Run simulation with coverage collection
$ openforge verify --sim --coverage

┌─────────────────────────────────────────────────┐
│  OpenForge EDA — Simulation Pipeline             │
└─────────────────────────────────────────────────┘

â–¸ Compiling with Verilator 5.028...
  Sources: src/rtl/ntt_butterfly.v, src/rtl/mod_reduce.v, src/rtl/twiddle_rom.v
  Top module: ntt_butterfly
  Flags: --coverage --trace --power-trace

â–¸ Running Cocotb testbenches...
  ✓ test_butterfly_exhaustive     10000/10000 passed     [4.2s]
  ✓ test_nist_vectors              48/48 passed           [0.3s]

â–¸ Coverage Report:
  Line coverage:     96.4%  (243/252)
  Toggle coverage:   89.7%  (412/459)
  FSM coverage:      100%   (6/6 states)

▸ Power trace collected: 50248 cycles → reports/power_trace.csv

━━━ SIMULATION PASSED ━━━
  2 tests passed, 0 failed
  Reports: reports/sim_report.html

The --coverage flag enables Verilator's line, toggle, and FSM coverage tracking. OpenForge also activates its power trace instrumentation mode (a Dyber extension to Verilator) to collect Hamming weight and Hamming distance traces for use in the side-channel analysis stage.

Simulation Options

Formal Verification #

OpenForge integrates SymbiYosys to formally prove properties about your design. The crypto-accelerator template includes pre-written SVA assertions from the OpenForge Cryptographic Property Library:

// formal/ntt_properties.sv — from OpenForge Crypto Property Library

// Butterfly output must be in valid range [0, Q)
property output_range_a;
    @(posedge clk) disable iff (!rst_n)
    valid_out |-> (a_out < Q);
endproperty

property output_range_b;
    @(posedge clk) disable iff (!rst_n)
    valid_out |-> (b_out < Q);
endproperty

// Butterfly correctness: a' = (a + ζ·b) mod q
property ct_butterfly_correct;
    @(posedge clk) disable iff (!rst_n)
    valid_in |-> ##2 (
        (a_out == (($past(a_in,2) + ($past(twiddle,2) * $past(b_in,2)) % Q) % Q)) &&
        (b_out == (($past(a_in,2) - ($past(twiddle,2) * $past(b_in,2)) % Q + Q) % Q))
    );
endproperty

// Fixed 2-cycle latency (constant-time)
property ct_fixed_latency;
    @(posedge clk) disable iff (!rst_n)
    valid_in |-> ##2 valid_out;
endproperty

assert property(output_range_a);
assert property(output_range_b);
assert property(ct_butterfly_correct);
assert property(ct_fixed_latency);

Run the formal verification pipeline:

# Run formal verification with default engines (Z3 + ABC)
$ openforge verify --formal

┌─────────────────────────────────────────────────┐
│  OpenForge EDA — Formal Verification Pipeline     │
└─────────────────────────────────────────────────┘

â–¸ Synthesizing with Yosys for formal backend...
â–¸ Running SymbiYosys with engines: smtbmc(z3), prove(abc)

  ✓ PROVEN  output_range_a         [BMC depth=50, 1.2s]
  ✓ PROVEN  output_range_b         [BMC depth=50, 1.1s]
  ✓ PROVEN  ct_butterfly_correct   [k-induction, 3.4s]
  ✓ PROVEN  ct_fixed_latency       [BMC depth=20, 0.4s]

━━━ FORMAL VERIFICATION PASSED ━━━
  4 properties proven, 0 failed, 0 inconclusive
  Reports: reports/formal_report.html

The formal engine uses bounded model checking (BMC) first to search for counterexamples, then k-induction or property-directed reachability (PDR) to achieve full proofs. Properties that cannot be proven within the timeout are reported as inconclusive.

Crypto Security Analysis #

This is where OpenForge differentiates from every commercial EDA tool. The Dyber Cryptographic Security Pod runs five specialized analysis engines against your design. Run the full crypto analysis suite:

# Run all crypto verification checks
$ openforge verify --crypto

┌─────────────────────────────────────────────────┐
│  OpenForge EDA — Crypto Security Analysis         │
└─────────────────────────────────────────────────┘

â–¸ Constant-Time Verification (openforge-ct)
  Secrets: [twiddle, b_in]  Public: [a_out, b_out, valid_out]
  ✓ No tainted control flow detected
  ✓ No secret-dependent memory access
  ✓ Fixed-latency execution confirmed (2 cycles)
  ✓ Formal CT proof via SymbiYosys: PROVEN

â–¸ Side-Channel Leakage Simulation (openforge-sca)
  Model: hamming_distance | Traces: 10000
  ✓ TVLA t-test: max |t| = 2.31 (threshold: 4.5)
  ✓ CPA correlation: max ρ = 0.12 (no significant leakage)
  âš  Advisory: pipeline register 'product' shows elevated HW correlation
     Recommendation: Add masking on multiplier output stage

â–¸ NTT/Polynomial Validation (openforge-ntt)
  Standard: FIPS 203 (ML-KEM) | Mode: Cooley-Tukey forward
  ✓ Butterfly arithmetic: matches reference
  ✓ Modular reduction: correct for all q=3329 inputs
  ✓ Output range: [0, Q) verified

▸ FIPS Compliance (openforge-fips) — skipped (no key storage in this module)
▸ Entropy Flow (openforge-entropy) — skipped (no entropy sources in this module)

━━━ CRYPTO ANALYSIS PASSED ━━━
  3 checks passed, 0 failed, 2 skipped, 1 advisory
  Reports: reports/crypto_report.html, reports/crypto_report.sarif

Each crypto analysis engine can also be run individually for targeted debugging:

# Run only constant-time analysis
$ openforge verify --crypto --constant-time

# Run side-channel simulation with more traces
$ openforge verify --crypto --side-channel --traces 50000

# Run NTT validation in exhaustive mode (all q² input pairs)
$ openforge verify --crypto --ntt --exhaustive

Viewing Results #

OpenForge generates reports in multiple formats. After running the full verification suite, your reports directory contains:

reports/
├── sim_report.html            # Interactive simulation report
├── coverage_report.html       # Code coverage breakdown
├── formal_report.html         # Formal proof status per property
├── crypto_report.html         # Crypto analysis dashboard
├── crypto_report.sarif        # SARIF for GitHub Security tab
├── power_trace.csv            # Hamming-model power traces
├── tvla_results.json          # TVLA t-test values per cycle
├── ntt_validation.json        # NTT reference comparison results
└── junit_results.xml          # JUnit XML for CI systems

Generate a consolidated HTML dashboard:

$ openforge report --format html --output reports/dashboard.html
✓ Generated consolidated report: reports/dashboard.html
✓ Open in browser: file:///home/user/ntt-butterfly/reports/dashboard.html

Using the Web UI #

If you deployed OpenForge with Docker Compose or Kubernetes, the Web UI provides a visual dashboard for managing projects and viewing results. Access it at http://localhost:8080 (or your configured hostname).

The Web UI offers:

To push a project to the Web UI from the CLI:

# Register project with OpenForge server
$ openforge project register --server http://localhost:8080

✓ Project 'ntt-butterfly' registered
✓ Project URL: http://localhost:8080/projects/ntt-butterfly

# Trigger remote verification run
$ openforge verify --all --remote

✓ Job submitted: job-2026-01-15-001
✓ Monitor: http://localhost:8080/jobs/job-2026-01-15-001

Next Steps #

Now that you've verified your first design through the full OpenForge pipeline, explore these topics to deepen your understanding: