From 113faf902a1cae54b2e42558ca8b8cc69ba025e3 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Tue, 18 Nov 2025 10:19:24 -0800
Subject: [PATCH] ebmc language interface implementation for Verilog

This adds an implementation of the ebmc_languaget interface for Verilog.
---
 src/ebmc/build_transition_system.cpp  |  9 ++-
 src/verilog/Makefile                  |  1 +
 src/verilog/verilog_ebmc_language.cpp | 85 +++++++++++++++++++++++++++
 src/verilog/verilog_ebmc_language.h   | 34 +++++++++++
 4 files changed, 127 insertions(+), 2 deletions(-)
 create mode 100644 src/verilog/verilog_ebmc_language.cpp
 create mode 100644 src/verilog/verilog_ebmc_language.h

diff --git a/src/ebmc/build_transition_system.cpp b/src/ebmc/build_transition_system.cpp
index f14dc10b6..cd8ca661b 100644
--- a/src/ebmc/build_transition_system.cpp
+++ b/src/ebmc/build_transition_system.cpp
@@ -21,6 +21,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <smvlang/smv_ebmc_language.h>
 #include <trans-word-level/show_module_hierarchy.h>
 #include <trans-word-level/show_modules.h>
+#include <verilog/verilog_ebmc_language.h>
 
 #include "ebmc_error.h"
 #include "ebmc_language_file.h"
@@ -372,7 +373,7 @@ std::optional<transition_systemt> ebmc_languagest::transition_system()
   {
     return smv_ebmc_languaget{cmdline, message_handler}.transition_system();
   }
-  else
+  else if(have_verilog)
   {
     if(cmdline.isset("preprocess"))
     {
@@ -406,6 +407,10 @@ std::optional<transition_systemt> ebmc_languagest::transition_system()
       return {};
     }
 
-    return get_transition_system(cmdline, message_handler);
+    return verilog_ebmc_languaget{cmdline, message_handler}.transition_system();
+  }
+  else
+  {
+    throw ebmc_errort{} << "no support for given input file extensions";
   }
 }
diff --git a/src/verilog/Makefile b/src/verilog/Makefile
index cfa50473c..62c341fbf 100644
--- a/src/verilog/Makefile
+++ b/src/verilog/Makefile
@@ -4,6 +4,7 @@ SRC = aval_bval_encoding.cpp \
       sva_expr.cpp \
       typename.cpp \
       verilog_bits.cpp \
+      verilog_ebmc_language.cpp \
       verilog_elaborate.cpp \
       verilog_elaborate_type.cpp \
       verilog_expr.cpp \
diff --git a/src/verilog/verilog_ebmc_language.cpp b/src/verilog/verilog_ebmc_language.cpp
new file mode 100644
index 000000000..c5d000c47
--- /dev/null
+++ b/src/verilog/verilog_ebmc_language.cpp
@@ -0,0 +1,85 @@
+/*******************************************************************\
+
+Module: Verilog Language Interface
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+/// \file
+/// Verilog Language Interface
+
+#include "verilog_ebmc_language.h"
+
+#include <util/cmdline.h>
+#include <util/get_module.h>
+#include <util/suffix.h>
+#include <util/unicode.h>
+
+#include <ebmc/ebmc_error.h>
+#include <ebmc/transition_system.h>
+
+#include "verilog_parser.h"
+#include "verilog_typecheck.h"
+
+#include <fstream>
+
+std::string verilog_file_name(const cmdlinet &cmdline)
+{
+  if(cmdline.args.size() == 0)
+    throw ebmc_errort{} << "no file name given";
+
+  if(cmdline.args.size() >= 2)
+    throw ebmc_errort{}.with_exit_code(1) << "give a single file only";
+
+  return cmdline.args.front();
+}
+
+verilog_parse_treet verilog_ebmc_languaget::parse()
+{
+  auto file_name = verilog_file_name(cmdline);
+
+  verilog_standardt standard;
+
+  if(has_suffix(file_name, ".sv") || cmdline.isset("systemverilog"))
+    standard = verilog_standardt::SV2023;
+  else if(cmdline.isset("vl2smv-extensions"))
+    standard = verilog_standardt::V2005_SMV;
+  else
+    standard = verilog_standardt::V2005_SMV;
+
+  verilog_parsert verilog_parser{standard, message_handler};
+
+  std::ifstream infile{widen_if_needed(file_name)};
+
+  if(!infile)
+    throw ebmc_errort{} << "failed to open " << file_name;
+
+  verilog_parser.set_file(file_name);
+  verilog_parser.in = &infile;
+
+  if(verilog_parser.parse())
+    throw ebmc_errort{} << "parsing has failed";
+
+  return std::move(verilog_parser.parse_tree);
+}
+
+std::optional<transition_systemt> verilog_ebmc_languaget::transition_system()
+{
+  auto parse_tree = parse();
+
+  transition_systemt result;
+
+  if(verilog_typecheck(
+       parse_tree, result.symbol_table, "main", message_handler))
+  {
+    throw ebmc_errort{} << "typechecking has failed";
+  }
+
+  result.main_symbol =
+    &get_module(result.symbol_table, "main", message_handler);
+
+  result.trans_expr = to_trans_expr(result.main_symbol->value);
+
+  return result;
+}
diff --git a/src/verilog/verilog_ebmc_language.h b/src/verilog/verilog_ebmc_language.h
new file mode 100644
index 000000000..d4fa52f27
--- /dev/null
+++ b/src/verilog/verilog_ebmc_language.h
@@ -0,0 +1,34 @@
+/*******************************************************************\
+
+Module: Verilog Language Interface
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+/// \file
+/// SMV Language Interface
+
+#ifndef EBMC_VERILOG_LANGUAGE_H
+#define EBMC_VERILOG_LANGUAGE_H
+
+#include <ebmc/ebmc_language.h>
+
+class verilog_parse_treet;
+
+class verilog_ebmc_languaget : public ebmc_languaget
+{
+public:
+  verilog_ebmc_languaget(cmdlinet &_cmdline, message_handlert &_message_handler)
+    : ebmc_languaget(_cmdline, _message_handler)
+  {
+  }
+
+  // produce the transition system, and return it
+  std::optional<transition_systemt> transition_system() override;
+
+protected:
+  verilog_parse_treet parse();
+};
+
+#endif // EBMC_VERILOG_LANGUAGE_H