[ImportVerilog] Look through labels on module-level concurrent assertions

[AmurG]

A statement label on a module-level concurrent assertion wraps it in a single-statement block, which defeats the module-scope conversion short-circuit. On current main the labeled assertion converts inside a moore.procedure always while its unlabeled twin converts at module scope, so a label silently changes which lowering an assertion gets:

module top(input logic clk, input logic a, input logic b);
  assert property (@(posedge clk) a |-> b);       // verif.clocked_assert at module scope
  CHK: assert property (@(posedge clk) a |-> b);  // same ops, nested in moore.procedure
endmodule

Labeled checkers are the norm in verification IP, and our own builtins.sv documents the artifact: its 19 labeled sampled-value assertions pin moore.procedure always wrappers that their unlabeled equivalents would not get.

Look through label blocks in the synthesized always wrapper so labeled and unlabeled assertions take the same path; for a body that reduces to a single concurrent assertion the two forms are equivalent (IEEE 1800-2017 16.14.6). Assertions in initial/final procedures keep their one-attempt semantics and are deliberately not rerouted.

Tested: new labeled-concurrent-assertions.sv (labeled == unlabeled at module scope; initial-block form not rerouted); builtins.sv expectations updated to the module-scope form (same per-assertion op chains, each block anchored on its ltl.clock + verif.assert).

Written with AI assistance; I've reviewed the diff and tests.

[circt-bot]

Results of circt-tests run for 9b73522 compared to results for 01b5614: no change to test results.