Overview
Bubble Sort Input Generation refers to the stimulus-generation step in the CRAVE verification flow in which randomized input arrays are produced for a CPU testbench running a bubble sort program. The arrays serve as stimuli for a CISC CPU (8 registers, 32-bit data width, IA-32 instruction subset with load/store, arithmetic, jump, and halt instructions) that is modeled at three levels of abstraction (C++ ISA, SystemC TLM with OSCI TLM-2.0, and a SystemC RTL five-stage pipeline). CRAVE generates both the programs (instruction sequences) and their inputs, which are reused as stimuli across all three models. The inputs then drive a simulation-based equivalence-checking flow applied to models at different abstraction levels.
Constraints Applied to the Input
The input arrays are randomized under a concise set of constraints (Figure 9 of the source), grouped by purpose:
- Size constraints —
0 < data().size() && data().size() < 1024. Bounds the array length to fit in the CPU memory. - Memory fit / no collision with the loaded program —
start() + 4 * data().size() <= 1024. Ensures the array fits in memory and does not overlap the loaded program. - Per-element width constraint —
foreach(data, _i, data()[_i] <= 0x00FFFFFF). Restricts the bit-width of each element. - Near-monotonic constraint —
foreach(data, _i, data()[_i] <= data()[_i-1] + 5). Forces the array to be nearly non-increasing, which is a challenging case for bubble sort.
The authors emphasize that such a concise set of constraints would not have been expressible with the SCV library because SCV lacks support for dynamic data structures.
Generation Performance
The reported average generation time with CRAVE for the first 1000 arrays is approximately 90 seconds (≈0.09 s per array).
Tooling and Related Concept
CRAVE (an advanced constrained-random verification environment for SystemC) is the tool that performs this input generation. Its ability to specify dynamic constraints over dynamic data structures is what enables the bubble sort scenario to be expressed concisely, in contrast to SCV.