Tool Integration Guide

OpenForge is built on a foundation of best-in-class open-source EDA tools — extended, instrumented, and orchestrated for cryptographic hardware verification. This guide documents the specific modifications OpenForge makes to each tool, how to configure them, and how to add your own tool integrations.

Overview #

OpenForge does not fork upstream tools. Instead, it extends them through compile-time options, runtime plugins, and wrapper scripts that preserve compatibility with upstream releases while adding cryptographic verification capabilities. Each tool runs inside its own Docker container with a standardized interface for input/output.

Verilator Extensions #

Verilator is OpenForge's primary simulation engine. OpenForge adds three instrumentation modes that enable security analysis without modifying your RTL source code.

A. Power Trace Instrumentation

The --power-trace flag enables per-cycle power estimation during simulation. For each clock cycle, Verilator computes the Hamming weight (count of 1-bits) and Hamming distance (XOR between consecutive values) of all monitored registers, producing a power trace file consumed by the side-channel simulator.

// PowerTraceModel — added to Verilator's tracing infrastructure
// File: src/V3PowerTrace.cpp

class PowerTraceModel {
public:
    enum Model {
        HAMMING_WEIGHT,      // Sum of 1-bits in registers
        HAMMING_DISTANCE,    // XOR between consecutive values
        SWITCHING_ACTIVITY   // Weighted by capacitance estimates
    };

    struct TracePoint {
        uint64_t cycle;
        double power_estimate;
        std::map<std::string, uint64_t> signal_values;
    };

    void recordCycle(const std::vector<SignalState>& signals) {
        TracePoint tp;
        tp.cycle = currentCycle++;
        double power = 0.0;

        for (const auto& sig : signals) {
            if (model == HAMMING_WEIGHT) {
                power += __builtin_popcountll(sig.value);
            } else if (model == HAMMING_DISTANCE) {
                power += __builtin_popcountll(sig.value ^ sig.prev_value);
            }
            tp.signal_values[sig.name] = sig.value;
        }

        tp.power_estimate = power;
        traces.push_back(tp);
    }

    void exportCSV(const std::string& filename);
    void exportHDF5(const std::string& filename); // For large traces
};

CLI Usage:

# Enable power trace during Verilator simulation
$ verilator --power-trace --power-model hamming_distance design.v

# Use RTL pragma to mark specific signals for monitoring
// In your Verilog source:
/*verilator power_trace_signal*/ reg [255:0] key_reg;

B. Taint Tracking for Constant-Time Analysis

The --taint-track flag enables dataflow tracking of secret-marked signals through the design. When a tainted signal reaches a control-flow decision or memory address, a violation is recorded with full trace-back to the taint source.

// TaintTracker — tracks secret data propagation
// File: src/V3TaintTrack.cpp

class TaintTracker {
public:
    void markSecret(const std::string& signal) {
        tainted_signals.insert(signal);
    }

    void propagate() {
        for (auto& assign : assignments) {
            if (hasTaintedOperand(assign.rhs)) {
                tainted_signals.insert(assign.lhs);

                // Check: tainted data reaches control flow
                if (isControlFlowDependent(assign.lhs)) {
                    violations.push_back({
                        .type = TAINTED_CONTROL_FLOW,
                        .signal = assign.lhs,
                        .location = assign.loc
                    });
                }

                // Check: tainted data used as memory address
                if (isMemoryAddress(assign.lhs)) {
                    violations.push_back({
                        .type = TAINTED_MEMORY_ACCESS,
                        .signal = assign.lhs,
                        .location = assign.loc
                    });
                }
            }
        }
    }
};

# Run taint tracking analysis
$ verilator --taint-track --secret-signals "key,seed,private" design.v

C. SAIF Export for Power Estimation

OpenForge's Verilator extension generates SAIF (Switching Activity Interchange Format) files for consumption by OpenSTA and OpenROAD power estimation flows. This bridges the gap between simulation and physical analysis.

// SAIFGenerator — switching activity export
class SAIFGenerator {
public:
    void recordToggle(const std::string& signal, uint64_t cycle) {
        activity[signal].toggles++;
        activity[signal].last_toggle_cycle = cycle;
    }

    void writeSAIF(const std::string& filename) {
        std::ofstream out(filename);
        out << "(SAIFILE\n";
        out << "  (SAIFVERSION \"2.0\")\n";
        out << "  (DIRECTION \"backward\")\n";
        out << "  (DESIGN\n";
        for (const auto& [sig, data] : activity) {
            out << "    (NET " << sig << "\n";
            out << "      (T0 " << data.low_time << ")\n";
            out << "      (T1 " << data.high_time << ")\n";
            out << "      (TC " << data.toggles << ")\n";
            out << "    )\n";
        }
        out << "  )\n)\n";
    }
};

D. Build Configuration

OpenForge's Verilator extensions are controlled via CMake options. When building the OpenForge Docker container, these are enabled by default:

# CMakeLists.txt — OpenForge Verilator build options
option(VERILATOR_POWER_TRACE "Enable power trace instrumentation" ON)
option(VERILATOR_TAINT_TRACK "Enable taint tracking analysis" ON)

if(VERILATOR_POWER_TRACE)
    add_definitions(-DPOWER_TRACE_ENABLED)
    target_sources(verilator PRIVATE src/V3PowerTrace.cpp)
endif()

if(VERILATOR_TAINT_TRACK)
    add_definitions(-DTAINT_TRACK_ENABLED)
    target_sources(verilator PRIVATE src/V3TaintTrack.cpp)
endif()

SymbiYosys / Yosys Extensions #

OpenForge extends the Yosys synthesis framework and SymbiYosys formal verification frontend with a cryptographic property library and an automated assertion insertion pass.

A. Cryptographic Property Library

The property library (share/formal/crypto_properties.sv) provides reusable SystemVerilog Assertions for common cryptographic verification patterns. These are automatically included when running formal verification through OpenForge.

// ═══════════════════════════════════════════
// OpenForge Cryptographic Property Library
// File: share/formal/crypto_properties.sv
// ═══════════════════════════════════════════

// ── CONSTANT-TIME PROPERTIES ──

// Control flow must not depend on secret
property ct_no_secret_branch(clk, secret, branch_cond);
    @(posedge clk)
    $stable(secret) |-> $stable(branch_cond);
endproperty

// Memory address must not depend on secret
property ct_no_secret_addr(clk, secret, addr);
    @(posedge clk)
    $stable(secret) |-> $stable(addr);
endproperty

// Fixed execution latency regardless of inputs
property ct_fixed_latency(clk, start, done, LATENCY);
    @(posedge clk)
    start |-> ##LATENCY done;
endproperty


// ── KEY HANDLING PROPERTIES ──

// Key zeroization within bounded cycles
property key_zeroization(clk, zeroize, key_reg, MAX_CYCLES);
    @(posedge clk)
    zeroize |-> ##[1:MAX_CYCLES] (key_reg == '0);
endproperty

// Key never appears on output bus
property key_isolation(clk, key_reg, output_bus);
    @(posedge clk)
    !(key_reg == output_bus) || (key_reg == '0);
endproperty


// ── FSM INTEGRITY PROPERTIES ──

// FSM stays in valid states
property fsm_valid_state(clk, state, VALID_STATES);
    @(posedge clk)
    state inside {VALID_STATES};
endproperty


// ── NTT / POLYNOMIAL PROPERTIES ──

// Cooley-Tukey butterfly correctness
property ntt_butterfly_correct(clk, valid, a_in, b_in, w, a_out, b_out, Q);
    @(posedge clk)
    valid |-> ##LATENCY (
        (a_out == (a_in + (w * b_in) % Q)) &&
        (b_out == ((a_in - (w * b_in) + Q) % Q))
    );
endproperty

B. Automated Assertion Insertion (crypto_check pass)

The crypto_check Yosys pass scans the design for cryptographic patterns and automatically inserts appropriate verification properties. It detects key signals by naming convention, FSM structures, and module annotations.

// Yosys pass — auto-insert crypto verification properties
// File: passes/formal/crypto_check.cc

struct CryptoCheckPass : public Pass {
    CryptoCheckPass() : Pass("crypto_check",
        "insert cryptographic verification properties") {}

    void execute(std::vector<std::string> args,
                 RTLIL::Design *design) override {
        std::set<std::string> key_signals;

        for (auto module : design->modules()) {
            for (auto wire : module->wires()) {
                // Auto-detect key signals by naming convention
                if (wire->name.str().find("key") != std::string::npos ||
                    wire->name.str().find("secret") != std::string::npos) {
                    key_signals.insert(wire->name.str());
                }
            }

            // Insert zeroization checks for all key signals
            for (const auto& key : key_signals)
                insertZeroizationCheck(module, key);

            // Insert constant-time checks if annotated
            if (hasConstantTimeAnnotation(module))
                insertConstantTimeChecks(module, key_signals);

            // Insert FSM integrity checks
            for (auto proc : module->processes)
                if (looksLikeFSM(proc))
                    insertFSMChecks(module, proc);
        }
    }
};

C. SymbiYosys Configuration Template

OpenForge generates .sby configuration files automatically from openforge.yaml. The template includes the crypto property library and assertion insertion pass:

# Auto-generated by OpenForge — templates/crypto_verify.sby
[options]
mode prove
depth 100

[engines]
smtbmc boolector
abc pdr

[script]
read_verilog -formal ${DESIGN_FILES}
read_verilog -formal $OPENFORGE_ROOT/share/formal/crypto_properties.sv
prep -top ${TOP_MODULE}
crypto_check -secrets ${SECRET_SIGNALS} -keys ${KEY_SIGNALS}

[files]
${DESIGN_FILES}

Cocotb Extensions #

OpenForge extends Cocotb with three Python packages for crypto-specific testbench capabilities: NIST test vector integration, power trace collection, and reference implementation comparison.

A. NIST Test Vector Loader

Automatically downloads, caches, and parses NIST CAVP/ACVP test vectors for all standardized PQC algorithms:

# openforge_cocotb/nist_vectors.py
from openforge_cocotb import NISTVectorLoader, CryptoTestRunner

# Load FIPS 203 ML-KEM test vectors
loader = NISTVectorLoader(cache_dir=".nist_vectors")
vectors = loader.load_vectors(
    algorithm="ML-KEM-768",
    operation="encapsulation"
)

# Supported algorithms:
# ML-KEM-512, ML-KEM-768, ML-KEM-1024  (FIPS 203)
# ML-DSA-44, ML-DSA-65, ML-DSA-87       (FIPS 204)
# SLH-DSA-*                              (FIPS 205)
# AES-128/192/256, SHA-3, SHAKE          (traditional)

# Run all vectors against your DUT
runner = CryptoTestRunner(dut, algorithm="ML-KEM-768")
report = await runner.run_all_vectors()

print(f"Vectors tested: {report.total}")
print(f"Passed: {report.passed}")
print(f"Failed: {report.failed}")

B. Power Trace Collector

Collects simulated power traces during Cocotb simulation, interfacing with Verilator's power trace instrumentation:

# openforge_cocotb/power_trace.py
import cocotb
from cocotb.triggers import RisingEdge
from openforge_cocotb import PowerTraceCollector

collector = PowerTraceCollector(dut, model='hamming_distance')

# Monitor specific signals
collector.add_signal("ntt_engine.butterfly.a_reg", weight=1.0)
collector.add_signal("ntt_engine.butterfly.b_reg", weight=1.0)
collector.add_signal("ntt_engine.butterfly.w_reg", weight=0.5)

# Start trace collection
collector.start_trace()

# Run your test sequence...
for i in range(10000):
    await drive_random_input(dut)
    await RisingEdge(dut.clk)

# End trace and export
trace = collector.end_trace()
trace.export_numpy("traces/mlkem_power.npy")
trace.export_csv("traces/mlkem_power.csv")

C. Reference NTT Implementation

A pure-Python reference implementation of FIPS 203/204 NTT for bit-accurate comparison against RTL output:

# openforge_cocotb/reference_ntt.py
from openforge_cocotb import ReferenceNTT

# Create reference for ML-KEM (q=3329, n=256)
ref = ReferenceNTT(standard="FIPS-203")

# Compare RTL output against reference
input_poly = [int(dut.poly_in[i].value) for i in range(256)]
expected = ref.forward_ntt(input_poly)
actual = [int(dut.poly_out[i].value) for i in range(256)]

assert expected == actual, f"NTT mismatch at index {mismatch_idx}"

D. Constant-Time Assertion Helper

# Verify fixed-cycle execution across random inputs
from openforge_cocotb import assert_constant_time

# Runs the operation 1000 times with random secrets
# and verifies cycle count is identical every time
await assert_constant_time(
    dut,
    operation="mlkem_encaps",
    input_generator=random_encaps_inputs,
    num_trials=1000,
    tolerance=0  # Zero tolerance — exactly same cycle count
)

OpenSTA Integration #

OpenForge uses OpenSTA for static timing analysis with crypto-specific reporting. The integration focuses on identifying timing paths that could create data-dependent execution time and consuming SAIF data from Verilator for power-aware timing analysis.

# openforge.yaml — OpenSTA configuration
analysis:
  timing:
    tool: opensta
    clock_period: 5.0ns         # 200 MHz target
    corner: tt_025C_1v80      # Typical corner
    report_paths: 50
    crypto_timing_check: true  # Flag data-dependent timing paths
  power:
    tool: openroad
    activity_file: sim/activity.saif  # From Verilator SAIF export

ChipWhisperer Integration #

OpenForge integrates with NewAE Technology's ChipWhisperer for post-silicon validation. Simulated power traces from openforge-sca can be compared against physical captures to validate the accuracy of the RTL power model and confirm that silicon countermeasures are effective.

Trace Correlation Workflow

# 1. Collect simulated traces during RTL verification
$ openforge verify --crypto --side-channel --traces 50000 \
    --export-traces traces/sim_traces.npy

# 2. Capture physical traces with ChipWhisperer
# (Using ChipWhisperer's own capture script)
$ python cw_capture.py --target QUAC100 --traces 50000 \
    --output traces/hw_traces.npy

# 3. Correlate simulation vs. silicon
$ openforge verify --crypto --side-channel \
    --compare-traces traces/hw_traces.npy \
    --sim-traces traces/sim_traces.npy \
    --correlation-threshold 0.85 \
    --report html --output reports/trace_correlation.html

The correlation report shows per-cycle alignment between simulated and measured traces, highlighting regions where the RTL model diverges from physical behavior. This is critical for validating that simulated TVLA/CPA results are predictive of silicon vulnerability.

OpenROAD Integration #

OpenROAD provides physical design capabilities (place and route, clock tree synthesis) and power analysis with IR drop estimation. OpenForge uses OpenROAD's power analysis with SAIF activity data from Verilator to produce more accurate power estimates than the Hamming model alone.

# Physical design flow (for ASIC targets like SkyWater SKY130)
$ openforge analyze --power --activity sim/activity.saif
$ openforge analyze --ir-drop --vectors sim/vectors.txt
$ openforge analyze --area

PDK Support #

OpenForge supports open-source and commercial PDKs for physical design and timing/power analysis:

Adding Custom Tools #

OpenForge's plugin architecture allows you to integrate custom tools into the verification pipeline. Each tool plugin implements a standard interface:

# Custom tool plugin template
from openforge.plugins import ToolPlugin, ToolResult

class MyCustomTool(ToolPlugin):
    name = "my-custom-tool"
    version = "1.0.0"
    stage = "analysis"  # lint | simulation | formal | crypto | analysis

    def configure(self, config: dict):
        """Parse tool-specific configuration from openforge.yaml"""
        self.threshold = config.get("threshold", 0.95)

    def validate_inputs(self, inputs: dict) -> bool:
        """Check required inputs are available"""
        return "design_files" in inputs

    def run(self, inputs: dict) -> ToolResult:
        """Execute the tool and return results"""
        # Your tool logic here
        return ToolResult(passed=True, artifacts={})

    def cleanup(self):
        """Clean up temporary files"""
        pass

Register your plugin in openforge.yaml:

plugins:
  - name: my-custom-tool
    module: my_package.openforge_plugin
    config:
      threshold: 0.99

Tool Version Matrix #

OpenForge pins specific tool versions in its Docker images to ensure reproducible results. The following versions are tested and supported: