Software Projects
Open source, hosted on gitlab.llama.gs.
Logic, Synthesis and Electronic Design Automation
-
Boolean Logic Library
A library for propositional logic representations: Boolean formulas, CNF, DNF, BDDs, hierarchical circuits, flat netlists, and their quantified variants (QBF, QCNF, QDNF). A single pipeline converts between them, lowering a circuit description to the conjunctive normal form a SAT or QBF solver requires. The foundational library every other project on this page depends on.
-
SMT Solver
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.
-
Fully Automated Circuit Designer
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. The five-gate full-subtractor shown here is one of its results, against the textbook seven.
-
Provably Minimal Automatic Test Pattern Generator
Finds test vectors for stuck-at faults in digital circuits, via PODEM, the D-algorithm, and two SAT-based searches. One SAT search is exact: it proves its vector sequence is the shortest possible, not just a good one — a guarantee few ATPG tools make. On the 74182 carry-lookahead generator, 67 faults reduce to 10 test vectors, each proven necessary. The exact search does not yet scale past small and medium circuits. Solved, it would cut integrated-circuit test cost directly: fewer vectors, less tester time per chip.
-
Circuit-to-Verilog Translator
Compiles our internal circuit Domain Specific Language (DSL) 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.
-
Verilog-to-Circuit Translator
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.
Diagnostics and Prognostics
-
Diagnosis Compiler
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.
-
Continuous Systems Diagnosis
The diagnosis compiler above, 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.
-
Fault Diagnosis Toolkit
Trains diagnostic engines from simulated sensor data. A model of a physical system — an ODE, a DAE, or an FMI co-simulation — is simulated under nominal and fault conditions, then used to train seven regression models or three nonlinear filters (Extended Kalman, Unscented Kalman, particle) that isolate which fault is present from sensor readings alone. Includes a Qt desktop application for browsing simulations, features, and diagnosis results.
-
Condition-Based Monitoring Platform
An instrumentation and data-collection platform for condition-based monitoring, applicable across equipment classes — HVAC, refrigeration, and others. It handles the physical side: custom firmware, a purpose-built sensor network, and a daemon streaming readings into a shared database. A temperature sensor is the first network node, currently in prototype. Diagnostic reasoning lives in a separate framework, which interfaces with this one directly: one collects data, the other diagnoses from it.