Skip to content

VERIFICATION.md

Latest commit

 

History

History
575 lines (464 loc) · 26.4 KB

VERIFICATION.md

File metadata and controls

575 lines (464 loc) · 26.4 KB
Raw

Z-Core Verification Documentation

Overview

This document describes the verification strategy, test coverage, and results for the Z-Core RISC-V processor.

Test Architecture

┌────────────────────────────────────────────────────────────────────────────┐
│                         Z-Core Test Environment                            │
│                                                                            │
│  ┌──────────────────────────────────────────────────────────────────────┐  │
│  │                    z_core_control_u_tb.sv                            │  │
│  │  ┌────────────────────────────────────────────────────────────────┐  │  │
│  │  │                    Test Orchestration                          │  │  │
│  │  │  - Program Loading (load_testN tasks)                          │  │  │
│  │  │  - CPU Reset Management                                        │  │  │
│  │  │  - Result Verification (check_reg, check_mem tasks)            │  │  │
│  │  │  - Pass/Fail Reporting                                         │  │  │
│  │  └────────────────────────────────────────────────────────────────┘  │  │
│  └──────────────────────────────────────────────────────────────────────┘  │
│                                    │                                       │
│                                    ▼                                       │
│  ┌──────────────────────────────────────────────────────────────────────┐  │
│  │                    Device Under Test (DUT)                           │  │
│  │  ┌────────────────────┐      AXI-Lite      ┌────────────────────┐    │  │
│  │  │  z_core_control_u  │◄──────────────────►│ axil_interconnect  │    │  │
│  │  │    (CPU Core)      │                    │                    │    │  │
│  │  └────────────────────┘                    └─────────┬──────────┘    │  │
│  │                                                      │               │  │
│  │                                          ┌───────────▼───────────┐   │  │
│  │                                          │   AXI-Lite Slaves     │   │  │
│  │                                          │ - Memory (64KB)       │   │  │
│  │                                          │ - UART (Wrapper)      │   │  │
│  │                                          │ - GPIO (Wrapper)      │   │  │
│  │                                          │ - Timer (Wrapper)     │   │  │
│  │                                          └───────────────────────┘   │  │
│  └──────────────────────────────────────────────────────────────────────┘  │
│                                                                            │
│                                                                            │
└────────────────────────────────────────────────────────────────────────────┘

Test Suites

Test 1: Arithmetic Operations

Purpose: Verify basic integer arithmetic

Instruction Test Case Expected
ADDI x2 = 0 + 10 10
ADDI x3 = 0 + 7 7
ADD x4 = x2 + x3 17
SUB x5 = x2 - x3 3
ADDI x6 = 0 + (-5) -5
ADD x7 = x4 + x6 12

Test 2: Logical Operations

Purpose: Verify bitwise operations

Instruction Test Case Expected
AND 0xFF & 0x0F 0x0F
OR 0xFF | 0x0F 0xFF
XOR 0xFF ^ 0x0F 0xF0
ANDI 0xFF & 0x55 0x55
ORI 0x00 | 0xAA 0xAA
XORI 0xAA ^ 0xFF 0x55

Test 3: Shift Operations

Purpose: Verify all shift variants

Instruction Test Case Expected
SLLI 1 << 4 16
SLLI 1 << 8 256
SRLI 0xFFFFFFFF >>> 24 0xFF
SRAI 0xFFFFFFFF >> 24 0xFFFFFFFF
SLL 1 << 8 (reg) 256
SRL 0xFFFFFFFF >>> 8 (reg) 0x00FFFFFF
SRA 0xFFFFFFFF >> 8 (reg) 0xFFFFFFFF

Test 4: Memory Operations

Purpose: Verify load/store functionality via AXI

Instruction Test Case Expected
SW Store 42 to addr 256 mem[256] = 42
SW Store 100 to addr 260 mem[260] = 100
LW Load from addr 256 x4 = 42
LW Load from addr 260 x5 = 100
SW Store 142 to addr 264 mem[264] = 142

Test 5: Compare Operations

Purpose: Verify signed and unsigned comparisons

Instruction Test Case Expected
SLT 10 < 20 (signed) 1
SLT 20 < 10 (signed) 0
SLTI 10 < 15 (signed imm) 1
SLTI 10 < 5 (signed imm) 0
SLTU 0xFFFFFFFF < 10 0
SLTIU 10 < 100 (unsigned imm) 1
SLTIU 0xFFFFFFFF < 1 0
SLTU 10 < 0xFFFFFFFF 1

Test 6: Upper Immediate

Purpose: Verify LUI and AUIPC

Instruction Test Case Expected
LUI Load 0x12345 << 12 0x12345000
ADDI Add lower bits 0x12345678
AUIPC PC + 0 8 (instruction address)
LUI Load 0xFFFFF << 12 0xFFFFF000

Test 7: Integration (Fibonacci)

Purpose: Verify multi-instruction sequences

Computes Fibonacci sequence: 1, 1, 2, 3, 5, 8, 13, 21
Stores result (21) to memory

Test 8: Branch Operations

Purpose: Verify all conditional branches

Instruction Condition Branch Taken?
BEQ 5 == 5 Yes
BNE 5 != 10 Yes
BLT 5 < 10 (signed) Yes
BGE 10 >= 5 (signed) Yes
BLTU 5 < 0xFFFFFFFF Yes
BGEU 0xFFFFFFFF >= 5 Yes
BEQ 5 == 10 No
BNE 5 != 5 No

Test 9: Jump Operations

Purpose: Verify JAL and JALR

Instruction Test Case Verification
JAL Jump +12, save return x1 = PC+4
JALR Jump to reg x4 = PC+4
JALR+offset Jump to reg+imm x7 = PC+4

Test 10: Backward Branch (Loop)

Purpose: Verify negative branch offsets

// Equivalent C code:
int counter = 0, sum = 0;
while (counter < 5) {
    sum += counter;
    counter++;
}
// Result: sum = 0+1+2+3+4 = 10

Test 11: IO Access (UART/GPIO)

Purpose: Verify AXI-Lite Interconnect routing to IO modules

Instruction Test Case Expected
SW Write to UART Base (0x0400_0000) OKAY Response
LW Read from UART Base Data = 0
SW Write to GPIO Base (0x0400_1000) OKAY Response
LW Read from GPIO Base Data = 0

Test 12: GPIO Bidirectional

Purpose: Verify GPIO bidirectional functionality via AXI-Lite

This test verifies that the GPIO module correctly handles:

  1. Output Mode: CPU configures pins as outputs and drives data
  2. Input Mode: CPU configures pins as inputs and reads external data
Step Action Expected Result
1 Write 0xFFFFFFFF to DIR (0x08) GPIO[31:0] = Output mode
2 Write 0xFF to DATA (0x00) gpio[31:0] = 0x000000FF
3 Write 0x00 to DIR (0x08) GPIO[31:0] = Input mode
4 TB drives 0xCAFEBABE gpio[31:0] = 0xCAFEBABE
5 Read DATA (0x00) x6 = 0xCAFEBABE

Test 13: Byte/Halfword Load/Store

Purpose: Verify LB, LH, LBU, LHU, SB, SH instructions

This test verifies sub-word memory access with proper sign/zero extension:

Instruction Offset Source Data Expected Result
LB 0 0xEF 0xFFFFFFEF (sign-extend)
LBU 0 0xEF 0x000000EF (zero-extend)
LH 0 0xBEEF 0xFFFFBEEF (sign-extend)
LHU 0 0xBEEF 0x0000BEEF (zero-extend)
LB 1 0xBE 0xFFFFFFBE (sign-extend)
LBU 2 0xAD 0x000000AD (zero-extend)
LH 2 0xDEAD 0xFFFFDEAD (sign-extend)
LHU 2 0xDEAD 0x0000DEAD (zero-extend)

Test 14: UART Loopback

Purpose: Verify UART TX and RX functionality via loopback

This test verifies that the UART module can transmit a byte and receive it back (either via external loopback or testbench connection):

  1. Write to TX: CPU writes 0x55 to UART TX_DATA register.
  2. Transmission: UART transmits the byte (start bit + 8 data bits + stop bit).
  3. Loopback: The transmitted signal is fed back to the RX pin.
  4. Reception: UART receives the byte and updates RX_DATA and STATUS registers.
  5. Verification: CPU checks STATUS (TX_EMPTY=1, RX_VALID=1) and RX_DATA (0x55).

Test 15: RAW Hazard Stress

Purpose: Stress test the forwarding unit with long chains of dependencies

ADDI x1, x0, 1
ADD x2, x1, x1  (Forward from WB or EX)
ADD x3, x2, x2
...
SLT x15, x13, x12

Test 16: Full ALU Coverage

Purpose: Verify all ALU operations including corner cases

  • Verify SRAI, SLTI, SLTIU
  • Verify OR, XOR, SLL, SRL, SRA, SLT, SLTU
  • Verify store-load with ALU results

Test 17: Nested Loops

Purpose: Verify complex control flow and register persistence

for (i=0; i<3; i++) {
    for (j=0; j<3; j++) {
        sum += i + j;
    }
}

Test 18: Memory Access Pattern Stress

Purpose: extensive verification of byte/halfword loads and stores

  • Writes sequences of bytes/halfwords
  • Reads them back with mixed signed/unsigned instructions (LB, LBU, LH, LHU)
  • Specific test for Store-Load hazards (Store followed immediately by Load to same address)

Test 19: Mixed Instruction Stress

Purpose: Randomized-style mix of all instruction types to catch interaction bugs

  • Interleaves ALU, Memory, Branch, and Jump instructions
  • Verifies LUI + ADDI large constant generation
  • Verifies JAL / JALR return address linking in complex flow

Test 20: Multiplication (M Extension)

Purpose: Verify MUL, MULH, MULHSU, MULHU instructions

Instruction Test Case Expected
MUL 6 × 7 42
MUL 100 × 200 20000
MULH 0x7FFFFFFF × 2 0 (upper 32 of signed)
MULHU 0x80000000 × 2 1 (upper 32 of unsigned)
MULHSU -1 × 0x80000000 0x7FFFFFFF

Test 21: Division (M Extension)

Purpose: Verify DIV, DIVU, REM, REMU instructions

Instruction Test Case Expected
DIVU 100 / 7 14
REMU 100 % 7 2
DIV -100 / 7 -14
REM -100 % 7 -2
DIVU 1000000 / 1000 1000
DIVU 5 / 10 0

Test 22: Division Forwarding

Purpose: Verify data forwarding works with division inputs

Tests three forwarding scenarios:

  1. ADD → DIVU: Division immediately after ALU operation
  2. MUL → DIVU: Division immediately after multiplication
  3. DIVU → DIVU: Back-to-back divisions using previous result

Test 23: M Extension + Control Flow

Purpose: Comprehensive stress test combining MUL, DIV, branches, and jumps

Step Operations Verification
1 MUL x4 = 6×7 x4 = 42
2 BLT (40 < 42?) Branch taken
3 DIVU x6 = 42/3 x6 = 14 (forwarding)
4 BEQ (x6 == 14?) Branch taken
5 JAL to subroutine x21 = return addr
6 MUL x8 = 14×7 (in sub) x8 = 98
7 JALR return Jump back
8 DIVU x9 = 98/7 x9 = 14

Test 24: Cache Locality Exploitation (Instruction Cache)

Purpose: Exercise the instruction cache with tight loops and nested control flow to validate high cache-hit behavior while preserving architectural correctness.

  • Runs multiple short loops designed to remain in a small hot working set.
  • Verifies final register/memory results and prints cache performance counters.

Test 25: I-Cache Conflict Miss Thrash (Direct-Mapped)

Purpose: Stress the instruction cache’s direct-mapped behavior by alternating execution between two hot code regions that intentionally alias to the same cache indices (separated by 0x400 bytes).

  • Validates that control flow remains correct under heavy conflict misses (correctness first).
  • Helps catch tag/index or valid-bit corner cases that don’t show up in pure-locality loops.

Test 26: I-Cache Conflict Miss Thrash (Direct-Mapped)

Purpose: Squeezee the pipeline as much as possible by exploiting instruction locallity. This locallity enables a throughput of one intruction per cycle.

Test 27: Correctness of Timer

Purpose: Verify the correctness of the timer module. Controls timer overflow and underflow.

Test 28: Correctness of External Counter Timer Mode

Purpose: Verify the correctness of the external counter timer mode.

Test 29: CSR Read/Write Operations (Zicsr)

Purpose: Verify all six CSR instructions with the mscratch register.

Instruction Test Case Expected
CSRRW Write 0, read back old value = 0 (reset)
CSRRW Write 0x42 old value = 0, mscratch = 0x42
CSRRS Read (rs1=x0, no set) 0x42
CSRRS Set bits 0xF old = 0x42, new = 0x4F
CSRRC Clear bits 0xF old = 0x4F, new = 0x40
CSRRWI Write zimm=0x1F old = 0x40, new = 0x1F
CSRRSI Set zimm=0 (no write) 0x1F
CSRRCI Clear bit 4 old = 0x1F, new = 0x0F

Test 30: Synchronous Exceptions

Purpose: Verify ECALL, EBREAK, and illegal instruction exception handling.

Exception mcause mepc mtval
ECALL 11 PC of ECALL 0
EBREAK 3 PC of EBREAK 0
Illegal (0xFFFFFFFF) 2 PC of insn 0xFFFFFFFF

Trap handler reads mcause/mepc/mtval, bumps mepc+4, stores results, and returns via MRET.

Test 31: Timer Compare-Match Interrupt

Purpose: Verify timer interrupt with MRET return.

  1. Configure timer with timecmp = 20, enable timer + IRQ.
  2. Spin-loop waiting for handler to set flag.
  3. Handler reads mcause, clears timer, sets flag, MRET.
  4. Verify mcause = 0x80000007 (Machine Timer Interrupt).

Test 32: Timer IRQ During Branch-Predicted Loop

Purpose: Verify interrupt handling during actively predicted branch loop.

A tight branch loop (50 iterations summing x10) runs while a timer is configured to fire mid-loop. The branch predictor trains on the loop, so when the timer fires, the interrupt must be deferred correctly during any in-progress misprediction flush cycles. After the handler clears the timer and returns via MRET, the loop must complete with the correct sum.

Check Expected
x10 (sum) 50
x11 (counter) 50
x20 (IRQ flag) 1
mem[256] 50
mem[260] 1

Test 33: Exception at Mispredicted Branch Target

Purpose: Verify trap priority when an exception occurs at a mispredicted branch target.

Three forward branches (cold predictor, likely mispredicted-not-taken) each jump to an exception-causing instruction: ECALL, EBREAK, and illegal instruction respectively. Validates that:

  • Synchronous exceptions take priority over misprediction flushes.
  • mepc correctly points to the faulting instruction.
  • MRET returns execution to the instruction after the exception.
Exception mcause mepc (stored as mepc+4)
ECALL at 0x28 11 0x2C
EBREAK at 0x48 3 0x4C
Illegal at 0x68 2 0x6C

Test 34: MRET Into Branch With Predictor State

Purpose: Verify MRET flush interaction with branch prediction.

A loop body contains an ECALL. The handler skips past the ECALL by writing mepc+4, which lands on the loop-back branch (BLT). This tests:

  • MRET flush (mret_in_ex in flush) does not conflict with subsequent branch prediction.
  • The branch predictor's trained/stale state from before the exception does not cause incorrect behavior.
  • The loop completes correctly after 5 iterations (5 ECALLs handled).
Check Expected
x10 (counter) 5
x20 (exception count) 5
mem[256] 5
mem[260] 5

Test 35-44: Data Cache Stress Tests

Purpose: Comprehensive verification of the 2-way set-associative write-back data cache.

Test Focus Description
35: Cache Round-Trip Hit semantics Write/read of 4 distinct addresses mapped to different sets, verifying 1-cycle hits.
36: Cache Way Conflict Associativity Reads 3 addresses aliasing to the same set to trigger way conflict, forcing LRU replacement.
37: Strided Cache Sweep Hit tracking Sweeps 8 addresses forcing an initial miss followed by a cache hit. Tests dcache_hit_pulse.
38: Hot Loop (I$+D$) System Locality Deep loop execution testing concurrent instruction cache and data cache hits without pipeline stalls.
39: Dirty-Eviction Writebacks Write-allocates lines and then forces eviction, verifying that dirty victim data is successfully written to backing RAM.
40: RMW Hit Storm Hit sustained throughput Rapid Load-Add-Store sequences at the same address, keeping the pipeline at high throughput (1 cycle load/store hits).
41: Load-Use LW→ADD Load-use + warm D$ 2-iteration loop: iter 1 warms I$ and D$; iter 2 runs LW→ADD back-to-back with sentinel x3=99. Stall must fire or x4/x5 read the sentinel instead of the loaded value (42 / 84).
42: Load-Use LB→ADDI Byte load-use Same loop structure as Test 41 with sign-extending LB→ADDI. Sentinel x4=5 makes a broken stall produce x5=6 instead of 0 (x4=-1 from 0xFF).
43: Load-Use LW→SW Load-to-store 2-iteration loop: LW loads 77, immediately followed by SW of the same register. On the warm iter, the store must use the forwarded load result or mem[0x304] stays 0.
44: Load-Use Dual D$ Hit Stale-data guard 2-iteration loop with two back-to-back D$ hits per iter (SW x7 then LW/ADDI twice). Alternating cached values (2 then 1) catch stale data_cache_data_out forwarding (x4/x6 would be 12 instead of 11).

Instruction Coverage

RV32IM Base Integer Instructions

Category Instructions Tested Coverage
Arithmetic ADD, SUB, ADDI Yes 100%
Logical AND, OR, XOR, ANDI, ORI, XORI Yes 100%
Shifts SLL, SRL, SRA, SLLI, SRLI, SRAI Yes 100%
Compare SLT, SLTU, SLTI, SLTIU Yes 100%
Branch BEQ, BNE, BLT, BGE, BLTU, BGEU Yes 100%
Jump JAL, JALR Yes 100%
Upper Imm LUI, AUIPC Yes 100%
Load LW, LB, LH, LBU, LHU Yes 100%
Store SW, SB, SH Yes 100%
M Extension MUL, MULH, MULHSU, MULHU Yes 100%
M Extension DIV, DIVU, REM, REMU Yes 100%
Zicsr CSRRW, CSRRS, CSRRC, CSRRWI, CSRRSI, CSRRCI Yes 100%
System ECALL, EBREAK, MRET Yes 100%

Test Flow Diagram

                    ┌─────────────┐
                    │    Start    │
                    └──────┬──────┘
                           │
              ┌────────────▼────────────┐
              │  Initialize Testbench   │
              │  - Create VCD dump      │
              │  - Setup clock          │
              └────────────┬────────────┘
                           │
         ┌─────────────────▼─────────────────┐
         │          For each test:           │
         │  ┌─────────────────────────────┐  │
         │  │  1. Load program to memory  │  │
         │  │  2. Reset CPU               │  │
         │  │  3. Wait for execution      │  │
         │  │  4. Check register values   │  │
         │  │  5. Check memory values     │  │
         │  │  6. Record pass/fail        │  │
         │  └─────────────────────────────┘  │
         └─────────────────┬─────────────────┘
                           │
              ┌────────────▼────────────┐
              │   Print Test Summary    │
              │   - Total tests         │
              │   - Passed/Failed       │
              └────────────┬────────────┘
                           │
                    ┌──────▼──────┐
                    │    End      │
                    └─────────────┘

Running Tests

Prerequisites

  • Icarus Verilog (iverilog) v11.0+
  • GTKWave (optional, for waveform viewing)

Commands

# Compile testbench
iverilog -g2012 -o sim/z_core_control_u_tb.vvp tb/z_core_control_u_tb.sv

# Run simulation
vvp sim/z_core_control_u_tb.vvp

# View waveforms
gtkwave sim/z_core_control_u_tb.vcd

Trap regression (exceptions and interrupts)

A dedicated trap-focused testbench (z_core_trap_tb.sv) exercises exceptions (ECALL, EBREAK, illegal instruction) and interrupts (MSI, MTI, MEI), plus masking, priority, and back-to-back stress. Use it for fast CI on trap-related changes.

Recipe Command Use case
Quick (trap only) make run TB_FILE=z_core_trap_tb.sv CI on CSR/trap RTL; ~25 checks, ~45k cycles
Full (control + trap) Run control TB then trap TB (see below) Full regression including ISA + traps

From the tb/ directory:

# Quick: trap regression only
make run TB_FILE=z_core_trap_tb.sv

# Full: main control TB then trap TB
make run TB_FILE=z_core_control_u_tb.sv
make run TB_FILE=z_core_trap_tb.sv

Use SIM=iverilog or SIM=questa if needed (e.g. make run TB_FILE=z_core_trap_tb.sv SIM=iverilog). See doc/EXCEPTIONS_AND_INTERRUPTS.md for trap coverage and design decisions.

Expected Output

╔═══════════════════════════════════════════════════════════╗
║           Z-Core RISC-V Processor Test Suite              ║
║                  RV32IM Instruction Set                   ║
╚═══════════════════════════════════════════════════════════╝

--- Loading Test 1: Arithmetic Operations ---
=== Test 1 Results: Arithmetic ===
  [PASS] ADDI x2, x0, 10: x2 = 10
  [PASS] ADD x4, x2, x3: x4 = 17
  ...

╔═══════════════════════════════════════════════════════════╗
║                    TEST SUMMARY                           ║
╠═══════════════════════════════════════════════════════════╣
║  Total Tests:  218                                        ║
║  Passed:       218                                        ║
║  Failed:        0                                         ║
╠═══════════════════════════════════════════════════════════╣
║         ✓ ALL TESTS PASSED SUCCESSFULLY ✓                 ║
╚═══════════════════════════════════════════════════════════╝

Waveform Analysis

Key signals to observe in GTKWave:

Signal Description
uut.PC Program Counter
uut.IR Instruction Register
uut.state FSM State (one-hot)
axil_arvalid/arready AXI Read handshake
axil_awvalid/awready AXI Write handshake
uut.reg_file.reg_r*_q Register values

RISCOF Compliance

Z-Core has passed all official RISCOF architectural tests for the RV32IM ISA.

Test Suite Status Tests
RV32IM Base Integer (I) All Passed 48
RV32M Multiply/Divide (M) All Passed 45
Zicsr (Privilege) All Passed 16
Total Compliance Tests All Passed 109

Extended Coverage Tests

In addition to the official RISCOF tests, Z-Core has been validated with 45 extended coverage tests generated by riscv_ctg (RISC-V Compliance Test Generator). These tests provide additional coverage for corner cases.

Test Suite Status
Generated RV32IM Tests All Passed

Note: The RISCOF verification infrastructure is maintained in a separate riscof/ directory (not included in the main repository). See the RISCOF directory's README for setup and usage instructions.

Future Verification Plans

  1. RISC-V official compliance tests (RISCOF)
  2. Run full RISCOF test suite for RV32IM
  3. Extended coverage tests (riscv_ctg)
  4. Full Zicsr extension and Privilege suite compliance
  5. Formal verification of critical paths and corner cases