Troubleshooting Guide

This guide covers common issues, diagnostic commands, and workarounds for the OpenForge EDA platform. Problems are organized by subsystem — start with the Diagnostic Commands section to gather information before diving into specific issues.

Diagnostic Commands #

Always start troubleshooting by gathering diagnostic information. The openforge doctor command checks your entire environment in one pass:

# Full environment diagnostic
$ openforge doctor

OpenForge Doctor v0.4.0
━━━━━━━━━━━━━━━━━━━━━━
  ✓ Python 3.11.7
  ✓ Verilator 5.024 (with power-trace extension)
  ✓ Yosys 0.40 (with crypto-check pass)
  ✓ SymbiYosys 0.40
  ✗ Boolector — not found (required for formal verification)
  ✓ Z3 4.13.0
  ✓ Cocotb 1.9.0
  ⚠ OpenSTA — version 2.4.0 detected (2.5.0 recommended)
  ✓ PDK: sky130 installed at /opt/pdk/sky130A
  ✓ License: valid (expires 2026-12-31)
  ✓ Configuration: openforge.yaml found and valid

2 issues found. Run 'openforge doctor --fix' to auto-repair.

# Auto-fix detected issues (installs missing tools)
$ openforge doctor --fix

# Verbose output for specific subsystem
$ openforge doctor --verbose --check verilator
$ openforge doctor --verbose --check pdk

# Export diagnostic report for support tickets
$ openforge doctor --export diagnostics.json

# Check tool extension compatibility
$ openforge doctor --check extensions

Installation Issues #

pip install openforge fails with build errors

Symptom: Compilation errors during pip install openforge-eda, typically involving C/C++ extension modules.

# Common cause: missing build dependencies
# Ubuntu/Debian:
$ sudo apt install build-essential python3-dev libffi-dev

# macOS:
$ xcode-select --install
$ brew install python@3.11

# Alternatively, use the Docker image to skip native compilation:
$ docker run -it ghcr.io/dyber/openforge:0.4.0

Docker image pull fails

Symptom: docker pull ghcr.io/dyber/openforge:0.4.0 returns authentication errors.

# Authenticate with GitHub Container Registry
$ echo $GITHUB_TOKEN | docker login ghcr.io -u USERNAME --password-stdin

# If behind a corporate proxy:
$ export HTTPS_PROXY=http://proxy.corp.example.com:8080
$ docker pull ghcr.io/dyber/openforge:0.4.0

Verilator extensions not detected

Symptom: openforge doctor shows Verilator as installed but without power-trace or taint-tracking extensions.

# Verify extensions are compiled in
$ verilator --version
# Should show: Verilator 5.024 (OpenForge patched)

# If it shows stock Verilator, rebuild from OpenForge source:
$ openforge tools install verilator --from-source

# Or ensure PATH prioritizes OpenForge's Verilator:
$ export PATH=$HOME/.openforge/tools/bin:$PATH

Verilator Problems #

Model compilation runs out of memory

Symptom: c++: fatal error: Killed signal terminated program cc1plus during Verilator model compilation.

# Reduce parallelism during C++ compilation
$ openforge verify --sim --verilator-threads 2

# Or set in openforge.yaml:
verilator:
  compile_jobs: 2       # Default: number of CPUs
  opt_level: "-O1"     # Reduce from default -O2

Power trace output is all zeros

Symptom: openforge verify --crypto --side-channel produces traces with no switching activity.

# Ensure the DUT is actually being driven during simulation
# Check that your testbench applies stimulus before trace collection starts

# Verify power model is configured
$ grep power_model openforge.yaml
verilator:
  extensions:
    power_trace:
      model: hamming_distance  # Must be set; options: hamming_weight, hamming_distance, switching
      signals: "top.dut.*"       # Ensure signal pattern matches your hierarchy

Taint tracking produces false positives

Symptom: Constant-time verifier flags operations that are intentionally not secret-dependent.

# Use taint annotations to mark public signals explicitly
# In your RTL, add comments recognized by openforge-ct:
wire [7:0] public_counter; // openforge:public
wire [7:0] key_byte;        // openforge:secret

# Or configure exclusions in openforge.yaml:
crypto_verification:
  constant_time:
    exclude_signals:
      - "top.dut.debug_*"
      - "top.dut.status_counter"

Yosys / SymbiYosys #

crypto_check pass not found

Symptom: ERROR: No such command: crypto_check when running Yosys.

# Ensure OpenForge's patched Yosys is on PATH
$ which yosys
# Should be: ~/.openforge/tools/bin/yosys

# If using system Yosys instead of OpenForge's:
$ openforge tools install yosys --from-source

# Verify crypto_check is available:
$ yosys -p "help crypto_check"

SymbiYosys timeout on formal proofs

Symptom: Formal verification runs for hours without completing, especially for key zeroization or isolation proofs.

# Use bounded model checking first to find shallow bugs:
$ openforge verify --formal --engine bmc --depth 50

# Then try induction with a shorter depth:
$ openforge verify --formal --engine pdr --timeout 1800

# Split complex properties into smaller lemmas in openforge.yaml:
formal_verification:
  strategy: incremental     # Prove lemmas bottom-up
  timeout: 1800
  engines:
    - name: boolector
      mode: bmc
    - name: z3
      mode: pdr

Simulation Failures #

NIST test vector mismatch

Symptom: FAIL: ML-KEM-768 encapsulation — output mismatch at byte 142

# 1. Verify NIST test vectors are up to date
$ openforge vectors update --all

# 2. Run with verbose comparison to see exact differences
$ openforge verify --sim --nist-vectors --verbose

# 3. Check for endianness issues (common with FIPS 203)
# ML-KEM uses little-endian byte ordering for polynomial coefficients.
# If your RTL outputs big-endian, add byte-swap in the testbench.

# 4. Dump waveforms for the failing test case
$ openforge verify --sim --nist-vectors --test-id MLKEM768-ENCAP-42 --waves

Simulation hangs or deadlocks

Symptom: Simulation runs indefinitely without producing output.

# Set a global timeout
$ openforge verify --sim --timeout 300   # 300 seconds

# Enable watchdog timer in testbench
cocotb_verification:
  watchdog:
    enabled: true
    timeout_cycles: 1000000  # Kill after 1M clock cycles

# Common causes:
# - Missing clock or reset in testbench
# - FSM stuck in illegal state (check with 'openforge verify --formal --fsm')
# - Combinational loop (detected by 'openforge verify --lint --combo-loop')

Formal Verification #

Property is "UNKNOWN" after timeout

Symptom: Formal engine returns UNKNOWN for a property — it couldn't prove or disprove it within the time limit.

# Try a different solver engine
$ openforge verify --formal --property key_zeroization --engine z3
$ openforge verify --formal --property key_zeroization --engine boolector

# Increase depth for bounded checking
$ openforge verify --formal --property key_zeroization --depth 200

# Break property into smaller sub-properties
# Instead of proving all key bits are zeroed simultaneously,
# prove per-register zeroization independently

# Add helper lemmas (assumptions that have been independently verified)
formal_verification:
  properties:
    key_zeroization:
      assume:
        - fsm_valid_state    # Assume FSM properties (already proven)

Assertion failure with no clear trace

Symptom: Formal tool reports assertion failure but the counter-example trace is hard to interpret.

# Generate waveform from counter-example
$ openforge verify --formal --property PROP_NAME --waves --output cex.vcd

# View in GTKWave
$ gtkwave cex.vcd

# Auto-annotate counter-example with signal explanations
$ openforge formal explain --cex cex.vcd --property PROP_NAME

Crypto Engine Errors #

Side-channel analysis: "Insufficient traces"

Symptom: ERROR: TVLA requires minimum 5000 traces, got 2048

# Increase trace count in configuration
crypto_verification:
  side_channel:
    tvla:
      trace_count: 10000    # Minimum 5000 for meaningful results

# Or override via CLI
$ openforge verify --crypto --side-channel --traces 10000

FIPS compliance: "Key zeroization: FORMAL_TIMEOUT"

Symptom: FIPS checker reports key zeroization as inconclusive because the formal proof timed out.

# This usually means the zeroization FSM is too complex for default settings

# 1. Increase formal timeout for FIPS checks specifically
crypto_verification:
  fips:
    checks:
      key_zeroization:
        formal_timeout: 7200  # 2 hours
        engine: z3            # Z3 often better for zeroization proofs

# 2. If still timing out, decompose the proof:
$ openforge verify --crypto --fips --check key_zeroization --decompose

NTT validation: "Twiddle factor mismatch at index N"

Symptom: NTT validator detects a mismatch between your twiddle factor ROM and the FIPS 203/204 specification.

# This is almost always a ROM initialization error.
# Generate the correct twiddle factors from the spec:
$ openforge crypto ntt-twiddles --algorithm mlkem --q 3329 --n 256 --output twiddles.hex

# Compare against your ROM file:
$ diff twiddles.hex path/to/your/twiddle_rom.hex

# Common causes:
# - Wrong primitive root of unity (ML-KEM uses ζ=17 mod 3329)
# - Bit-reversal applied incorrectly to twiddle indices
# - Endianness mismatch in ROM initialization file

Entropy flow: "No entropy sources detected"

Symptom: Entropy analyzer cannot find QRNG/TRNG source signals in the design.

# Annotate entropy sources in RTL
wire [31:0] trng_output; // openforge:entropy_source

# Or configure source signals explicitly:
crypto_verification:
  entropy_flow:
    sources:
      - signal: "top.dut.qrng.raw_bits"
        type: qrng
        min_entropy_per_bit: 0.95

Performance Issues #

Verification takes much longer than expected

# Profile verification to find bottlenecks
$ openforge verify --all --profile --output profile.json

# View time breakdown
$ openforge report profile profile.json

  Stage                Time       % Total
  ─────────────────────────────────────────
  Verilator compile    4m 12s     28.1%
  Simulation           3m 45s     25.0%
  Formal (boolector)   5m 20s     35.5%
  Crypto: CT           0m 42s      4.7%
  Crypto: NTT          1m 01s      6.7%
  ─────────────────────────────────────────
  Total               15m 00s    100.0%

High memory usage during formal verification

# Limit solver memory
formal_verification:
  memory_limit: 8G      # Default: unlimited

# Use Boolector instead of Z3 for lower memory usage on bit-vector problems
$ openforge verify --formal --engine boolector

PDK & Technology #

SkyWater SKY130 PDK not found

# Install via OpenForge
$ openforge pdk install sky130

# Or set the path if already installed:
$ openforge config set pdk.sky130.path /opt/pdk/sky130A

# Verify PDK installation
$ openforge doctor --check pdk

Timing analysis reports negative slack

Symptom: OpenSTA reports negative setup slack after place-and-route.

# Check if you're using SAIF activity data (more accurate than default)
$ openforge verify --timing --saif sim_activity.saif

# Common fixes:
# - Reduce target clock frequency
# - Pipeline long combinational paths (especially NTT butterflies)
# - Use multi-cycle path constraints for paths that don't need single-cycle

CI/CD Pipeline #

GitHub Actions: container image pull fails

# Ensure GHCR authentication is configured
jobs:
  verify:
    runs-on: ubuntu-latest
    container:
      image: ghcr.io/dyber/openforge:0.4.0
      credentials:
        username: ${{ github.actor }}
        password: ${{ secrets.GITHUB_TOKEN }}

CI cache not restoring correctly

# Ensure cache key includes all inputs that affect compiled outputs
- uses: actions/cache@v4
  with:
    path: .openforge/cache
    key: openforge-${{ hashFiles('src/**/*.v', 'src/**/*.sv', 'openforge.yaml') }}
    restore-keys: |
      openforge-

# Clear stale cache entries
$ openforge cache clean --older-than 7d

SARIF upload rejected by GitHub

# Validate SARIF before upload
$ openforge report validate --format sarif results/crypto.sarif

# Common issue: too many results (GitHub limits to 5000 per SARIF file)
# Split by engine:
$ openforge verify --crypto --constant-time --report sarif --output results/ct.sarif
$ openforge verify --crypto --side-channel --report sarif --output results/sca.sarif

Log Analysis #

OpenForge writes detailed logs to .openforge/logs/. Each verification run creates a timestamped log directory.

# View latest log
$ openforge log show --latest

# View logs for a specific run
$ openforge log show --run-id 2025-01-15T143022

# Filter by severity
$ openforge log show --latest --level error

# Search across all logs
$ openforge log search "TVLA threshold exceeded"

# Enable debug-level logging for a run
$ OPENFORGE_LOG_LEVEL=debug openforge verify --all

Log Directory Structure

.openforge/logs/
├── 2025-01-15T143022/
│   ├── openforge.log          # Master log (all subsystems)
│   ├── verilator.log          # Verilator compilation + simulation
│   ├── yosys.log              # Yosys synthesis + crypto_check
│   ├── symbiyosys.log         # Formal verification engine output
│   ├── crypto/
│   │   ├── constant_time.log  # CT analysis details
│   │   ├── side_channel.log   # SCA traces + TVLA results
│   │   ├── fips.log           # FIPS check details
│   │   └── ntt.log            # NTT validation output
│   └── timing.log             # OpenSTA timing analysis
└── latest -> 2025-01-15T143022/

Known Limitations #

Getting Support #

When filing a support request, always include the diagnostic report:

# Generate diagnostic bundle for support
$ openforge doctor --export diagnostics.json
$ openforge log show --latest --export latest_log.txt

# Create a minimal reproducer (anonymizes design files)
$ openforge support bundle --anonymize --output support_bundle.tar.gz