CIRCT  19.0.0git
Public Member Functions | Private Member Functions | Private Attributes | List of all members
circt::Solver::Circuit Class Reference

The representation of a circuit within a logical engine. More...

#include <Circuit.h>

Collaboration diagram for circt::Solver::Circuit:
Collaboration graph
[legend]

Public Member Functions

 Circuit (llvm::Twine name, Solver &solver)
 
void addInput (mlir::Value)
 Add an input to the circuit; internally a new value gets allocated. More...
 
void addOutput (mlir::Value)
 Add an output to the circuit. More...
 
llvm::ArrayRef< z3::expr > getInputs ()
 Recover the inputs. More...
 
llvm::ArrayRef< z3::expr > getOutputs ()
 Recover the outputs. More...
 
void addConstant (mlir::Value result, const mlir::APInt &value)
 
void addInstance (llvm::StringRef instanceName, circt::hw::HWModuleOp op, mlir::OperandRange arguments, mlir::ResultRange results)
 
void performAdd (mlir::Value result, mlir::OperandRange operands)
 
void performAnd (mlir::Value result, mlir::OperandRange operands)
 
void performConcat (mlir::Value result, mlir::OperandRange operands)
 
void performDivS (mlir::Value result, mlir::Value lhs, mlir::Value rhs)
 
void performDivU (mlir::Value result, mlir::Value lhs, mlir::Value rhs)
 
void performExtract (mlir::Value result, mlir::Value input, uint32_t lowBit)
 
mlir::LogicalResult performICmp (mlir::Value result, circt::comb::ICmpPredicate predicate, mlir::Value lhs, mlir::Value rhs)
 
void performModS (mlir::Value result, mlir::Value lhs, mlir::Value rhs)
 
void performModU (mlir::Value result, mlir::Value lhs, mlir::Value rhs)
 
void performMul (mlir::Value result, mlir::OperandRange operands)
 
void performMux (mlir::Value result, mlir::Value cond, mlir::Value trueValue, mlir::Value falseValue)
 
void performOr (mlir::Value result, mlir::OperandRange operands)
 
void performParity (mlir::Value result, mlir::Value input)
 
void performReplicate (mlir::Value result, mlir::Value input)
 
void performShl (mlir::Value result, mlir::Value lhs, mlir::Value rhs)
 
void performShrS (mlir::Value result, mlir::Value lhs, mlir::Value rhs)
 
void performShrU (mlir::Value result, mlir::Value lhs, mlir::Value rhs)
 
void performSub (mlir::Value result, mlir::OperandRange operands)
 
void performXor (mlir::Value result, mlir::OperandRange operands)
 

Private Member Functions

void variadicOperation (mlir::Value result, mlir::OperandRange operands, llvm::function_ref< z3::expr(const z3::expr &, const z3::expr &)> operation)
 Helper function for performing a variadic operation: it executes a lambda over a range of operands. More...
 
z3::expr fetchOrAllocateExpr (mlir::Value value)
 Returns the expression allocated for the input value in the logical backend if one has been allocated - otherwise allocates and returns a new expression. More...
 
void allocateConstant (mlir::Value opResult, const mlir::APInt &opValue)
 Allocates a constant value in the logical backend and returns its representing expression. More...
 
void constrainResult (mlir::Value &result, z3::expr &expr)
 Constrains the result of a MLIR operation to be equal a given logical express, simulating an assignment. More...
 
z3::expr bvToBool (const z3::expr &condition)
 Convert from bitvector to bool sort. More...
 
z3::expr boolToBv (const z3::expr &condition)
 Convert from a boolean sort to the corresponding 1-width bitvector. More...
 

Private Attributes

std::string name
 The name of the circuit; it corresponds to its scope within the parsed IR. More...
 
unsigned assignments
 A counter for how many assignments have occurred; it's used to uniquely name new values as they have to be represented within the logical engine's context. More...
 
Solversolver
 The solver environment the circuit belongs to. More...
 
llvm::SmallVector< z3::expr > inputs
 The list for the circuit's inputs. More...
 
llvm::SmallVector< z3::expr > outputs
 The list for the circuit's outputs. More...
 
llvm::DenseMap< mlir::Value, z3::expr > exprTable
 A map from IR values to their corresponding logical representation. More...
 

Detailed Description

The representation of a circuit within a logical engine.

This class defines a circuit as an abstraction of its underlying logical constraints. Its various methods act in a builder pattern fashion, declaring new constraints over a Z3 context.

Definition at line 35 of file Circuit.h.

Constructor & Destructor Documentation

◆ Circuit()

circt::Solver::Circuit::Circuit ( llvm::Twine  name,
Solver solver 
)
inline

Definition at line 37 of file Circuit.h.

References assignments.

Member Function Documentation

◆ addConstant()

void Solver::Circuit::addConstant ( mlir::Value  result,
const mlir::APInt &  value 
)

Definition at line 52 of file Circuit.cpp.

References lec::dbgs().

◆ addInput()

void Solver::Circuit::addInput ( mlir::Value  )

Add an input to the circuit; internally a new value gets allocated.

Definition at line 27 of file Circuit.cpp.

References lec::dbgs(), and inputs.

◆ addInstance()

void Solver::Circuit::addInstance ( llvm::StringRef  instanceName,
circt::hw::HWModuleOp  op,
mlir::OperandRange  arguments,
mlir::ResultRange  results 
)

Definition at line 58 of file Circuit.cpp.

References assert(), lec::dbgs(), inputs, outputs, and circt::LogicExporter::run().

◆ addOutput()

void Solver::Circuit::addOutput ( mlir::Value  )

Add an output to the circuit.

Definition at line 35 of file Circuit.cpp.

References lec::dbgs(), and outputs.

◆ allocateConstant()

void Solver::Circuit::allocateConstant ( mlir::Value  opResult,
const mlir::APInt &  opValue 
)
private

Allocates a constant value in the logical backend and returns its representing expression.

Definition at line 421 of file Circuit.cpp.

References assert(), lec::dbgs(), lec::printExpr(), and lec::printValue().

◆ boolToBv()

z3::expr Solver::Circuit::boolToBv ( const z3::expr &  condition)
private

Convert from a boolean sort to the corresponding 1-width bitvector.

Definition at line 474 of file Circuit.cpp.

◆ bvToBool()

z3::expr Solver::Circuit::bvToBool ( const z3::expr &  condition)
private

Convert from bitvector to bool sort.

Definition at line 468 of file Circuit.cpp.

◆ constrainResult()

void Solver::Circuit::constrainResult ( mlir::Value &  result,
z3::expr &  expr 
)
private

Constrains the result of a MLIR operation to be equal a given logical express, simulating an assignment.

Definition at line 449 of file Circuit.cpp.

References lec::dbgs(), and lec::printExpr().

◆ fetchOrAllocateExpr()

z3::expr Solver::Circuit::fetchOrAllocateExpr ( mlir::Value  value)
private

Returns the expression allocated for the input value in the logical backend if one has been allocated - otherwise allocates and returns a new expression.

Allocates an IR value in the logical backend and returns its representing expression.

Definition at line 385 of file Circuit.cpp.

References assert(), builder, lec::dbgs(), lec::printExpr(), lec::printValue(), valueName(), and width.

◆ getInputs()

llvm::ArrayRef< z3::expr > Solver::Circuit::getInputs ( )

Recover the inputs.

Definition at line 43 of file Circuit.cpp.

References inputs.

Referenced by circt::Solver::constrainCircuits().

◆ getOutputs()

llvm::ArrayRef< z3::expr > Solver::Circuit::getOutputs ( )

Recover the outputs.

Definition at line 46 of file Circuit.cpp.

References outputs.

Referenced by circt::Solver::constrainCircuits().

◆ performAdd()

void Solver::Circuit::performAdd ( mlir::Value  result,
mlir::OperandRange  operands 
)

Definition at line 102 of file Circuit.cpp.

References lec::dbgs().

◆ performAnd()

void Solver::Circuit::performAnd ( mlir::Value  result,
mlir::OperandRange  operands 
)

Definition at line 109 of file Circuit.cpp.

References lec::dbgs().

◆ performConcat()

void Solver::Circuit::performConcat ( mlir::Value  result,
mlir::OperandRange  operands 
)

Definition at line 116 of file Circuit.cpp.

References concat(), and lec::dbgs().

◆ performDivS()

void Solver::Circuit::performDivS ( mlir::Value  result,
mlir::Value  lhs,
mlir::Value  rhs 
)

Definition at line 123 of file Circuit.cpp.

References lec::dbgs().

◆ performDivU()

void Solver::Circuit::performDivU ( mlir::Value  result,
mlir::Value  lhs,
mlir::Value  rhs 
)

Definition at line 134 of file Circuit.cpp.

References lec::dbgs().

◆ performExtract()

void Solver::Circuit::performExtract ( mlir::Value  result,
mlir::Value  input,
uint32_t  lowBit 
)

Definition at line 145 of file Circuit.cpp.

References lec::dbgs(), and width.

◆ performICmp()

LogicalResult Solver::Circuit::performICmp ( mlir::Value  result,
circt::comb::ICmpPredicate  predicate,
mlir::Value  lhs,
mlir::Value  rhs 
)

Definition at line 157 of file Circuit.cpp.

References lec::dbgs().

◆ performModS()

void Solver::Circuit::performModS ( mlir::Value  result,
mlir::Value  lhs,
mlir::Value  rhs 
)

Definition at line 213 of file Circuit.cpp.

References lec::dbgs().

◆ performModU()

void Solver::Circuit::performModU ( mlir::Value  result,
mlir::Value  lhs,
mlir::Value  rhs 
)

Definition at line 224 of file Circuit.cpp.

References lec::dbgs().

◆ performMul()

void Solver::Circuit::performMul ( mlir::Value  result,
mlir::OperandRange  operands 
)

Definition at line 235 of file Circuit.cpp.

References lec::dbgs().

◆ performMux()

void Solver::Circuit::performMux ( mlir::Value  result,
mlir::Value  cond,
mlir::Value  trueValue,
mlir::Value  falseValue 
)

Definition at line 242 of file Circuit.cpp.

References lec::dbgs().

◆ performOr()

void Solver::Circuit::performOr ( mlir::Value  result,
mlir::OperandRange  operands 
)

Definition at line 257 of file Circuit.cpp.

References lec::dbgs().

◆ performParity()

void Solver::Circuit::performParity ( mlir::Value  result,
mlir::Value  input 
)

Definition at line 264 of file Circuit.cpp.

References lec::dbgs(), and width.

◆ performReplicate()

void Solver::Circuit::performReplicate ( mlir::Value  result,
mlir::Value  input 
)

Definition at line 282 of file Circuit.cpp.

References concat(), and lec::dbgs().

◆ performShl()

void Solver::Circuit::performShl ( mlir::Value  result,
mlir::Value  lhs,
mlir::Value  rhs 
)

Definition at line 301 of file Circuit.cpp.

References lec::dbgs().

◆ performShrS()

void Solver::Circuit::performShrS ( mlir::Value  result,
mlir::Value  lhs,
mlir::Value  rhs 
)

Definition at line 313 of file Circuit.cpp.

References lec::dbgs().

◆ performShrU()

void Solver::Circuit::performShrU ( mlir::Value  result,
mlir::Value  lhs,
mlir::Value  rhs 
)

Definition at line 325 of file Circuit.cpp.

References lec::dbgs().

◆ performSub()

void Solver::Circuit::performSub ( mlir::Value  result,
mlir::OperandRange  operands 
)

Definition at line 336 of file Circuit.cpp.

References lec::dbgs().

◆ performXor()

void Solver::Circuit::performXor ( mlir::Value  result,
mlir::OperandRange  operands 
)

Definition at line 343 of file Circuit.cpp.

References lec::dbgs().

◆ variadicOperation()

void Solver::Circuit::variadicOperation ( mlir::Value  result,
mlir::OperandRange  operands,
llvm::function_ref< z3::expr(const z3::expr &, const z3::expr &)>  operation 
)
private

Helper function for performing a variadic operation: it executes a lambda over a range of operands.

Definition at line 352 of file Circuit.cpp.

References lec::dbgs(), and lec::printValue().

Member Data Documentation

◆ assignments

unsigned circt::Solver::Circuit::assignments
private

A counter for how many assignments have occurred; it's used to uniquely name new values as they have to be represented within the logical engine's context.

Definition at line 106 of file Circuit.h.

Referenced by Circuit().

◆ exprTable

llvm::DenseMap<mlir::Value, z3::expr> circt::Solver::Circuit::exprTable
private

A map from IR values to their corresponding logical representation.

Definition at line 114 of file Circuit.h.

◆ inputs

llvm::SmallVector<z3::expr> circt::Solver::Circuit::inputs
private

The list for the circuit's inputs.

Definition at line 110 of file Circuit.h.

Referenced by addInstance().

◆ name

std::string circt::Solver::Circuit::name
private

The name of the circuit; it corresponds to its scope within the parsed IR.

Definition at line 102 of file Circuit.h.

◆ outputs

llvm::SmallVector<z3::expr> circt::Solver::Circuit::outputs
private

The list for the circuit's outputs.

Definition at line 112 of file Circuit.h.

Referenced by addInstance().

◆ solver

Solver& circt::Solver::Circuit::solver
private

The solver environment the circuit belongs to.

Definition at line 108 of file Circuit.h.


The documentation for this class was generated from the following files: