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..23e5c031a --- /dev/null +++ b/regression/verilog/property/named_property2.desc @@ -0,0 +1,9 @@ +CORE +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 +-- 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 diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index 21495841a..b2134c086 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -1770,7 +1770,7 @@ void verilog_typecheckt::convert_property_declaration( auto base_name = declaration.base_name(); auto full_identifier = hierarchical_identifier(base_name); - convert_expr(declaration.cond()); + convert_sva(declaration.cond()); make_boolean(declaration.cond()); auto type = bool_typet{};