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

Inference: The paper presents a MATLAB toolbox that replays counterexamples emitted by DSVerifier, a bounded model checker for fixed-point digital filters and controllers. Its central claim is reproducibility: a verifier’s assignments are converted into concrete 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. The implementation supports six realization forms: DFI, DFII, TDFII, DDFI, DDFII, and TDDFII. The paper states: “DSValidator can validate counterexamples related to overflow, limit-cycle, stability, and minimum-phase.” (section 1, p. 1)

technique: exchangeable counterexample format

Inference: What it is: a text .out record carries property, numerator and denominator, bound, sample time, integer/fractional bits, realization, 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, implementation <13,3>, realization DFI, range {-1,1}, ten inputs, and ten expected outputs (section 3.1, p. 3).

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)

Inference: How: (1) have the verifier write an .out file; (2) extract the fields with the shell script; (3) parse them into MATLAB variables; (4) apply finite-word-length quantization and fixed-point operations; (5) simulate the selected realization and property; (6) compare simulated and verifier outputs; (7) save the record in .MAT and report reproducibility. These are the paper’s five validation steps: “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”; “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.” (section 3.2, p. 4)

Inference: Verus form: Inference: 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.

Inference: Evidence and limits: the case study has 11 UAV controllers, 33 numerical formats (three per controller), and three realizations, yielding 99 verification tasks per property and 396 total (section 4.1, p. 5). DSVerifier produced 24 overflow, 27 limit-cycle, 54 minimum-phase, and 54 stability counterexamples, 159 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; these are averages of 20 executions on an otherwise idle Intel Core i7-2600 3.40 GHz with 24 GB RAM (sections 4.2–4.3, pp. 5–6). The one irreproducible limit-cycle result exposed a DSVerifier DFII bug: intermediate-operation overflow had been omitted, and the developer fixed it (section 4.3, p. 6). Stability and minimum-phase replay roots are computed after FWL quantization; a root modulus at least one means failure. Overflow replay checks -2^(n-1) < y(n) < 2^(n-1)-2^-l. LCO replay compares amplitude and period, while Bauer’s exhaustive method is used to establish absence of limit cycles for asymptotically stable systems (section 2.2, pp. 2–3).

what stays trusted and product implication

Inference: The replay trusts MATLAB arithmetic, parser correctness, the chosen realization, and the verifier’s counterexample encoding. Inference: 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. Inference: 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 Checked 2026-10-15 against paper chaves2016dsvalidator: full comparison completed; metadata and unsupported claims reviewed; experiments not reproduced

Last edited: 2026-10-15