Configuration Reference

OF-CFG-001 v0.4.0

Complete specification for openforge.yaml, the project configuration file. This file must be placed at the root of every OpenForge project and defines all project metadata, design sources, verification settings, analysis configuration, and CI/CD integration. Validate your config at any time with openforge config validate.

Overview #

The configuration file is structured into five top-level sections:

Section	Purpose	Required
`project`	Project metadata â€” name, top module, target PDK	Yes
`design`	Design file paths â€” RTL sources, includes, constraints	Yes
`verification`	Verification settings â€” simulation, formal, crypto checks	No (defaults used)
`analysis`	Physical analysis â€” timing, power, area targets	No
`ci_integration`	CI/CD pipeline triggers and stages	No

`project` #

project:
  name: "my-ntt-accelerator"    # Project identifier (alphanumeric, hyphens)
  top_module: "ntt_top"           # Top-level RTL module name
  target_pdk: "sky130"            # Target PDK: sky130 | gf22fdx
  description: "ML-KEM NTT accelerator for QCORE-C1"   # Optional
  version: "1.0.0"               # Semantic version (optional)

Field	Type	Required	Description
`name`	string	Yes	Unique project identifier. Used in directory names, URLs, and reports.
`top_module`	string	Yes	Top-level Verilog/SystemVerilog module name for synthesis and simulation.
`target_pdk`	string	Yes	Process design kit. `sky130` for prototyping, `gf22fdx` for production.
`description`	string	No	Human-readable project description.
`version`	string	No	Semantic version string.

`design` #

design:
  sources:                         # RTL source files (glob patterns supported)
    - src/rtl/*.v
    - src/rtl/*.sv
    - src/rtl/ntt/*.v
  includes:                        # Include/header directories
    - src/include/
  constraints:                     # SDC timing constraint files
    - constraints/timing.sdc
  exclude:                         # Files to exclude from sources (optional)
    - src/rtl/deprecated_*.v

Field	Type	Required	Description
`sources`	list[string]	Yes	RTL source files. Supports glob patterns (``, `*`). Verilog (`.v`), SystemVerilog (`.sv`), VHDL (`.vhd`).
`includes`	list[string]	No	Directories added to the include search path (`+incdir+`).
`constraints`	list[string]	No	SDC timing constraint files for OpenSTA analysis.
`exclude`	list[string]	No	Glob patterns for files to exclude from source collection.

`verification` #

Top-level verification configuration. Contains sub-sections for simulation, formal verification, and crypto-specific checks.

`verification.simulation` #

verification:
  simulation:
    tool: verilator                # verilator | icarus | ghdl
    testbenches:
      - tb/test_ntt_butterfly.py
      - tb/test_mlkem_encaps.py
    coverage:
      line: true
      toggle: true
      fsm: true
    trace:
      enabled: false
      format: fst                  # vcd | fst
    power_trace: true              # Enable Hamming-model power traces
    timeout: 3600                 # Seconds
    seed: 42                      # Random seed (null for random)

Field	Type	Default	Description
`tool`	string	`verilator`	Simulation engine. Verilator for speed, Icarus for event-driven compatibility.
`testbenches`	list[string]	Auto-detect `tb/*.py`	Cocotb testbench files to execute.
`coverage.line`	boolean	`true`	Enable line coverage tracking.
`coverage.toggle`	boolean	`true`	Enable signal toggle coverage.
`coverage.fsm`	boolean	`true`	Enable FSM state/transition coverage.
`power_trace`	boolean	`false`	Collect Hamming-model power traces (requires Dyber-extended Verilator).
`timeout`	integer	`3600`	Simulation timeout in seconds.
`seed`	integer\|null	`null`	Random seed for reproducibility. Null for random.

`verification.formal` #

verification:
  formal:
    tool: symbiyosys
    properties:
      - formal/ntt_properties.sv
      - formal/fsm_properties.sv
      - formal/crypto_properties.sv
    engines:
      - smtbmc: z3                 # Bounded model checking with Z3
      - prove: abc                 # Unbounded proofs with ABC PDR
    depth: 50                     # BMC exploration depth
    timeout: 3600                 # Per-property timeout (seconds)
    auto_assert: true             # Auto-insert crypto assertions via Yosys pass

Field	Type	Default	Description
`tool`	string	`symbiyosys`	Formal verification frontend.
`properties`	list[string]	Auto-detect `formal/*.sv`	SVA property files to verify.
`engines`	list[map]	`[{smtbmc: z3}, {prove: abc}]`	Formal engines and solvers.
`depth`	integer	`50`	BMC exploration depth (number of clock cycles).
`timeout`	integer	`3600`	Timeout per property in seconds.
`auto_assert`	boolean	`true`	Enable automatic crypto assertion insertion via Yosys pass.

`verification.crypto_verification` #

The crypto verification section configures all five Dyber proprietary analysis engines. Each engine can be individually enabled/disabled and configured.

verification:
  crypto_verification:
    constant_time:
      enabled: true
      secrets:                     # Signal names containing secret data
        - "key_reg"
        - "seed"
        - "private_key"
      public:                      # Signals safe to leak
        - "ciphertext"
        - "public_key"

    side_channel:
      enabled: true
      power_model: hamming_distance  # hamming_weight | hamming_distance | switching
      tvla_threshold: 4.5           # Welch's t-test threshold
      num_traces: 10000

    entropy_analysis:
      enabled: true
      sources:
        - signal: "qrng_out"
          min_entropy: 0.99
      sinks:
        - signal: "key_gen_seed"
          required_entropy: 256

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

    ntt_validation:
      enabled: true
      standard: "FIPS-203"          # FIPS-203 | FIPS-204
      exhaustive_test: true

`analysis` #

analysis:
  timing:
    tool: opensta
    clock_period: 5.0ns           # Target clock period (200 MHz)
    corner: typical               # typical | fast | slow

  power:
    tool: openroad
    activity_file: sim/activity.saif  # From Verilator SAIF export

  area:
    tool: yosys

Field	Type	Default	Description
`timing.tool`	string	`opensta`	Static timing analysis tool.
`timing.clock_period`	string	Required	Target clock period with unit (e.g., `5.0ns`, `10ns`).
`timing.corner`	string	`typical`	Process corner: `typical`, `fast`, `slow`.
`power.activity_file`	string	Auto from sim	SAIF switching activity file for realistic power numbers.
`area.tool`	string	`yosys`	Area estimation via synthesis gate count.

`ci_integration` #

ci_integration:
  github_actions: true
  on_push:                          # Stages triggered on push to any branch
    - lint
    - simulation
    - formal_quick                  # BMC only, reduced depth
  on_pr:                            # Stages triggered on pull request
    - full_verification             # All sim + formal + basic crypto
  nightly:                          # Stages triggered on nightly schedule
    - crypto_verification           # Full crypto suite
    - exhaustive_ntt                # NTT exhaustive test (long-running)
  report_format: sarif             # Output format for CI: sarif | junit | json

Complete Example #

A full openforge.yaml for an ML-KEM accelerator project targeting the QCORE-C1 chiplet:

# openforge.yaml â€” QCORE-C1 ML-KEM Accelerator

project:
  name: "qcore-c1-mlkem"
  top_module: "qcore_top"
  target_pdk: "sky130"
  description: "ML-KEM/ML-DSA accelerator for QCORE-C1 chiplet"
  version: "0.9.0"

design:
  sources:
    - src/rtl/*.v
    - src/rtl/*.sv
    - src/rtl/ntt/*.v
    - src/rtl/keymgmt/*.v
  includes:
    - src/include/
  constraints:
    - constraints/timing.sdc

verification:
  simulation:
    tool: verilator
    testbenches:
      - tb/test_ntt_butterfly.py
      - tb/test_mlkem_encaps.py
      - tb/test_mldsa_sign.py
      - tb/test_keymgmt.py
    coverage:
      line: true
      toggle: true
      fsm: true
    power_trace: true

  formal:
    tool: symbiyosys
    properties:
      - formal/ntt_properties.sv
      - formal/keymgmt_properties.sv
      - formal/fsm_properties.sv
    engines:
      - smtbmc: z3
      - prove: abc
    depth: 50
    auto_assert: true

  crypto_verification:
    constant_time:
      enabled: true
      secrets: ["key_reg", "seed", "private_key", "nonce"]
      public: ["ciphertext", "public_key", "signature"]

    side_channel:
      enabled: true
      power_model: hamming_distance
      tvla_threshold: 4.5
      num_traces: 10000

    entropy_analysis:
      enabled: true
      sources:
        - signal: "qrng_out"
          min_entropy: 0.99
      sinks:
        - signal: "key_gen_seed"
          required_entropy: 256

    fips_compliance:
      enabled: true
      level: "140-3 Level 2"
      checks: [key_zeroization, self_test_coverage, error_handling, rng_health_tests]

    ntt_validation:
      enabled: true
      standard: "FIPS-203"
      exhaustive_test: true

analysis:
  timing:
    tool: opensta
    clock_period: 5.0ns
  power:
    tool: openroad
    activity_file: sim/activity.saif
  area:
    tool: yosys

ci_integration:
  github_actions: true
  on_push: [lint, simulation, formal_quick]
  on_pr: [full_verification]
  nightly: [crypto_verification, exhaustive_ntt]

Was this page helpful? Send feedback to docs@dyber.org

Configuration Reference

Overview #

project #

design #

verification #

verification.simulation #

verification.formal #

verification.crypto_verification #

analysis #

ci_integration #