Software Projects

Boolean logic in all of its usual shapes — formulas, CNF and DNF, BDDs, hierarchical circuits and flat netlists, quantified or not — and one pipeline connecting them, so a circuit written to be read by a person ends up in a form a SAT or QBF solver will take. The base package everything else here is built on.

An SMT solver for quantifier-free integer arithmetic, by eager bit-blasting: the arithmetic becomes circuitry and a SAT solver does the rest, with no theory-propagation loop anywhere. Beyond satisfiability it enumerates every solution and minimizes an objective by binary search. Rectangle packing, N-queens and Sudoku come worked out in full.

Exact circuit synthesis. Given a specification and a library of available gates, it asks whether some circuit of a given size matches that specification on every input — a question with one quantifier too many for SAT, so it goes to a QBF solver instead. What comes back is provably minimal, or provably impossible.

Compiles llogic's circuit language down to Verilog, so a design written for a solver can be simulated, synthesized, or put on an FPGA like any other. The module hierarchy survives the trip: nothing is flattened, instantiations stay instantiations, and flip-flops acquire the clock the source language has no word for.

The same road in the other direction, so existing Verilog can be reasoned about rather than only run. Structural Verilog is parsed and rewritten into circuits, with expression trees broken back down into gates. Every circuit that makes the round trip is checked by a SAT solver to still compute what it did before.

A compiler for a modelling language that describes not only what a system does, but what it does once parts of it have broken. From one such model it derives the diagnostic reasoning itself — given what a system was observed to do, which set of components failing would account for it.

Lydia rebuilt in modern C++, and widened from discrete circuits to systems that behave continuously. It simulates a model through an ODE solver, estimates the parameters a fault would have to have, and searches the space of failure candidates exhaustively or greedily as the size of the problem demands.