CIRCT
19.0.0git

A satisfiability checker for circuit equivalence. More...
#include <Solver.h>
Classes  
class  Circuit 
The representation of a circuit within a logical engine. More...  
Public Member Functions  
Solver (mlir::MLIRContext *mlirCtx, bool statisticsOpt)  
~Solver ()=default  
mlir::LogicalResult  solve () 
Solve the equivalence problem between the two circuits, then present the results to the user. More...  
Circuit *  addCircuit (llvm::StringRef name) 
Create a new circuit to be compared and return it. More...  
Private Member Functions  
void  printModel () 
Prints a model satisfying the solved constraints. More...  
void  printAssertions () 
Prints the constraints which were added to the solver. More...  
void  printStatistics () 
Prints the internal statistics of the SMT solver for benchmarking purposes and operational insight. More...  
mlir::LogicalResult  constrainCircuits () 
Formulates additional constraints which are satisfiable if only if the two circuits which are being compared are NOT equivalent, in which case there would be a model acting as a counterexample. More...  
Private Attributes  
llvm::DenseMap< mlir::StringAttr, mlir::Value >  symbolTable 
A map from internal solver symbols to the IR values they represent. More...  
Circuit *  circuits [2] 
The two circuits to be compared. More...  
mlir::MLIRContext *  mlirCtx 
The MLIR context of reference, owning all the MLIR entities. More...  
z3::context  context 
The Z3 context of reference, owning all the declared values, constants and expressions. More...  
z3::solver  solver 
The Z3 solver acting as the logical engine backend. More...  
bool  statisticsOpt 
The value of the statistics commandline option. More...  
A satisfiability checker for circuit equivalence.
This class interfaces with an external SMT solver acting as a logical engine. First spawn two circuits through addCircuit
; after collecting their logical constraints, the solve
method will compare them and report whether they result to be equivalent or, when not, also printing a model acting as a counterexample.
Solver::Solver  (  mlir::MLIRContext *  mlirCtx, 
bool  statisticsOpt  
) 
Definition at line 26 of file Solver.cpp.

default 
Solver::Circuit * Solver::addCircuit  (  llvm::StringRef  name  ) 
Create a new circuit to be compared and return it.
Definition at line 65 of file Solver.cpp.

private 
Formulates additional constraints which are satisfiable if only if the two circuits which are being compared are NOT equivalent, in which case there would be a model acting as a counterexample.
The procedure fails when detecting a mismatch of arity or type between the inputs and outputs of the circuits.
Definition at line 139 of file Solver.cpp.
References circuits, context, lec::errs(), circt::Solver::Circuit::getInputs(), circt::Solver::Circuit::getOutputs(), and solver.
Referenced by solve().

private 
Prints the constraints which were added to the solver.
Compared to solver.assertions().to_string() this method exposes each assertion as a z3::expression for eventual indepth debugging.
Definition at line 115 of file Solver.cpp.
References lec::dbgs(), and solver.
Referenced by solve().

private 
Prints a model satisfying the solved constraints.
Definition at line 79 of file Solver.cpp.
References builder, mlirCtx, lec::outs(), solver, and symbolTable.
Referenced by solve().

private 
Prints the internal statistics of the SMT solver for benchmarking purposes and operational insight.
Definition at line 125 of file Solver.cpp.
References lec::outs(), and solver.
Referenced by solve().
LogicalResult Solver::solve  (  ) 
Solve the equivalence problem between the two circuits, then present the results to the user.
Definition at line 32 of file Solver.cpp.
References constrainCircuits(), lec::errs(), lec::outs(), printAssertions(), printModel(), printStatistics(), solver, and statisticsOpt.

private 
The two circuits to be compared.
Definition at line 65 of file Solver.h.
Referenced by addCircuit(), and constrainCircuits().

private 
The Z3 context of reference, owning all the declared values, constants and expressions.
Definition at line 70 of file Solver.h.
Referenced by constrainCircuits().

private 
The MLIR context of reference, owning all the MLIR entities.
Definition at line 67 of file Solver.h.
Referenced by printModel().

private 
The Z3 solver acting as the logical engine backend.
Definition at line 72 of file Solver.h.
Referenced by constrainCircuits(), printAssertions(), printModel(), printStatistics(), and solve().

private 

private 
A map from internal solver symbols to the IR values they represent.
Definition at line 63 of file Solver.h.
Referenced by printModel().