From a489081277da6187c085b0545313b4adc6c9f87c Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sun, 9 Feb 2025 09:05:25 +0000
Subject: [PATCH] SystemVerilog: parsing and type checking for default

This adds parsing and type checking for default clocking and default disable
iff.

Synthesis support is still missing.
---
 regression/verilog/SVA/default_disable1.desc |  5 +++--
 src/hw_cbmc_irep_ids.h                       |  2 ++
 src/verilog/parser.y                         |  2 ++
 src/verilog/verilog_elaborate.cpp            |  6 ++++++
 src/verilog/verilog_interfaces.cpp           |  6 ++++++
 src/verilog/verilog_synthesis.cpp            |  8 ++++++++
 src/verilog/verilog_typecheck.cpp            | 11 +++++++++++
 7 files changed, 38 insertions(+), 2 deletions(-)

diff --git a/regression/verilog/SVA/default_disable1.desc b/regression/verilog/SVA/default_disable1.desc
index 76d1f386c..4d1e4fad4 100644
--- 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
index c405df8de..2348f7870 100644
--- 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
index d8f6d5dc7..ee0a7ba31 100644
--- 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
index ccd7cce11..a6ab359eb 100644
--- 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
index d3d4721fc..692ea38a3 100644
--- 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
index e516dcc35..ee12837dc 100644
--- 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
index 03400d46c..d3519aa36 100644
--- 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));