mirror of https://github.com/llvm/circt.git
[LEC] Clean up LogicExporter and add missing namespace; NFC
Remove some code duplication in `LogicExporter.cpp` and add missing `circt` namespaces around the library pieces.
This commit is contained in:
Fabian Schuiki
parent
eb5090b4ba
commit
e2b602dec7
|
|
@ -25,6 +25,8 @@
|
|||
#include <string>
|
||||
#include <z3++.h>
|
||||
|
||||
namespace circt {
|
||||
|
||||
/// The representation of a circuit within a logical engine.
|
||||
///
|
||||
/// This class defines a circuit as an abstraction of its underlying
|
||||
|
|
@ -113,4 +115,6 @@ private:
|
|||
llvm::DenseMap<mlir::Value, z3::expr> exprTable;
|
||||
};
|
||||
|
||||
} // namespace circt
|
||||
|
||||
#endif // TOOLS_CIRCT_LEC_CIRCUIT_H
|
||||
|
|
|
|||
|
|
@ -24,6 +24,8 @@
|
|||
#include "llvm/ADT/StringRef.h"
|
||||
#include <string>
|
||||
|
||||
namespace circt {
|
||||
|
||||
/// A class traversing MLIR IR to extrapolate the logic of a given circuit.
|
||||
///
|
||||
/// This class implements a MLIR exporter which searches the IR for the
|
||||
|
|
@ -37,103 +39,9 @@ public:
|
|||
|
||||
/// Initializes the exporting by visiting the builtin module.
|
||||
mlir::LogicalResult run(mlir::ModuleOp &module);
|
||||
mlir::LogicalResult run(hw::HWModuleOp &module);
|
||||
|
||||
private:
|
||||
/// This class provides logic-exporting functions for the implemented
|
||||
/// operations, along with a dispatcher to visit the correct handler.
|
||||
struct Visitor
|
||||
: public circt::hw::StmtVisitor<Visitor, mlir::LogicalResult,
|
||||
Solver::Circuit *>,
|
||||
public circt::hw::TypeOpVisitor<Visitor, mlir::LogicalResult,
|
||||
Solver::Circuit *>,
|
||||
public circt::comb::CombinationalVisitor<Visitor, mlir::LogicalResult,
|
||||
Solver::Circuit *> {
|
||||
// StmtVisitor definitions
|
||||
// Handle implemented `hw` statement operations.
|
||||
static mlir::LogicalResult visitStmt(circt::hw::InstanceOp &op,
|
||||
Solver::Circuit *circuit);
|
||||
static mlir::LogicalResult visitStmt(circt::hw::OutputOp &op,
|
||||
Solver::Circuit *circuit);
|
||||
|
||||
/// Collects unhandled `hw` statement operations.
|
||||
static mlir::LogicalResult visitStmt(mlir::Operation *op,
|
||||
Solver::Circuit *circuit);
|
||||
|
||||
/// Handles invalid `hw` statement operations.
|
||||
mlir::LogicalResult visitInvalidStmt(mlir::Operation *op,
|
||||
Solver::Circuit *circuit);
|
||||
|
||||
// TypeOpVisitor definitions
|
||||
// Handle implemented `hw` type operations.
|
||||
static mlir::LogicalResult visitTypeOp(circt::hw::ConstantOp &op,
|
||||
Solver::Circuit *circuit);
|
||||
|
||||
/// Collects unhandled `hw` type operations.
|
||||
static mlir::LogicalResult visitTypeOp(mlir::Operation *op,
|
||||
Solver::Circuit *circuit);
|
||||
|
||||
/// Handles invalid `hw` type operations.
|
||||
mlir::LogicalResult visitInvalidTypeOp(mlir::Operation *op,
|
||||
Solver::Circuit *circuit);
|
||||
|
||||
// CombinationalVisitor definitions
|
||||
// Handle implemented `comb` operations.
|
||||
static mlir::LogicalResult visitComb(circt::comb::AddOp &op,
|
||||
Solver::Circuit *circuit);
|
||||
static mlir::LogicalResult visitComb(circt::comb::AndOp &op,
|
||||
Solver::Circuit *circuit);
|
||||
static mlir::LogicalResult visitComb(circt::comb::ConcatOp &op,
|
||||
Solver::Circuit *circuit);
|
||||
static mlir::LogicalResult visitComb(circt::comb::DivSOp &op,
|
||||
Solver::Circuit *circuit);
|
||||
static mlir::LogicalResult visitComb(circt::comb::DivUOp &op,
|
||||
Solver::Circuit *circuit);
|
||||
static mlir::LogicalResult visitComb(circt::comb::ExtractOp &op,
|
||||
Solver::Circuit *circuit);
|
||||
static mlir::LogicalResult visitComb(circt::comb::ICmpOp &op,
|
||||
Solver::Circuit *circuit);
|
||||
static mlir::LogicalResult visitComb(circt::comb::ModSOp &op,
|
||||
Solver::Circuit *circuit);
|
||||
static mlir::LogicalResult visitComb(circt::comb::ModUOp &op,
|
||||
Solver::Circuit *circuit);
|
||||
static mlir::LogicalResult visitComb(circt::comb::MulOp &op,
|
||||
Solver::Circuit *circuit);
|
||||
static mlir::LogicalResult visitComb(circt::comb::MuxOp &op,
|
||||
Solver::Circuit *circuit);
|
||||
static mlir::LogicalResult visitComb(circt::comb::OrOp &op,
|
||||
Solver::Circuit *circuit);
|
||||
static mlir::LogicalResult visitComb(circt::comb::ParityOp &op,
|
||||
Solver::Circuit *circuit);
|
||||
static mlir::LogicalResult visitComb(circt::comb::ReplicateOp &op,
|
||||
Solver::Circuit *circuit);
|
||||
static mlir::LogicalResult visitComb(circt::comb::ShlOp &op,
|
||||
Solver::Circuit *circuit);
|
||||
static mlir::LogicalResult visitComb(circt::comb::ShrSOp &op,
|
||||
Solver::Circuit *circuit);
|
||||
static mlir::LogicalResult visitComb(circt::comb::ShrUOp &op,
|
||||
Solver::Circuit *circuit);
|
||||
static mlir::LogicalResult visitComb(circt::comb::SubOp &op,
|
||||
Solver::Circuit *circuit);
|
||||
static mlir::LogicalResult visitComb(circt::comb::XorOp &op,
|
||||
Solver::Circuit *circuit);
|
||||
|
||||
// Additional definitions
|
||||
/// Handles `builtin.module` logic exporting.
|
||||
static mlir::LogicalResult visitBuiltin(mlir::ModuleOp &op,
|
||||
Solver::Circuit *circuit,
|
||||
llvm::StringRef targetModule);
|
||||
|
||||
/// Handles `hw.module` logic exporting.
|
||||
static mlir::LogicalResult visitHW(circt::hw::HWModuleOp &op,
|
||||
Solver::Circuit *circuit);
|
||||
|
||||
/// Reports a failure whenever an unhandled operation is visited.
|
||||
static mlir::LogicalResult visitUnhandledOp(mlir::Operation *op);
|
||||
|
||||
/// Dispatches an operation to the appropriate visit function.
|
||||
mlir::LogicalResult dispatch(mlir::Operation *op, Solver::Circuit *circuit);
|
||||
};
|
||||
|
||||
// For Solver::Circuit::addInstance to access Visitor::visitHW.
|
||||
friend Solver::Circuit;
|
||||
|
||||
|
|
@ -144,4 +52,6 @@ private:
|
|||
Solver::Circuit *circuit;
|
||||
};
|
||||
|
||||
} // namespace circt
|
||||
|
||||
#endif // TOOLS_CIRCT_LEC_LOGICEXPORTER_H
|
||||
|
|
|
|||
|
|
@ -19,6 +19,8 @@
|
|||
#include "mlir/IR/Value.h"
|
||||
#include <z3++.h>
|
||||
|
||||
namespace circt {
|
||||
|
||||
/// A satisfiability checker for circuit equivalence
|
||||
///
|
||||
/// This class interfaces with an external SMT solver acting as a logical
|
||||
|
|
@ -72,4 +74,6 @@ private:
|
|||
bool statisticsOpt;
|
||||
};
|
||||
|
||||
} // namespace circt
|
||||
|
||||
#endif // TOOLS_CIRCT_LEC_SOLVER_H
|
||||
|
|
|
|||
|
|
@ -19,8 +19,11 @@
|
|||
|
||||
#define DEBUG_TYPE "lec-circuit"
|
||||
|
||||
using namespace mlir;
|
||||
using namespace circt;
|
||||
|
||||
/// Add an input to the circuit; internally a new value gets allocated.
|
||||
void Solver::Circuit::addInput(mlir::Value value) {
|
||||
void Solver::Circuit::addInput(Value value) {
|
||||
LLVM_DEBUG(lec::dbgs() << name << " addInput\n");
|
||||
lec::Scope indent;
|
||||
z3::expr input = allocateValue(value);
|
||||
|
|
@ -28,7 +31,7 @@ void Solver::Circuit::addInput(mlir::Value value) {
|
|||
}
|
||||
|
||||
/// Add an output to the circuit.
|
||||
void Solver::Circuit::addOutput(mlir::Value value) {
|
||||
void Solver::Circuit::addOutput(Value value) {
|
||||
LLVM_DEBUG(lec::dbgs() << name << " addOutput\n");
|
||||
// Referenced value already assigned, fetching from expression table.
|
||||
z3::expr output = fetchExpr(value);
|
||||
|
|
@ -45,8 +48,7 @@ llvm::ArrayRef<z3::expr> Solver::Circuit::getOutputs() { return outputs; }
|
|||
// `hw` dialect operations
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
void Solver::Circuit::addConstant(mlir::Value opResult,
|
||||
const mlir::APInt &opValue) {
|
||||
void Solver::Circuit::addConstant(Value opResult, const APInt &opValue) {
|
||||
LLVM_DEBUG(lec::dbgs() << name << " addConstant\n");
|
||||
lec::Scope indent;
|
||||
allocateConstant(opResult, opValue);
|
||||
|
|
@ -54,8 +56,7 @@ void Solver::Circuit::addConstant(mlir::Value opResult,
|
|||
|
||||
void Solver::Circuit::addInstance(llvm::StringRef instanceName,
|
||||
circt::hw::HWModuleOp op,
|
||||
mlir::OperandRange arguments,
|
||||
mlir::ResultRange results) {
|
||||
OperandRange arguments, ResultRange results) {
|
||||
LLVM_DEBUG(lec::dbgs() << name << " addInstance\n");
|
||||
lec::Scope indent;
|
||||
LLVM_DEBUG(lec::dbgs() << "instance name: " << instanceName << "\n");
|
||||
|
|
@ -66,7 +67,7 @@ void Solver::Circuit::addInstance(llvm::StringRef instanceName,
|
|||
Circuit instance(name + "@" + instanceName + suffix, solver);
|
||||
// Export logic to the instance's circuit by visiting the IR of the
|
||||
// instanced module.
|
||||
auto res = LogicExporter::Visitor::visitHW(op, &instance);
|
||||
auto res = LogicExporter(op.getModuleName(), &instance).run(op);
|
||||
assert(res.succeeded() && "Instance visit failed");
|
||||
|
||||
// Constrain the inputs and outputs of the instanced circuit to, respectively,
|
||||
|
|
@ -75,7 +76,7 @@ void Solver::Circuit::addInstance(llvm::StringRef instanceName,
|
|||
LLVM_DEBUG(lec::dbgs() << "instance inputs:\n");
|
||||
lec::Scope indent;
|
||||
auto *input = instance.inputs.begin();
|
||||
for (mlir::Value argument : arguments) {
|
||||
for (Value argument : arguments) {
|
||||
LLVM_DEBUG(lec::dbgs() << "input\n");
|
||||
z3::expr argExpr = fetchExpr(argument);
|
||||
solver.solver.add(argExpr == *input++);
|
||||
|
|
@ -96,32 +97,28 @@ void Solver::Circuit::addInstance(llvm::StringRef instanceName,
|
|||
// `comb` dialect operations
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
void Solver::Circuit::performAdd(mlir::Value result,
|
||||
mlir::OperandRange operands) {
|
||||
void Solver::Circuit::performAdd(Value result, OperandRange operands) {
|
||||
LLVM_DEBUG(lec::dbgs() << name << " perform Add\n");
|
||||
lec::Scope indent;
|
||||
variadicOperation(result, operands,
|
||||
[](auto op1, auto op2) { return op1 + op2; });
|
||||
}
|
||||
|
||||
void Solver::Circuit::performAnd(mlir::Value result,
|
||||
mlir::OperandRange operands) {
|
||||
void Solver::Circuit::performAnd(Value result, OperandRange operands) {
|
||||
LLVM_DEBUG(lec::dbgs() << name << " perform And\n");
|
||||
lec::Scope indent;
|
||||
variadicOperation(result, operands,
|
||||
[](auto op1, auto op2) { return z3::operator&(op1, op2); });
|
||||
}
|
||||
|
||||
void Solver::Circuit::performConcat(mlir::Value result,
|
||||
mlir::OperandRange operands) {
|
||||
void Solver::Circuit::performConcat(Value result, OperandRange operands) {
|
||||
LLVM_DEBUG(lec::dbgs() << name << " perform Concat\n");
|
||||
lec::Scope indent;
|
||||
variadicOperation(result, operands,
|
||||
[](auto op1, auto op2) { return z3::concat(op1, op2); });
|
||||
}
|
||||
|
||||
void Solver::Circuit::performDivS(mlir::Value result, mlir::Value lhs,
|
||||
mlir::Value rhs) {
|
||||
void Solver::Circuit::performDivS(Value result, Value lhs, Value rhs) {
|
||||
LLVM_DEBUG(lec::dbgs() << name << " perform DivS\n");
|
||||
lec::Scope indent;
|
||||
LLVM_DEBUG(lec::dbgs() << "lhs:\n");
|
||||
|
|
@ -132,8 +129,7 @@ void Solver::Circuit::performDivS(mlir::Value result, mlir::Value lhs,
|
|||
constrainResult(result, op);
|
||||
}
|
||||
|
||||
void Solver::Circuit::performDivU(mlir::Value result, mlir::Value lhs,
|
||||
mlir::Value rhs) {
|
||||
void Solver::Circuit::performDivU(Value result, Value lhs, Value rhs) {
|
||||
LLVM_DEBUG(lec::dbgs() << name << " perform DivU\n");
|
||||
lec::Scope indent;
|
||||
LLVM_DEBUG(lec::dbgs() << "lhs:\n");
|
||||
|
|
@ -144,7 +140,7 @@ void Solver::Circuit::performDivU(mlir::Value result, mlir::Value lhs,
|
|||
constrainResult(result, op);
|
||||
}
|
||||
|
||||
void Solver::Circuit::performExtract(mlir::Value result, mlir::Value input,
|
||||
void Solver::Circuit::performExtract(Value result, Value input,
|
||||
uint32_t lowBit) {
|
||||
LLVM_DEBUG(lec::dbgs() << name << " performExtract\n");
|
||||
lec::Scope indent;
|
||||
|
|
@ -156,10 +152,9 @@ void Solver::Circuit::performExtract(mlir::Value result, mlir::Value input,
|
|||
constrainResult(result, extract);
|
||||
}
|
||||
|
||||
mlir::LogicalResult
|
||||
Solver::Circuit::performICmp(mlir::Value result,
|
||||
circt::comb::ICmpPredicate predicate,
|
||||
mlir::Value lhs, mlir::Value rhs) {
|
||||
LogicalResult Solver::Circuit::performICmp(Value result,
|
||||
circt::comb::ICmpPredicate predicate,
|
||||
Value lhs, Value rhs) {
|
||||
LLVM_DEBUG(lec::dbgs() << name << " performICmp\n");
|
||||
lec::Scope indent;
|
||||
LLVM_DEBUG(lec::dbgs() << "lhs:\n");
|
||||
|
|
@ -206,15 +201,14 @@ Solver::Circuit::performICmp(mlir::Value result,
|
|||
case circt::comb::ICmpPredicate::wne:
|
||||
result.getDefiningOp()->emitError(
|
||||
"n-state logic predicates are not supported");
|
||||
return mlir::failure();
|
||||
return failure();
|
||||
};
|
||||
|
||||
constrainResult(result, icmp);
|
||||
return mlir::success();
|
||||
return success();
|
||||
}
|
||||
|
||||
void Solver::Circuit::performModS(mlir::Value result, mlir::Value lhs,
|
||||
mlir::Value rhs) {
|
||||
void Solver::Circuit::performModS(Value result, Value lhs, Value rhs) {
|
||||
LLVM_DEBUG(lec::dbgs() << name << " perform ModS\n");
|
||||
lec::Scope indent;
|
||||
LLVM_DEBUG(lec::dbgs() << "lhs:\n");
|
||||
|
|
@ -225,8 +219,7 @@ void Solver::Circuit::performModS(mlir::Value result, mlir::Value lhs,
|
|||
constrainResult(result, op);
|
||||
}
|
||||
|
||||
void Solver::Circuit::performModU(mlir::Value result, mlir::Value lhs,
|
||||
mlir::Value rhs) {
|
||||
void Solver::Circuit::performModU(Value result, Value lhs, Value rhs) {
|
||||
LLVM_DEBUG(lec::dbgs() << name << " perform ModU\n");
|
||||
lec::Scope indent;
|
||||
LLVM_DEBUG(lec::dbgs() << "lhs:\n");
|
||||
|
|
@ -237,17 +230,15 @@ void Solver::Circuit::performModU(mlir::Value result, mlir::Value lhs,
|
|||
constrainResult(result, op);
|
||||
}
|
||||
|
||||
void Solver::Circuit::performMul(mlir::Value result,
|
||||
mlir::OperandRange operands) {
|
||||
void Solver::Circuit::performMul(Value result, OperandRange operands) {
|
||||
LLVM_DEBUG(lec::dbgs() << name << " perform Mul\n");
|
||||
lec::Scope indent;
|
||||
variadicOperation(result, operands,
|
||||
[](auto op1, auto op2) { return op1 * op2; });
|
||||
}
|
||||
|
||||
void Solver::Circuit::performMux(mlir::Value result, mlir::Value cond,
|
||||
mlir::Value trueValue,
|
||||
mlir::Value falseValue) {
|
||||
void Solver::Circuit::performMux(Value result, Value cond, Value trueValue,
|
||||
Value falseValue) {
|
||||
LLVM_DEBUG(lec::dbgs() << name << " performMux\n");
|
||||
lec::Scope indent;
|
||||
LLVM_DEBUG(lec::dbgs() << "cond:\n");
|
||||
|
|
@ -261,15 +252,14 @@ void Solver::Circuit::performMux(mlir::Value result, mlir::Value cond,
|
|||
constrainResult(result, mux);
|
||||
}
|
||||
|
||||
void Solver::Circuit::performOr(mlir::Value result,
|
||||
mlir::OperandRange operands) {
|
||||
void Solver::Circuit::performOr(Value result, OperandRange operands) {
|
||||
LLVM_DEBUG(lec::dbgs() << name << " perform Or\n");
|
||||
lec::Scope indent;
|
||||
variadicOperation(result, operands,
|
||||
[](auto op1, auto op2) { return op1 | op2; });
|
||||
}
|
||||
|
||||
void Solver::Circuit::performParity(mlir::Value result, mlir::Value input) {
|
||||
void Solver::Circuit::performParity(Value result, Value input) {
|
||||
LLVM_DEBUG(lec::dbgs() << name << " performParity\n");
|
||||
lec::Scope indent;
|
||||
LLVM_DEBUG(lec::dbgs() << "input:\n");
|
||||
|
|
@ -287,7 +277,7 @@ void Solver::Circuit::performParity(mlir::Value result, mlir::Value input) {
|
|||
constrainResult(result, parity);
|
||||
}
|
||||
|
||||
void Solver::Circuit::performReplicate(mlir::Value result, mlir::Value input) {
|
||||
void Solver::Circuit::performReplicate(Value result, Value input) {
|
||||
LLVM_DEBUG(lec::dbgs() << name << " performReplicate\n");
|
||||
lec::Scope indent;
|
||||
LLVM_DEBUG(lec::dbgs() << "input:\n");
|
||||
|
|
@ -306,8 +296,7 @@ void Solver::Circuit::performReplicate(mlir::Value result, mlir::Value input) {
|
|||
constrainResult(result, replicate);
|
||||
}
|
||||
|
||||
void Solver::Circuit::performShl(mlir::Value result, mlir::Value lhs,
|
||||
mlir::Value rhs) {
|
||||
void Solver::Circuit::performShl(Value result, Value lhs, Value rhs) {
|
||||
LLVM_DEBUG(lec::dbgs() << name << " perform Shl\n");
|
||||
lec::Scope indent;
|
||||
LLVM_DEBUG(lec::dbgs() << "lhs:\n");
|
||||
|
|
@ -319,8 +308,7 @@ void Solver::Circuit::performShl(mlir::Value result, mlir::Value lhs,
|
|||
}
|
||||
|
||||
// Arithmetic shift right.
|
||||
void Solver::Circuit::performShrS(mlir::Value result, mlir::Value lhs,
|
||||
mlir::Value rhs) {
|
||||
void Solver::Circuit::performShrS(Value result, Value lhs, Value rhs) {
|
||||
LLVM_DEBUG(lec::dbgs() << name << " perform ShrS\n");
|
||||
lec::Scope indent;
|
||||
LLVM_DEBUG(lec::dbgs() << "lhs:\n");
|
||||
|
|
@ -332,8 +320,7 @@ void Solver::Circuit::performShrS(mlir::Value result, mlir::Value lhs,
|
|||
}
|
||||
|
||||
// Logical shift right.
|
||||
void Solver::Circuit::performShrU(mlir::Value result, mlir::Value lhs,
|
||||
mlir::Value rhs) {
|
||||
void Solver::Circuit::performShrU(Value result, Value lhs, Value rhs) {
|
||||
LLVM_DEBUG(lec::dbgs() << name << " perform ShrU\n");
|
||||
lec::Scope indent;
|
||||
LLVM_DEBUG(lec::dbgs() << "lhs:\n");
|
||||
|
|
@ -344,16 +331,14 @@ void Solver::Circuit::performShrU(mlir::Value result, mlir::Value lhs,
|
|||
constrainResult(result, op);
|
||||
}
|
||||
|
||||
void Solver::Circuit::performSub(mlir::Value result,
|
||||
mlir::OperandRange operands) {
|
||||
void Solver::Circuit::performSub(Value result, OperandRange operands) {
|
||||
LLVM_DEBUG(lec::dbgs() << name << " perform Sub\n");
|
||||
lec::Scope indent;
|
||||
variadicOperation(result, operands,
|
||||
[](auto op1, auto op2) { return op1 - op2; });
|
||||
}
|
||||
|
||||
void Solver::Circuit::performXor(mlir::Value result,
|
||||
mlir::OperandRange operands) {
|
||||
void Solver::Circuit::performXor(Value result, OperandRange operands) {
|
||||
LLVM_DEBUG(lec::dbgs() << name << " perform Xor\n");
|
||||
lec::Scope indent;
|
||||
variadicOperation(result, operands,
|
||||
|
|
@ -363,14 +348,14 @@ void Solver::Circuit::performXor(mlir::Value result,
|
|||
/// Helper function for performing a variadic operation: it executes a lambda
|
||||
/// over a range of operands.
|
||||
void Solver::Circuit::variadicOperation(
|
||||
mlir::Value result, mlir::OperandRange operands,
|
||||
Value result, OperandRange operands,
|
||||
llvm::function_ref<z3::expr(const z3::expr &, const z3::expr &)>
|
||||
operation) {
|
||||
LLVM_DEBUG(lec::dbgs() << "variadic operation\n");
|
||||
lec::Scope indent;
|
||||
// Vacuous base case.
|
||||
auto it = operands.begin();
|
||||
mlir::Value operand = *it;
|
||||
Value operand = *it;
|
||||
z3::expr varOp = exprTable.find(operand)->second;
|
||||
{
|
||||
LLVM_DEBUG(lec::dbgs() << "first operand:\n");
|
||||
|
|
@ -394,11 +379,11 @@ void Solver::Circuit::variadicOperation(
|
|||
|
||||
/// Allocates an IR value in the logical backend and returns its representing
|
||||
/// expression.
|
||||
z3::expr Solver::Circuit::allocateValue(mlir::Value value) {
|
||||
z3::expr Solver::Circuit::allocateValue(Value value) {
|
||||
std::string valueName = name + "%" + std::to_string(assignments++);
|
||||
LLVM_DEBUG(lec::dbgs() << "allocating value:\n");
|
||||
lec::Scope indent;
|
||||
mlir::Type type = value.getType();
|
||||
Type type = value.getType();
|
||||
assert(type.isSignlessInteger() && "Unsupported type");
|
||||
unsigned int width = type.getIntOrFloatBitWidth();
|
||||
// Technically allowed for the `hw` dialect but
|
||||
|
|
@ -409,8 +394,8 @@ z3::expr Solver::Circuit::allocateValue(mlir::Value value) {
|
|||
LLVM_DEBUG(lec::printValue(value));
|
||||
auto exprInsertion = exprTable.insert(std::pair(value, expr));
|
||||
assert(exprInsertion.second && "Value not inserted in expression table");
|
||||
mlir::Builder builder(solver.mlirCtx);
|
||||
mlir::StringAttr symbol = builder.getStringAttr(valueName);
|
||||
Builder builder(solver.mlirCtx);
|
||||
StringAttr symbol = builder.getStringAttr(valueName);
|
||||
auto symInsertion = solver.symbolTable.insert(std::pair(symbol, value));
|
||||
assert(symInsertion.second && "Value not inserted in symbol table");
|
||||
return expr;
|
||||
|
|
@ -418,8 +403,7 @@ z3::expr Solver::Circuit::allocateValue(mlir::Value value) {
|
|||
|
||||
/// Allocates a constant value in the logical backend and returns its
|
||||
/// representing expression.
|
||||
void Solver::Circuit::allocateConstant(mlir::Value result,
|
||||
const mlir::APInt &value) {
|
||||
void Solver::Circuit::allocateConstant(Value result, const APInt &value) {
|
||||
// `The constant operation produces a constant value
|
||||
// of standard integer type without a sign`
|
||||
const z3::expr constant =
|
||||
|
|
@ -431,7 +415,7 @@ void Solver::Circuit::allocateConstant(mlir::Value result,
|
|||
}
|
||||
|
||||
/// Fetches the corresponding logical expression for a given IR value.
|
||||
z3::expr Solver::Circuit::fetchExpr(mlir::Value &value) {
|
||||
z3::expr Solver::Circuit::fetchExpr(Value &value) {
|
||||
z3::expr expr = exprTable.find(value)->second;
|
||||
lec::Scope indent;
|
||||
LLVM_DEBUG(lec::printExpr(expr));
|
||||
|
|
@ -441,7 +425,7 @@ z3::expr Solver::Circuit::fetchExpr(mlir::Value &value) {
|
|||
|
||||
/// Constrains the result of a MLIR operation to be equal a given logical
|
||||
/// express, simulating an assignment.
|
||||
void Solver::Circuit::constrainResult(mlir::Value &result, z3::expr &expr) {
|
||||
void Solver::Circuit::constrainResult(Value &result, z3::expr &expr) {
|
||||
LLVM_DEBUG(lec::dbgs() << "constraining result:\n");
|
||||
lec::Scope indent;
|
||||
{
|
||||
|
|
|
|||
|
|
@ -18,440 +18,211 @@
|
|||
|
||||
#define DEBUG_TYPE "lec-exporter"
|
||||
|
||||
using namespace circt;
|
||||
using namespace mlir;
|
||||
|
||||
namespace {
|
||||
/// Helper function to provide a common debug formatting for
|
||||
/// an operation's list of operands.
|
||||
template <class ConcreteOp>
|
||||
static void debugOperands(ConcreteOp op) {
|
||||
for (const mlir::OpOperand &operand : op->getOpOperands()) {
|
||||
mlir::Value value = operand.get();
|
||||
lec::dbgs() << "Operand:\n";
|
||||
lec::Scope indent;
|
||||
lec::printValue(value);
|
||||
}
|
||||
}
|
||||
|
||||
/// Helper function to provide a common debug formatting for
|
||||
/// an operation's result.
|
||||
static void debugOpResult(mlir::Value result) {
|
||||
lec::dbgs() << "Result:\n";
|
||||
lec::Scope indent;
|
||||
lec::printValue(result);
|
||||
}
|
||||
/// This class provides logic-exporting functions for the implemented
|
||||
/// operations, along with a dispatcher to visit the correct handler.
|
||||
struct Visitor : public hw::StmtVisitor<Visitor, LogicalResult>,
|
||||
public hw::TypeOpVisitor<Visitor, LogicalResult>,
|
||||
public comb::CombinationalVisitor<Visitor, LogicalResult> {
|
||||
using hw::StmtVisitor<Visitor, LogicalResult>::visitStmt;
|
||||
using hw::TypeOpVisitor<Visitor, LogicalResult>::visitTypeOp;
|
||||
using comb::CombinationalVisitor<Visitor, LogicalResult>::visitComb;
|
||||
friend class hw::StmtVisitor<Visitor, LogicalResult>;
|
||||
friend class hw::TypeOpVisitor<Visitor, LogicalResult>;
|
||||
friend class comb::CombinationalVisitor<Visitor, LogicalResult>;
|
||||
|
||||
/// Helper function to provide a common debug formatting for
|
||||
/// an operation's list of results.
|
||||
template <class ConcreteOp>
|
||||
static void debugOpResults(mlir::OpTrait::VariadicResults<ConcreteOp> *op) {
|
||||
lec::dbgs() << "Results:\n";
|
||||
for (mlir::OpResult result : op->getResults()) {
|
||||
lec::Scope indent;
|
||||
lec::dbgs() << "#" << result.getResultNumber() << " ";
|
||||
debugOpResult(result);
|
||||
}
|
||||
}
|
||||
Visitor(Solver::Circuit *circuit) : circuit(circuit) {}
|
||||
Solver::Circuit *circuit;
|
||||
|
||||
/// Helper function to provide a common debug formatting for
|
||||
/// an operation's list of attributes.
|
||||
static void debugAttributes(llvm::ArrayRef<mlir::NamedAttribute> attributes) {
|
||||
lec::dbgs() << "Attributes:\n";
|
||||
lec::Scope indent;
|
||||
for (mlir::NamedAttribute attr : attributes) {
|
||||
lec::dbgs() << attr.getName().getValue() << ": " << attr.getValue() << "\n";
|
||||
}
|
||||
}
|
||||
} // anonymous namespace
|
||||
|
||||
/// Initializes the exporter by visiting the builtin module.
|
||||
mlir::LogicalResult LogicExporter::run(mlir::ModuleOp &builtinModule) {
|
||||
mlir::LogicalResult outcome =
|
||||
Visitor::visitBuiltin(builtinModule, circuit, moduleName);
|
||||
return outcome;
|
||||
}
|
||||
|
||||
//===----------------------------------------------------------------------===//
|
||||
// Visitor implementation
|
||||
//===----------------------------------------------------------------------===//
|
||||
// StmtVisitor implementation
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
mlir::LogicalResult
|
||||
LogicExporter::Visitor::visitStmt(circt::hw::InstanceOp &op,
|
||||
Solver::Circuit *circuit) {
|
||||
LLVM_DEBUG(lec::dbgs() << "Visiting hw.instance\n");
|
||||
lec::Scope indent;
|
||||
LLVM_DEBUG(lec::dbgs() << op->getName() << "\n");
|
||||
LLVM_DEBUG(debugAttributes(op->getAttrs()));
|
||||
LLVM_DEBUG(debugOperands(op));
|
||||
LLVM_DEBUG(debugOpResults(&op));
|
||||
llvm::StringRef instanceName = op.getInstanceName();
|
||||
LLVM_DEBUG(lec::dbgs() << "Instance name: " << instanceName << "\n");
|
||||
llvm::StringRef targetModule = op.getModuleName();
|
||||
LLVM_DEBUG(lec::dbgs() << "Target module name: " << targetModule << "\n");
|
||||
llvm::Optional<llvm::StringRef> innerSym = op.getInnerSym();
|
||||
LLVM_DEBUG(lec::dbgs() << "Inner symbol: " << innerSym << "\n");
|
||||
|
||||
auto hwModule = llvm::dyn_cast_if_present<circt::hw::HWModuleOp>(
|
||||
op.getReferencedModule());
|
||||
if (hwModule) {
|
||||
circuit->addInstance(instanceName.str(), hwModule, op->getOperands(),
|
||||
op->getResults());
|
||||
return mlir::success();
|
||||
}
|
||||
op.emitError("expected referenced module `" + targetModule + "` not found");
|
||||
return mlir::failure();
|
||||
}
|
||||
|
||||
mlir::LogicalResult
|
||||
LogicExporter::Visitor::visitStmt(circt::hw::OutputOp &op,
|
||||
Solver::Circuit *circuit) {
|
||||
LLVM_DEBUG(lec::dbgs() << "Visiting hw.output\n");
|
||||
lec::Scope indent;
|
||||
LLVM_DEBUG(debugOperands(op));
|
||||
for (auto operand : op.getOperands())
|
||||
circuit->addOutput(operand);
|
||||
return mlir::success();
|
||||
}
|
||||
|
||||
/// Collects unhandled `hw` statement operations.
|
||||
mlir::LogicalResult
|
||||
LogicExporter::Visitor::visitStmt(mlir::Operation *op,
|
||||
Solver::Circuit *circuit) {
|
||||
return visitUnhandledOp(op);
|
||||
}
|
||||
|
||||
/// Handles invalid `hw` statement operations.
|
||||
mlir::LogicalResult
|
||||
LogicExporter::Visitor::visitInvalidStmt(mlir::Operation *op,
|
||||
Solver::Circuit *circuit) {
|
||||
// op is not valid for StmtVisitor.
|
||||
// Attempt dispatching it to TypeOpVisitor next.
|
||||
return dispatchTypeOpVisitor(op, circuit);
|
||||
}
|
||||
|
||||
//===----------------------------------------------------------------------===//
|
||||
// TypeOpVisitor implementation
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
mlir::LogicalResult
|
||||
LogicExporter::Visitor::visitTypeOp(circt::hw::ConstantOp &op,
|
||||
Solver::Circuit *circuit) {
|
||||
LLVM_DEBUG(lec::dbgs() << "Visiting hw.constant\n");
|
||||
lec::Scope indent;
|
||||
mlir::Value result = op.getResult();
|
||||
LLVM_DEBUG(lec::printValue(result));
|
||||
mlir::APInt value = op.getValue();
|
||||
LLVM_DEBUG(lec::printAPInt(value));
|
||||
circuit->addConstant(result, value);
|
||||
return mlir::success();
|
||||
}
|
||||
|
||||
/// Collects unhandled `hw` type operations.
|
||||
mlir::LogicalResult
|
||||
LogicExporter::Visitor::visitTypeOp(mlir::Operation *op,
|
||||
Solver::Circuit *circuit) {
|
||||
return visitUnhandledOp(op);
|
||||
}
|
||||
|
||||
/// Handles invalid `hw` type operations.
|
||||
mlir::LogicalResult
|
||||
LogicExporter::Visitor::visitInvalidTypeOp(mlir::Operation *op,
|
||||
Solver::Circuit *circuit) {
|
||||
// op is neither valid for StmtVisitor nor TypeOpVisitor.
|
||||
// Attempt dispatching it to CombinationalVisitor next.
|
||||
return dispatchCombinationalVisitor(op, circuit);
|
||||
}
|
||||
|
||||
//===----------------------------------------------------------------------===//
|
||||
// CombinationalVisitor implementation
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
// This macro is used to reject the visited operation when n-state logic is
|
||||
// not supported.
|
||||
#define REJECT_N_STATE_LOGIC() \
|
||||
if (!twoState) { \
|
||||
op.emitError("`bin` attribute unset, but n-state logic is not supported"); \
|
||||
return mlir::failure(); \
|
||||
}
|
||||
|
||||
// This macro implements the visiting function for a `comb` operation accepting
|
||||
// a variadic number of operands.
|
||||
template <typename OpTy, typename FnTy>
|
||||
static mlir::LogicalResult visitVariadicCombOp(Solver::Circuit *circuit,
|
||||
OpTy op, FnTy fn) {
|
||||
LLVM_DEBUG(lec::dbgs() << "Visiting " << op->getName() << "\n");
|
||||
lec::Scope indent;
|
||||
LLVM_DEBUG(debugOperands(op));
|
||||
bool twoState = op.getTwoState();
|
||||
REJECT_N_STATE_LOGIC();
|
||||
mlir::Value result = op.getResult();
|
||||
LLVM_DEBUG(debugOpResult(result));
|
||||
(circuit->*fn)(result, op.getOperands());
|
||||
return mlir::success();
|
||||
}
|
||||
|
||||
// This macro implements the visiting function for a `comb` operation accepting
|
||||
// two operands.
|
||||
template <typename OpTy, typename FnTy>
|
||||
static mlir::LogicalResult visitBinaryCombOp(Solver::Circuit *circuit, OpTy op,
|
||||
FnTy fn) {
|
||||
LLVM_DEBUG(lec::dbgs() << "Visiting " << op->getName() << "\n");
|
||||
lec::Scope indent;
|
||||
LLVM_DEBUG(debugOperands(op));
|
||||
bool twoState = op.getTwoState();
|
||||
REJECT_N_STATE_LOGIC();
|
||||
auto lhs = op.getLhs();
|
||||
auto rhs = op.getRhs();
|
||||
auto result = op.getResult();
|
||||
LLVM_DEBUG(debugOpResult(result));
|
||||
(circuit->*fn)(result, lhs, rhs);
|
||||
return mlir::success();
|
||||
}
|
||||
|
||||
// This macro implements the visiting function for a `comb` operation accepting
|
||||
// one operand.
|
||||
template <typename OpTy, typename FnTy>
|
||||
static mlir::LogicalResult visitUnaryCombOp(Solver::Circuit *circuit, OpTy op,
|
||||
FnTy fn) {
|
||||
LLVM_DEBUG(lec::dbgs() << "Visiting " << op->getName() << "\n");
|
||||
lec::Scope indent;
|
||||
LLVM_DEBUG(debugOperands(op));
|
||||
bool twoState = op.getTwoState();
|
||||
REJECT_N_STATE_LOGIC();
|
||||
auto input = op.getInput();
|
||||
auto result = op.getResult();
|
||||
LLVM_DEBUG(debugOpResult(result));
|
||||
(circuit->*fn)(result, input);
|
||||
return mlir::success();
|
||||
}
|
||||
|
||||
mlir::LogicalResult
|
||||
LogicExporter::Visitor::visitComb(circt::comb::AddOp &op,
|
||||
Solver::Circuit *circuit) {
|
||||
return visitVariadicCombOp(circuit, op, &Solver::Circuit::performAdd);
|
||||
}
|
||||
|
||||
mlir::LogicalResult
|
||||
LogicExporter::Visitor::visitComb(circt::comb::AndOp &op,
|
||||
Solver::Circuit *circuit) {
|
||||
return visitVariadicCombOp(circuit, op, &Solver::Circuit::performAnd);
|
||||
}
|
||||
|
||||
mlir::LogicalResult
|
||||
LogicExporter::Visitor::visitComb(circt::comb::ConcatOp &op,
|
||||
Solver::Circuit *circuit) {
|
||||
LLVM_DEBUG(lec::dbgs() << "Visiting comb.concat\n");
|
||||
lec::Scope indent;
|
||||
LLVM_DEBUG(debugOperands(op));
|
||||
mlir::Value result = op.getResult();
|
||||
LLVM_DEBUG(debugOpResult(result));
|
||||
circuit->performConcat(result, op.getOperands());
|
||||
return mlir::success();
|
||||
}
|
||||
|
||||
mlir::LogicalResult
|
||||
LogicExporter::Visitor::visitComb(circt::comb::DivSOp &op,
|
||||
Solver::Circuit *circuit) {
|
||||
return visitBinaryCombOp(circuit, op, &Solver::Circuit::performDivS);
|
||||
}
|
||||
|
||||
mlir::LogicalResult
|
||||
LogicExporter::Visitor::visitComb(circt::comb::DivUOp &op,
|
||||
Solver::Circuit *circuit) {
|
||||
return visitBinaryCombOp(circuit, op, &Solver::Circuit::performDivU);
|
||||
}
|
||||
|
||||
mlir::LogicalResult
|
||||
LogicExporter::Visitor::visitComb(circt::comb::ExtractOp &op,
|
||||
Solver::Circuit *circuit) {
|
||||
LLVM_DEBUG(lec::dbgs() << "Visiting comb.extract\n");
|
||||
lec::Scope indent;
|
||||
LLVM_DEBUG(debugOperands(op));
|
||||
auto input = op.getInput();
|
||||
uint32_t lowBit = op.getLowBit();
|
||||
LLVM_DEBUG(lec::dbgs() << "lowBit: " << lowBit << "\n");
|
||||
auto result = op.getResult();
|
||||
LLVM_DEBUG(debugOpResult(result));
|
||||
circuit->performExtract(result, input, lowBit);
|
||||
return mlir::success();
|
||||
}
|
||||
|
||||
mlir::LogicalResult
|
||||
LogicExporter::Visitor::visitComb(circt::comb::ICmpOp &op,
|
||||
Solver::Circuit *circuit) {
|
||||
LLVM_DEBUG(lec::dbgs() << "Visiting comb.icmp\n");
|
||||
lec::Scope indent;
|
||||
LLVM_DEBUG(debugOperands(op));
|
||||
bool twoState = op.getTwoState();
|
||||
REJECT_N_STATE_LOGIC();
|
||||
circt::comb::ICmpPredicate predicate = op.getPredicate();
|
||||
auto lhs = op.getLhs();
|
||||
auto rhs = op.getRhs();
|
||||
auto result = op.getResult();
|
||||
LLVM_DEBUG(debugOpResult(result));
|
||||
mlir::LogicalResult comparisonResult =
|
||||
circuit->performICmp(result, predicate, lhs, rhs);
|
||||
return comparisonResult;
|
||||
}
|
||||
|
||||
mlir::LogicalResult
|
||||
LogicExporter::Visitor::visitComb(circt::comb::ModSOp &op,
|
||||
Solver::Circuit *circuit) {
|
||||
return visitBinaryCombOp(circuit, op, &Solver::Circuit::performModS);
|
||||
}
|
||||
|
||||
mlir::LogicalResult
|
||||
LogicExporter::Visitor::visitComb(circt::comb::ModUOp &op,
|
||||
Solver::Circuit *circuit) {
|
||||
return visitBinaryCombOp(circuit, op, &Solver::Circuit::performModU);
|
||||
}
|
||||
|
||||
mlir::LogicalResult
|
||||
LogicExporter::Visitor::visitComb(circt::comb::MulOp &op,
|
||||
Solver::Circuit *circuit) {
|
||||
return visitVariadicCombOp(circuit, op, &Solver::Circuit::performMul);
|
||||
}
|
||||
|
||||
mlir::LogicalResult
|
||||
LogicExporter::Visitor::visitComb(circt::comb::MuxOp &op,
|
||||
Solver::Circuit *circuit) {
|
||||
LLVM_DEBUG(lec::dbgs() << "Visiting comb.mux\n");
|
||||
lec::Scope indent;
|
||||
LLVM_DEBUG(debugOperands(op));
|
||||
bool twoState = op.getTwoState();
|
||||
REJECT_N_STATE_LOGIC();
|
||||
auto cond = op.getCond();
|
||||
auto trueValue = op.getTrueValue();
|
||||
auto falseValue = op.getFalseValue();
|
||||
auto result = op.getResult();
|
||||
LLVM_DEBUG(debugOpResult(result));
|
||||
circuit->performMux(result, cond, trueValue, falseValue);
|
||||
return mlir::success();
|
||||
}
|
||||
|
||||
mlir::LogicalResult
|
||||
LogicExporter::Visitor::visitComb(circt::comb::OrOp &op,
|
||||
Solver::Circuit *circuit) {
|
||||
return visitVariadicCombOp(circuit, op, &Solver::Circuit::performOr);
|
||||
}
|
||||
|
||||
mlir::LogicalResult
|
||||
LogicExporter::Visitor::visitComb(circt::comb::ParityOp &op,
|
||||
Solver::Circuit *circuit) {
|
||||
return visitUnaryCombOp(circuit, op, &Solver::Circuit::performParity);
|
||||
}
|
||||
|
||||
mlir::LogicalResult
|
||||
LogicExporter::Visitor::visitComb(circt::comb::ReplicateOp &op,
|
||||
Solver::Circuit *circuit) {
|
||||
LLVM_DEBUG(lec::dbgs() << "Visiting comb.replicate\n");
|
||||
lec::Scope indent;
|
||||
LLVM_DEBUG(debugOperands(op));
|
||||
auto input = op.getInput();
|
||||
auto result = op.getResult();
|
||||
LLVM_DEBUG(debugOpResult(result));
|
||||
circuit->performReplicate(result, input);
|
||||
return mlir::success();
|
||||
}
|
||||
|
||||
mlir::LogicalResult
|
||||
LogicExporter::Visitor::visitComb(circt::comb::ShlOp &op,
|
||||
Solver::Circuit *circuit) {
|
||||
return visitBinaryCombOp(circuit, op, &Solver::Circuit::performShl);
|
||||
}
|
||||
|
||||
mlir::LogicalResult
|
||||
LogicExporter::Visitor::visitComb(circt::comb::ShrSOp &op,
|
||||
Solver::Circuit *circuit) {
|
||||
return visitBinaryCombOp(circuit, op, &Solver::Circuit::performShrS);
|
||||
}
|
||||
|
||||
mlir::LogicalResult
|
||||
LogicExporter::Visitor::visitComb(circt::comb::ShrUOp &op,
|
||||
Solver::Circuit *circuit) {
|
||||
return visitBinaryCombOp(circuit, op, &Solver::Circuit::performShrU);
|
||||
}
|
||||
|
||||
mlir::LogicalResult
|
||||
LogicExporter::Visitor::visitComb(circt::comb::SubOp &op,
|
||||
Solver::Circuit *circuit) {
|
||||
return visitVariadicCombOp(circuit, op, &Solver::Circuit::performSub);
|
||||
}
|
||||
|
||||
mlir::LogicalResult
|
||||
LogicExporter::Visitor::visitComb(circt::comb::XorOp &op,
|
||||
Solver::Circuit *circuit) {
|
||||
return visitVariadicCombOp(circuit, op, &Solver::Circuit::performXor);
|
||||
}
|
||||
|
||||
//===----------------------------------------------------------------------===//
|
||||
// Additional Visitor implementations
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
/// Handles `builtin.module` logic exporting.
|
||||
mlir::LogicalResult
|
||||
LogicExporter::Visitor::visitBuiltin(mlir::ModuleOp &op,
|
||||
Solver::Circuit *circuit,
|
||||
llvm::StringRef targetModule) {
|
||||
LLVM_DEBUG(lec::dbgs() << "Visiting `builtin.module`\n");
|
||||
lec::Scope indent;
|
||||
// Currently only `hw.module` handling is implemented.
|
||||
for (auto hwModule : op.getOps<circt::hw::HWModuleOp>()) {
|
||||
llvm::StringRef moduleName = hwModule.getName();
|
||||
LLVM_DEBUG(lec::dbgs() << "found `hw.module@" << moduleName << "`\n");
|
||||
|
||||
// When no module name is specified the first module encountered is
|
||||
// selected.
|
||||
if (targetModule.empty() || moduleName == targetModule) {
|
||||
lec::Scope indent;
|
||||
LLVM_DEBUG(lec::dbgs() << "proceeding with this module\n");
|
||||
return visitHW(hwModule, circuit);
|
||||
/// Handles `builtin.module` logic exporting.
|
||||
LogicalResult visit(ModuleOp op, llvm::StringRef targetModule) {
|
||||
for (auto hwModule : op.getOps<hw::HWModuleOp>()) {
|
||||
if (targetModule.empty() || hwModule.getName() == targetModule) {
|
||||
LLVM_DEBUG(llvm::dbgs()
|
||||
<< "Using module `" << hwModule.getName() << "`\n");
|
||||
return visit(hwModule);
|
||||
}
|
||||
}
|
||||
op.emitError("module not found");
|
||||
return failure();
|
||||
}
|
||||
op.emitError("expected `" + targetModule + "` module not found");
|
||||
return mlir::failure();
|
||||
}
|
||||
|
||||
/// Handles `hw.module` logic exporting.
|
||||
mlir::LogicalResult LogicExporter::Visitor::visitHW(circt::hw::HWModuleOp &op,
|
||||
Solver::Circuit *circuit) {
|
||||
LLVM_DEBUG(lec::dbgs() << "Visiting `hw.module@" << op.getName() << "`\n");
|
||||
lec::Scope indent;
|
||||
LLVM_DEBUG(debugAttributes(op->getAttrs()));
|
||||
LLVM_DEBUG(lec::dbgs() << "Arguments:\n");
|
||||
for (mlir::BlockArgument argument : op.getArguments()) {
|
||||
lec::Scope indent;
|
||||
LLVM_DEBUG(lec::dbgs() << "Argument\n");
|
||||
{
|
||||
lec::Scope indent;
|
||||
LLVM_DEBUG(lec::printValue(argument));
|
||||
/// Handles `hw.module` logic exporting.
|
||||
LogicalResult visit(hw::HWModuleOp op) {
|
||||
for (auto argument : op.getArguments())
|
||||
circuit->addInput(argument);
|
||||
for (auto &op : op.getOps())
|
||||
if (failed(dispatch(&op)))
|
||||
return failure();
|
||||
return success();
|
||||
}
|
||||
|
||||
LogicalResult visitUnhandledOp(Operation *op) {
|
||||
op->emitOpError("not supported");
|
||||
return failure();
|
||||
}
|
||||
|
||||
/// Dispatches an operation to the appropriate visit function.
|
||||
LogicalResult dispatch(Operation *op) { return dispatchStmtVisitor(op); }
|
||||
|
||||
//===--------------------------------------------------------------------===//
|
||||
// hw::StmtVisitor
|
||||
//===--------------------------------------------------------------------===//
|
||||
|
||||
LogicalResult visitStmt(hw::InstanceOp op) {
|
||||
if (auto hwModule =
|
||||
llvm::dyn_cast<hw::HWModuleOp>(op.getReferencedModule())) {
|
||||
circuit->addInstance(op.getInstanceName(), hwModule, op->getOperands(),
|
||||
op->getResults());
|
||||
return success();
|
||||
}
|
||||
circuit->addInput(argument);
|
||||
op.emitError("instantiated module `" + op.getModuleName() +
|
||||
"` is not an HW module");
|
||||
return failure();
|
||||
}
|
||||
|
||||
// Traverse the module's IR, dispatching the appropriate visiting function.
|
||||
Visitor visitor;
|
||||
for (mlir::Operation &op : op.getOps()) {
|
||||
mlir::LogicalResult outcome = visitor.dispatch(&op, circuit);
|
||||
if (outcome.failed())
|
||||
return outcome;
|
||||
LogicalResult visitStmt(hw::OutputOp op) {
|
||||
for (auto operand : op.getOperands())
|
||||
circuit->addOutput(operand);
|
||||
return success();
|
||||
}
|
||||
|
||||
return mlir::success();
|
||||
LogicalResult visitInvalidStmt(Operation *op) {
|
||||
return dispatchTypeOpVisitor(op);
|
||||
}
|
||||
LogicalResult visitUnhandledStmt(Operation *op) {
|
||||
return visitUnhandledOp(op);
|
||||
}
|
||||
|
||||
//===--------------------------------------------------------------------===//
|
||||
// hw::TypeOpVisitor
|
||||
//===--------------------------------------------------------------------===//
|
||||
|
||||
LogicalResult visitTypeOp(hw::ConstantOp op) {
|
||||
circuit->addConstant(op.getResult(), op.getValue());
|
||||
return success();
|
||||
}
|
||||
|
||||
LogicalResult visitInvalidTypeOp(Operation *op) {
|
||||
return dispatchCombinationalVisitor(op);
|
||||
}
|
||||
LogicalResult visitUnhandledTypeOp(Operation *op) {
|
||||
return visitUnhandledOp(op);
|
||||
}
|
||||
|
||||
//===--------------------------------------------------------------------===//
|
||||
// comb::CombinationalVisitor
|
||||
//===--------------------------------------------------------------------===//
|
||||
|
||||
// Visit a comb operation with a variadic number of operands.
|
||||
template <typename OpTy, typename FnTy>
|
||||
LogicalResult visitVariadicCombOp(OpTy op, FnTy fn) {
|
||||
if (!op.getTwoState())
|
||||
return op.emitOpError("without 'bin' unsupported");
|
||||
(circuit->*fn)(op.getResult(), op.getOperands());
|
||||
return success();
|
||||
}
|
||||
|
||||
// Visit a comb operation with two operands.
|
||||
template <typename OpTy, typename FnTy>
|
||||
LogicalResult visitBinaryCombOp(OpTy op, FnTy fn) {
|
||||
if (!op.getTwoState())
|
||||
return op.emitOpError("without 'bin' unsupported");
|
||||
(circuit->*fn)(op.getResult(), op.getLhs(), op.getRhs());
|
||||
return success();
|
||||
}
|
||||
|
||||
// Visit a comb operation with one operand.
|
||||
template <typename OpTy, typename FnTy>
|
||||
LogicalResult visitUnaryCombOp(OpTy op, FnTy fn) {
|
||||
if (!op.getTwoState())
|
||||
return op.emitOpError("without 'bin' unsupported");
|
||||
(circuit->*fn)(op.getResult(), op.getInput());
|
||||
return success();
|
||||
}
|
||||
|
||||
LogicalResult visitComb(comb::AddOp op) {
|
||||
return visitVariadicCombOp(op, &Solver::Circuit::performAdd);
|
||||
}
|
||||
LogicalResult visitComb(comb::AndOp op) {
|
||||
return visitVariadicCombOp(op, &Solver::Circuit::performAnd);
|
||||
}
|
||||
LogicalResult visitComb(comb::ConcatOp op) {
|
||||
circuit->performConcat(op.getResult(), op.getOperands());
|
||||
return success();
|
||||
}
|
||||
LogicalResult visitComb(comb::DivSOp op) {
|
||||
return visitBinaryCombOp(op, &Solver::Circuit::performDivS);
|
||||
}
|
||||
LogicalResult visitComb(comb::DivUOp op) {
|
||||
return visitBinaryCombOp(op, &Solver::Circuit::performDivU);
|
||||
}
|
||||
LogicalResult visitComb(comb::ExtractOp op) {
|
||||
circuit->performExtract(op.getResult(), op.getInput(), op.getLowBit());
|
||||
return success();
|
||||
}
|
||||
LogicalResult visitComb(comb::ICmpOp op) {
|
||||
if (!op.getTwoState())
|
||||
return op.emitOpError("without 'bin' unsupported");
|
||||
return circuit->performICmp(op.getResult(), op.getPredicate(), op.getLhs(),
|
||||
op.getRhs());
|
||||
}
|
||||
LogicalResult visitComb(comb::ModSOp op) {
|
||||
return visitBinaryCombOp(op, &Solver::Circuit::performModS);
|
||||
}
|
||||
LogicalResult visitComb(comb::ModUOp op) {
|
||||
return visitBinaryCombOp(op, &Solver::Circuit::performModU);
|
||||
}
|
||||
LogicalResult visitComb(comb::MulOp op) {
|
||||
return visitVariadicCombOp(op, &Solver::Circuit::performMul);
|
||||
}
|
||||
LogicalResult visitComb(comb::MuxOp op) {
|
||||
if (!op.getTwoState())
|
||||
return op.emitOpError("without 'bin' unsupported");
|
||||
circuit->performMux(op.getResult(), op.getCond(), op.getTrueValue(),
|
||||
op.getFalseValue());
|
||||
return success();
|
||||
}
|
||||
LogicalResult visitComb(comb::OrOp op) {
|
||||
return visitVariadicCombOp(op, &Solver::Circuit::performOr);
|
||||
}
|
||||
LogicalResult visitComb(comb::ParityOp op) {
|
||||
return visitUnaryCombOp(op, &Solver::Circuit::performParity);
|
||||
}
|
||||
LogicalResult visitComb(comb::ReplicateOp op) {
|
||||
circuit->performReplicate(op.getResult(), op.getInput());
|
||||
return success();
|
||||
}
|
||||
LogicalResult visitComb(comb::ShlOp op) {
|
||||
return visitBinaryCombOp(op, &Solver::Circuit::performShl);
|
||||
}
|
||||
LogicalResult visitComb(comb::ShrSOp op) {
|
||||
return visitBinaryCombOp(op, &Solver::Circuit::performShrS);
|
||||
}
|
||||
LogicalResult visitComb(comb::ShrUOp op) {
|
||||
return visitBinaryCombOp(op, &Solver::Circuit::performShrU);
|
||||
}
|
||||
LogicalResult visitComb(comb::SubOp op) {
|
||||
return visitVariadicCombOp(op, &Solver::Circuit::performSub);
|
||||
}
|
||||
LogicalResult visitComb(comb::XorOp op) {
|
||||
return visitVariadicCombOp(op, &Solver::Circuit::performXor);
|
||||
}
|
||||
|
||||
LogicalResult visitUnhandledComb(Operation *op) {
|
||||
return visitUnhandledOp(op);
|
||||
}
|
||||
};
|
||||
} // namespace
|
||||
|
||||
LogicalResult LogicExporter::run(ModuleOp &builtinModule) {
|
||||
return Visitor(circuit).visit(builtinModule, moduleName);
|
||||
}
|
||||
|
||||
/// Reports a failure whenever an unhandled operation is visited.
|
||||
mlir::LogicalResult
|
||||
LogicExporter::Visitor::visitUnhandledOp(mlir::Operation *op) {
|
||||
return mlir::failure();
|
||||
}
|
||||
|
||||
/// Dispatches an operation to the appropriate visit function.
|
||||
mlir::LogicalResult LogicExporter::Visitor::dispatch(mlir::Operation *op,
|
||||
Solver::Circuit *circuit) {
|
||||
// Attempt dispatching the operation to the StmtVisitor; if it is an invalid
|
||||
// `hw` statement operation, the StmtVisitor will dispatch it to another
|
||||
// visitor, and so on in a chain until it gets dispatched to the appropriate
|
||||
// visitor.
|
||||
return dispatchStmtVisitor(op, circuit);
|
||||
LogicalResult LogicExporter::run(hw::HWModuleOp &module) {
|
||||
return Visitor(circuit).visit(module);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -20,22 +20,25 @@
|
|||
|
||||
#define DEBUG_TYPE "lec-solver"
|
||||
|
||||
Solver::Solver(mlir::MLIRContext *mlirCtx, bool statisticsOpt)
|
||||
using namespace circt;
|
||||
using namespace mlir;
|
||||
|
||||
Solver::Solver(MLIRContext *mlirCtx, bool statisticsOpt)
|
||||
: circuits{}, mlirCtx(mlirCtx), context(), solver(context),
|
||||
statisticsOpt(statisticsOpt) {}
|
||||
|
||||
/// Solve the equivalence problem between the two circuits, then present the
|
||||
/// results to the user.
|
||||
mlir::LogicalResult Solver::solve() {
|
||||
LogicalResult Solver::solve() {
|
||||
// Constrain the circuits for equivalence checking to be made:
|
||||
// require them to produce different outputs starting from the same inputs.
|
||||
if (constrainCircuits().failed())
|
||||
return mlir::failure();
|
||||
return failure();
|
||||
|
||||
// Instruct the logical engine to solve the constraints:
|
||||
// if they can't be satisfied it must mean the two circuits are functionally
|
||||
// equivalent. Otherwise, print a model to act as a counterexample.
|
||||
mlir::LogicalResult outcome = mlir::success();
|
||||
LogicalResult outcome = success();
|
||||
switch (solver.check()) {
|
||||
case z3::unsat:
|
||||
lec::outs() << "c1 == c2\n";
|
||||
|
|
@ -43,10 +46,10 @@ mlir::LogicalResult Solver::solve() {
|
|||
case z3::sat:
|
||||
lec::outs() << "c1 != c2\n";
|
||||
printModel();
|
||||
outcome = mlir::failure();
|
||||
outcome = failure();
|
||||
break;
|
||||
case z3::unknown:
|
||||
outcome = mlir::failure();
|
||||
outcome = failure();
|
||||
lec::errs() << "circt-lec error: solver ran out of time\n";
|
||||
}
|
||||
|
||||
|
|
@ -78,20 +81,20 @@ void Solver::printModel() {
|
|||
lec::Scope indent;
|
||||
z3::model model = solver.get_model();
|
||||
for (unsigned int i = 0; i < model.size(); i++) {
|
||||
// Recover the corresponding mlir::Value for the z3::expression
|
||||
// Recover the corresponding Value for the z3::expression
|
||||
// then emit a remark for its location.
|
||||
z3::func_decl f = model.get_const_decl(i);
|
||||
mlir::Builder builder(mlirCtx);
|
||||
Builder builder(mlirCtx);
|
||||
std::string symbolStr = f.name().str();
|
||||
mlir::StringAttr symbol = builder.getStringAttr(symbolStr);
|
||||
mlir::Value value = symbolTable.find(symbol)->second;
|
||||
StringAttr symbol = builder.getStringAttr(symbolStr);
|
||||
Value value = symbolTable.find(symbol)->second;
|
||||
z3::expr e = model.get_const_interp(f);
|
||||
mlir::emitRemark(value.getLoc(), "");
|
||||
// Explicitly unfolded asm printing for `mlir::Value`.
|
||||
if (auto arg = value.dyn_cast<mlir::BlockArgument>()) {
|
||||
emitRemark(value.getLoc(), "");
|
||||
// Explicitly unfolded asm printing for `Value`.
|
||||
if (auto arg = value.dyn_cast<BlockArgument>()) {
|
||||
// Value is an argument rather than a SSA'ed value of an operation.
|
||||
mlir::Operation *parentOp = value.getParentRegion()->getParentOp();
|
||||
if (auto op = llvm::dyn_cast<circt::hw::HWModuleOp>(parentOp)) {
|
||||
Operation *parentOp = value.getParentRegion()->getParentOp();
|
||||
if (auto op = llvm::dyn_cast<hw::HWModuleOp>(parentOp)) {
|
||||
// Argument of a `hw.module`.
|
||||
lec::outs() << "argument name: " << op.getArgNames()[arg.getArgNumber()]
|
||||
<< "\n";
|
||||
|
|
@ -133,7 +136,7 @@ void Solver::printStatistics() {
|
|||
/// 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.
|
||||
mlir::LogicalResult Solver::constrainCircuits() {
|
||||
LogicalResult Solver::constrainCircuits() {
|
||||
// TODO: Perform these failure checks before nalyzing the whole IR of the
|
||||
// modules during the pass.
|
||||
auto c1Inputs = circuits[0]->getInputs();
|
||||
|
|
@ -144,7 +147,7 @@ mlir::LogicalResult Solver::constrainCircuits() {
|
|||
// Can't compare two circuits with different number of inputs.
|
||||
if (nc1Inputs != nc2Inputs) {
|
||||
lec::errs() << "circt-lec error: different input arity\n";
|
||||
return mlir::failure();
|
||||
return failure();
|
||||
}
|
||||
|
||||
const auto *c1inIt = c1Inputs.begin();
|
||||
|
|
@ -153,7 +156,7 @@ mlir::LogicalResult Solver::constrainCircuits() {
|
|||
// Can't compare two circuits when their ith inputs differ in type.
|
||||
if (c1inIt->get_sort().bv_size() != c2inIt->get_sort().bv_size()) {
|
||||
lec::errs() << "circt-lec error: input #" << i + 1 << " type mismatch\n";
|
||||
return mlir::failure();
|
||||
return failure();
|
||||
}
|
||||
// Their ith inputs have to be equivalent.
|
||||
solver.add(*c1inIt++ == *c2inIt++);
|
||||
|
|
@ -167,7 +170,7 @@ mlir::LogicalResult Solver::constrainCircuits() {
|
|||
// Can't compare two circuits with different number of outputs.
|
||||
if (nc1Outputs != nc2Outputs) {
|
||||
lec::errs() << "circt-lec error: different output arity\n";
|
||||
return mlir::failure();
|
||||
return failure();
|
||||
}
|
||||
|
||||
const auto *c1outIt = c1Outputs.begin();
|
||||
|
|
@ -176,11 +179,11 @@ mlir::LogicalResult Solver::constrainCircuits() {
|
|||
// Can't compare two circuits when their ith outputs differ in type.
|
||||
if (c1outIt->get_sort().bv_size() != c2outIt->get_sort().bv_size()) {
|
||||
lec::errs() << "circt-lec error: output #" << i + 1 << " type mismatch\n";
|
||||
return mlir::failure();
|
||||
return failure();
|
||||
}
|
||||
// Their ith outputs have to be equivalent.
|
||||
solver.add(*c1outIt++ != *c2outIt++);
|
||||
}
|
||||
|
||||
return mlir::success();
|
||||
return success();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -27,6 +27,9 @@
|
|||
|
||||
namespace cl = llvm::cl;
|
||||
|
||||
using namespace mlir;
|
||||
using namespace circt;
|
||||
|
||||
//===----------------------------------------------------------------------===//
|
||||
// Command-line options declaration
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
|
@ -72,22 +75,21 @@ static cl::opt<bool, true> statistics(
|
|||
/// traverses their IR to export the logical constraints from the given circuit
|
||||
/// description to an internal circuit representation, lastly, these will be
|
||||
/// compared and solved for equivalence.
|
||||
static mlir::LogicalResult executeLEC(mlir::MLIRContext &context) {
|
||||
static LogicalResult executeLEC(MLIRContext &context) {
|
||||
// Parse the provided input files.
|
||||
if (verbose)
|
||||
lec::outs() << "Parsing input file\n";
|
||||
mlir::OwningOpRef<mlir::ModuleOp> file1 =
|
||||
mlir::parseSourceFile<mlir::ModuleOp>(fileName1, &context);
|
||||
OwningOpRef<ModuleOp> file1 = parseSourceFile<ModuleOp>(fileName1, &context);
|
||||
if (!file1)
|
||||
return mlir::failure();
|
||||
return failure();
|
||||
|
||||
mlir::OwningOpRef<mlir::ModuleOp> file2;
|
||||
OwningOpRef<ModuleOp> file2;
|
||||
if (!fileName2.empty()) {
|
||||
if (verbose)
|
||||
lec::outs() << "Parsing second input file\n";
|
||||
file2 = mlir::parseSourceFile<mlir::ModuleOp>(fileName2, &context);
|
||||
file2 = parseSourceFile<ModuleOp>(fileName2, &context);
|
||||
if (!file2)
|
||||
return mlir::failure();
|
||||
return failure();
|
||||
} else if (verbose)
|
||||
lec::outs() << "Second input file not specified\n";
|
||||
|
||||
|
|
@ -101,9 +103,9 @@ static mlir::LogicalResult executeLEC(mlir::MLIRContext &context) {
|
|||
if (verbose)
|
||||
lec::outs() << "Analyzing the first circuit\n";
|
||||
auto exporter = std::make_unique<LogicExporter>(moduleName1, c1);
|
||||
mlir::ModuleOp m = file1.get();
|
||||
ModuleOp m = file1.get();
|
||||
if (failed(exporter->run(m)))
|
||||
return mlir::failure();
|
||||
return failure();
|
||||
|
||||
// Repeat the same procedure for the second circuit.
|
||||
if (verbose)
|
||||
|
|
@ -111,9 +113,9 @@ static mlir::LogicalResult executeLEC(mlir::MLIRContext &context) {
|
|||
auto exporter2 = std::make_unique<LogicExporter>(moduleName2, c2);
|
||||
// In case a second input file was not specified, the first input file will
|
||||
// be used instead.
|
||||
mlir::ModuleOp m2 = fileName2.empty() ? m : file2.get();
|
||||
ModuleOp m2 = fileName2.empty() ? m : file2.get();
|
||||
if (failed(exporter2->run(m2)))
|
||||
return mlir::failure();
|
||||
return failure();
|
||||
|
||||
// The logical constraints have been exported to their respective circuit
|
||||
// representations and can now be solved for equivalence.
|
||||
|
|
@ -129,7 +131,7 @@ static mlir::LogicalResult executeLEC(mlir::MLIRContext &context) {
|
|||
int main(int argc, char **argv) {
|
||||
// Configure the relevant command-line options.
|
||||
cl::HideUnrelatedOptions(mainCategory);
|
||||
mlir::registerMLIRContextCLOptions();
|
||||
registerMLIRContextCLOptions();
|
||||
cl::AddExtraVersionPrinter(
|
||||
[](llvm::raw_ostream &os) { os << circt::getCirctVersion() << '\n'; });
|
||||
|
||||
|
|
@ -145,13 +147,13 @@ int main(int argc, char **argv) {
|
|||
llvm::setBugReportMsg(circt::circtBugReportMsg);
|
||||
|
||||
// Register the supported CIRCT dialects and create a context to work with.
|
||||
mlir::DialectRegistry registry;
|
||||
DialectRegistry registry;
|
||||
registry.insert<circt::comb::CombDialect, circt::hw::HWDialect>();
|
||||
mlir::MLIRContext context(registry);
|
||||
MLIRContext context(registry);
|
||||
|
||||
// Setup of diagnostic handling.
|
||||
llvm::SourceMgr sourceMgr;
|
||||
mlir::SourceMgrDiagnosticHandler sourceMgrHandler(sourceMgr, &context);
|
||||
SourceMgrDiagnosticHandler sourceMgrHandler(sourceMgr, &context);
|
||||
// Avoid printing a superfluous note on diagnostic emission.
|
||||
context.printOpOnDiagnostic(false);
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue