Logic simplification and analysis tools

This crate provides tools for logic optimization, synthesis, technology mapping and analysis. Our goal is to provide an easy-to-use library, and improve its quality over time to match industrial tools.

Quaigh provides a command line tool, that can be installed using Cargo: cargo install quaigh.

To show available commands:

quaigh help

The atpg command performs automatic test pattern generation, to create test vectors for a design.

quaigh atpg mydesign.bench -o atpg.test

The check-equivalence command performs bounded equivalence checking to confirm that a design's functionality is preserved after transformations.

quaigh equiv mydesign.bench optimized.bench

The optimize command performs logic optimization. At the moment, logic optimization is far from state of the art: for production designs, you should generally stick to the tools included in Yosys.

quaigh opt mydesign.bench -o optimized.bench

Quaigh supports a subset of the Blif file format, as well as the simple Bench file format used by ISCAS benchmarks. Benchmarks can be downloaded here. More features will be added over time, such as technology mapping, operator optimization, ... The complete documentation is available on docs.rs.

The main datastructure, Network, is a typical Gate-Inverter-Graph representation of a logic circuit. Inverters are implicit, occupying just one bit in Signal. It supports many kinds of logic, and all can coexist in the same circuit:

• Complex gates such as Xor, Mux and Maj3 are all first class citizens;
• Flip-flops with enable and reset are represented directly.

In most logic optimization libraries (ABC, Mockturtle, ...), there are many different ways to represent logic, with separate datastructures: AIG, MIG, LUT, ... Depending on the circuit, one view or the other might be preferable. Taking advantage of them all may require splitting the circuit, making most operations much more complex. More generic netlists, like Yosys RTLIL, will allow all kind of logic gates in a single datastructure. Since they do not restrict the functions represented, they are difficult to work with directly for logic optimization.

Quaigh aims in-between. All algorithms share the same netlist representation, Network, but there are some limitations to make it easy to optimize:

• all gates have a single output, representing a single binary value,
• the gates are kept in topological order (a gate has an index higher than its inputs),
• names and design hierarchy are not represented.

For example, here is a full adder circuit:

let mut net = Network::new();
let i0 = net.add_input();
let i1 = net.add_input();
let i2 = net.add_input();
let carry = net.add(Gate::maj(i0, i1, i2));
let out = net.add(Gate::xor3(i0, i1, i2));
net.add_output(carry);
net.add_output(out);

Apart from the core datastructure, Quaigh has algorithms for logic optimization, simulation (including fault simulation) and test pattern generation. For optimization and equivalence checking, Quaigh relies on other packages as much as possible:

• Kissat (using rustsat) as a Sat solver,
• Highs (using good_lp) as an optimization solver.