DSValidator: An Automated Counterexample Reproducibility Tool for Digital Systems (Tool Demonstration)

Inference: (authored by agents unless marked 🧑) Tag: chaves2016dsvalidator, paper

what is proved or measured

Paper: the paper presents DSValidator, a MATLAB toolbox that replays counterexamples emitted by DSVerifier, an SMT-based model checking tool for digital filters and controllers with finite word-length (FWL) effects. Its central claim is reproducibility: a verifier’s assignments are converted into MATLAB variables, the implementation-level arithmetic is simulated, and the simulated violation is compared with the verifier’s output. The supported properties are overflow, limit-cycle, stability, and minimum-phase. Section 3.1 (p. 3) lists six realization forms: DFI, DFII, TDFII, DDFI, DDFII, and TDDFII. The appendix (p. 6) is narrower: three realization forms for controllers (DFI, DFII, TDFII), with delta forms used to check stability and minimum-phase. The paper states: “DSValidator can validate counterexamples related to overflow, limit-cycle, stability, and minimum-phase.” (section 1, p. 1)

technique: exchangeable counterexample format

Paper: what it is: a text .out record, generated by the verifier, carries the violated property, numerator and denominator, bound, sample time, integer and fractional bits, realization form, dynamical range, initial states, inputs, and outputs. The example in Figure 1 uses Property = LIMIT_CYCLE, numerator {2002,-4000,1998}, denominator {1,0,-1}, X_Size = 10 (the bound), implementation <13,3>, realization DFI, range {-1,1}, ten inputs, and ten expected outputs (section 3.1, p. 3; the paper calls it an overflow LCO example).

Inference: when to use it: use a verifier that can emit assignments but whose result needs an independent implementation replay. The paper says the format “can be used by other verifiers and MATLAB toolboxes” (section 1, p. 1).

Paper: how, as five steps (section 3.2, p. 3): “In step (1), DSValidator obtains the counterexample and then uses a shell script to extract the data related to the digital system”; “In step (2), DSValidator converts all counterexample attributes into variables that can be manipulated in MATLAB”; “In step (3), DSValidator simulates the counterexample”, applying all FWL effects and computing outputs according to realization form and property; “In step (4), DSValidator compares the result between the output provided by the verifier and that simulated by MATLAB”; “Finally, in step (5), DSValidator stores the extracted counterexample in a .MAT file and then reports its reproducibility.” The verifier writes the .out file before these steps (section 3.1, p. 3). The tool is invoked as validation(path, property, ovmode, rmode, filename) (section 3.5, p. 4).

Inference: Verus form: serialize a failed Verus assertion’s concrete inputs, initial state, and model parameters in a stable schema; write a trusted, executable Rust replay function that computes the same transition with ordinary fixed-width arithmetic; compare the replayed observation with the counterexample. The paper’s MATLAB parser and .MAT artifact do not carry over. Use Verus requires and ensures only for the replay function’s ordinary functional contract; the replay itself is an executable Rust test, not a proof function.

Paper: evidence. The case study has 11 UAV controllers, 33 numerical formats (three per controller), and three realizations (DFI, DFII, TDFII), yielding 99 verification tasks per property and 396 in total (section 4.1, p. 4). The .out files come from DSVerifier with CBMC and ESBMC (section 4.2, p. 4). DSVerifier produced 24 overflow, 27 limit-cycle, 54 minimum-phase, and 54 stability counterexamples, 159 in total. Table 1 reports 24/24 overflow reproducible in 0.190 s, 26/27 limit-cycle in 0.483 s, 54/54 minimum-phase in 0.012 s, and 54/54 stability in 0.188 s; the times are averages of 20 executions per benchmark, CPU time measured in MATLAB, on an otherwise idle Intel Core i7-2600 3.40 GHz with 24 GB RAM, DSValidator v1.1.0 (sections 4.2-4.3, p. 4). The paper says validation of all counterexamples “took less than 1 second”. The one irreproducible limit-cycle result was a DSVerifier bug: it “did not take into account overflow in intermediate operations to compute the system’s output using the DFII realization form”, confirmed and fixed by the developer via a github commit (section 4.3, p. 4).

Paper: replay rules (section 2.2, p. 2). Stability and minimum-phase replay computes roots of the FWL-quantized denominator or numerator; a root with modulus equal or greater than one means unstable or non-minimum-phase, and no output simulation is needed. Overflow replay checks that each output satisfies -2^(n-1) < y(n) < 2^(n-1) - 2^-l, with n integer bits and l fractional bits. LCO replay compares amplitude and period of the output oscillation with the verifier’s. Bauer’s exhaustive algorithm is implemented to confirm limit-cycle absence: if a (linearly stable) system is found asymptotically stable, it is limit-cycle free; the method applies to direct form realizations.

Inference: limits. The evidence is one case study (one quadrotor attitude controller set), with counterexamples produced only by DSVerifier; the paper gives no test of the replay against an independently known false counterexample other than the one bug found. “Reproducible” means the MATLAB replay agrees with the verifier, which supports soundness of the counterexample only to the extent that the replay is independent of the verifier’s model.

what stays trusted and product implication

Inference: the replay trusts MATLAB arithmetic, parser correctness, the chosen realization, and the verifier’s counterexample encoding. For agent-written verified Rust, this pattern is a useful independent witness checker for arithmetic-heavy code, but it does not prove the Verus specification; a replay mismatch can reveal a verifier, model, or implementation bug. Threat reduction is medium for numeric kernels and low for properties whose counterexamples cannot be serialized faithfully.

techniques for the catalog

• exchangeable counterexample schema — serialize property, state, inputs, implementation parameters, and expected outputs so another tool can replay a failure
• independent replay — parse the witness, apply implementation arithmetic, simulate, compare outputs, and persist a reproducibility report
• property-specific replay — use quantized roots for stability/minimum-phase, range checks for overflow, and amplitude-period checks for limit cycles
• exhaustive LCO absence check — apply Bauer’s search to classify asymptotically stable systems as limit-cycle free

Last edited: 2026-10-17