Skip to content

Target real RISC-V cores for exhaustive XIF verification #7

@metasmile

Description

@metasmile

The current ev constraint model and fixtures are toy examples. The tool must validate itself against actual production RISC-V cores to become a complete verification platform.

Goal

Establish ev as a self-sufficient verification tool by modeling, testing, and exhaustively verifying the custom extension interfaces of at least two top-tier RISC-V cores.

Candidates

  • CVA6 (OpenHW Group) — XIF interface, documented, production-grade. Already name-checked in sample.xif.yaml target field but never actually modeled.
  • Ibex (lowRISC) — simpler ALU extension, well-documented, good for demonstrating the value of exhaustive over random.

Deliverables per core

  1. XIF / extension interface spec analyzed and translated into ev constraint YAML
  2. Realistic fixture files (e.g., rv32i_vector_mac.xif.yaml, simple_alu_ext.xif.yaml)
  3. ev check passes with deterministic, auditable results
  4. Any coverage gaps vs. existing random-simulation approaches documented
  5. Results shared with the corresponding open-source core community

This is self-contained

SSCCS and Nexus do not need to change for this. ev produces Facts as JSON output. When the verification results are valid and complete, Nexus consumes them naturally through the existing ingestion pipeline (Facts in object storage → sync worker → knowledge graph). No cross-project coordination required.

Stacking order

  1. Evaluate current constraint/projector gaps against real XIF specs
  2. Implement missing constraint/projector types
  3. Create CVA6 and/or Ibex fixture files
  4. Run, validate, document

Metadata

Metadata

Assignees

No one assigned

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions