PV2 Manthangenerates a depencency function linking two arguments of a given function

Data-driven approach to Boolean functional synthesis

Application domain/field

Boolean functional synthesis

Type of tool

Synthesis tool

Expected input

F(X,Y) formula


Either as a QDIMACS or Verilog input file

Expected output

Boolean function Ψ such that F(X,Y)=F(X,Ψ(X)).


"In the context of applications, the sets X and Y are viewed as inputs and outputs, and the formula F(X,Y) is viewed as the functional specification capturing the relation between X and Y". It uses ABC, PicoSAT, Open-WBO and Scikit-Learn.


Repository: https://github.com/meelgroup/manthan

Related papers

Manthan: A Data-Driven Approach for Boolean Function Synthesis

Last publication date

14 July 2020

Related tools

Compared in the paper to C2Syn, BFSS and CADET.

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.