Developer Guide

This guide covers advanced development workflows with OpenForge — writing custom testbenches, formal properties, crypto security annotations, workflow pipelines, and plugins. If you're new to OpenForge, start with the Getting Started guide first.

Overview #

OpenForge provides a layered development experience. At the simplest level, you write RTL and testbenches, configure openforge.yaml, and run openforge verify --all. At the advanced level, you can write custom Cocotb coroutines with OpenForge's power trace API, create formal property libraries for your specific design patterns, annotate your RTL with crypto security metadata, define custom multi-stage workflow pipelines, and build plugins that extend the platform's analysis capabilities.

Custom Design Flows #

The default verification flow runs lint → simulation → formal → crypto → analysis in sequence (with parallelism within stages). You can customize this by defining explicit stage ordering in openforge.yaml:

# openforge.yaml — Custom flow with only simulation + crypto checks
verification:
  flow:
    stages:
      - name: lint
        tool: verible
        fail_on: error              # error | warning | never

      - name: simulation
        tool: verilator
        depends_on: [lint]
        config:
          coverage: true
          power_trace: true
          trace_format: fst

      - name: constant_time
        tool: openforge-ct
        depends_on: [simulation]

      - name: side_channel
        tool: openforge-sca
        depends_on: [simulation]       # Needs power traces from sim

      - name: ntt_validate
        tool: openforge-ntt
        depends_on: [lint]            # Can run in parallel with sim

Stages sharing the same depends_on run in parallel. In this example, constant_time and side_channel both depend on simulation and will run concurrently once simulation completes. The ntt_validate stage only depends on lint, so it starts as soon as linting passes — even before simulation finishes.

Writing Cocotb Testbenches #

OpenForge extends Cocotb with several utilities for cryptographic hardware verification. Import them from openforge.cocotb:

from openforge.cocotb import (
    NistVectorLoader,       # Load NIST ACVP / CAVP test vectors
    ReferenceNTT,           # FIPS 203/204 NTT reference implementation
    PowerTraceCollector,    # Collect Hamming-model power traces
    CryptoTestContext,      # Context manager for crypto test sequences
    assert_constant_time,   # Assert operation took fixed cycles
)

NIST Test Vector Integration

OpenForge provides a NistVectorLoader that parses NIST ACVP (Automated Cryptographic Validation Protocol) and CAVP test vector JSON files. This ensures your implementation is validated against the official reference vectors for ML-KEM, ML-DSA, SLH-DSA, and other PQC algorithms.

import cocotb
from cocotb.triggers import RisingEdge
from openforge.cocotb import NistVectorLoader

@cocotb.test()
async def test_mlkem_encaps(dut):
    """Validate ML-KEM encapsulation against NIST ACVP vectors."""
    loader = NistVectorLoader("tb/nist_vectors/ML-KEM-768.json")

    for vector in loader.encapsulation_vectors():
        # Drive inputs
        dut.public_key.value = vector.ek  # Encapsulation key
        dut.entropy.value = vector.m      # Randomness
        dut.start.value = 1
        await RisingEdge(dut.clk)
        dut.start.value = 0

        # Wait for completion
        while not dut.done.value:
            await RisingEdge(dut.clk)

        # Check outputs against reference
        assert dut.ciphertext.value == vector.ct, \
            f"Ciphertext mismatch on vector {vector.tcId}"
        assert dut.shared_secret.value == vector.ss, \
            f"Shared secret mismatch on vector {vector.tcId}"

Power Trace Collection

For side-channel analysis, collect power traces during simulation using OpenForge's PowerTraceCollector. This works with the Verilator power trace instrumentation to capture Hamming weight/distance data per clock cycle.

from openforge.cocotb import PowerTraceCollector

@cocotb.test()
async def test_with_power_traces(dut):
    """Collect power traces for side-channel analysis."""
    collector = PowerTraceCollector(
        dut,
        signals=["ntt_core.product", "ntt_core.a_d1", "key_reg"],
        model="hamming_distance"
    )

    async with collector.recording():
        for i in range(10000):
            # Drive random inputs
            dut.data_in.value = random.randint(0, 2**12 - 1)
            dut.valid_in.value = 1
            await RisingEdge(dut.clk)

    # Export for openforge-sca consumption
    collector.export_csv("reports/power_traces.csv")
    collector.export_hdf5("reports/power_traces.h5")  # For large trace sets

Constant-Time Assertions

from openforge.cocotb import assert_constant_time

@cocotb.test()
async def test_constant_time_ntt(dut):
    """Verify NTT completes in exactly the same number of cycles for all inputs."""
    latencies = []
    for _ in range(1000):
        dut.a_in.value = random.randint(0, 3328)
        dut.b_in.value = random.randint(0, 3328)
        dut.twiddle.value = random.randint(0, 3328)
        dut.valid_in.value = 1
        await RisingEdge(dut.clk)
        dut.valid_in.value = 0

        cycles = 0
        while not dut.valid_out.value:
            await RisingEdge(dut.clk)
            cycles += 1

        latencies.append(cycles)

    # All latencies must be identical
    assert_constant_time(latencies, tolerance=0)

Coverage with PyVSC #

OpenForge integrates PyVSC for constrained random stimulus generation and functional coverage. This is particularly useful for covering the full range of cryptographic parameters:

import vsc
from openforge.cocotb import CryptoCoverage

@vsc.covergroup
class NttButterflyCovertg:
    def __init__(self):
        self.a = vsc.coverpoint(
            lambda: self.a_val,
            bins={"zero": vsc.bin(0), "low": vsc.bin_range(1, 831),
                  "mid": vsc.bin_range(832, 2496), "high": vsc.bin_range(2497, 3328)}
        )
        self.b = vsc.coverpoint(
            lambda: self.b_val,
            bins={"zero": vsc.bin(0), "low": vsc.bin_range(1, 831),
                  "mid": vsc.bin_range(832, 2496), "high": vsc.bin_range(2497, 3328)}
        )
        # Cross coverage: all (a_range x b_range) combinations
        self.ab_cross = vsc.cross([self.a, self.b])

    def sample(self, a, b):
        self.a_val = a
        self.b_val = b
        self.sample()  # Trigger coverage collection

Writing Formal Properties #

OpenForge ships a Cryptographic Property Library with pre-written SVA templates. You can use these directly or write custom properties.

Using the Crypto Property Library

Include the library in your formal directory and instantiate templates:

// formal/my_properties.sv
`include "openforge/crypto_properties.sv"

module my_properties (
    input clk, rst_n,
    input [255:0] key_reg,
    input zeroize,
    input [3:0] state,
    input error_flag
);

// Key zeroization within 100 cycles
assert property(
    key_zeroization(clk, zeroize, key_reg, 100)
);

// FSM never enters invalid state
assert property(
    fsm_valid_state(clk, state, '{4'd0, 4'd1, 4'd2, 4'd3, 4'd4, 4'd5})
);

// Error state is sticky (no escape without reset)
assert property(
    error_state_sticky(clk, !rst_n, state, 4'd5)
);

endmodule

Available Property Templates

Crypto Security Annotations #

OpenForge uses annotations in your openforge.yaml to direct the crypto security engines. These annotations tell the engines which signals contain secrets, where entropy enters the design, and what compliance requirements apply.

crypto_verification:
  # Constant-time analysis configuration
  constant_time:
    enabled: true
    secrets:                          # Signals containing secret data
      - "key_reg"
      - "seed"
      - "private_key"
      - "nonce"
    public:                           # Signals that are safe to leak
      - "ciphertext"
      - "public_key"
      - "valid_out"

  # Side-channel simulation
  side_channel:
    enabled: true
    power_model: hamming_distance    # hamming_weight | hamming_distance | switching
    tvla_threshold: 4.5             # t-test threshold for leakage detection
    num_traces: 10000

  # Entropy flow analysis
  entropy_analysis:
    enabled: true
    sources:
      - signal: "qrng_out"
        min_entropy: 0.99           # bits per sample
        type: QRNG
    sinks:
      - signal: "key_gen_seed"
        required_entropy: 256       # bits
        purpose: key_generation

  # FIPS compliance
  fips_compliance:
    enabled: true
    level: "140-3 Level 2"
    checks:
      - key_zeroization
      - self_test_coverage
      - error_handling
      - rng_health_tests
      - approved_algorithms

  # NTT validation
  ntt_validation:
    enabled: true
    standard: "FIPS-203"            # FIPS-203 (ML-KEM) | FIPS-204 (ML-DSA)
    exhaustive_test: true           # Test all q² input combinations

Custom Workflow Pipelines #

For complex projects, define multi-stage verification pipelines with conditional execution, parameterized stages, and custom aggregation:

# openforge.yaml — Multi-target pipeline
verification:
  flow:
    stages:
      - name: quick_check
        description: "Fast lint + basic sim for developer iteration"
        steps:
          - tool: verible
            config: {rules: default}
          - tool: verilator
            config: {testbenches: ["tb/smoke_test.py"]}

      - name: full_verify
        description: "Complete verification for PR merge gates"
        depends_on: [quick_check]
        steps:
          - tool: verilator
            config: {coverage: true, power_trace: true}
          - tool: symbiyosys
            config: {timeout: 3600}

      - name: crypto_audit
        description: "Full crypto security analysis for nightly builds"
        depends_on: [full_verify]
        steps:
          - tool: openforge-ct
          - tool: openforge-sca
            config: {num_traces: 50000}
          - tool: openforge-fips
          - tool: openforge-ntt
            config: {exhaustive: true}

Run specific stages from the CLI:

# Run only the quick check stage
$ openforge verify --stage quick_check

# Run the full pipeline through crypto_audit
$ openforge verify --stage crypto_audit

Plugin Development #

OpenForge supports plugins for adding custom analysis engines, report formats, and tool integrations. Plugins are Python packages that register with OpenForge via entry points.

Plugin Structure

openforge-plugin-mycheck/
├── pyproject.toml
├── src/
│   └── openforge_mycheck/
│       ├── __init__.py
│       ├── analyzer.py        # Analysis engine implementation
│       └── report.py          # Report generator

Registering a Plugin

# pyproject.toml
[project.entry-points."openforge.plugins"]
mycheck = "openforge_mycheck:MyCheckPlugin"

# src/openforge_mycheck/__init__.py
from openforge.plugin import AnalysisPlugin, AnalysisResult

class MyCheckPlugin(AnalysisPlugin):
    name = "mycheck"
    description = "Custom security analysis engine"

    def analyze(self, project, config) -> AnalysisResult:
        """Run custom analysis on the design."""
        design_files = project.get_design_files()
        # ... your analysis logic ...
        return AnalysisResult(
            passed=True,
            findings=[],
            report_data={"custom_metric": 42}
        )

Once installed (pip install openforge-plugin-mycheck), use it in openforge.yaml:

verification:
  flow:
    stages:
      - name: custom_check
        tool: mycheck                # Matches plugin name

Custom Report Templates #

OpenForge generates reports in HTML, JUnit XML, SARIF, and JSON formats. You can create custom HTML report templates using Jinja2:

# Place custom templates in your project
reports/templates/my_report.html.j2

# Generate with custom template
$ openforge report --template reports/templates/my_report.html.j2 --output reports/custom.html

Available template variables include project (project metadata), results (all verification results), coverage (coverage data), crypto (crypto analysis findings), and timing (STA results).

Best Practices #