diff --git a/regression/verilog/SVA/named_property1.desc b/regression/verilog/property/named_property1.desc similarity index 100% rename from regression/verilog/SVA/named_property1.desc rename to regression/verilog/property/named_property1.desc diff --git a/regression/verilog/SVA/named_property1.sv b/regression/verilog/property/named_property1.sv similarity index 100% rename from regression/verilog/SVA/named_property1.sv rename to regression/verilog/property/named_property1.sv diff --git a/regression/verilog/property/named_property2.desc b/regression/verilog/property/named_property2.desc new file mode 100644 index 000000000..a24ff735d --- /dev/null +++ b/regression/verilog/property/named_property2.desc @@ -0,0 +1,11 @@ +KNOWNBUG +named_property2.sv +--bound 20 +^\[main\.assert\.1\] always main\.x_is_eventually_ten: PROVED up to bound 20$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +The type checker only allows expressions, not properties in property ... +endproperty. diff --git a/regression/verilog/property/named_property2.sv b/regression/verilog/property/named_property2.sv new file mode 100644 index 000000000..8e602154b --- /dev/null +++ b/regression/verilog/property/named_property2.sv @@ -0,0 +1,12 @@ +module main(input clk); + + reg [31:0] x = 0; + always_ff @(posedge clk) x++; + + property x_is_eventually_ten; + s_eventually x == 10 + endproperty : x_is_eventually_ten + + assert property (x_is_eventually_ten); + +endmodule diff --git a/regression/verilog/SVA/recursive_property1.desc b/regression/verilog/property/recursive_property1.desc similarity index 100% rename from regression/verilog/SVA/recursive_property1.desc rename to regression/verilog/property/recursive_property1.desc diff --git a/regression/verilog/SVA/recursive_property1.sv b/regression/verilog/property/recursive_property1.sv similarity index 100% rename from regression/verilog/SVA/recursive_property1.sv rename to regression/verilog/property/recursive_property1.sv