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 9/27/2026

Evidence 16 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

36 connections

SystemC uses → 100% 3e

The syntax of CRAVE is designed to fit with SystemC, implying integration and use alongside SystemC models.

SCV compares with → 100% 3e

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

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.

BDD-based Constraint Solving uses → 100% 2e

The text states BDD-based techniques have been integrated into CRAVE’s solver portfolio, indicating use of this technique.

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_obj ← part of 100% 2e

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

rand_vec<T> ← part of 100% 2e

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

Bubble Sort Input Generation evaluates → 100% 2e

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

Generator ← part of 100% 2e

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

Program Input Generation evaluates → 100% 2e

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

accellera-official/crave part of → 90% 1e

The text points to the Accellera GitHub location for CRAVE, implying the repository hosts the CRAVE codebase.

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.

Simulation-based Equivalence Checking evaluates → 85% 1e

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

Constrained random stimuli generation implements → 98% 1e

The project describes CRAVE as a library specifically for constrained random stimuli generation, indicating it implements this technique.

Constraint specification API ← part of 90% 1e

A new API for specifying random variables/objects is presented as a feature of CRAVE, indicating it is a component of the tool.

Dynamic constraints implements → 95% 1e

CRAVE allows run-time control of constraints, which corresponds to implementing dynamic constraints.

Inline constraints implements → 95% 1e

The feature list states inline constraints can be formulated and changed at run-time, indicating implementation within CRAVE.

Parallel constraint-solving implements → 90% 1e

Parallel constraint solving is listed as a feature of CRAVE, implying the tool implements this technique.

SAT/SMT-based constraint solving uses → 95% 1e

SAT/SMT-based techniques are integrated in CRAVE’s constraint solving, showing use of these methods.

Portfolio approach for constraint solving uses → 95% 1e

CRAVE employs a portfolio of techniques to speed up constraint solution generation, indicating use of a portfolio approach.

Verification Working Group (VWG) authored by → 85% 1e

The passage credits VWG with further development of CRAVE, indicating authorship/maintainership by this organization.

Accellera Systems Initiative published by → 85% 1e

CRAVE is hosted on the official Accellera GitHub, indicating publication under the Accellera Systems Initiative umbrella.

SAT Solving uses → 100% 1e

CRAVE provides an integrated interface to SAT 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