circt/test/firtool/chisel_assert.fir

59 lines
2.1 KiB
Plaintext

; RUN: firtool %s --add-companion-assume | FileCheck %s
FIRRTL version 4.0.0
circuit ChiselVerif:
; CHECK: module ChiselVerif
public module ChiselVerif:
input clock: Clock
input cond: UInt<1>
input enable: UInt<1>
; CHECK: wire [[GEN:.+]] = ~enable | cond;
; CHECK: assert property
; CHECK-NOT: $error
intrinsic(circt_chisel_assert, clock, cond, enable)
; CHECK: `ifdef MACRO_GUARD
; CHECK-NEXT: `ifdef ASDF
; CHECK: label_for_assert_with_format_string
; CHECK: assert property
; CHECK: "message: %d"
; CHECK: $sampled(cond)
intrinsic(circt_chisel_assert<format = "message: %d",
label = "label for assert with format string",
guards = "MACRO_GUARD;ASDF">,
clock, cond, enable, cond)
; Special if-else-fatal pattern, assert-like.
; No guards or labels for normal emission flow.
; CHECK: $error("ief: %d"
; CHECK: $fatal
intrinsic(circt_chisel_ifelsefatal<format = "ief: %d",
label = "label for ifelsefatal assert",
guards = "MACRO_GUARD;ASDF">,
clock, cond, enable, enable)
; CHECK: `ifdef USE_PROPERTY_AS_CONSTRAINT
; CHECK-NEXT: assume property (@(posedge clock) [[GEN]]);
; CHECK-NEXT: `ifdef MACRO_GUARD
; CHECK-NEXT: `ifdef ASDF
; CHECK-NEXT: assume__label_for_assert_with_format_string:
; CHECK-NEXT: assume property (@(posedge clock) [[GEN]]);
; CHECK-NEXT: assume__label_for_ifelsefatal_assert:
; CHECK-SAME: assume property (@(posedge clock) [[GEN]]);
; CHECK-NEXT: `endif
; CHECK-NEXT: `endif
; CHECK-NEXT:`endif
; CHECK: label_for_assume
; CHECK: assume property
; CHECK: "text: %d"
; CHECK: $sampled(enable)
intrinsic(circt_chisel_assume<format = "text: %d",
label = "label for assume">,
clock, cond, enable, enable)
; CHECK: label_for_cover
; CHECK: cover property
intrinsic(circt_chisel_cover<label = "label for cover">,
clock, cond, enable)