From 729e0abf7268b41e43d61fa2e720c486158d3ac1 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 16 Jan 2025 10:13:51 -0800 Subject: [PATCH] SystemVerilog: allow SVA in property ... endproperty This changes the type checker to allow SVA in property ... endproperty. --- regression/verilog/property/named_property2.desc | 4 +--- src/verilog/verilog_typecheck.cpp | 2 +- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/regression/verilog/property/named_property2.desc b/regression/verilog/property/named_property2.desc index a24ff735..23e5c031 100644 --- a/regression/verilog/property/named_property2.desc +++ b/regression/verilog/property/named_property2.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE named_property2.sv --bound 20 ^\[main\.assert\.1\] always main\.x_is_eventually_ten: PROVED up to bound 20$ @@ -7,5 +7,3 @@ named_property2.sv -- ^warning: ignoring -- -The type checker only allows expressions, not properties in property ... -endproperty. diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index 21495841..b2134c08 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{};