Skip to content

RustSys verification plan

SYNTH-REQ-0801 Every netlist produced by the suites is checked by the independent synthesis checker (docs/specs/check/synth.md), which proves equivalence of the netlist and the RTL under SYNTH-REQ-0201 and the state correspondence of SYNTH-REQ-0603.

SYNTH-REQ-0802 Suites (verification/suites/synth/): - corpus: hand-written RTL modules typical of digital designs (counters, state machines, FIFOs, arithmetic units, arbiters, encoders, CRC and LFSR generators, shifters, register files, pipelines using packages, structures, enumerations and generate constructs), synthesized with each synthetic library of rustsys-fixtures; - random: seeded random RTL modules produced by rustsys-fixtures covering operators, widths, signedness, procedural control flow and registers; - known-answer: combinational modules with at most 16 inputs whose netlists are compared with exhaustive truth tables computed by an f64-free scalar evaluator of the RTL; - metamorphic: resynthesis of a synthesized netlist is equivalent to it (idempotence up to equivalence); renaming a module port does not change the cell counts; reordering independent module items does not change the netlist function; - defects: planted defects in synthesized netlists (rustsys-defects) must be reported by the checker, one case per defect class.

SYNTH-REQ-0803 Unit tests cover every requirement of this specification that is observable at the crate API, and cite the requirement IDs.