Bit Operators in SCV Constraints

Background

The SystemC Verification (SCV) Library provides constraint-based randomization for SystemC models. Internally, a constraint is represented by its characteristic function, which is true for all solutions of the constraint, and the characteristic function is stored as a reduced, ordered Binary Decision Diagram (BDD). The BDD package CUDD is used by the SCV library for this representation. Internally, an expression is held in the class scv_expression as an expression tree whose leaf nodes are variables or constants and whose non-terminal nodes are marked with operators. The constraint solver operates on individual bits when solving constraints.

Operator Support in the Original SCV Constraint Solver

The operators supported by the original SCV constraint solver were limited to:

Arithmetic operators: +, -, *
Relational operators: ==, !=, >, >=, <, <=
Logical operators: !, &&, ||

Bit operators were not part of this set. Because the SCV constraint solver works on individual bits, each bit operator has to be mapped to the corresponding BDD synthesis operations; for a bitwise AND, for example, the resulting bit vector is computed by the BDD-AND operation applied to each bit of the two input vectors. Several special cases (different vector lengths, different data types, and similar) must also be taken into account.

Bit Operators Added by the Improvements

The paper Improvements for Constraint Solving in the SystemC Verification Library addresses this gap by implementing the following bit operators so that verification engineers can write simpler and more compact constraints:

Bitwise and: a() & b()
Bitwise or: a() | b()
Bitwise not: ~a()
Bit-select: a()[i] for constant i
Slice-select: a().range(x, y) for constant x and y

According to the authors, "bit operators are very important for the verification engineer during the specification of constraints. Bit operators allow for simpler and more compact formulations of complex constraints."

Implementation

The implementation was carried out in the scv_expression class:

The corresponding operators were overloaded.
New member functions were added to support the new operations.

Because the SCV library stores the internal representation of constraint expressions as an expression tree inside scv_expression, and constructs BDDs from that tree, overloading these operators in scv_expression is what makes the new bitwise and selection operations available inside the SCV_CONSTRAINT() macro.

Related Concepts

The paper introduces this concept as one of two main improvements to the SCV library; the second improvement is guaranteeing a uniform distribution of constraint solutions, which requires correcting the per-node probabilities computed during a pre-processing weighting traversal (the original solver only weights the initial BDD once and therefore fails to keep probabilities uniform after simplifications such as fixing variables to certain values).
scv_expression is the code artifact that implements the overloaded operators and new member functions that make bit operators usable inside SCV constraints.