[major] Allow assert message to be a format string

[uenoku]

This commit allow assert statement's message string to be a format string which is corrently expressed as printf-encoded assertion. CIRCT side PR is https://github.com/llvm/circt/pull/6621

This also adds missing grammar for verif statements.

[jackkoenig]

Unless someone more clever than me has an idea on how this can be backwards compatible, I think this is a major change since assert and assume messages containing % will now be rejected

[dtzSiFive]

Unless someone more clever than me has an idea on how this can be backwards compatible, I think this is a major change since assert and assume messages containing % will now be rejected

If they contain invalid format strings (or missing arguments for the otherwise valid string) there will likely be problems and possibly rejected by tools.

This already is the case and has been for some time, FWIW, arguably this is updating the spec to reflect reality and to allow specifying operands for what's already a format string in practice. ..or implementation has been wrong for some time but even with that framing FWIW this is unlikely to break anything as a result.

But focusing solely on the FIRRTL spec what you say makes sense, but I don't think there's any utility in ensuring or worrying about backwards compatibility since in practice this isn't something folks are able to rely on today. So probably can rest easy on that front at least :+1: .

Example:

circuit Assert:
  module Assert:
    input clock: Clock
    input cond: UInt<1>
    input enable: UInt<1>

    assert(clock, cond, enable, "Testing: %d")

->

// Generated by CIRCT firtool-1.63.0g20240129_8e3d29f
module Assert(
  input clock,
        cond,
        enable
);

  always @(posedge clock) begin
    if (enable)
      assert(cond) else $error("Testing: %d");
  end // always @(posedge)
endmodule

Which if you consult your SV spec or feed through, e.g., verilator, will complain.

[uenoku]

Could someone merge this? Thanks!