CRAVE

Tool

CRAVE is a constrained-randomization library used by the SystemC port of the UVM library. It provides an integrated interface to BDD and SAT solvers, but the cited DVCon paper reports limitations for complex RISCV-DV constraints, multicore parallelism, and native memory footprint of random variables.

First seen 5/25/2026

Last seen 7/2/2026

Evidence 15 chunks

Wiki v1

WIKI

Overview

CRAVE is described as a library used by the SystemC port of the UVM library for constrained randomization. The same source states that CRAVE provides an integrated interface to a set of Binary Decision Diagram (BDD) and Satisfiability (SAT) solvers. [CRAVE constrained-randomization role; CRAVE solver interface]

Use in SystemC verification

READ FULL ARTICLE →

NEIGHBORHOOD

No graph connections found for this entity yet. It may appear in future ingestion runs.

explore full graph →

RELATIONSHIPS

26 connections

SCV compares with → 100% 3e

CRAVE is experimentally compared to the SCV library in terms of constraint solving performance.

Generator ← part of 100% 2e

Generator is a class in CRAVE for standalone inline and incremental constraint specification.

Bubble Sort Input Generation evaluates → 100% 2e

CRAVE is evaluated for generating bubble sort inputs as a program input generation scenario.

Program Input Generation evaluates → 100% 2e

CRAVE is applied to program input generation for a CPU testbench.

SystemC uses → 100% 2e

CRAVE is designed for SystemC models as a verification environment.

Stimuli Generation implements → 95% 2e

CRAVE implements stimuli generation via constrained random verification.

Dynamic Constraint Management implements → 100% 2e

CRAVE implements dynamic constraint management, enabling enabling/disabling of constraints at runtime.

Inline Constraints implements → 100% 2e

CRAVE supports inline constraints that can be formulated and changed at runtime.

CRAVE: An Advanced Constrained Random Verification Environment for SystemC ← introduces 100% 2e

The paper introduces CRAVE as an advanced constrained random verification environment for SystemC.

Over-constraint Analysis implements → 100% 2e

CRAVE supports automatic debugging of unsatisfiable/over-constrained constraints.

Portfolio Constraint Solving implements → 100% 2e

CRAVE uses a portfolio approach combining BDD and SMT-based solvers for constraint solving.

BDD-based Constraint Solving implements → 100% 2e

CRAVE integrates BDD-based constraint-solving techniques.

SAT-based Constraint Solving implements → 100% 2e

CRAVE integrates SAT-based constraint-solving techniques.

SMT-based Constraint Solving implements → 100% 2e

CRAVE integrates SMT-based constraint-solving techniques.

metaSMT uses → 100% 2e

CRAVE uses metaSMT for implementing the constraint-solving backend.

Constrained Random Verification implements → 100% 2e

CRAVE implements Constrained Random Verification for SystemC models.

rand_vec<T> ← part of 100% 2e

rand_vec<T> is a template class in CRAVE for constrained randomization of vectors.

rand_obj ← part of 100% 2e

rand_obj is a base class provided by CRAVE for complex constrained random objects.

Simulation-based Equivalence Checking evaluates → 85% 1e

CRAVE is used to generate stimuli for simulation-based equivalence checking between SystemC models.

SAT Solving uses → 100% 1e

CRAVE provides an integrated interface to SAT solvers.

UVM-SystemC ← uses 100% 1e

The SystemC port of UVM relies on the CRAVE library for constrained randomization.

Incremental Constraint Specification implements → 100% 1e

CRAVE supports incremental constraint specification via the Generator class.

randv<T> ← part of 100% 1e

randv<T> is a core template class provided by CRAVE for random variables.

Five-Stage Pipeline CPU evaluates → 90% 1e

CRAVE is used to generate stimuli for a five-stage pipeline CPU model.

CISC CPU evaluates → 90% 1e

CRAVE is applied to verify a CISC CPU with 8 registers.

BDD-based Constraint Solving uses → 100% 1e

CRAVE provides an integrated interface to BDD solvers.

LINKED ENTITIES

2 links

SystemC used_with The evidence discusses CRAVE in the context of SystemC and states that SystemC and CRAVE do not offer multicore parallelism.

riscv-dv reported_limitation_with The evidence states that CRAVE cannot handle complex RISCV-DV constraints in the described context.

CITATIONS

7 sources

7 citations — click to expand

[1] CRAVE constrained-randomization role [PDF] Crafting a Million Instructions/Sec RISCV-DV - DVCon Proceedings

[2] CRAVE solver interface [PDF] Crafting a Million Instructions/Sec RISCV-DV - DVCon Proceedings

[3] SystemC UVM reliance on CRAVE [PDF] Crafting a Million Instructions/Sec RISCV-DV - DVCon Proceedings

[4] CRAVE wrapper-template random variables [PDF] Crafting a Million Instructions/Sec RISCV-DV - DVCon Proceedings

[5] Complex RISCV-DV constraint limitation [PDF] Crafting a Million Instructions/Sec RISCV-DV - DVCon Proceedings

[6] Multicore parallelism limitation [PDF] Crafting a Million Instructions/Sec RISCV-DV - DVCon Proceedings

[7] Native memory-footprint limitation [PDF] Crafting a Million Instructions/Sec RISCV-DV - DVCon Proceedings