Skip to content

Commit b1cae94

Browse files
fabianschuikifabianschuiki
authored
[Verif] Mark SymbolicValueOp result as MemAlloc (#8208)
Add the `MemAlloc` side effect to the result of `verif.symbolic_value`. This allows the canonicalizer to delete the op if it has no users while still preventing CSE from mergin multiple symbolic values. Also add a few placeholders to the `lower-contracts.mlir` test to make it more robust.
1 parent 1892650 commit b1cae94

File tree

4 files changed

+131
-119
lines changed

4 files changed

+131
-119
lines changed

‎include/circt/Dialect/Verif/VerifOps.td

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -356,7 +356,7 @@ def SymbolicValueOp : VerifOp<"symbolic_value", [
356356
symbolic values that violate asserts or make covers true. This value is not
357357
fixed - the value taken can vary arbitrarily between timesteps.
358358
}];
359-
let results = (outs AnyType:$result);
359+
let results = (outs Res<AnyType, "", [MemAlloc]>:$result);
360360
let assemblyFormat = "attr-dict `:` type($result)";
361361
}
362362

‎test/Dialect/Verif/canonicalization.mlir

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -56,3 +56,10 @@ hw.module @clockedCover(in %clock : i1, in %a : i1, in %en : i1) {
5656
%clk = ltl.clock %a, posedge %clock : i1
5757
verif.cover %clk if %en : !ltl.sequence
5858
}
59+
60+
// CHECK-LABEL: @RemoveUnusedSymbolicValues
61+
hw.module @RemoveUnusedSymbolicValues() {
62+
// CHECK-NOT: verif.symbolic_value
63+
// CHECK: hw.output
64+
%0 = verif.symbolic_value : i32
65+
}

‎test/Dialect/Verif/cse.mlir

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
// RUN: circt-opt --cse %s | FileCheck %s
2+
3+
// CHECK-LABEL: @SymbolicValuesMustNotCSE
4+
hw.module @SymbolicValuesMustNotCSE(out a: i32, out b: i32) {
5+
// CHECK: [[TMP1:%.+]] = verif.symbolic_value
6+
// CHECK: [[TMP2:%.+]] = verif.symbolic_value
7+
// CHECK: hw.output [[TMP1]], [[TMP2]]
8+
%0 = verif.symbolic_value : i32
9+
%1 = verif.symbolic_value : i32
10+
hw.output %0, %1 : i32, i32
11+
}

‎test/Dialect/Verif/lower-contracts.mlir

Lines changed: 112 additions & 118 deletions
Original file line numberDiff line numberDiff line change
@@ -1,21 +1,21 @@
11
// RUN: circt-opt --lower-contracts --simplify-assume-eq --canonicalize --cse %s | FileCheck %s
22

3-
// CHECK: hw.module @Mul9(in %a : i42, out z : i42) {
3+
// CHECK-LABEL: hw.module @Mul9
44
// CHECK-NEXT: %c9_i42 = hw.constant 9 : i42
5-
// CHECK-NEXT: %0 = comb.mul %a, %c9_i42 : i42
6-
// CHECK-NEXT: hw.output %0 : i42
5+
// CHECK-NEXT: [[TMP:%.+]] = comb.mul %a, %c9_i42 : i42
6+
// CHECK-NEXT: hw.output [[TMP]] : i42
77
// CHECK-NEXT: }
88

9-
// CHECK: verif.formal @Mul9_CheckContract_0 {
9+
// CHECK-LABEL: verif.formal @Mul9_CheckContract_0
1010
// CHECK-NEXT: %c0_i3 = hw.constant 0 : i3
1111
// CHECK-NEXT: %c9_i42 = hw.constant 9 : i42
12-
// CHECK-NEXT: %0 = verif.symbolic_value : i42
13-
// CHECK-NEXT: %1 = comb.extract %0 from 0 : (i42) -> i39
14-
// CHECK-NEXT: %2 = comb.concat %1, %c0_i3 : i39, i3
15-
// CHECK-NEXT: %3 = comb.add %0, %2 : i42
16-
// CHECK-NEXT: %4 = comb.mul %0, %c9_i42 : i42
17-
// CHECK-NEXT: %5 = comb.icmp eq %3, %4 : i42
18-
// CHECK-NEXT: verif.assert %5 : i1
12+
// CHECK-NEXT: [[A:%.+]] = verif.symbolic_value : i42
13+
// CHECK-NEXT: [[TMP1:%.+]] = comb.extract [[A]] from 0 : (i42) -> i39
14+
// CHECK-NEXT: [[TMP2:%.+]] = comb.concat [[TMP1]], %c0_i3 : i39, i3
15+
// CHECK-NEXT: [[TMP1:%.+]] = comb.add [[A]], [[TMP2]] : i42
16+
// CHECK-NEXT: [[TMP2:%.+]] = comb.mul [[A]], %c9_i42 : i42
17+
// CHECK-NEXT: [[TMP3:%.+]] = comb.icmp eq [[TMP1]], [[TMP2]] : i42
18+
// CHECK-NEXT: verif.assert [[TMP3]] : i1
1919
// CHECK-NEXT: }
2020

2121
hw.module @Mul9(in %a: i42, out z: i42) {
@@ -31,34 +31,34 @@ hw.module @Mul9(in %a: i42, out z: i42) {
3131
hw.output %2 : i42
3232
}
3333

34-
// CHECK: hw.module @CarrySaveCompress3to2(in %a0 : i42, in %a1 : i42, in %a2 : i42, out z0 : i42, out z1 : i42) {
35-
// CHECK-NEXT: %0 = verif.symbolic_value : i42
36-
// CHECK-NEXT: %1 = verif.symbolic_value : i42
37-
// CHECK-NEXT: %2 = comb.add %a0, %a1, %a2 : i42
38-
// CHECK-NEXT: %3 = comb.add %0, %1 : i42
39-
// CHECK-NEXT: %4 = comb.icmp eq %2, %3 : i42
40-
// CHECK-NEXT: verif.assume %4 : i1
41-
// CHECK-NEXT: hw.output %0, %1 : i42, i42
34+
// CHECK-LABEL: hw.module @CarrySaveCompress3to2
35+
// CHECK-NEXT: [[Z0:%.+]] = verif.symbolic_value : i42
36+
// CHECK-NEXT: [[Z1:%.+]] = verif.symbolic_value : i42
37+
// CHECK-NEXT: [[TMP1:%.+]] = comb.add %a0, %a1, %a2 : i42
38+
// CHECK-NEXT: [[TMP2:%.+]] = comb.add [[Z0]], [[Z1]] : i42
39+
// CHECK-NEXT: [[TMP3:%.+]] = comb.icmp eq [[TMP1]], [[TMP2]] : i42
40+
// CHECK-NEXT: verif.assume [[TMP3]] : i1
41+
// CHECK-NEXT: hw.output [[Z0]], [[Z1]] : i42, i42
4242
// CHECK-NEXT: }
4343

44-
// CHECK: verif.formal @CarrySaveCompress3to2_CheckContract_0 {
44+
// CHECK-LABEL: verif.formal @CarrySaveCompress3to2_CheckContract_0
4545
// CHECK-NEXT: %false = hw.constant false
46-
// CHECK-NEXT: %0 = verif.symbolic_value : i42
47-
// CHECK-NEXT: %1 = verif.symbolic_value : i42
48-
// CHECK-NEXT: %2 = verif.symbolic_value : i42
49-
// CHECK-NEXT: %3 = comb.extract %0 from 0 : (i42) -> i41
50-
// CHECK-NEXT: %4 = comb.extract %1 from 0 : (i42) -> i41
51-
// CHECK-NEXT: %5 = comb.or %3, %4 : i41
52-
// CHECK-NEXT: %6 = comb.extract %2 from 0 : (i42) -> i41
53-
// CHECK-NEXT: %7 = comb.and %5, %6 : i41
54-
// CHECK-NEXT: %8 = comb.and %3, %4 : i41
55-
// CHECK-NEXT: %9 = comb.or %8, %7 : i41
56-
// CHECK-NEXT: %10 = comb.concat %9, %false : i41, i1
57-
// CHECK-NEXT: %11 = comb.xor %0, %1, %2 : i42
58-
// CHECK-NEXT: %12 = comb.add %0, %1, %2 : i42
59-
// CHECK-NEXT: %13 = comb.add %11, %10 : i42
60-
// CHECK-NEXT: %14 = comb.icmp eq %12, %13 : i42
61-
// CHECK-NEXT: verif.assert %14 : i1
46+
// CHECK-NEXT: [[A0:%.+]] = verif.symbolic_value : i42
47+
// CHECK-NEXT: [[A1:%.+]] = verif.symbolic_value : i42
48+
// CHECK-NEXT: [[A2:%.+]] = verif.symbolic_value : i42
49+
// CHECK-NEXT: [[TMP1:%.+]] = comb.extract [[A0]] from 0 : (i42) -> i41
50+
// CHECK-NEXT: [[TMP2:%.+]] = comb.extract [[A1]] from 0 : (i42) -> i41
51+
// CHECK-NEXT: [[TMP3:%.+]] = comb.or [[TMP1]], [[TMP2]] : i41
52+
// CHECK-NEXT: [[TMP4:%.+]] = comb.extract [[A2]] from 0 : (i42) -> i41
53+
// CHECK-NEXT: [[TMP5:%.+]] = comb.and [[TMP3]], [[TMP4]] : i41
54+
// CHECK-NEXT: [[TMP3:%.+]] = comb.and [[TMP1]], [[TMP2]] : i41
55+
// CHECK-NEXT: [[TMP4:%.+]] = comb.or [[TMP3]], [[TMP5]] : i41
56+
// CHECK-NEXT: [[TMP1:%.+]] = comb.concat [[TMP4]], %false : i41, i1
57+
// CHECK-NEXT: [[TMP2:%.+]] = comb.xor [[A0]], [[A1]], [[A2]] : i42
58+
// CHECK-NEXT: [[TMP3:%.+]] = comb.add [[A0]], [[A1]], [[A2]] : i42
59+
// CHECK-NEXT: [[TMP4:%.+]] = comb.add [[TMP2]], [[TMP1]] : i42
60+
// CHECK-NEXT: [[TMP1:%.+]] = comb.icmp eq [[TMP3]], [[TMP4]] : i42
61+
// CHECK-NEXT: verif.assert [[TMP1]] : i1
6262
// CHECK-NEXT: }
6363

6464
hw.module @CarrySaveCompress3to2(
@@ -81,38 +81,38 @@ hw.module @CarrySaveCompress3to2(
8181
hw.output %z0, %z1 : i42, i42
8282
}
8383

84-
// CHECK: hw.module @ShiftLeft(in %a : i8, in %b : i8, out z : i8) {
84+
// CHECK-LABEL: hw.module @ShiftLeft
8585
// CHECK-NEXT: %c8_i8 = hw.constant 8 : i8
86-
// CHECK-NEXT: %0 = comb.icmp ult %b, %c8_i8 : i8
87-
// CHECK-NEXT: verif.assert %0 : i1
88-
// CHECK-NEXT: %1 = comb.shl %a, %b : i8
89-
// CHECK-NEXT: hw.output %1 : i8
86+
// CHECK-NEXT: [[TMP0:%.+]] = comb.icmp ult %b, %c8_i8 : i8
87+
// CHECK-NEXT: verif.assert [[TMP0]] : i1
88+
// CHECK-NEXT: [[TMP1:%.+]] = comb.shl %a, %b : i8
89+
// CHECK-NEXT: hw.output [[TMP1]] : i8
9090
// CHECK-NEXT: }
9191

92-
// CHECK: verif.formal @ShiftLeft_CheckContract_0 {} {
92+
// CHECK-LABEL: verif.formal @ShiftLeft_CheckContract_0
9393
// CHECK-NEXT: %false = hw.constant false
9494
// CHECK-NEXT: %c0_i2 = hw.constant 0 : i2
9595
// CHECK-NEXT: %c0_i4 = hw.constant 0 : i4
9696
// CHECK-NEXT: %c8_i8 = hw.constant 8 : i8
97-
// CHECK-NEXT: %0 = verif.symbolic_value : i8
98-
// CHECK-NEXT: %1 = verif.symbolic_value : i8
99-
// CHECK-NEXT: %2 = comb.extract %1 from 0 : (i8) -> i4
100-
// CHECK-NEXT: %3 = comb.concat %2, %c0_i4 : i4, i4
101-
// CHECK-NEXT: %4 = comb.extract %0 from 2 : (i8) -> i1
102-
// CHECK-NEXT: %5 = comb.mux %4, %3, %1 : i8
103-
// CHECK-NEXT: %6 = comb.extract %5 from 0 : (i8) -> i6
104-
// CHECK-NEXT: %7 = comb.concat %6, %c0_i2 : i6, i2
105-
// CHECK-NEXT: %8 = comb.extract %0 from 1 : (i8) -> i1
106-
// CHECK-NEXT: %9 = comb.mux %8, %7, %5 : i8
107-
// CHECK-NEXT: %10 = comb.extract %9 from 0 : (i8) -> i7
108-
// CHECK-NEXT: %11 = comb.concat %10, %false : i7, i1
109-
// CHECK-NEXT: %12 = comb.extract %0 from 0 : (i8) -> i1
110-
// CHECK-NEXT: %13 = comb.mux %12, %11, %9 : i8
111-
// CHECK-NEXT: %14 = comb.icmp ult %0, %c8_i8 : i8
112-
// CHECK-NEXT: verif.assume %14 : i1
113-
// CHECK-NEXT: %15 = comb.shl %1, %0 : i8
114-
// CHECK-NEXT: %16 = comb.icmp eq %13, %15 : i8
115-
// CHECK-NEXT: verif.assert %16 : i1
97+
// CHECK-NEXT: [[TMP0:%.+]] = verif.symbolic_value : i8
98+
// CHECK-NEXT: [[TMP1:%.+]] = verif.symbolic_value : i8
99+
// CHECK-NEXT: [[TMP2:%.+]] = comb.extract [[TMP1]] from 0 : (i8) -> i4
100+
// CHECK-NEXT: [[TMP3:%.+]] = comb.concat [[TMP2]], %c0_i4 : i4, i4
101+
// CHECK-NEXT: [[TMP4:%.+]] = comb.extract [[TMP0]] from 2 : (i8) -> i1
102+
// CHECK-NEXT: [[TMP5:%.+]] = comb.mux [[TMP4]], [[TMP3]], [[TMP1]] : i8
103+
// CHECK-NEXT: [[TMP6:%.+]] = comb.extract [[TMP5]] from 0 : (i8) -> i6
104+
// CHECK-NEXT: [[TMP7:%.+]] = comb.concat [[TMP6]], %c0_i2 : i6, i2
105+
// CHECK-NEXT: [[TMP8:%.+]] = comb.extract [[TMP0]] from 1 : (i8) -> i1
106+
// CHECK-NEXT: [[TMP9:%.+]] = comb.mux [[TMP8]], [[TMP7]], [[TMP5]] : i8
107+
// CHECK-NEXT: [[TMP10:%.+]] = comb.extract [[TMP9]] from 0 : (i8) -> i7
108+
// CHECK-NEXT: [[TMP11:%.+]] = comb.concat [[TMP10]], %false : i7, i1
109+
// CHECK-NEXT: [[TMP12:%.+]] = comb.extract [[TMP0]] from 0 : (i8) -> i1
110+
// CHECK-NEXT: [[TMP13:%.+]] = comb.mux [[TMP12]], [[TMP11]], [[TMP9]] : i8
111+
// CHECK-NEXT: [[TMP14:%.+]] = comb.icmp ult [[TMP0]], %c8_i8 : i8
112+
// CHECK-NEXT: verif.assume [[TMP14]] : i1
113+
// CHECK-NEXT: [[TMP15:%.+]] = comb.shl [[TMP1]], [[TMP0]] : i8
114+
// CHECK-NEXT: [[TMP16:%.+]] = comb.icmp eq [[TMP13]], [[TMP15]] : i8
115+
// CHECK-NEXT: verif.assert [[TMP16]] : i1
116116
// CHECK-NEXT: }
117117

118118
hw.module @ShiftLeft(in %a: i8, in %b: i8, out z: i8) {
@@ -147,13 +147,8 @@ hw.module @ShiftLeft(in %a: i8, in %b: i8, out z: i8) {
147147
hw.output %z : i8
148148
}
149149

150-
// CHECK: hw.module @NoContract(in %a : i42, out z : i42) {
151-
// CHECK-NEXT: %c0_i3 = hw.constant 0 : i3
152-
// CHECK-NEXT: %0 = comb.extract %a from 0 : (i42) -> i39
153-
// CHECK-NEXT: %1 = comb.concat %0, %c0_i3 : i39, i3
154-
// CHECK-NEXT: %2 = comb.add %a, %1 : i42
155-
// CHECK-NEXT: hw.output %2 : i42
156-
// CHECK-NEXT: }
150+
// CHECK-LABEL: hw.module @NoContract
151+
// CHECK-NOT: verif.formal
157152

158153
hw.module @NoContract(in %a: i42, out z: i42) {
159154
%c3_i42 = hw.constant 3 : i42
@@ -162,38 +157,38 @@ hw.module @NoContract(in %a: i42, out z: i42) {
162157
hw.output %1 : i42
163158
}
164159

165-
// CHECK: hw.module @TwoContracts(in %a : i42, out z : i42) {
160+
// CHECK-LABEL: hw.module @TwoContracts
166161
// CHECK-NEXT: %false = hw.constant false
167162
// CHECK-NEXT: %c2_i42 = hw.constant 2 : i42
168-
// CHECK-NEXT: %0 = comb.icmp ult %a, %c2_i42 : i42
169-
// CHECK-NEXT: verif.assert %0 : i1
170-
// CHECK-NEXT: %1 = comb.extract %a from 0 : (i42) -> i41
171-
// CHECK-NEXT: %2 = comb.concat %1, %false : i41, i1
172-
// CHECK-NEXT: hw.output %2 : i42
163+
// CHECK-NEXT: [[TMP0:%.+]] = comb.icmp ult %a, %c2_i42 : i42
164+
// CHECK-NEXT: verif.assert [[TMP0]] : i1
165+
// CHECK-NEXT: [[TMP1:%.+]] = comb.extract %a from 0 : (i42) -> i41
166+
// CHECK-NEXT: [[TMP2:%.+]] = comb.concat [[TMP1]], %false : i41, i1
167+
// CHECK-NEXT: hw.output [[TMP2]] : i42
173168
// CHECK-NEXT: }
174169

175-
// CHECK: verif.formal @TwoContracts_CheckContract_0 {} {
170+
// CHECK-LABEL: verif.formal @TwoContracts_CheckContract_0
176171
// CHECK-NEXT: %c2_i42 = hw.constant 2 : i42
177-
// CHECK-NEXT: %0 = verif.symbolic_value : i42
178-
// CHECK-NEXT: %1 = comb.extract %0 from 0 : (i42) -> i41
179-
// CHECK-NEXT: %2 = comb.icmp ult %0, %c2_i42 : i42
180-
// CHECK-NEXT: verif.assume %2 : i1
181-
// CHECK-NEXT: %3 = comb.icmp eq %1, %1 : i41
182-
// CHECK-NEXT: verif.assert %3 : i1
172+
// CHECK-NEXT: [[TMP0:%.+]] = verif.symbolic_value : i42
173+
// CHECK-NEXT: [[TMP1:%.+]] = comb.extract [[TMP0]] from 0 : (i42) -> i41
174+
// CHECK-NEXT: [[TMP2:%.+]] = comb.icmp ult [[TMP0]], %c2_i42 : i42
175+
// CHECK-NEXT: verif.assume [[TMP2]] : i1
176+
// CHECK-NEXT: [[TMP3:%.+]] = comb.icmp eq [[TMP1]], [[TMP1]] : i41
177+
// CHECK-NEXT: verif.assert [[TMP3]] : i1
183178
// CHECK-NEXT: }
184179

185-
// CHECK: verif.formal @TwoContracts_CheckContract_1 {} {
180+
// CHECK-LABEL: verif.formal @TwoContracts_CheckContract_1
186181
// CHECK-NEXT: %false = hw.constant false
187182
// CHECK-NEXT: %c2_i42 = hw.constant 2 : i42
188-
// CHECK-NEXT: %0 = verif.symbolic_value : i42
189-
// CHECK-NEXT: %1 = verif.symbolic_value : i42
190-
// CHECK-NEXT: %2 = comb.icmp ult %0, %c2_i42 : i42
191-
// CHECK-NEXT: verif.assert %2 : i1
192-
// CHECK-NEXT: %3 = comb.extract %0 from 0 : (i42) -> i41
193-
// CHECK-NEXT: %4 = comb.concat %3, %false : i41, i1
194-
// CHECK-NEXT: %5 = comb.icmp eq %1, %4 : i42
195-
// CHECK-NEXT: verif.assume %5 : i1
196-
// CHECK-NEXT: verif.assert %5 : i1
183+
// CHECK-NEXT: [[TMP0:%.+]] = verif.symbolic_value : i42
184+
// CHECK-NEXT: [[TMP1:%.+]] = verif.symbolic_value : i42
185+
// CHECK-NEXT: [[TMP2:%.+]] = comb.icmp ult [[TMP0]], %c2_i42 : i42
186+
// CHECK-NEXT: verif.assert [[TMP2]] : i1
187+
// CHECK-NEXT: [[TMP3:%.+]] = comb.extract [[TMP0]] from 0 : (i42) -> i41
188+
// CHECK-NEXT: [[TMP4:%.+]] = comb.concat [[TMP3]], %false : i41, i1
189+
// CHECK-NEXT: [[TMP5:%.+]] = comb.icmp eq [[TMP1]], [[TMP4]] : i42
190+
// CHECK-NEXT: verif.assume [[TMP5]] : i1
191+
// CHECK-NEXT: verif.assert [[TMP5]] : i1
197192
// CHECK-NEXT: }
198193

199194
hw.module @TwoContracts(in %a: i42, out z: i42) {
@@ -215,41 +210,40 @@ hw.module @TwoContracts(in %a: i42, out z: i42) {
215210
hw.output %4 : i42
216211
}
217212

218-
// CHECK: hw.module @NestedContract(in %a : i42, in %b : i42, in %s : i1, out z : i42) {
213+
// CHECK-LABEL: hw.module @NestedContract
219214
// CHECK-NEXT: %false = hw.constant false
220-
// CHECK-NEXT: %0 = comb.extract %a from 0 : (i42) -> i41
221-
// CHECK-NEXT: %1 = comb.concat %0, %false : i41, i1
222-
// CHECK-NEXT: %2 = comb.mul %a, %a : i42
223-
// CHECK-NEXT: %3 = scf.if %s -> (i42) {
224-
// CHECK-NEXT: %6 = comb.add %1, %2 : i42
225-
// CHECK-NEXT: scf.yield %6 : i42
215+
// CHECK-NEXT: [[TMP0:%.+]] = comb.extract %a from 0 : (i42) -> i41
216+
// CHECK-NEXT: [[TMP1:%.+]] = comb.concat [[TMP0]], %false : i41, i1
217+
// CHECK-NEXT: [[TMP2:%.+]] = comb.mul %a, %a : i42
218+
// CHECK-NEXT: [[TMP3:%.+]] = scf.if %s -> (i42) {
219+
// CHECK-NEXT: [[TMP6:%.+]] = comb.add [[TMP1]], [[TMP2]] : i42
220+
// CHECK-NEXT: scf.yield [[TMP6]] : i42
226221
// CHECK-NEXT: } else {
227-
// CHECK-NEXT: %6 = comb.mul %1, %2 : i42
228-
// CHECK-NEXT: scf.yield %6 : i42
222+
// CHECK-NEXT: [[TMP6:%.+]] = comb.mul [[TMP1]], [[TMP2]] : i42
223+
// CHECK-NEXT: scf.yield [[TMP6]] : i42
229224
// CHECK-NEXT: }
230-
// CHECK-NEXT: %4 = verif.symbolic_value : i42
231-
// CHECK-NEXT: %5 = comb.icmp eq %3, %b : i42
232-
// CHECK-NEXT: verif.assume %5 : i1
233-
// CHECK-NEXT: hw.output %3 : i42
225+
// CHECK-NEXT: [[TMP5:%.+]] = comb.icmp eq [[TMP3]], %b : i42
226+
// CHECK-NEXT: verif.assume [[TMP5]] : i1
227+
// CHECK-NEXT: hw.output [[TMP3]] : i42
234228
// CHECK-NEXT: }
235229

236-
// CHECK: verif.formal @NestedContract_CheckContract_0 {} {
230+
// CHECK-LABEL: verif.formal @NestedContract_CheckContract_0
237231
// CHECK-NEXT: %false = hw.constant false
238-
// CHECK-NEXT: %0 = verif.symbolic_value : i42
239-
// CHECK-NEXT: %1 = verif.symbolic_value : i1
240-
// CHECK-NEXT: %2 = verif.symbolic_value : i42
241-
// CHECK-NEXT: %3 = comb.mul %2, %2 : i42
242-
// CHECK-NEXT: %4 = comb.extract %2 from 0 : (i42) -> i41
243-
// CHECK-NEXT: %5 = comb.concat %4, %false : i41, i1
244-
// CHECK-NEXT: %6 = scf.if %1 -> (i42) {
245-
// CHECK-NEXT: %8 = comb.add %5, %3 : i42
246-
// CHECK-NEXT: scf.yield %8 : i42
232+
// CHECK-NEXT: [[TMP0:%.+]] = verif.symbolic_value : i42
233+
// CHECK-NEXT: [[TMP1:%.+]] = verif.symbolic_value : i1
234+
// CHECK-NEXT: [[TMP2:%.+]] = verif.symbolic_value : i42
235+
// CHECK-NEXT: [[TMP3:%.+]] = comb.mul [[TMP2]], [[TMP2]] : i42
236+
// CHECK-NEXT: [[TMP4:%.+]] = comb.extract [[TMP2]] from 0 : (i42) -> i41
237+
// CHECK-NEXT: [[TMP5:%.+]] = comb.concat [[TMP4]], %false : i41, i1
238+
// CHECK-NEXT: [[TMP6:%.+]] = scf.if [[TMP1]] -> (i42) {
239+
// CHECK-NEXT: [[TMP8:%.+]] = comb.add [[TMP5]], [[TMP3]] : i42
240+
// CHECK-NEXT: scf.yield [[TMP8]] : i42
247241
// CHECK-NEXT: } else {
248-
// CHECK-NEXT: %8 = comb.mul %5, %3 : i42
249-
// CHECK-NEXT: scf.yield %8 : i42
242+
// CHECK-NEXT: [[TMP8:%.+]] = comb.mul [[TMP5]], [[TMP3]] : i42
243+
// CHECK-NEXT: scf.yield [[TMP8]] : i42
250244
// CHECK-NEXT: }
251-
// CHECK-NEXT: %7 = comb.icmp eq %6, %0 : i42
252-
// CHECK-NEXT: verif.assert %7 : i1
245+
// CHECK-NEXT: [[TMP7:%.+]] = comb.icmp eq [[TMP6]], [[TMP0]] : i42
246+
// CHECK-NEXT: verif.assert [[TMP7]] : i1
253247
// CHECK-NEXT: }
254248

255249
hw.module @NestedContract(in %a: i42, in %b: i42, in %s: i1, out z: i42) {

0 commit comments

Comments
 (0)