Here you will find tutorials that will help you use the Constrained Random Verification (CRV) tools offered in chiselverify.

Constrained Random Verification is a very powerful tool that allows a verification engineer to automate the testing process by defining constraints that direct randomized inputs to a DUT, allowing one to obtain more interesting results than with purely uniform randomness. This can then be adapted in order to create a Coverage-Based mutational workflow, which means that coverage outputs are used in order to update constraints until a certain coverage amount is attained.

CRV needs two main elements in order to function:

• Constraint Satisfaction Problem (CSP) Solver: Back-end of the CRV tool, solves an equation defined by a given set of constraints and random variables.
• Constraint Programming Language: Front-end of the CRV tool, allows for the user to define constraints and random variables.

ChiselVerify's CRV uses the JaCoP CSP Solver as a back-end.

Our CRV library offers a specialized constraint definition language as a front-end. Constraints are defined as a type of RandObj. Each RandObj represents a Constraint Satisfaction Problem and needs to be solvable in order to generate random outputs.

There are 3 main elements in the Constraint Programming Language:

• Random Objects
• Random Variables
• Constraints

Here is an example of how to use to CRV tools to define constraints:

class Packet extends RandObj(new Model(3)) {
    val idx = new Randc("idx", 0, 10)
    val size = new Rand("size", 1, 100)
    val len = new Rand("len", 1, 100)
    val payload: Array[Rand] = Array.tabulate(11)(
        new Rand(s"byte[$_]", 1, 100)
    )

    //Example Constraint with operations
    val single = payload(0) #= (len #- size)
	
    //Example conditional constraint
    val conditional = IfCon(len #= 1) {
        payload.size #= 3
    } ElseC {
        payload.size #= 10
    }
    val idxConst = idx #< payload.size
}
//Instantiate RandObj
val pckt = new Packet

//Check that the constraints were solvable
assert(pckt.randomize)

// [...] ChiselTest boilerplate [...]

//Example use of random variables in a DUT
while(pckt.randomize && /*Coverage isn't 80%*/) {
    dut.portA.poke(
        pckt.payload(pckt.idx.value()).value()
    )

    // [...] Sample the coverage and update constraints
}

The Coverage and ChiselTest code was left out, since it is out of the scope of this tutorial.
Other usage examples can be found in src/test/scala/backends/jacopsrc/test/scala/verifyTests/crv/backends/jacop/.

Next topic: Random Objects or return home