A Logic Synthesis tool based on "Mockturtle: EPFL Logic Synthesis Library " and "ABC: System for Sequential Logic Synthesis and Formal Verification""

logic-synthesis

Go to file

潘鸿洋 7b67d87713 Update README.md		2022-12-14 08:56:39 +08:00
.gitignore	Initial commit	2022-12-14 08:51:36 +08:00
LICENSE	Initial commit	2022-12-14 08:51:36 +08:00
README.md	Update README.md	2022-12-14 08:56:39 +08:00

README.md

phyLS (powerful )

This is

The SAT part is same as normal SAT solver.

The implementation of the AllSAT part differs from incremental enumeration because we do not add blocking conditions for existing solutions, but rather compute the matrices to obtain all the solutions in one pass.

Requirements

A modern compiler is required to build the libraries. Compiled successfully with Clang 6.0.1, Clang 12.0.0, GCC 7.3.0, and GCC 8.2.0.

How to Compile

git clone --recursive https://github.com/panhongyang0/phySAT.git
cd phySAT
mkdir build
cd build
cmake ..
make
./bin/phySAT

Useage

help  // all useful commands
1. cnf -f xx.cnf // CNF-based AllSAT solver, the benchmark is in <benchmark>