Merge pull request #981 from diffblue/default-disable-iff-not-supported

SystemVerilog: parsing and type checking for default
diffblue · Feb 9, 2025 · e750bad · e750bad
2 parents 31591f7 + a489081
commit e750bad
Show file tree

Hide file tree

Showing 7 changed files with 38 additions and 2 deletions.
diff --git a/regression/verilog/SVA/default_disable1.desc b/regression/verilog/SVA/default_disable1.desc
@@ -1,7 +1,8 @@
-KNOWNBUG
+CORE
 default_disable1.sv
 
-^EXIT=10$
+^file .* line 5: default disable iff is unsupported$
+^EXIT=2$
 ^SIGNAL=0$
 --
 ^warning: ignoring

diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
@@ -80,6 +80,8 @@ IREP_ID_ONE(verilog_array_range)
 IREP_ID_ONE(verilog_assignment_pattern)
 IREP_ID_ONE(verilog_associative_array)
 IREP_ID_ONE(verilog_declarations)
+IREP_ID_ONE(verilog_default_clocking)
+IREP_ID_ONE(verilog_default_disable)
 IREP_ID_ONE(verilog_lifetime)
 IREP_ID_ONE(verilog_logical_equality)
 IREP_ID_ONE(verilog_logical_inequality)

diff --git a/src/verilog/parser.y b/src/verilog/parser.y
@@ -1032,7 +1032,9 @@ module_or_generate_item_declaration:
 	| genvar_declaration
 	| clocking_declaration
 	| TOK_DEFAULT TOK_CLOCKING clocking_identifier ';'
+		{ init($$, ID_verilog_default_clocking); mto($$, $3); }
 	| TOK_DEFAULT TOK_DISABLE TOK_IFF expression_or_dist ';'
+		{ init($$, ID_verilog_default_disable); mto($$, $4); }
 	;
 
 non_port_module_item:

diff --git a/src/verilog/verilog_elaborate.cpp b/src/verilog/verilog_elaborate.cpp
@@ -850,6 +850,12 @@ void verilog_typecheckt::collect_symbols(
   else if(module_item.id() == ID_verilog_covergroup)
   {
   }
+  else if(module_item.id() == ID_verilog_default_clocking)
+  {
+  }
+  else if(module_item.id() == ID_verilog_default_disable)
+  {
+  }
   else if(module_item.id() == ID_verilog_property_declaration)
   {
     collect_symbols(to_verilog_property_declaration(module_item));

diff --git a/src/verilog/verilog_interfaces.cpp b/src/verilog/verilog_interfaces.cpp
@@ -306,6 +306,12 @@ void verilog_typecheckt::interface_module_item(
   else if(module_item.id() == ID_verilog_covergroup)
   {
   }
+  else if(module_item.id() == ID_verilog_default_clocking)
+  {
+  }
+  else if(module_item.id() == ID_verilog_default_disable)
+  {
+  }
   else if(module_item.id() == ID_verilog_property_declaration)
   {
   }

diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp
@@ -3282,6 +3282,14 @@ void verilog_synthesist::synth_module_item(
   else if(module_item.id() == ID_verilog_covergroup)
   {
   }
+  else if(module_item.id() == ID_verilog_default_clocking)
+  {
+  }
+  else if(module_item.id() == ID_verilog_default_disable)
+  {
+    throw errort().with_location(module_item.source_location())
+      << "default disable iff is unsupported";
+  }
   else if(module_item.id() == ID_verilog_property_declaration)
   {
   }

diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp
@@ -1740,6 +1740,17 @@ void verilog_typecheckt::convert_module_item(
   else if(module_item.id() == ID_verilog_covergroup)
   {
   }
+  else if(module_item.id() == ID_verilog_default_clocking)
+  {
+    exprt &cond = to_unary_expr(module_item).op();
+    convert_expr(cond);
+  }
+  else if(module_item.id() == ID_verilog_default_disable)
+  {
+    exprt &cond = to_unary_expr(module_item).op();
+    convert_expr(cond);
+    make_boolean(cond);
+  }
   else if(module_item.id() == ID_verilog_property_declaration)
   {
     convert_property_declaration(to_verilog_property_declaration(module_item));