CIRCT  19.0.0git
Circuit.h
Go to the documentation of this file.
1 //===-- Circuit.h - intermediate representation for circuits ----*- C++ -*-===//
2 //
3 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4 // See https://llvm.org/LICENSE.txt for license information.
5 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6 //
7 //===----------------------------------------------------------------------===//
8 ///
9 /// This file defines an intermediate representation for circuits acting as
10 /// an abstraction for constraints defined over an SMT's solver context.
11 ///
12 //===----------------------------------------------------------------------===//
13 
14 // NOLINTNEXTLINE
15 #ifndef TOOLS_CIRCT_LEC_CIRCUIT_H
16 #define TOOLS_CIRCT_LEC_CIRCUIT_H
17 
18 #include "Solver.h"
20 #include "circt/Dialect/HW/HWOps.h"
21 #include "circt/Support/LLVM.h"
22 #include "mlir/IR/Value.h"
23 #include "llvm/ADT/StringRef.h"
24 #include "llvm/ADT/Twine.h"
25 #include <string>
26 #include <z3++.h>
27 
28 namespace circt {
29 
30 /// The representation of a circuit within a logical engine.
31 ///
32 /// This class defines a circuit as an abstraction of its underlying
33 /// logical constraints. Its various methods act in a builder pattern fashion,
34 /// declaring new constraints over a Z3 context.
36 public:
37  Circuit(llvm::Twine name, Solver &solver) : name(name.str()), solver(solver) {
38  assignments = 0;
39  };
40  /// Add an input to the circuit; internally a new value gets allocated.
41  void addInput(mlir::Value);
42  /// Add an output to the circuit.
43  void addOutput(mlir::Value);
44  /// Recover the inputs.
45  llvm::ArrayRef<z3::expr> getInputs();
46  /// Recover the outputs.
47  llvm::ArrayRef<z3::expr> getOutputs();
48 
49  // `hw` dialect operations.
50  void addConstant(mlir::Value result, const mlir::APInt &value);
51  void addInstance(llvm::StringRef instanceName, circt::hw::HWModuleOp op,
52  mlir::OperandRange arguments, mlir::ResultRange results);
53 
54  // `comb` dialect operations.
55  void performAdd(mlir::Value result, mlir::OperandRange operands);
56  void performAnd(mlir::Value result, mlir::OperandRange operands);
57  void performConcat(mlir::Value result, mlir::OperandRange operands);
58  void performDivS(mlir::Value result, mlir::Value lhs, mlir::Value rhs);
59  void performDivU(mlir::Value result, mlir::Value lhs, mlir::Value rhs);
60  void performExtract(mlir::Value result, mlir::Value input, uint32_t lowBit);
61  mlir::LogicalResult performICmp(mlir::Value result,
62  circt::comb::ICmpPredicate predicate,
63  mlir::Value lhs, mlir::Value rhs);
64  void performModS(mlir::Value result, mlir::Value lhs, mlir::Value rhs);
65  void performModU(mlir::Value result, mlir::Value lhs, mlir::Value rhs);
66  void performMul(mlir::Value result, mlir::OperandRange operands);
67  void performMux(mlir::Value result, mlir::Value cond, mlir::Value trueValue,
68  mlir::Value falseValue);
69  void performOr(mlir::Value result, mlir::OperandRange operands);
70  void performParity(mlir::Value result, mlir::Value input);
71  void performReplicate(mlir::Value result, mlir::Value input);
72  void performShl(mlir::Value result, mlir::Value lhs, mlir::Value rhs);
73  void performShrS(mlir::Value result, mlir::Value lhs, mlir::Value rhs);
74  void performShrU(mlir::Value result, mlir::Value lhs, mlir::Value rhs);
75  void performSub(mlir::Value result, mlir::OperandRange operands);
76  void performXor(mlir::Value result, mlir::OperandRange operands);
77 
78 private:
79  /// Helper function for performing a variadic operation: it executes a lambda
80  /// over a range of operands.
81  void variadicOperation(
82  mlir::Value result, mlir::OperandRange operands,
83  llvm::function_ref<z3::expr(const z3::expr &, const z3::expr &)>
84  operation);
85  /// Returns the expression allocated for the input value in the logical
86  /// backend if one has been allocated - otherwise allocates and returns a new
87  /// expression
88  z3::expr fetchOrAllocateExpr(mlir::Value value);
89  /// Allocates a constant value in the logical backend and returns its
90  /// representing expression.
91  void allocateConstant(mlir::Value opResult, const mlir::APInt &opValue);
92  /// Constrains the result of a MLIR operation to be equal a given logical
93  /// express, simulating an assignment.
94  void constrainResult(mlir::Value &result, z3::expr &expr);
95 
96  /// Convert from bitvector to bool sort.
97  z3::expr bvToBool(const z3::expr &condition);
98  /// Convert from a boolean sort to the corresponding 1-width bitvector.
99  z3::expr boolToBv(const z3::expr &condition);
100 
101  /// The name of the circuit; it corresponds to its scope within the parsed IR.
102  std::string name;
103  /// A counter for how many assignments have occurred; it's used to uniquely
104  /// name new values as they have to be represented within the logical engine's
105  /// context.
106  unsigned assignments;
107  /// The solver environment the circuit belongs to.
109  /// The list for the circuit's inputs.
110  llvm::SmallVector<z3::expr> inputs;
111  /// The list for the circuit's outputs.
112  llvm::SmallVector<z3::expr> outputs;
113  /// A map from IR values to their corresponding logical representation.
114  llvm::DenseMap<mlir::Value, z3::expr> exprTable;
115 };
116 
117 } // namespace circt
118 
119 #endif // TOOLS_CIRCT_LEC_CIRCUIT_H
The representation of a circuit within a logical engine.
Definition: Circuit.h:35
z3::expr fetchOrAllocateExpr(mlir::Value value)
Returns the expression allocated for the input value in the logical backend if one has been allocated...
Definition: Circuit.cpp:385
llvm::ArrayRef< z3::expr > getOutputs()
Recover the outputs.
Definition: Circuit.cpp:46
void performConcat(mlir::Value result, mlir::OperandRange operands)
Definition: Circuit.cpp:116
void performAdd(mlir::Value result, mlir::OperandRange operands)
Definition: Circuit.cpp:102
void performParity(mlir::Value result, mlir::Value input)
Definition: Circuit.cpp:264
llvm::DenseMap< mlir::Value, z3::expr > exprTable
A map from IR values to their corresponding logical representation.
Definition: Circuit.h:114
z3::expr bvToBool(const z3::expr &condition)
Convert from bitvector to bool sort.
Definition: Circuit.cpp:468
void performShl(mlir::Value result, mlir::Value lhs, mlir::Value rhs)
Definition: Circuit.cpp:301
std::string name
The name of the circuit; it corresponds to its scope within the parsed IR.
Definition: Circuit.h:102
void addInstance(llvm::StringRef instanceName, circt::hw::HWModuleOp op, mlir::OperandRange arguments, mlir::ResultRange results)
Definition: Circuit.cpp:58
void performMux(mlir::Value result, mlir::Value cond, mlir::Value trueValue, mlir::Value falseValue)
Definition: Circuit.cpp:242
mlir::LogicalResult performICmp(mlir::Value result, circt::comb::ICmpPredicate predicate, mlir::Value lhs, mlir::Value rhs)
Definition: Circuit.cpp:157
void performOr(mlir::Value result, mlir::OperandRange operands)
Definition: Circuit.cpp:257
void performXor(mlir::Value result, mlir::OperandRange operands)
Definition: Circuit.cpp:343
void allocateConstant(mlir::Value opResult, const mlir::APInt &opValue)
Allocates a constant value in the logical backend and returns its representing expression.
Definition: Circuit.cpp:421
void performShrS(mlir::Value result, mlir::Value lhs, mlir::Value rhs)
Definition: Circuit.cpp:313
llvm::ArrayRef< z3::expr > getInputs()
Recover the inputs.
Definition: Circuit.cpp:43
void performMul(mlir::Value result, mlir::OperandRange operands)
Definition: Circuit.cpp:235
void performSub(mlir::Value result, mlir::OperandRange operands)
Definition: Circuit.cpp:336
llvm::SmallVector< z3::expr > outputs
The list for the circuit's outputs.
Definition: Circuit.h:112
void performDivU(mlir::Value result, mlir::Value lhs, mlir::Value rhs)
Definition: Circuit.cpp:134
void addConstant(mlir::Value result, const mlir::APInt &value)
Definition: Circuit.cpp:52
llvm::SmallVector< z3::expr > inputs
The list for the circuit's inputs.
Definition: Circuit.h:110
void performAnd(mlir::Value result, mlir::OperandRange operands)
Definition: Circuit.cpp:109
Solver & solver
The solver environment the circuit belongs to.
Definition: Circuit.h:108
void addInput(mlir::Value)
Add an input to the circuit; internally a new value gets allocated.
Definition: Circuit.cpp:27
void performExtract(mlir::Value result, mlir::Value input, uint32_t lowBit)
Definition: Circuit.cpp:145
unsigned assignments
A counter for how many assignments have occurred; it's used to uniquely name new values as they have ...
Definition: Circuit.h:106
void performModS(mlir::Value result, mlir::Value lhs, mlir::Value rhs)
Definition: Circuit.cpp:213
void performReplicate(mlir::Value result, mlir::Value input)
Definition: Circuit.cpp:282
void performShrU(mlir::Value result, mlir::Value lhs, mlir::Value rhs)
Definition: Circuit.cpp:325
void performModU(mlir::Value result, mlir::Value lhs, mlir::Value rhs)
Definition: Circuit.cpp:224
void constrainResult(mlir::Value &result, z3::expr &expr)
Constrains the result of a MLIR operation to be equal a given logical express, simulating an assignme...
Definition: Circuit.cpp:449
void addOutput(mlir::Value)
Add an output to the circuit.
Definition: Circuit.cpp:35
void performDivS(mlir::Value result, mlir::Value lhs, mlir::Value rhs)
Definition: Circuit.cpp:123
Circuit(llvm::Twine name, Solver &solver)
Definition: Circuit.h:37
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.
Definition: Circuit.cpp:352
z3::expr boolToBv(const z3::expr &condition)
Convert from a boolean sort to the corresponding 1-width bitvector.
Definition: Circuit.cpp:474
A satisfiability checker for circuit equivalence.
Definition: Solver.h:31
This file defines an intermediate representation for circuits acting as an abstraction for constraint...
Definition: DebugAnalysis.h:21