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

#include <Circuit.h>

Collaboration diagram for circt::Solver::Circuit:

[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...

Solver &	solver
	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(), inputs, and value.

◆ 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(), outputs, and value.

◆ 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(), lec::printValue(), and value.

◆ 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(), value, 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:

/home/runner/work/circt-www/circt-www/circt_src/include/circt/LogicalEquivalence/Circuit.h
/home/runner/work/circt-www/circt-www/circt_src/lib/LogicalEquivalence/Circuit.cpp

Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

◆ Circuit()

Member Function Documentation

◆ addConstant()

◆ addInput()

◆ addInstance()

◆ addOutput()

◆ allocateConstant()

◆ boolToBv()

◆ bvToBool()

◆ constrainResult()

◆ fetchOrAllocateExpr()

◆ getInputs()

◆ getOutputs()

◆ performAdd()

◆ performAnd()

◆ performConcat()

◆ performDivS()

◆ performDivU()

◆ performExtract()

◆ performICmp()

◆ performModS()

◆ performModU()

◆ performMul()

◆ performMux()

◆ performOr()

◆ performParity()

◆ performReplicate()

◆ performShl()

◆ performShrS()

◆ performShrU()

◆ performSub()

◆ performXor()

◆ variadicOperation()

Member Data Documentation

◆ assignments

◆ exprTable

◆ inputs

◆ name

◆ outputs

◆ solver