Verification & Compliance

Dyber delivers production-grade verification infrastructure alongside every IP core. The verification suite ensures algorithmic correctness, security property compliance, and readiness for industry certification. This page documents the verification methodology, deliverables, and compliance support provided with each IP license.

Overview #

UVM Verification Environment #

Every Dyber IP core ships with a complete Universal Verification Methodology (UVM) environment. The UVM testbench is the primary functional verification vehicle and is designed to be reusable in the integrator's system-level verification environment.

Architecture: The UVM environment includes an AMBA bus agent (AXI4-Lite, AXI4, or APB depending on the core interface), a reference model that computes expected outputs using a C/Python golden reference, a scoreboard that compares DUT outputs against expected values, and coverage collectors that track operational coverage.

┌──────────────────────────────────────────────┐
│  UVM Test                                     │
│  ├── Sequence Library  (KAT, random, stress)  │
│  ├── AMBA Agent        (driver + monitor)     │
│  ├── Reference Model   (C golden reference)   │
│  ├── Scoreboard        (expected vs. actual)  │
│  └── Coverage          (functional + code)    │
├──────────────────────────────────────────────┤
│  DUT (Dyber IP Core)                          │
└──────────────────────────────────────────────┘

Sequence library: Pre-built test sequences include NIST KAT-driven tests (deterministic), constrained-random tests (wide coverage), stress tests (back-to-back operations, interrupt storms), and error injection tests (invalid commands, malformed input).

Reusability: The UVM environment is designed for integration into the customer's system-level testbench. AMBA agents follow UVM standard practices and can be replaced with the integrator's existing bus agents. The reference model and scoreboard are standalone components that connect to any compatible monitor interface.

NIST KAT Validation #

Every algorithm accelerator is validated against the complete NIST Known Answer Test (KAT) vector sets published alongside each standard. KAT validation provides bit-exact correctness verification — a single bit error in any intermediate computation will cause a KAT failure.

KAT tests are included as UVM sequences and also as standalone self-test firmware that can execute on the target platform without a simulation environment. The self-test firmware is suitable for power-on self-test (POST) in FIPS-compliant deployments.

Formal Verification #

Formal verification uses mathematical proof to demonstrate that security properties hold for all possible input combinations and state sequences — not just the states exercised by simulation. Dyber provides SystemVerilog Assertion (SVA) property libraries for each IP core.

Security properties verified formally:

Formal assertions are provided in SVA format compatible with commercial (Synopsys VC Formal, Cadence JasperGold, Siemens Questa Formal) and open-source (SymbiYosys) formal verification tools.

Functional Coverage #

The UVM environment includes comprehensive functional coverage models that track which operational scenarios have been exercised during verification:

Operation coverage: Every algorithm operation (KeyGen, Encaps, Decaps, Sign, Verify) at every security level has been executed at least once.

Parameter coverage: All parameter set combinations (ML-KEM-512/768/1024, ML-DSA-44/65/87, etc.) have been tested.

Interface coverage: All AMBA transaction types (read, write, burst, error response) have been exercised.

Corner case coverage: Edge cases including maximum-length messages, minimum-length messages, all-zero inputs, all-one inputs, and boundary values for polynomial coefficients.

Concurrency coverage: Back-to-back operations, interrupt during operation, reset during operation, and concurrent access patterns.

Coverage reports are generated in standard UCDB format compatible with all major EDA vendor tools.

Side-Channel Verification #

For IP cores with the DYBER-MASK masking option, Dyber provides side-channel verification results using industry-standard methodologies:

TVLA (Test Vector Leakage Assessment): Fixed-vs-random t-test evaluation at first order. The evaluation captures simulated power traces from gate-level simulation with activity annotation, computing the t-statistic at each sample point. A |t| < 4.5 threshold across all sample points confirms no detectable first-order leakage at the evaluated trace count.

Constant-time netlist analysis: Automated tooling traverses the post-synthesis netlist to verify that no multiplexer select signals, memory address bits, or clock gate enables depend on nets that carry secret data. This catches tool-introduced timing dependencies that are not visible in the RTL.

Hamming weight/distance modeling: Simulated power models based on Hamming weight and Hamming distance of register transitions provide the power trace data for TVLA. While simulated traces do not capture all physical effects (coupling, process variation), they are effective at identifying first-order leakage from algorithmic sources.

FIPS 140-3 Compliance #

Dyber provides comprehensive documentation and implementation support for FIPS 140-3 certification. The actual certification is performed by the integrator (as the module boundary depends on the specific SoC integration), but Dyber provides all the cryptographic module content required for the submission.

Common Criteria #

For Common Criteria (ISO/IEC 15408) evaluation, Dyber provides security target documentation targeting EAL4+ assurance level. The protection profile is based on cryptographic module protection profiles with PQC algorithm extensions.

Deliverables include: Security Target (ST) document, functional specification (ADV_FSP), TOE design (ADV_TSD), implementation representation guidance (ADV_IMP), and guidance documentation (AGD_OPE, AGD_PRE). The evaluation laboratory engagement and certification body interaction are the integrator's responsibility.

Automotive & Aerospace #

ISO 26262 (Automotive): Safety-critical variants of algorithm accelerators are available targeting ASIL-B readiness. Deliverables include FMEA (Failure Mode and Effects Analysis), diagnostic coverage analysis, and safety manual. The safety-critical variants include additional error detection logic (parity on memory, ECC on data paths) and deterministic failure modes.

DO-178C (Aerospace): Aerospace variants targeting DAL-C readiness are available with full requirements traceability, structural coverage analysis, and verification documentation formatted for DER review.

ACVP Test Vectors #

In addition to static NIST KAT vectors, Dyber's verification suite supports the Automated Cryptographic Validation Protocol (ACVP) test vector format. ACVP is the mechanism used by NIST's CAVP for algorithm validation and is required for FIPS certification of new algorithm implementations.

The UVM testbench includes an ACVP vector parser that ingests ACVP JSON test vector files and generates UVM sequences. This enables integrators to run the latest ACVP test vectors from NIST's ACVTS (Automated Cryptographic Validation Testing System) against their specific hardware build without modifying the testbench.

Regression Methodology #

Dyber maintains a continuous regression infrastructure that runs the full verification suite against every RTL change before release. Integrators receive IP that has passed:

Nightly regression: Full UVM test suite (all KAT vectors, constrained-random, stress tests) across all supported configurations and security levels. Code coverage (>95% line, >90% condition/toggle) and functional coverage targets verified.

Release regression: Extended test suite including formal verification proofs, TVLA evaluation (for masked variants), lint clean checks, synthesis runs on all supported FPGA platforms, and timing closure verification.

Customer regression: When integrators report issues or request modifications, regression tests specific to the integration context are added to the suite and maintained going forward.