diff --git a/lib/Conversion/ImportVerilog/Structure.cpp b/lib/Conversion/ImportVerilog/Structure.cpp
index f6275263ea37..166d36ebd134 100644
--- a/lib/Conversion/ImportVerilog/Structure.cpp
+++ b/lib/Conversion/ImportVerilog/Structure.cpp
@@ -849,6 +849,36 @@ struct ModuleVisitor : public BaseVisitor {
                                  const slang::ast::Statement &body) {
     if (body.as_if<slang::ast::ConcurrentAssertionStatement>())
       return context.convertStatement(body);
+
+    // A labeled module-level concurrent assertion (`CHK: assert property
+    // (p);`) arrives wrapped in a single-statement block, which used to
+    // fall through into the generic procedure path: the assertion then
+    // converted inside a `moore.procedure always` while its unlabeled twin
+    // converted at module scope, so a label silently changed which lowering
+    // an assertion got (and downstream consumers of module-scope assertions
+    // never saw the labeled one). Look through label blocks so labeled and
+    // unlabeled assertions take the same path. Only the `always` wrapper is
+    // treated this way -- for a body that reduces to a single concurrent
+    // assertion the two forms are equivalent (IEEE 1800-2017 16.14.6);
+    // concurrent assertions in initial/final procedures have one-attempt
+    // semantics and must not become continuous module-scope assertions.
+    if (kind == moore::ProcedureKind::Always) {
+      const slang::ast::Statement *stmt = &body;
+      while (true) {
+        if (auto *block = stmt->as_if<slang::ast::BlockStatement>()) {
+          stmt = &block->body;
+          continue;
+        }
+        if (auto *list = stmt->as_if<slang::ast::StatementList>();
+            list && list->list.size() == 1) {
+          stmt = list->list[0];
+          continue;
+        }
+        break;
+      }
+      if (stmt->as_if<slang::ast::ConcurrentAssertionStatement>())
+        return context.convertStatement(*stmt);
+    }
     auto procOp = moore::ProcedureOp::create(builder, loc, kind);
     OpBuilder::InsertionGuard guard(builder);
     builder.setInsertionPointToEnd(&procOp.getBody().emplaceBlock());
diff --git a/test/Conversion/ImportVerilog/builtins.sv b/test/Conversion/ImportVerilog/builtins.sv
index 5c41d95a9cd8..860621c8e1ea 100644
--- a/test/Conversion/ImportVerilog/builtins.sv
+++ b/test/Conversion/ImportVerilog/builtins.sv
@@ -457,8 +457,7 @@ module SampleValueBuiltins #() (
   // CHECK: [[CLKWIRE:%.+]] = moore.net name "clk_i" wire : <l1>
   // CHECK: [[DATAWIRE:%.+]] = moore.net name "data_i" wire : <l8>
   // CHECK: [[DATABITWIRE:%.+]] = moore.net name "data_bit_i" wire : <i8>
-  // CHECK: moore.procedure always {
-  // CHECK-NEXT: [[C:%.+]] = moore.read [[CLKWIRE]] : <l1>
+  // CHECK: [[C:%.+]] = moore.read [[CLKWIRE]] : <l1>
   // CHECK-NEXT: [[C_INT:%.+]] = moore.logic_to_int [[C]] : l1
   // CHECK-NEXT: [[CB:%.+]] = moore.to_builtin_int [[C_INT]] : i1
   // CHECK-NEXT: [[CLK:%.+]] = moore.read [[CLKWIRE]] : <l1>
@@ -468,9 +467,10 @@ module SampleValueBuiltins #() (
   // CHECK-NEXT: [[C2_INT:%.+]] = moore.logic_to_int [[C2]] : l1
   // CHECK-NEXT: [[CURRENT:%.+]] = moore.to_builtin_int [[C2_INT]] : i1
   // CHECK-NEXT: [[SAMPLED:%.+]] = ltl.sampled [[CURRENT]] : i1
+  // CHECK: ltl.clock
+  // CHECK: verif.assert
   sampled_clk: assert property (@(posedge clk_i) clk_i |=> $sampled(clk_i));
-  // CHECK: moore.procedure always {
-  // CHECK-NEXT: [[C:%.+]] = moore.read [[CLKWIRE]] : <l1>
+  // CHECK: [[C:%.+]] = moore.read [[CLKWIRE]] : <l1>
   // CHECK-NEXT: [[C_INT:%.+]] = moore.logic_to_int [[C]] : l1
   // CHECK-NEXT: [[CB:%.+]] = moore.to_builtin_int [[C_INT]] : i1
   // CHECK-NEXT: [[CLK:%.+]] = moore.read [[CLKWIRE]] : <l1>
@@ -481,10 +481,11 @@ module SampleValueBuiltins #() (
   // CHECK-NEXT: [[CURRENT:%.+]] = moore.to_builtin_int [[C2_INT]] : i1
   // CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 clk [[CLK_I1]] : i1
   // CHECK-NEXT: [[ROSE:%.+]] = comb.icmp ult [[PAST]], [[CURRENT]] : i1
+  // CHECK: ltl.clock
+  // CHECK: verif.assert
   rising_clk: assert property (@(posedge clk_i) clk_i |=> $rose(clk_i));
   // Check that the output of rose can be used by non-LTL ops
-  // CHECK: moore.procedure always {
-  // CHECK-NEXT: [[C1:%.+]] = moore.read [[CLKWIRE]] : <l1>
+  // CHECK: [[C1:%.+]] = moore.read [[CLKWIRE]] : <l1>
   // CHECK-NEXT: [[CLK:%.+]] = moore.read [[CLKWIRE]] : <l1>
   // CHECK-NEXT: [[CLK_INT:%.+]] = moore.logic_to_int [[CLK]] : l1
   // CHECK-NEXT: [[CLK_I1:%.+]] = moore.to_builtin_int [[CLK_INT]] : i1
@@ -496,9 +497,10 @@ module SampleValueBuiltins #() (
   // CHECK-NEXT: [[ROSE_INT:%.+]] = moore.from_builtin_int [[ROSE]] : i1
   // CHECK-NEXT: [[ROSE_LOGIC:%.+]] = moore.int_to_logic [[ROSE_INT]] : i1
   // CHECK-NEXT: [[EQ:%.+]] = moore.eq [[C1]], [[ROSE_LOGIC]] : l1 -> l1
+  // CHECK: ltl.clock
+  // CHECK: verif.assert
   rose_eq: assert property (@(posedge clk_i) clk_i == $rose(clk_i));
-  // CHECK: moore.procedure always {
-  // CHECK-NEXT: [[C:%.+]] = moore.read [[CLKWIRE]] : <l1>
+  // CHECK: [[C:%.+]] = moore.read [[CLKWIRE]] : <l1>
   // CHECK-NEXT: [[C_INT:%.+]] = moore.logic_to_int [[C]] : l1
   // CHECK-NEXT: [[CB:%.+]] = moore.to_builtin_int [[C_INT]] : i1
   // CHECK-NEXT: [[CLK:%.+]] = moore.read [[CLKWIRE]] : <l1>
@@ -509,10 +511,11 @@ module SampleValueBuiltins #() (
   // CHECK-NEXT: [[CURRENT:%.+]] = moore.to_builtin_int [[C2_INT]] : i1
   // CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 clk [[CLK_I1]] : i1
   // CHECK-NEXT: [[FELL:%.+]] = comb.icmp ugt [[PAST]], [[CURRENT]] : i1
+  // CHECK: ltl.clock
+  // CHECK: verif.assert
   falling_clk: assert property (@(posedge clk_i) clk_i |=> $fell(clk_i));
   // Check that the output of fell can be used by non-LTL ops
-  // CHECK: moore.procedure always {
-  // CHECK-NEXT: [[C1:%.+]] = moore.read [[CLKWIRE]] : <l1>
+  // CHECK: [[C1:%.+]] = moore.read [[CLKWIRE]] : <l1>
   // CHECK-NEXT: [[CLK:%.+]] = moore.read [[CLKWIRE]] : <l1>
   // CHECK-NEXT: [[CLK_INT:%.+]] = moore.logic_to_int [[CLK]] : l1
   // CHECK-NEXT: [[CLK_I1:%.+]] = moore.to_builtin_int [[CLK_INT]] : i1
@@ -524,9 +527,10 @@ module SampleValueBuiltins #() (
   // CHECK-NEXT: [[FELL_INT:%.+]] = moore.from_builtin_int [[FELL]] : i1
   // CHECK-NEXT: [[FELL_LOGIC:%.+]] = moore.int_to_logic [[FELL_INT]] : i1
   // CHECK-NEXT: [[EQ:%.+]] = moore.eq [[C1]], [[FELL_LOGIC]] : l1 -> l1
+  // CHECK: ltl.clock
+  // CHECK: verif.assert
   fell_eq: assert property (@(posedge clk_i) clk_i == $fell(clk_i));
-  // CHECK: moore.procedure always {
-  // CHECK-NEXT: [[C:%.+]] = moore.read [[CLKWIRE]] : <l1>
+  // CHECK: [[C:%.+]] = moore.read [[CLKWIRE]] : <l1>
   // CHECK-NEXT: [[C_INT:%.+]] = moore.logic_to_int [[C]] : l1
   // CHECK-NEXT: [[CB:%.+]] = moore.to_builtin_int [[C_INT]] : i1
   // CHECK-NEXT: [[CLK:%.+]] = moore.read [[CLKWIRE]] : <l1>
@@ -537,10 +541,11 @@ module SampleValueBuiltins #() (
   // CHECK-NEXT: [[CURRENT:%.+]] = moore.to_builtin_int [[C2_INT]] : i1
   // CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 clk [[CLK_I1]] : i1
   // CHECK-NEXT: [[STABLE:%.+]] = comb.icmp eq [[PAST]], [[CURRENT]] : i1
+  // CHECK: ltl.clock
+  // CHECK: verif.assert
   stable_clk: assert property (@(posedge clk_i) clk_i |=> $stable(clk_i));
   // Check that the output of stable can be used by non-LTL ops
-  // CHECK: moore.procedure always {
-  // CHECK-NEXT: [[C1:%.+]] = moore.read [[CLKWIRE]] : <l1>
+  // CHECK: [[C1:%.+]] = moore.read [[CLKWIRE]] : <l1>
   // CHECK-NEXT: [[CLK:%.+]] = moore.read [[CLKWIRE]] : <l1>
   // CHECK-NEXT: [[CLK_INT:%.+]] = moore.logic_to_int [[CLK]] : l1
   // CHECK-NEXT: [[CLK_I1:%.+]] = moore.to_builtin_int [[CLK_INT]] : i1
@@ -552,9 +557,10 @@ module SampleValueBuiltins #() (
   // CHECK-NEXT: [[STABLE_INT:%.+]] = moore.from_builtin_int [[STABLE]] : i1
   // CHECK-NEXT: [[STABLE_LOGIC:%.+]] = moore.int_to_logic [[STABLE_INT]] : i1
   // CHECK-NEXT: [[EQ:%.+]] = moore.eq [[C1]], [[STABLE_LOGIC]] : l1 -> l1
+  // CHECK: ltl.clock
+  // CHECK: verif.assert
   stable_eq: assert property (@(posedge clk_i) clk_i == $stable(clk_i));
-  // CHECK: moore.procedure always {
-  // CHECK-NEXT: [[C:%.+]] = moore.read [[CLKWIRE]] : <l1>
+  // CHECK: [[C:%.+]] = moore.read [[CLKWIRE]] : <l1>
   // CHECK-NEXT: [[C_INT:%.+]] = moore.logic_to_int [[C]] : l1
   // CHECK-NEXT: [[CB:%.+]] = moore.to_builtin_int [[C_INT]] : i1
   // CHECK-NEXT: [[CLK:%.+]] = moore.read [[CLKWIRE]] : <l1>
@@ -565,10 +571,11 @@ module SampleValueBuiltins #() (
   // CHECK-NEXT: [[CURRENT:%.+]] = moore.to_builtin_int [[C2_INT]] : i1
   // CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 clk [[CLK_I1]] : i1
   // CHECK-NEXT: [[CHANGED:%.+]] = comb.icmp ne [[PAST]], [[CURRENT]] : i1
+  // CHECK: ltl.clock
+  // CHECK: verif.assert
   changed_clk: assert property (@(posedge clk_i) clk_i |=> $changed(clk_i));
   // Check that the output of changed can be used by non-LTL ops
-  // CHECK: moore.procedure always {
-  // CHECK-NEXT: [[C1:%.+]] = moore.read [[CLKWIRE]] : <l1>
+  // CHECK: [[C1:%.+]] = moore.read [[CLKWIRE]] : <l1>
   // CHECK-NEXT: [[CLK:%.+]] = moore.read [[CLKWIRE]] : <l1>
   // CHECK-NEXT: [[CLK_INT:%.+]] = moore.logic_to_int [[CLK]] : l1
   // CHECK-NEXT: [[CLK_I1:%.+]] = moore.to_builtin_int [[CLK_INT]] : i1
@@ -580,9 +587,10 @@ module SampleValueBuiltins #() (
   // CHECK-NEXT: [[CHANGED_INT:%.+]] = moore.from_builtin_int [[CHANGED]] : i1
   // CHECK-NEXT: [[CHANGED_LOGIC:%.+]] = moore.int_to_logic [[CHANGED_INT]] : i1
   // CHECK-NEXT: [[EQ:%.+]] = moore.eq [[C1]], [[CHANGED_LOGIC]] : l1 -> l1
+  // CHECK: ltl.clock
+  // CHECK: verif.assert
   changed_eq: assert property (@(posedge clk_i) clk_i == $changed(clk_i));
-  // CHECK: moore.procedure always {
-  // CHECK-NEXT: [[C:%.+]] = moore.read [[CLKWIRE]] : <l1>
+  // CHECK: [[C:%.+]] = moore.read [[CLKWIRE]] : <l1>
   // CHECK-NEXT: [[C_INT:%.+]] = moore.logic_to_int [[C]] : l1
   // CHECK-NEXT: [[CB:%.+]] = moore.to_builtin_int [[C_INT]] : i1
   // CHECK-NEXT: [[CLK:%.+]] = moore.read [[CLKWIRE]] : <l1>
@@ -592,10 +600,11 @@ module SampleValueBuiltins #() (
   // CHECK-NEXT: [[C2_INT:%.+]] = moore.logic_to_int [[C2]] : l1
   // CHECK-NEXT: [[CURRENT:%.+]] = moore.to_builtin_int [[C2_INT]] : i1
   // CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 clk [[CLK_I1]] : i1
+  // CHECK: ltl.clock
+  // CHECK: verif.assert
   past_clk: assert property (@(posedge clk_i) clk_i |=> $past(clk_i));
   // Check that the output of past can be used by non-LTL ops
-  // CHECK: moore.procedure always {
-  // CHECK-NEXT: [[C1:%.+]] = moore.read [[CLKWIRE]] : <l1>
+  // CHECK: [[C1:%.+]] = moore.read [[CLKWIRE]] : <l1>
   // CHECK-NEXT: [[CLK:%.+]] = moore.read [[CLKWIRE]] : <l1>
   // CHECK-NEXT: [[CLK_INT:%.+]] = moore.logic_to_int [[CLK]] : l1
   // CHECK-NEXT: [[CLK_I1:%.+]] = moore.to_builtin_int [[CLK_INT]] : i1
@@ -606,10 +615,11 @@ module SampleValueBuiltins #() (
   // CHECK-NEXT: [[PAST_INT:%.+]] = moore.from_builtin_int [[PAST]] : i1
   // CHECK-NEXT: [[PAST_LOGIC:%.+]] = moore.int_to_logic [[PAST_INT]] : i1
   // CHECK-NEXT: [[EQ:%.+]] = moore.eq [[C1]], [[PAST_LOGIC]] : l1 -> l1
+  // CHECK: ltl.clock
+  // CHECK: verif.assert
   past_eq: assert property (@(posedge clk_i) clk_i == $past(clk_i));
   // Test $past on wider bitvectors
-  // CHECK: moore.procedure always {
-  // CHECK-NEXT: [[D1:%.+]] = moore.read [[DATAWIRE]] : <l8>
+  // CHECK: [[D1:%.+]] = moore.read [[DATAWIRE]] : <l8>
   // CHECK-NEXT: [[CLK:%.+]] = moore.read [[CLKWIRE]] : <l1>
   // CHECK-NEXT: [[CLK_INT:%.+]] = moore.logic_to_int [[CLK]] : l1
   // CHECK-NEXT: [[CLK_I1:%.+]] = moore.to_builtin_int [[CLK_INT]] : i1
@@ -620,18 +630,19 @@ module SampleValueBuiltins #() (
   // CHECK-NEXT: [[PAST_INT:%.+]] = moore.from_builtin_int [[PAST]] : i8
   // CHECK-NEXT: [[PAST_LOGIC:%.+]] = moore.int_to_logic [[PAST_INT]] : i8
   // CHECK-NEXT: [[EQ:%.+]] = moore.eq [[D1]], [[PAST_LOGIC]] : l8 -> l1
+  // CHECK: ltl.clock
+  // CHECK: verif.assert
   past_data: assert property (@(posedge clk_i) data_i == $past(data_i));
 
-  // CHECK: moore.procedure always {
   // CHECK: [[D:%.+]] = moore.read [[DATAWIRE]] : <l8>
   // CHECK: [[RED:%.+]] = moore.reduce_xor [[D]] : l8 -> l1
   // CHECK: [[X:%.+]] = moore.constant bX : l1
   // CHECK: [[CEQ:%.+]] = moore.case_eq [[RED]], [[X]] : l1
   // CHECK: [[CEQ_I1:%.+]] = moore.to_builtin_int [[CEQ]] : i1
   // CHECK: ltl.clock [[CEQ_I1]]
+  // CHECK: verif.assert
   isunknown_data: assert property (@(posedge clk_i) $isunknown(data_i));
 
-  // CHECK: moore.procedure always {
   // CHECK: [[D:%.+]] = moore.read [[DATAWIRE]] : <l8>
   // CHECK: [[RED:%.+]] = moore.reduce_xor [[D]] : l8 -> l1
   // CHECK: [[X:%.+]] = moore.constant bX : l1
@@ -650,9 +661,9 @@ module SampleValueBuiltins #() (
   // CHECK: [[RES_LOGIC:%.+]] = moore.int_to_logic [[RES_INT]] : i1
   // CHECK: [[RES_BUILTIN:%.+]] = moore.to_builtin_int [[RES_INT]] : i1
   // CHECK: ltl.clock [[RES_BUILTIN]]
+  // CHECK: verif.assert
   onehot0_data: assert property (@(posedge clk_i) $onehot0(data_i));
 
-  // CHECK: moore.procedure always {
   // CHECK: [[D:%.+]] = moore.read [[DATAWIRE]] : <l8>
   // CHECK: [[RED:%.+]] = moore.reduce_xor [[D]] : l8 -> l1
   // CHECK: [[X:%.+]] = moore.constant bX : l1
@@ -673,9 +684,9 @@ module SampleValueBuiltins #() (
   // CHECK: [[RES_LOGIC:%.+]] = moore.int_to_logic [[RES_INT]] : i1
   // CHECK: [[RES_BUILTIN:%.+]] = moore.to_builtin_int [[RES_INT]] : i1
   // CHECK: ltl.clock [[RES_BUILTIN]]
+  // CHECK: verif.assert
   onehot_data: assert property (@(posedge clk_i) $onehot(data_i));
 
-  // CHECK: moore.procedure always {
   // CHECK: [[D:%.+]] = moore.read [[DATABITWIRE]] : <i8>
   // CHECK: [[DB:%.+]] = moore.to_builtin_int [[D]] : i8
   // CHECK: [[ONE:%.+]] = hw.constant 1 : i8
@@ -686,9 +697,9 @@ module SampleValueBuiltins #() (
   // CHECK: [[EQ_INT:%.+]] = moore.from_builtin_int [[EQ]] : i1
   // CHECK: [[EQ_BUILTIN:%.+]] = moore.to_builtin_int [[EQ_INT]] : i1
   // CHECK: ltl.clock [[EQ_BUILTIN]]
+  // CHECK: verif.assert
   onehot0_bit_data: assert property (@(posedge clk_i) $onehot0(data_bit_i));
 
-  // CHECK: moore.procedure always {
   // CHECK: [[D:%.+]] = moore.read [[DATABITWIRE]] : <i8>
   // CHECK: [[DB:%.+]] = moore.to_builtin_int [[D]] : i8
   // CHECK: [[ONE:%.+]] = hw.constant 1 : i8
@@ -701,9 +712,9 @@ module SampleValueBuiltins #() (
   // CHECK: [[RES_INT:%.+]] = moore.from_builtin_int [[AND2]] : i1
   // CHECK: [[RES_BUILTIN:%.+]] = moore.to_builtin_int [[RES_INT]] : i1
   // CHECK: ltl.clock [[RES_BUILTIN]]
+  // CHECK: verif.assert
   onehot_bit_data: assert property (@(posedge clk_i) $onehot(data_bit_i));
 
-  // CHECK: moore.procedure always {
   // CHECK: [[D:%.+]] = moore.read [[DATAWIRE]] : <l8>
   // CHECK: [[D_L2I:%.+]] = moore.logic_to_int [[D]] : l8
   // CHECK: [[DB:%.+]] = moore.to_builtin_int [[D_L2I]] : i8
@@ -716,10 +727,11 @@ module SampleValueBuiltins #() (
   // CHECK: [[SEXT:%.+]] = moore.zext [[RES_INT]] : i4 -> i32
   // CHECK: [[ZERO:%.+]] = moore.constant 0 : i32
   // CHECK: [[EQ:%.+]] = moore.eq [[SEXT]], [[ZERO]] : i32 -> i1
+  // CHECK: ltl.clock
+  // CHECK: verif.assert
   countones_data:
     assert property (@(posedge clk_i) $countones(data_i) == 0);
 
-  // CHECK: moore.procedure always {
   // CHECK: [[D:%.+]] = moore.read [[DATABITWIRE]] : <i8>
   // CHECK: [[DB:%.+]] = moore.to_builtin_int [[D]] : i8
   // CHECK: [[Z3:%.+]] = hw.constant 0 : i3
@@ -732,6 +744,8 @@ module SampleValueBuiltins #() (
   // CHECK: [[SEXT:%.+]] = moore.zext [[RES_INT]] : i4 -> i32
   // CHECK: [[ZERO:%.+]] = moore.constant 0 : i32
   // CHECK: [[EQ:%.+]] = moore.eq [[SEXT]], [[ZERO]] : i32 -> i1
+  // CHECK: ltl.clock
+  // CHECK: verif.assert
   countones_bit_data:
     assert property (@(posedge clk_i) $countones(data_bit_i) == 0);
 endmodule
diff --git a/test/Conversion/ImportVerilog/labeled-concurrent-assertions.sv b/test/Conversion/ImportVerilog/labeled-concurrent-assertions.sv
new file mode 100644
index 000000000000..ac179bae26c9
--- /dev/null
+++ b/test/Conversion/ImportVerilog/labeled-concurrent-assertions.sv
@@ -0,0 +1,38 @@
+// RUN: circt-translate --import-verilog %s | FileCheck %s
+// REQUIRES: slang
+// UNSUPPORTED: valgrind
+
+// A statement label on a module-level concurrent assertion (`CHK: assert
+// property (p);`) wraps the statement in a single-statement block, which
+// used to defeat the module-scope conversion short-circuit: the labeled
+// assertion converted inside a `moore.procedure always` while its unlabeled
+// twin converted at module scope, so downstream consumers of module-scope
+// assertions never saw the labeled one. A label must not change which
+// lowering an assertion gets.
+
+// CHECK-LABEL: moore.module @LabeledAssert
+module LabeledAssert(input logic clk, input logic a, input logic b);
+  // Unlabeled and labeled convert identically, at module scope.
+  // CHECK: ltl.implication
+  // CHECK: ltl.clock
+  // CHECK: verif.assert
+  // CHECK: ltl.implication
+  // CHECK: ltl.clock
+  // CHECK: verif.assert
+  // CHECK-NOT: moore.procedure
+  assert property (@(posedge clk) a |-> b);
+  CHK: assert property (@(posedge clk) a |-> b);
+endmodule
+
+// Concurrent assertions written in an `initial` block have one-attempt
+// semantics (IEEE 1800-2017 16.14.6) and must NOT be rerouted to a
+// continuous module-scope assertion by the label look-through.
+// CHECK-LABEL: moore.module @InitialNotRerouted
+module InitialNotRerouted(input logic clk, input logic a);
+  // CHECK: moore.procedure initial
+  // CHECK: ltl.clock
+  // CHECK: verif.assert
+  initial begin
+    LBL2: assert property (@(posedge clk) a);
+  end
+endmodule