Skip to content

Commit 4627696

Browse files
fabianschuikiclaude
fabianschuiki
and
claude
committed
[Verif] Preserve labeled assert/assume ops during canonicalization
The EraseIfEnableFalse and EraseIfPropertyTrue canonicalization patterns unconditionally erased verif.assert and verif.assume ops (and their clocked variants) when they were trivially true or disabled. This silently dropped user-visible labels that users expect to see in the output regardless of optimizations. Instead of erasing labeled ops, replace them with trivially-satisfied versions that preserve the label: set the property to constant true, clear the enable, and for clocked ops replace a non-constant clock with constant false. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent a4a4f74 commit 4627696

File tree

2 files changed

+176
-23
lines changed

2 files changed

+176
-23
lines changed

‎lib/Dialect/Verif/VerifOps.cpp‎

Lines changed: 77 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@
1414
#include "circt/Support/CustomDirectiveImpl.h"
1515
#include "circt/Support/FoldUtils.h"
1616
#include "mlir/IR/Builders.h"
17+
#include "mlir/IR/Matchers.h"
1718
#include "mlir/IR/OpImplementation.h"
1819
#include "mlir/IR/PatternMatch.h"
1920
#include "mlir/IR/SymbolTable.h"
@@ -76,12 +77,13 @@ struct RemoveEnableTrue : public OpRewritePattern<Op> {
7677
if (!enableConst || !enableConst.getValue().isOne())
7778
return failure();
7879

79-
rewriter.modifyOpInPlace(op, [&]() { op.getEnableMutable().clear(); });
80+
rewriter.modifyOpInPlace(op, [&] { op.getEnableMutable().clear(); });
8081
return success();
8182
}
8283
};
8384

84-
/// Delete operation if enable is `false`.
85+
/// Delete operation if enable is `false`. If the operation has a label,
86+
/// preserve it as a trivially-true assertion instead of erasing it.
8587
template <typename Op>
8688
struct EraseIfEnableFalse : public OpRewritePattern<Op> {
8789
using OpRewritePattern<Op>::OpRewritePattern;
@@ -91,43 +93,95 @@ struct EraseIfEnableFalse : public OpRewritePattern<Op> {
9193
Value enable = op.getEnable();
9294
if (!enable)
9395
return failure();
94-
auto enableConst = enable.getDefiningOp<hw::ConstantOp>();
95-
if (!enableConst || !enableConst.getValue().isZero())
96+
APInt enableValue;
97+
if (!matchPattern(enable, m_ConstantInt(&enableValue)) ||
98+
!enableValue.isZero())
9699
return failure();
97100

98-
rewriter.eraseOp(op);
99-
return success();
101+
// If the op has no label, erase it. Otherwise preserve it as a
102+
// trivially-satisfied assertion instead of erasing it.
103+
if (!op.getLabel()) {
104+
rewriter.eraseOp(op);
105+
return success();
106+
}
107+
108+
// Replace the property with a constant true if it isn't already.
109+
bool changed = false;
110+
IntegerAttr propAttr;
111+
if (!matchPattern(op.getProperty(), m_Constant(&propAttr)) ||
112+
!propAttr.getValue().isOne()) {
113+
auto trueVal = hw::ConstantOp::create(rewriter, op.getLoc(), APInt(1, 1));
114+
rewriter.modifyOpInPlace(
115+
op, [&] { op.getPropertyMutable().assign(trueVal); });
116+
changed = true;
117+
}
118+
119+
// Clear the enable.
120+
if (op.getEnable()) {
121+
rewriter.modifyOpInPlace(op, [&] { op.getEnableMutable().clear(); });
122+
changed = true;
123+
}
124+
125+
// For clocked ops, replace the clock with a constant if it isn't one.
126+
if constexpr (std::is_same_v<Op, ClockedAssertOp> ||
127+
std::is_same_v<Op, ClockedAssumeOp>) {
128+
Attribute attr;
129+
if (!matchPattern(op.getClock(), m_Constant(&attr))) {
130+
auto falseVal =
131+
hw::ConstantOp::create(rewriter, op.getLoc(), APInt(1, 0));
132+
rewriter.modifyOpInPlace(
133+
op, [&] { op.getClockMutable().assign(falseVal); });
134+
changed = true;
135+
}
136+
}
137+
138+
return success(changed);
100139
}
101140
};
102141

103-
/// Delete operation if property is `ltl.boolean_constant true` or
104-
/// `hw.constant true`.
142+
/// Delete operation if property is a constant true. If the operation has a
143+
/// label, preserve it instead of erasing it, since the label is expected to be
144+
/// visible in the output.
105145
template <typename Op>
106146
struct EraseIfPropertyTrue : public OpRewritePattern<Op> {
107147
using OpRewritePattern<Op>::OpRewritePattern;
108148

109149
LogicalResult matchAndRewrite(Op op,
110150
PatternRewriter &rewriter) const override {
111-
Value property = op.getProperty();
112-
113-
// Check for ltl.boolean_constant true
114-
if (auto boolConst =
115-
property.template getDefiningOp<ltl::BooleanConstantOp>()) {
116-
if (boolConst.getValueAttr().getValue()) {
117-
rewriter.eraseOp(op);
118-
return success();
119-
}
151+
// Check if the property is a constant true.
152+
IntegerAttr propAttr;
153+
if (!matchPattern(op.getProperty(), m_Constant(&propAttr)) ||
154+
!propAttr.getValue().isOne())
155+
return failure();
156+
157+
// If the op has no label, erase it. Otherwise preserve it instead of
158+
// erasing it. The property is already trivially true.
159+
if (!op.getLabel()) {
160+
rewriter.eraseOp(op);
161+
return success();
162+
}
163+
164+
// Clear the enable if present.
165+
bool changed = false;
166+
if (op.getEnable()) {
167+
rewriter.modifyOpInPlace(op, [&] { op.getEnableMutable().clear(); });
168+
changed = true;
120169
}
121170

122-
// Check for hw.constant true (for i1 properties)
123-
if (auto hwConst = property.template getDefiningOp<hw::ConstantOp>()) {
124-
if (hwConst.getValue().isOne()) {
125-
rewriter.eraseOp(op);
126-
return success();
171+
// For clocked ops, replace the clock with a constant if it isn't one.
172+
if constexpr (std::is_same_v<Op, ClockedAssertOp> ||
173+
std::is_same_v<Op, ClockedAssumeOp>) {
174+
Attribute attr;
175+
if (!matchPattern(op.getClock(), m_Constant(&attr))) {
176+
auto falseVal =
177+
hw::ConstantOp::create(rewriter, op.getLoc(), APInt(1, 0));
178+
rewriter.modifyOpInPlace(
179+
op, [&] { op.getClockMutable().assign(falseVal); });
180+
changed = true;
127181
}
128182
}
129183

130-
return failure();
184+
return success(changed);
131185
}
132186
};
133187

‎test/Dialect/Verif/canonicalization.mlir‎

Lines changed: 99 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -48,6 +48,23 @@ hw.module @AssertEnableFalse(in %a : i1) {
4848
verif.assert %a if %false : i1
4949
}
5050

51+
// CHECK-LABEL: @AssertEnableFalseLabeled
52+
hw.module @AssertEnableFalseLabeled(in %a : i1) {
53+
%false = hw.constant false
54+
// CHECK: verif.assert %true label "foo" : i1
55+
// CHECK-NOT: if
56+
verif.assert %a if %false label "foo" : i1
57+
}
58+
59+
// CHECK-LABEL: @AssertEnableFalseBooleanConstantTrueLabeled
60+
hw.module @AssertEnableFalseBooleanConstantTrueLabeled() {
61+
%false = hw.constant false
62+
%prop = ltl.boolean_constant true
63+
// CHECK: [[PROP:%.+]] = ltl.boolean_constant true
64+
// CHECK: verif.assert [[PROP]] label "foo" : !ltl.property
65+
verif.assert %prop if %false label "foo" : !ltl.property
66+
}
67+
5168
// CHECK-LABEL: @AssertBooleanConstantTrue
5269
hw.module @AssertBooleanConstantTrue() {
5370
%prop = ltl.boolean_constant true
@@ -56,6 +73,14 @@ hw.module @AssertBooleanConstantTrue() {
5673
// CHECK: hw.output
5774
}
5875

76+
// CHECK-LABEL: @AssertBooleanConstantTrueLabeled
77+
hw.module @AssertBooleanConstantTrueLabeled() {
78+
%prop = ltl.boolean_constant true
79+
// CHECK: [[PROP:%.+]] = ltl.boolean_constant true
80+
// CHECK: verif.assert [[PROP]] label "foo" : !ltl.property
81+
verif.assert %prop label "foo" : !ltl.property
82+
}
83+
5984
// CHECK-LABEL: @AssertHWConstantTrue
6085
hw.module @AssertHWConstantTrue() {
6186
%true = hw.constant true
@@ -64,6 +89,13 @@ hw.module @AssertHWConstantTrue() {
6489
// CHECK: hw.output
6590
}
6691

92+
// CHECK-LABEL: @AssertHWConstantTrueLabeled
93+
hw.module @AssertHWConstantTrueLabeled() {
94+
%true = hw.constant true
95+
// CHECK: verif.assert %true label "foo" : i1
96+
verif.assert %true label "foo" : i1
97+
}
98+
6799
// CHECK-LABEL: @AssertEnableTrue
68100
hw.module @AssertEnableTrue(in %a : i1) {
69101
%true = hw.constant true
@@ -92,6 +124,14 @@ hw.module @AssumeEnableFalse(in %a : i1) {
92124
verif.assume %a if %false : i1
93125
}
94126

127+
// CHECK-LABEL: @AssumeEnableFalseLabeled
128+
hw.module @AssumeEnableFalseLabeled(in %a : i1) {
129+
%false = hw.constant false
130+
// CHECK: verif.assume %true label "foo" : i1
131+
// CHECK-NOT: if
132+
verif.assume %a if %false label "foo" : i1
133+
}
134+
95135
// CHECK-LABEL: @AssumeBooleanConstantTrue
96136
hw.module @AssumeBooleanConstantTrue() {
97137
%prop = ltl.boolean_constant true
@@ -100,6 +140,14 @@ hw.module @AssumeBooleanConstantTrue() {
100140
// CHECK: hw.output
101141
}
102142

143+
// CHECK-LABEL: @AssumeBooleanConstantTrueLabeled
144+
hw.module @AssumeBooleanConstantTrueLabeled() {
145+
%prop = ltl.boolean_constant true
146+
// CHECK: [[PROP:%.+]] = ltl.boolean_constant true
147+
// CHECK: verif.assume [[PROP]] label "foo" : !ltl.property
148+
verif.assume %prop label "foo" : !ltl.property
149+
}
150+
103151
// CHECK-LABEL: @AssumeHWConstantTrue
104152
hw.module @AssumeHWConstantTrue() {
105153
%true = hw.constant true
@@ -108,6 +156,13 @@ hw.module @AssumeHWConstantTrue() {
108156
// CHECK: hw.output
109157
}
110158

159+
// CHECK-LABEL: @AssumeHWConstantTrueLabeled
160+
hw.module @AssumeHWConstantTrueLabeled() {
161+
%true = hw.constant true
162+
// CHECK: verif.assume %true label "foo" : i1
163+
verif.assume %true label "foo" : i1
164+
}
165+
111166
// CHECK-LABEL: @AssumeEnableTrue
112167
hw.module @AssumeEnableTrue(in %a : i1) {
113168
%true = hw.constant true
@@ -192,6 +247,13 @@ hw.module @ClockedAssertEnableFalse(in %clock : i1, in %a : i1) {
192247
verif.clocked_assert %a if %false, posedge %clock : i1
193248
}
194249

250+
// CHECK-LABEL: @ClockedAssertEnableFalseLabeled
251+
hw.module @ClockedAssertEnableFalseLabeled(in %clock : i1, in %a : i1) {
252+
%false = hw.constant false
253+
// CHECK: verif.clocked_assert %true, posedge %false label "foo" : i1
254+
verif.clocked_assert %a if %false, posedge %clock label "foo" : i1
255+
}
256+
195257
// CHECK-LABEL: @ClockedAssertBooleanConstantTrue
196258
hw.module @ClockedAssertBooleanConstantTrue(in %clock : i1) {
197259
%prop = ltl.boolean_constant true
@@ -200,6 +262,14 @@ hw.module @ClockedAssertBooleanConstantTrue(in %clock : i1) {
200262
// CHECK: hw.output
201263
}
202264

265+
// CHECK-LABEL: @ClockedAssertBooleanConstantTrueLabeled
266+
hw.module @ClockedAssertBooleanConstantTrueLabeled(in %clock : i1) {
267+
%prop = ltl.boolean_constant true
268+
// CHECK: [[PROP:%.+]] = ltl.boolean_constant true
269+
// CHECK: verif.clocked_assert [[PROP]], posedge %false label "foo" : !ltl.property
270+
verif.clocked_assert %prop, posedge %clock label "foo" : !ltl.property
271+
}
272+
203273
// CHECK-LABEL: @ClockedAssertHWConstantTrue
204274
hw.module @ClockedAssertHWConstantTrue(in %clock : i1) {
205275
%true = hw.constant true
@@ -208,6 +278,13 @@ hw.module @ClockedAssertHWConstantTrue(in %clock : i1) {
208278
// CHECK: hw.output
209279
}
210280

281+
// CHECK-LABEL: @ClockedAssertHWConstantTrueLabeled
282+
hw.module @ClockedAssertHWConstantTrueLabeled(in %clock : i1) {
283+
%true = hw.constant true
284+
// CHECK: verif.clocked_assert %true, posedge %false label "foo" : i1
285+
verif.clocked_assert %true, posedge %clock label "foo" : i1
286+
}
287+
211288
//===----------------------------------------------------------------------===//
212289
// ClockedAssumeOp
213290
//===----------------------------------------------------------------------===//
@@ -229,6 +306,13 @@ hw.module @ClockedAssumeEnableFalse(in %clock : i1, in %a : i1) {
229306
verif.clocked_assume %a if %false, posedge %clock : i1
230307
}
231308

309+
// CHECK-LABEL: @ClockedAssumeEnableFalseLabeled
310+
hw.module @ClockedAssumeEnableFalseLabeled(in %clock : i1, in %a : i1) {
311+
%false = hw.constant false
312+
// CHECK: verif.clocked_assume %true, posedge %false label "foo" : i1
313+
verif.clocked_assume %a if %false, posedge %clock label "foo" : i1
314+
}
315+
232316
// CHECK-LABEL: @ClockedAssumeBooleanConstantTrue
233317
hw.module @ClockedAssumeBooleanConstantTrue(in %clock : i1) {
234318
%prop = ltl.boolean_constant true
@@ -237,6 +321,14 @@ hw.module @ClockedAssumeBooleanConstantTrue(in %clock : i1) {
237321
// CHECK: hw.output
238322
}
239323

324+
// CHECK-LABEL: @ClockedAssumeBooleanConstantTrueLabeled
325+
hw.module @ClockedAssumeBooleanConstantTrueLabeled(in %clock : i1) {
326+
%prop = ltl.boolean_constant true
327+
// CHECK: [[PROP:%.+]] = ltl.boolean_constant true
328+
// CHECK: verif.clocked_assume [[PROP]], posedge %false label "foo" : !ltl.property
329+
verif.clocked_assume %prop, posedge %clock label "foo" : !ltl.property
330+
}
331+
240332
// CHECK-LABEL: @ClockedAssumeHWConstantTrue
241333
hw.module @ClockedAssumeHWConstantTrue(in %clock : i1) {
242334
%true = hw.constant true
@@ -245,6 +337,13 @@ hw.module @ClockedAssumeHWConstantTrue(in %clock : i1) {
245337
// CHECK: hw.output
246338
}
247339

340+
// CHECK-LABEL: @ClockedAssumeHWConstantTrueLabeled
341+
hw.module @ClockedAssumeHWConstantTrueLabeled(in %clock : i1) {
342+
%true = hw.constant true
343+
// CHECK: verif.clocked_assume %true, posedge %false label "foo" : i1
344+
verif.clocked_assume %true, posedge %clock label "foo" : i1
345+
}
346+
248347
//===----------------------------------------------------------------------===//
249348
// ClockedCoverOp
250349
//===----------------------------------------------------------------------===//

0 commit comments

Comments
 (0)