Printf-encoded verification deprecation

[dtzSiFive]

Summary

Using printf strings to encode verification operations is deprecated. This is a transparent change to Chisel users, as Chisel no longer uses this for assert/assume/cover.

For the deprecation period, a warning will be emitted for these, and eventually this will be treated just like any other printf.

If you're seeing the warning, you should migrate to using intrinsics instead, and eventually FIRRTL will support what's needed without intrinsics. Post on this thread if you have any questions or concerns.

Details

Historically, special printf strings nested within when statements were used to encode various verification intent. While normal assert/assume/cover statements are emitted by Chisel they're always placeholders with the printf containing a payload indicating what really is requested. For example:

FIRRTL version 4.0.0
circuit TestCover:
  public module TestCover:
    input clock: Clock
    input cond: UInt<1>
    input enable: UInt<1>
    input value: UInt<5>

    assert(clock, cond, enable, "hello")
    when not(cond):
      printf(clock, enable, "Assertion failed: [verif-library-assume]<extraction-summary>{\"predicateModifier\":{\"type\":\"noMod\"},\"conditionalCompileToggles\":[{\"type\":\"unrOnly\"},{\"type\":\"formalOnly\"}],\"labelExts\":[\"assume\",\"label\"],\"format\":{\"type\":\"ifElseFatal\"},\"baseMsg\":\"assume hello world testing: %d\"}", value)

Which generates:

// Generated by CIRCT firtool-1.73.0g20240430_3ef492c
module TestCover(
  input       clock,
              cond,
              enable,
  input [4:0] value
);

  `ifdef USE_UNR_ONLY_CONSTRAINTS
    `ifdef USE_FORMAL_ONLY_CONSTRAINTS
      assume__verif_library_assume_label:
        assume property (@(posedge clock) ~enable | cond)
        else $error("assume hello world testing: %d", $sampled(value));
    `endif // USE_FORMAL_ONLY_CONSTRAINTS
  `endif // USE_UNR_ONLY_CONSTRAINTS
endmodule

Examples include variations of assert, assume, and cover -- with more control over their lowering, inserted preprocessor guards, and other features.

These have been deprecated in favor of using intrinsics, see: https://circt.llvm.org/docs/Dialects/FIRRTL/FIRRTLIntrinsics/ .

The end-goal is to extend FIRRTL so that the standard assert/assume/cover and other language features are enough for our needs. Until then, intrinsics have been added and should be used instead.

The example above is captured using the assume intrinsic:

FIRRTL version 4.0.0
circuit TestCover:
  public module TestCover:
    input clock: Clock
    input cond: UInt<1>
    input enable: UInt<1>
    input value: UInt<5>

    intrinsic(circt_chisel_assume<label="verif_library_assume_label", format="assume hello world testing: %d", guards = "USE_UNR_ONLY_CONSTRAINTS;USE_FORMAL_ONLY_CONSTRAINTS">, clock, cond, enable, value)