Verification Status

Comprehensive verification results for the MHX™ Ternary RISC-V Core.

Test Suites
7/7
All passing
Code Coverage
85.2%
Line coverage
Formal Proofs
50/50
Assertions verified

Test Suites

RTL Linting (Verilator)

No warnings or errors

Passing

~2min

RTL Linting (Verible)

Code style compliant

Passing

~1min

Ternary ALU Unit Tests

All arithmetic operations verified

Passing

~5min

Neural Unit Tests

MAC, ReLU, sigmoid, tanh tested

Passing

~8min

Register File Tests

Read/write integrity confirmed

Passing

~3min

Integration Tests

Full pipeline simulation

Passing

~15min

Formal Verification

50 assertions proved

Passing

~20min

Code Coverage

Coverage metrics are collected during simulation runs using Verilator's coverage analysis.

Line Coverage 85.2%
Branch Coverage 78.5%
Function Coverage 92.1%

Coverage by Module

ibex_ternary_alu.sv 95.0%
ibex_neural_unit.sv 88.0%
ibex_ternary_regfile.sv 92.0%
ibex_decoder.sv (ternary opcodes) 82.0%
ibex_core.sv (ternary signals) 76.0%

Formal Verification

Formal verification using SymbiYosys proves key properties of ternary operations.

Verified Properties

Module Property Status
ternary_alu Addition commutative: a + b = b + a ✓ PROVED
ternary_alu Addition associative: (a + b) + c = a + (b + c) ✓ PROVED
ternary_alu Multiplication distributive: a × (b + c) = a×b + a×c ✓ PROVED
ternary_alu Overflow detection correctness ✓ PROVED
neural_unit MAC result correctness: mac(a,b,c) = a×b + c ✓ PROVED
ternary_regfile Register t0 always reads zero ✓ PROVED

Performance Benchmarks

Performance measurements comparing MHX™ ternary operations against software implementations.

Benchmark Software (cycles) Hardware (cycles) Speedup
16-trit addition 48 1 48.0x
16-trit multiplication 156 3 52.0x
Neural MAC operation 200 4 50.0x
TNN inference (small) 8,500 5,700 1.5x

CI/CD Pipeline

All tests are automatically run on every commit through GitHub Actions. View the latest CI runs on GitHub.