terapines
/
circt
mirror of https://github.com/llvm/circt.git
2
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

[circt-bmc] Support `seq.firreg` with sync reset (#8698) 

This adds support for seq.firreg with synchronous reset in ExternalizeRegistersPass.
This commit is contained in:
Yicheng Liu 2025-07-22 00:34:37 +08:00 committed by GitHub
parent 888e6787e4
commit 331820d6d0
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
4 changed files with 158 additions and 46 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
integration_test/circt-bmc/seq.mlir
View File

@ -70,3 +70,18 @@ hw.module @Counter_with_reset(in %clk: !seq.clock, in %rst: i1, out count: i3) {
verif.assert %neq : i1
hw.output %reg : i3
}
// Check that reset of firreg can be triggered
// RUN: circt-bmc %s -b 4 --module Counter_with_firreg_sync_reset --shared-libs=%libz3 | FileCheck %s --check-prefix=FIRREGRESET
// FIRREGRESET: Assertion can be violated!
hw.module @Counter_with_firreg_sync_reset(in %clk: !seq.clock, in %rst: i1, out count: i3) {
%c0_i3 = hw.constant 0 : i3
%c1_i3 = hw.constant 1 : i3
%regPlusOne = comb.add %reg, %c1_i3 : i3
%reg = seq.firreg %regPlusOne clock %clk reset sync %rst, %c0_i3 preset 1 : i3
%neq = comb.icmp bin ne %reg, %c0_i3 : i3
// Assertion will be violated if the reset is triggered
verif.assert %neq : i1
hw.output %reg : i3
}

130
lib/Tools/circt-bmc/ExternalizeRegisters.cpp
View File

@ -43,17 +43,23 @@ struct ExternalizeRegistersPass
: public circt::impl::ExternalizeRegistersBase<ExternalizeRegistersPass> {
using ExternalizeRegistersBase::ExternalizeRegistersBase;
void runOnOperation() override;
private:
DenseMap<StringAttr, SmallVector<Type>> addedInputs;
DenseMap<StringAttr, SmallVector<StringAttr>> addedInputNames;
DenseMap<StringAttr, SmallVector<Type>> addedOutputs;
DenseMap<StringAttr, SmallVector<StringAttr>> addedOutputNames;
DenseMap<StringAttr, SmallVector<Attribute>> initialValues;
LogicalResult externalizeReg(HWModuleOp module, Operation *op, Twine regName,
Value clock, Attribute initState, Value reset,
bool isAsync, Value resetValue, Value next);
};
} // namespace
void ExternalizeRegistersPass::runOnOperation() {
auto &instanceGraph = getAnalysis<hw::InstanceGraph>();
DenseSet<Operation *> handled;
DenseMap<StringAttr, SmallVector<Type>> addedInputs;
DenseMap<StringAttr, SmallVector<StringAttr>> addedInputNames;
DenseMap<StringAttr, SmallVector<Type>> addedOutputs;
DenseMap<StringAttr, SmallVector<StringAttr>> addedOutputNames;
DenseMap<StringAttr, SmallVector<Attribute>> initialValues;
// Iterate over all instances in the instance graph. This ensures we visit
// every module, even private top modules (private and never instantiated).
@ -86,12 +92,7 @@ void ExternalizeRegistersPass::runOnOperation() {
}
module->walk([&](Operation *op) {
if (auto regOp = dyn_cast<seq::CompRegOp>(op)) {
if (!isa<BlockArgument>(regOp.getClk())) {
regOp.emitError("only clocks directly given as block arguments "
"are supported");
return signalPassFailure();
}
mlir::Attribute initState;
mlir::Attribute initState = {};
if (auto initVal = regOp.getInitialValue()) {
// Find the constant op that defines the reset value in an initial
// block (if it exists)
@ -111,40 +112,36 @@ void ExternalizeRegistersPass::runOnOperation() {
"not yet supported");
return signalPassFailure();
}
} else {
// If there's no initial value just add a unit attribute to maintain
// one-to-one correspondence with module ports
initState = mlir::UnitAttr::get(&getContext());
}
addedInputs[module.getSymNameAttr()].push_back(regOp.getType());
addedOutputs[module.getSymNameAttr()].push_back(
regOp.getInput().getType());
OpBuilder builder(regOp);
auto regName = regOp.getName();
StringAttr newInputName, newOutputName;
if (regName && !regName.value().empty()) {
newInputName = builder.getStringAttr(regName.value() + "_state");
newOutputName = builder.getStringAttr(regName.value() + "_input");
} else {
newInputName =
builder.getStringAttr("reg_" + Twine(numRegs) + "_state");
newOutputName =
builder.getStringAttr("reg_" + Twine(numRegs) + "_input");
}
addedInputNames[module.getSymNameAttr()].push_back(newInputName);
addedOutputNames[module.getSymNameAttr()].push_back(newOutputName);
initialValues[module.getSymNameAttr()].push_back(initState);
Twine regName = regOp.getName() && !(regOp.getName().value().empty())
? regOp.getName().value()
: "reg_" + Twine(numRegs);
regOp.getResult().replaceAllUsesWith(
module.appendInput(newInputName, regOp.getType()).second);
if (auto reset = regOp.getReset()) {
auto resetValue = regOp.getResetValue();
auto mux = builder.create<comb::MuxOp>(
regOp.getLoc(), regOp.getType(), reset, resetValue,
regOp.getInput());
module.appendOutput(newOutputName, mux);
} else {
module.appendOutput(newOutputName, regOp.getInput());
if (failed(externalizeReg(module, op, regName, regOp.getClk(),
initState, regOp.getReset(), false,
regOp.getResetValue(), regOp.getInput()))) {
return signalPassFailure();
}
regOp->erase();
++numRegs;
return;
}
if (auto regOp = dyn_cast<seq::FirRegOp>(op)) {
mlir::Attribute initState = {};
if (auto preset = regOp.getPreset()) {
// Get preset value as initState
initState = mlir::IntegerAttr::get(
mlir::IntegerType::get(&getContext(), preset->getBitWidth()),
*preset);
}
Twine regName = regOp.getName().empty() ? "reg_" + Twine(numRegs)
: regOp.getName();
if (failed(externalizeReg(module, op, regName, regOp.getClk(),
initState, regOp.getReset(),
regOp.getIsAsync(), regOp.getResetValue(),
regOp.getNext()))) {
return signalPassFailure();
}
regOp->erase();
++numRegs;
@ -210,3 +207,50 @@ void ExternalizeRegistersPass::runOnOperation() {
}
}
}
LogicalResult ExternalizeRegistersPass::externalizeReg(
HWModuleOp module, Operation *op, Twine regName, Value clock,
Attribute initState, Value reset, bool isAsync, Value resetValue,
Value next) {
if (!isa<BlockArgument>(clock)) {
op->emitError("only clocks directly given as block arguments "
"are supported");
return failure();
}
OpBuilder builder(op);
auto result = op->getResult(0);
auto regType = result.getType();
// If there's no initial value just add a unit attribute to maintain
// one-to-one correspondence with module ports
initialValues[module.getSymNameAttr()].push_back(
initState ? initState : mlir::UnitAttr::get(&getContext()));
StringAttr newInputName(builder.getStringAttr(regName + "_state")),
newOutputName(builder.getStringAttr(regName + "_next"));
addedInputs[module.getSymNameAttr()].push_back(regType);
addedInputNames[module.getSymNameAttr()].push_back(newInputName);
addedOutputs[module.getSymNameAttr()].push_back(next.getType());
addedOutputNames[module.getSymNameAttr()].push_back(newOutputName);
// Replace the register with newInput and newOutput
auto newInput = module.appendInput(newInputName, regType).second;
result.replaceAllUsesWith(newInput);
if (reset) {
if (isAsync) {
// Async reset
op->emitError("registers with an async reset are not yet supported");
return failure();
}
// Sync reset
auto mux = builder.create<comb::MuxOp>(op->getLoc(), regType, reset,
resetValue, next);
module.appendOutput(newOutputName, mux);
} else {
// No reset
module.appendOutput(newOutputName, next);
}
return success();
}

8
test/Tools/circt-bmc/externalize-registers-errors.mlir
View File

@ -54,3 +54,11 @@ hw.module @reg_with_instance_initial(in %clk: !seq.clock, in %in: i32, out out:
%1 = seq.compreg %in, %clk initial %init : i32
hw.output %1 : i32
}
// -----
hw.module @firreg_with_async_reset(in %clk: !seq.clock, in %rst: i1, in %in: i32, out out: i32) {
%c0_i32 = hw.constant 0 : i32
// expected-error @below {{registers with an async reset are not yet supported}}
%1 = seq.firreg %in clock %clk reset async %rst, %c0_i32 : i32
hw.output %1 : i32
}

51
test/Tools/circt-bmc/externalize-registers.mlir
View File

@ -58,8 +58,8 @@ hw.module @nested_reg(in %clk: !seq.clock, in %in0: i32, in %in1: i32, out out:
hw.output %0 : i32
}
// CHECK: hw.module @nested_nested_reg(in [[CLK:%.+]] : !seq.clock, in [[IN0:%.+]] : i32, in [[IN1:%.+]] : i32, in %single_reg_state : i32, in %top_reg_state : i32, out {{.+}} : i32, out single_reg_input : i32, out top_reg_input : i32) attributes {initial_values = [0 : i32, unit], num_regs = 2 : i32} {
// CHECK: [[INSTOUT:%.+]], [[INSTREG:%.+]] = hw.instance "nested_reg" @nested_reg(clk: [[CLK]]: !seq.clock, in0: [[IN0]]: i32, in1: [[IN1]]: i32, single_reg_state: %single_reg_state: i32) -> ({{.+}}: i32, single_reg_input: i32)
// CHECK: hw.module @nested_nested_reg(in [[CLK:%.+]] : !seq.clock, in [[IN0:%.+]] : i32, in [[IN1:%.+]] : i32, in %single_reg_state : i32, in %top_reg_state : i32, out {{.+}} : i32, out single_reg_next : i32, out top_reg_next : i32) attributes {initial_values = [0 : i32, unit], num_regs = 2 : i32} {
// CHECK: [[INSTOUT:%.+]], [[INSTREG:%.+]] = hw.instance "nested_reg" @nested_reg(clk: [[CLK]]: !seq.clock, in0: [[IN0]]: i32, in1: [[IN1]]: i32, single_reg_state: %single_reg_state: i32) -> ({{.+}}: i32, single_reg_next: i32)
// CHECK: hw.output %top_reg_state, [[INSTREG]], [[INSTOUT]]
// CHECK: }
hw.module @nested_nested_reg(in %clk: !seq.clock, in %in0: i32, in %in1: i32, out out: i32) {
@ -68,7 +68,7 @@ hw.module @nested_nested_reg(in %clk: !seq.clock, in %in0: i32, in %in1: i32, ou
hw.output %top_reg : i32
}
// CHECK: hw.module @different_initial_values(in [[CLK:%.+]] : !seq.clock, in [[IN:%.+]] : i32, in %reg0_state : i32, in %reg1_state : i32, in %reg2_state : i32, out reg0_input : i32, out reg1_input : i32, out reg2_input : i32) attributes {initial_values = [0 : i32, 42 : i32, unit], num_regs = 3 : i32} {
// CHECK: hw.module @different_initial_values(in [[CLK:%.+]] : !seq.clock, in [[IN:%.+]] : i32, in %reg0_state : i32, in %reg1_state : i32, in %reg2_state : i32, out reg0_next : i32, out reg1_next : i32, out reg2_next : i32) attributes {initial_values = [0 : i32, 42 : i32, unit], num_regs = 3 : i32} {
// CHECK: [[INITIAL:%.+]]:2 = seq.initial() {
// CHECK: [[C0_I32:%.+]] = hw.constant 0 : i32
// CHECK: [[C42_I32:%.+]] = hw.constant 42 : i32
@ -98,3 +98,48 @@ hw.module @reg_with_reset(in %clk: !seq.clock, in %rst: i1, in %in: i32, out out
%1 = seq.compreg %in, %clk reset %rst, %c0_i32 : i32
hw.output %1 : i32
}
// -----
// CHECK: hw.module @one_firreg(in [[CLK:%.+]] : !seq.clock, in [[IN0:%.+]] : i32, in [[IN1:%.+]] : i32, in [[OLD_REG:%.+]] : i32, out {{.+}} : i32, out {{.+}} : i32) attributes {initial_values = [0 : i32], num_regs = 1 : i32} {
// CHECK: [[ADD:%.+]] = comb.add [[IN0]], [[IN1]]
// CHECK: hw.output [[OLD_REG]], [[ADD]]
// CHECK: }
hw.module @one_firreg(in %clk: !seq.clock, in %in0: i32, in %in1: i32, out out: i32) {
%0 = comb.add %in0, %in1 : i32
%single_reg = seq.firreg %0 clock %clk preset 0 : i32
hw.output %single_reg : i32
}
// CHECK: hw.module @compreg_and_firreg(in [[CLK:%.+]] : !seq.clock, in [[IN0:%.+]] : i32, in [[IN1:%.+]] : i32, in [[OLD_REG0:%.+]] : i32, in [[OLD_REG1:%.+]] : i32, out {{.+}} : i32, out {{.+}} : i32, out {{.+}} : i32) attributes {initial_values = [unit, unit], num_regs = 2 : i32} {
// CHECK: [[ADD:%.+]] = comb.add [[IN0]], [[IN1]]
// CHECK: hw.output [[OLD_REG1]], [[ADD]], [[OLD_REG0]]
// CHECK: }
hw.module @compreg_and_firreg(in %clk: !seq.clock, in %in0: i32, in %in1: i32, out out: i32) {
%0 = comb.add %in0, %in1 : i32
%1 = seq.compreg %0, %clk : i32
%2 = seq.firreg %1 clock %clk : i32
hw.output %2 : i32
}
// CHECK: hw.module @named_firregs(in [[CLK:%.+]] : !seq.clock, in [[IN0:%.+]] : i32, in [[IN1:%.+]] : i32, in %firstreg_state : i32, in %secondreg_state : i32, out {{.+}} : i32, out {{.+}} : i32, out {{.+}} : i32) attributes {initial_values = [unit, unit], num_regs = 2 : i32} {
// CHECK: [[ADD:%.+]] = comb.add [[IN0]], [[IN1]]
// CHECK: hw.output %secondreg_state, [[ADD]], %firstreg_state
// CHECK: }
hw.module @named_firregs(in %clk: !seq.clock, in %in0: i32, in %in1: i32, out out: i32) {
%0 = comb.add %in0, %in1 : i32
%firstreg = seq.firreg %0 clock %clk : i32
%secondreg = seq.firreg %firstreg clock %clk : i32
hw.output %secondreg : i32
}
// CHECK: hw.module @firreg_with_sync_reset(in [[CLK:%.+]] : !seq.clock, in [[RST:%.+]] : i1, in [[IN:%.+]] : i32, in [[OLD_REG1:%.+]] : i32, out {{.+}} : i32, out {{.+}} : i32) attributes {initial_values = [unit], num_regs = 1 : i32} {
// CHECK: [[C0_I32:%.+]] = hw.constant 0 : i32
// CHECK: [[MUX1:%.+]] = comb.mux [[RST]], [[C0_I32]], [[IN]] : i32
// CHECK: hw.output [[OLD_REG1]], [[MUX1]]
// CHECK: }
hw.module @firreg_with_sync_reset(in %clk: !seq.clock, in %rst: i1, in %in: i32, out out: i32) {
%c0_i32 = hw.constant 0 : i32
%1 = seq.firreg %in clock %clk reset sync %rst, %c0_i32 : i32
hw.output %1 : i32
}