The Proof Center

Verification
Evidence.

This is where claims become checkable. Methodology, sample artifacts, and a release package you can inspect, so a technical evaluation can begin from evidence, not assertions.

01 Verification methodology ↓
02 Formal verification examples ↓
03 Test traceability ↓
04 Benchmark methodology ↓
05 Provenance examples ↓
06 Sample release package ↓
07 Example generated artifact ↓

§ 01Verification Methodology

Four independent layers, each closing before the next.

Static / Lint

Verilator + Yosys. Every warning is resolved or carries a written waiver - nothing is silently suppressed.

Formal

SVA properties with bounded and unbounded proofs via SymbiYosys.

Simulation

UVM 1800.2 + cocotb: scoreboards, covergroups, SVA binds, and an ARM protocol checker as a hard gate.

Regression

Reproducible seeds; full suite re-run on every change before release.

§ 02Formal Verification Examples

Properties, not vibes.

sva_nfa_props.sv · excerpt SVA

// no match asserted without a started scan
property p_match_requires_scan;
  @(posedge clk) disable iff (!rst_n)
    match_valid |-> scan_active;
endproperty
a_match_scan: assert property(p_match_requires_scan);

// backpressure is honoured: no drop while !ready
property p_no_drop_on_stall;
  @(posedge clk) disable iff (!rst_n)
    (valid && !ready) |=> $stable(data);
endproperty
a_no_drop: assert property(p_no_drop_on_stall);

proof summary · illustrative

property	mode	result
p_match_requires_scan	unbounded	✓ PASS
p_no_drop_on_stall	unbounded	✓ PASS
p_fsm_no_deadlock	k=40	✓ PASS
p_onehot_state	unbounded	✓ PASS

§ 03Test Traceability

Every test answers to a requirement.

Tests are not a pile of files; they are the leaves of a chain. Each UVM test and cocotb test implements an item in the verification plan, and each plan item exists because a numbered engineering requirement demands it. For the Regex Accelerator that chain covers 74 of 75 requirements - and the one gap is documented, not hidden.

66/66 UVM tests · hard protocol gate61/61 cocotb bring-up regression2 scoreboards14 SVA bind modules8 covergroups

01
engineering requirement

numbered, frozen at stage 1

REQ-FUNC-001
02
verification plan item

goal, method, closure criterion

VP-NFA-001
03
test

UVM sequence or cocotb test

L5_single_match

requirement	plan item	test	kind
REQ-CSR-010	VP-OCL-003	L1_register_connectivity	cocotb
REQ-TBL-005	VP-TBL-002	table_load_window_commit_test	UVM
REQ-FUNC-001	VP-NFA-001	nfa_golden_model_test	UVM
REQ-IRQ-030	VP-IRQ-001	irq_threshold_e2e_test	UVM
REQ-MATCH-021	VP-MATCH-007	L6_match_ring_drain	cocotb
REQ-PERF-200	VP-PERF-002	throughput_16gbps_sustained_test	UVM

// representative mapping. coverage closure is reported per release inside the signed package, never as a site-wide headline.

§ 04Benchmark Methodology

No number without its conditions.

metric	value	conditions
Throughput · sparse	9.5 Gbps	measured · cocotb + Verilator RTL sim · 250 MHz model
Throughput · dense	7.4 Gbps	measured · adversarial single-char pattern · burst path
Regression	61 / 61	bring-up suite PASS · register access 46/46
Clock	250 MHz	AWS F2 · Virtex UltraScale+ VU47P · single clock domain
NFA capacity	256K states	runtime-programmable URAM transition tables
Rule capacity	8,192 rules	512 character-class tables
URAM footprint	~9%	default configuration on VU47P - headroom for scaling

// benchmarks are configuration-specific. We do not publish standalone, condition-free numbers.

§ 05Provenance Examples

Every artifact traces to its source.

01
requirement

REQ-FUNC-001

#a3f1
02
architecture

arch/nfa_subsys.md

#9b22
03
rtl

nfa_byte_lane.sv

#7f3a
04
testbench

tb_coco/

#c41e
05
release

regex-v1.0.tgz

#d0e8

// short hashes shown for illustration; full SHA-256 manifests ship in the package.

§ 06Sample Release Package

Inspect the whole package.

regex-accel-v1.0/9 items

regex-accel-v1.0/
├── requirements/        # traceable, numbered
├── architecture/        # frozen spec
├── rtl/                 # synthesizable SV
├── verification/        # UVM env + seqs
├── coverage/            # closure report
├── formal/              # SVA + proofs
├── benchmarks/          # with conditions
├── MANIFEST.sha256      # every file hashed
└── RELEASE.sig          # signed

verification

✓Requirements traceability
✓Architecture specification
✓Generated RTL
✓Verification collateral
✓Coverage results

Request sample package →

§ 07Example Generated Artifact

Generated within architectural bounds.

nfa_byte_lane.sv · excerptgenerated · reviewed

// AUTO-GENERATED within frozen architecture, traceable to REQ-FUNC-001
module nfa_byte_lane #(
  parameter int MAX_STATES = 262144,  // 256K NFA states
  parameter int MAX_RULES  = 8192
)(
  input  logic        axi_clk, rst_n,
  input  logic [7:0]  byte_in,
  input  logic        byte_valid,
  // transition tables written at runtime - no resynthesis
  input  logic        tbl_we,
  output logic        match_valid,
  output logic [12:0] match_rule_id
);
  // active-state vector, formally checked via SVA properties
  // ...
endmodule

// architecture constrains generation, engineers review and approve before release.

VerificationEvidence.