From ffa161e9538539efd47166e99016b6c6ac9c1ab5 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 27 Aug 2025 08:57:53 -0700 Subject: [PATCH] KNOWNBUG test for property that is a sequence --- regression/verilog/property/named_property4.desc | 9 +++++++++ regression/verilog/property/named_property4.sv | 10 ++++++++++ 2 files changed, 19 insertions(+) create mode 100644 regression/verilog/property/named_property4.desc create mode 100644 regression/verilog/property/named_property4.sv diff --git a/regression/verilog/property/named_property4.desc b/regression/verilog/property/named_property4.desc new file mode 100644 index 000000000..6d543939e --- /dev/null +++ b/regression/verilog/property/named_property4.desc @@ -0,0 +1,9 @@ +KNOWNBUG +named_property4.sv + +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +This triggers an internal error. diff --git a/regression/verilog/property/named_property4.sv b/regression/verilog/property/named_property4.sv new file mode 100644 index 000000000..95ff50a3a --- /dev/null +++ b/regression/verilog/property/named_property4.sv @@ -0,0 +1,10 @@ +module main(input a, b); + + // a property that is a sequence + property lemma; + a ##1 b + endproperty + + assert property (lemma); + +endmodule