Skip to content

Commit bf1f0b2

Browse files
committed
[ExportVerilog] Fix Precedence module to include clock input for ltl.delay operations
1 parent 450c584 commit bf1f0b2

File tree

1 file changed

+3
-4
lines changed

1 file changed

+3
-4
lines changed

test/Conversion/ExportVerilog/verif.mlir

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -210,16 +210,15 @@ hw.module @Properties(in %clk: i1, in %a: i1, in %b: i1) {
210210
}
211211

212212
// CHECK-LABEL: module Precedence
213-
hw.module @Precedence(in %a: i1, in %b: i1) {
214-
%true = hw.constant true
213+
hw.module @Precedence(in %clk: i1, in %a: i1, in %b: i1) {
215214
// CHECK: assert property ((a or ##0 b) and b);
216-
%a0 = ltl.delay %true, posedge, %b, 0, 0 : i1
215+
%a0 = ltl.delay %clk, posedge, %b, 0, 0 : i1
217216
%a1 = ltl.or %a, %a0 : i1, !ltl.sequence
218217
%a2 = ltl.and %a1, %b : !ltl.sequence, i1
219218
sv.assert_property %a2 : !ltl.sequence
220219

221220
// CHECK: assert property (##1 (a or ##0 b));
222-
%d0 = ltl.delay %true, posedge, %a1, 1, 0 : !ltl.sequence
221+
%d0 = ltl.delay %clk, posedge, %a1, 1, 0 : !ltl.sequence
223222
sv.assert_property %d0 : !ltl.sequence
224223

225224
// CHECK: assert property (not (a or ##0 b));

0 commit comments

Comments
 (0)