This benchmark suite presented at the FAC'14 conference is a collection of device models with testbenches that are interesting for formal
circuit verification. Most circuits are written in plain spice, to maximize the
set of compatible simulators. We have verified that they work with gnucap-uf,
ngspice, spectre and xyce. Some circuits make use of verilog-a behavioural models.
These currently only work with gnucap-uf and spectre.
The circuits are ready for simulation and verification. We check some properties and some equivalences in the benchmakr suite. For details see the enclosed README files.