diff --git a/src/ebmc/build_transition_system.cpp b/src/ebmc/build_transition_system.cpp
index dbedc5e13..17386fb0b 100644
--- a/src/ebmc/build_transition_system.cpp
+++ b/src/ebmc/build_transition_system.cpp
@@ -9,339 +9,16 @@ Author: Daniel Kroening, dkr@amazon.com
 #include "build_transition_system.h"
 
 #include <util/cmdline.h>
-#include <util/get_module.h>
 #include <util/message.h>
-#include <util/namespace.h>
-#include <util/options.h>
-#include <util/unicode.h>
 
-#include <langapi/language.h>
-#include <langapi/language_util.h>
-#include <langapi/mode.h>
 #include <smvlang/smv_ebmc_language.h>
-#include <trans-word-level/show_module_hierarchy.h>
+#include <verilog/verilog_ebmc_language.h>
 
 #include "ebmc_error.h"
-#include "ebmc_language_file.h"
-#include "ebmc_version.h"
-#include "output_file.h"
-#include "show_modules.h"
 #include "transition_system.h"
 
 #include <fstream>
-#include <iostream>
-
-void preprocess(const cmdlinet &cmdline, message_handlert &message_handler)
-{
-  messaget message(message_handler);
-
-  if(cmdline.args.size() != 1)
-    throw ebmc_errort{}.with_exit_code(1)
-      << "please give exactly one file to preprocess";
-
-  const auto &filename = cmdline.args.front();
-  std::ifstream infile(widen_if_needed(filename));
-
-  if(!infile)
-    throw ebmc_errort{}.with_exit_code(1)
-      << "failed to open input file `" << filename << "'";
-
-  auto language = get_language_from_filename(filename);
-
-  if(language == nullptr)
-  {
-    source_locationt location;
-    location.set_file(filename);
-    throw ebmc_errort{}.with_location(location).with_exit_code(1)
-      << "failed to figure out type of file";
-  }
-
-  optionst options;
-
-  // do -I
-  if(cmdline.isset('I'))
-    options.set_option("I", cmdline.get_values('I'));
-
-  options.set_option("force-systemverilog", cmdline.isset("systemverilog"));
-
-  // do -D
-  if(cmdline.isset('D'))
-    options.set_option("defines", cmdline.get_values('D'));
-
-  language->set_language_options(options, message_handler);
-
-  if(language->preprocess(infile, filename, std::cout, message_handler))
-    throw ebmc_errort{}.with_exit_code(1);
-}
-
-static bool parse(
-  const cmdlinet &cmdline,
-  const std::string &filename,
-  ebmc_language_filest &language_files,
-  message_handlert &message_handler)
-{
-  messaget message(message_handler);
-
-  std::ifstream infile(widen_if_needed(filename));
-
-  if(!infile)
-  {
-    message.error() << "failed to open input file `" << filename << "'"
-                    << messaget::eom;
-    return true;
-  }
-
-  auto &lf = language_files.add_file(filename);
-  lf.filename = filename;
-  lf.language = get_language_from_filename(filename);
-
-  if(lf.language == nullptr)
-  {
-    source_locationt location;
-    location.set_file(filename);
-    message.error().source_location = location;
-    message.error() << "failed to figure out type of file" << messaget::eom;
-    return true;
-  }
-
-  languaget &language = *lf.language;
-
-  optionst options;
-
-  // do -I
-  if(cmdline.isset('I'))
-    options.set_option("I", cmdline.get_values('I'));
-
-  options.set_option("force-systemverilog", cmdline.isset("systemverilog"));
-  options.set_option("vl2smv-extensions", cmdline.isset("vl2smv-extensions"));
-  options.set_option("warn-implicit-nets", cmdline.isset("warn-implicit-nets"));
-
-  // do -D
-  if(cmdline.isset('D'))
-    options.set_option("defines", cmdline.get_values('D'));
-
-  // do --ignore-initial
-  if(cmdline.isset("ignore-initial"))
-    options.set_option("ignore-initial", true);
-
-  // do --initial-zero
-  if(cmdline.isset("initial-zero"))
-    options.set_option("initial-zero", true);
-
-  language.set_language_options(options, message_handler);
-
-  message.status() << "Parsing " << filename << messaget::eom;
-
-  if(language.parse(infile, filename, message_handler))
-  {
-    message.error() << "PARSING ERROR\n";
-    return true;
-  }
-
-  lf.get_modules();
-
-  return false;
-}
-
-bool parse(
-  const cmdlinet &cmdline,
-  ebmc_language_filest &language_files,
-  message_handlert &message_handler)
-{
-  for(unsigned i = 0; i < cmdline.args.size(); i++)
-  {
-    if(parse(cmdline, cmdline.args[i], language_files, message_handler))
-      return true;
-  }
-  return false;
-}
-
-bool get_main(
-  const cmdlinet &cmdline,
-  message_handlert &message_handler,
-  transition_systemt &transition_system)
-{
-  std::string top_module;
-
-  if(cmdline.isset("module"))
-    top_module = cmdline.get_value("module");
-  else if(cmdline.isset("top"))
-    top_module = cmdline.get_value("top");
-
-  try
-  {
-    transition_system.main_symbol =
-      &get_module(transition_system.symbol_table, top_module, message_handler);
-    transition_system.trans_expr =
-      to_trans_expr(transition_system.main_symbol->value);
-  }
-
-  catch(int e)
-  {
-    return true;
-  }
-
-  return false;
-}
-
-void make_next_state(exprt &expr)
-{
-  for(auto &sub_expression : expr.operands())
-    make_next_state(sub_expression);
-
-  if(expr.id() == ID_symbol)
-    expr.id(ID_next_symbol);
-}
-
-int get_transition_system(
-  const cmdlinet &cmdline,
-  message_handlert &message_handler,
-  transition_systemt &transition_system)
-{
-  messaget message(message_handler);
-
-  //
-  // parsing
-  //
-  ebmc_language_filest language_files;
-
-  if(parse(cmdline, language_files, message_handler))
-    return 1;
-
-  if(cmdline.isset("show-parse"))
-  {
-    language_files.show_parse(std::cout, message_handler);
-    return 0;
-  }
-
-  //
-  // type checking
-  //
-
-  message.status() << "Converting" << messaget::eom;
-
-  if(language_files.typecheck(transition_system.symbol_table, message_handler))
-  {
-    message.error() << "CONVERSION ERROR" << messaget::eom;
-    return 2;
-  }
-
-  if(cmdline.isset("show-modules"))
-  {
-    show_modulest::from_symbol_table(transition_system.symbol_table)
-      .plain_text(std::cout);
-    return 0;
-  }
-
-  if(cmdline.isset("modules-xml"))
-  {
-    auto filename = cmdline.get_value("modules-xml");
-    auto out_file = output_filet{filename};
-    show_modulest::from_symbol_table(transition_system.symbol_table)
-      .xml(out_file.stream());
-    return 0;
-  }
-
-  if(cmdline.isset("json-modules"))
-  {
-    auto out_file = output_filet{cmdline.get_value("json-modules")};
-    show_modulest::from_symbol_table(transition_system.symbol_table)
-      .json(out_file.stream());
-    return 0;
-  }
-
-  if(cmdline.isset("show-symbol-table"))
-  {
-    std::cout << transition_system.symbol_table;
-    return 0;
-  }
-
-  // get module name
-
-  if(get_main(cmdline, message_handler, transition_system))
-    return 1;
-
-  if(cmdline.isset("show-module-hierarchy"))
-  {
-    DATA_INVARIANT(
-      transition_system.main_symbol != nullptr, "must have main_symbol");
-    show_module_hierarchy(
-      transition_system.symbol_table,
-      *transition_system.main_symbol,
-      std::cout);
-    return 0;
-  }
-
-  // --reset given?
-  if(cmdline.isset("reset"))
-  {
-    namespacet ns(transition_system.symbol_table);
-    exprt reset_constraint = to_expr(
-      ns, transition_system.main_symbol->name, cmdline.get_value("reset"));
-
-    // we want the constraint to be boolean
-    reset_constraint =
-      typecast_exprt::conditional_cast(reset_constraint, bool_typet{});
-
-    // true in initial state
-    transt new_trans_expr = transition_system.trans_expr;
-    new_trans_expr.init() = and_exprt(new_trans_expr.init(), reset_constraint);
-
-    // and not anymore afterwards
-    exprt reset_next_state = reset_constraint;
-    make_next_state(reset_next_state);
-
-    new_trans_expr.trans() =
-      and_exprt(new_trans_expr.trans(), not_exprt(reset_next_state));
-    transition_system.trans_expr = new_trans_expr;
-  }
-
-  return -1; // done with the transition system
-}
-
-transition_systemt get_transition_system(
-  const cmdlinet &cmdline,
-  message_handlert &message_handler)
-{
-  transition_systemt transition_system;
-  auto exit_code =
-    get_transition_system(cmdline, message_handler, transition_system);
-  if(exit_code != -1)
-    throw ebmc_errort().with_exit_code(exit_code);
-  return transition_system;
-}
-
-int show_parse(const cmdlinet &cmdline, message_handlert &message_handler)
-{
-  transition_systemt dummy_transition_system;
-  return get_transition_system(
-    cmdline, message_handler, dummy_transition_system);
-}
-
-int show_modules(const cmdlinet &cmdline, message_handlert &message_handler)
-{
-  transition_systemt dummy_transition_system;
-  return get_transition_system(
-    cmdline, message_handler, dummy_transition_system);
-}
-
-int show_module_hierarchy(
-  const cmdlinet &cmdline,
-  message_handlert &message_handler)
-{
-  transition_systemt dummy_transition_system;
-  return get_transition_system(
-    cmdline, message_handler, dummy_transition_system);
-}
-
-int show_symbol_table(
-  const cmdlinet &cmdline,
-  message_handlert &message_handler)
-{
-  transition_systemt dummy_transition_system;
-  return get_transition_system(
-    cmdline, message_handler, dummy_transition_system);
-}
+#include <set>
 
 static std::set<std::string> file_extensions(const cmdlinet::argst &args)
 {
@@ -379,40 +56,12 @@ std::optional<transition_systemt> ebmc_languagest::transition_system()
   {
     return smv_ebmc_languaget{cmdline, message_handler}.transition_system();
   }
+  else if(have_verilog)
+  {
+    return verilog_ebmc_languaget{cmdline, message_handler}.transition_system();
+  }
   else
   {
-    if(cmdline.isset("preprocess"))
-    {
-      preprocess(cmdline, message_handler);
-      return {};
-    }
-
-    if(cmdline.isset("show-parse"))
-    {
-      show_parse(cmdline, message_handler);
-      return {};
-    }
-
-    if(
-      cmdline.isset("show-modules") || cmdline.isset("modules-xml") ||
-      cmdline.isset("json-modules"))
-    {
-      show_modules(cmdline, message_handler);
-      return {};
-    }
-
-    if(cmdline.isset("show-module-hierarchy"))
-    {
-      show_module_hierarchy(cmdline, message_handler);
-      return {};
-    }
-
-    if(cmdline.isset("show-symbol-table"))
-    {
-      show_symbol_table(cmdline, message_handler);
-      return {};
-    }
-
-    return get_transition_system(cmdline, message_handler);
+    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..68434a7c6
--- /dev/null
+++ b/src/verilog/verilog_ebmc_language.cpp
@@ -0,0 +1,288 @@
+/*******************************************************************\
+
+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/ebmc_language_file.h>
+#include <ebmc/output_file.h>
+#include <ebmc/show_modules.h>
+#include <ebmc/transition_system.h>
+#include <langapi/language_util.h>
+#include <trans-word-level/show_module_hierarchy.h>
+
+#include "verilog_language.h"
+#include "verilog_parser.h"
+#include "verilog_typecheck.h"
+
+#include <fstream>
+#include <iostream>
+
+static void
+preprocess(const cmdlinet &cmdline, message_handlert &message_handler)
+{
+  messaget message(message_handler);
+
+  if(cmdline.args.size() != 1)
+    throw ebmc_errort{}.with_exit_code(1)
+      << "please give exactly one file to preprocess";
+
+  const auto &filename = cmdline.args.front();
+  std::ifstream infile(widen_if_needed(filename));
+
+  if(!infile)
+    throw ebmc_errort{}.with_exit_code(1)
+      << "failed to open input file `" << filename << "'";
+
+  auto language = new_verilog_language();
+
+  optionst options;
+
+  // do -I
+  if(cmdline.isset('I'))
+    options.set_option("I", cmdline.get_values('I'));
+
+  options.set_option("force-systemverilog", cmdline.isset("systemverilog"));
+
+  // do -D
+  if(cmdline.isset('D'))
+    options.set_option("defines", cmdline.get_values('D'));
+
+  language->set_language_options(options, message_handler);
+
+  if(language->preprocess(infile, filename, std::cout, message_handler))
+    throw ebmc_errort{}.with_exit_code(1);
+}
+
+static bool parse(
+  const cmdlinet &cmdline,
+  const std::string &filename,
+  ebmc_language_filest &language_files,
+  message_handlert &message_handler)
+{
+  messaget message(message_handler);
+
+  std::ifstream infile(widen_if_needed(filename));
+
+  if(!infile)
+  {
+    message.error() << "failed to open input file `" << filename << "'"
+                    << messaget::eom;
+    return true;
+  }
+
+  auto &lf = language_files.add_file(filename);
+  lf.filename = filename;
+  lf.language = new_verilog_language();
+  languaget &language = *lf.language;
+
+  optionst options;
+
+  // do -I
+  if(cmdline.isset('I'))
+    options.set_option("I", cmdline.get_values('I'));
+
+  options.set_option("force-systemverilog", cmdline.isset("systemverilog"));
+  options.set_option("vl2smv-extensions", cmdline.isset("vl2smv-extensions"));
+  options.set_option("warn-implicit-nets", cmdline.isset("warn-implicit-nets"));
+
+  // do -D
+  if(cmdline.isset('D'))
+    options.set_option("defines", cmdline.get_values('D'));
+
+  // do --ignore-initial
+  if(cmdline.isset("ignore-initial"))
+    options.set_option("ignore-initial", true);
+
+  // do --initial-zero
+  if(cmdline.isset("initial-zero"))
+    options.set_option("initial-zero", true);
+
+  language.set_language_options(options, message_handler);
+
+  message.status() << "Parsing " << filename << messaget::eom;
+
+  if(language.parse(infile, filename, message_handler))
+  {
+    message.error() << "PARSING ERROR\n";
+    return true;
+  }
+
+  lf.get_modules();
+
+  return false;
+}
+
+static bool parse(
+  const cmdlinet &cmdline,
+  ebmc_language_filest &language_files,
+  message_handlert &message_handler)
+{
+  for(unsigned i = 0; i < cmdline.args.size(); i++)
+  {
+    if(parse(cmdline, cmdline.args[i], language_files, message_handler))
+      return true;
+  }
+  return false;
+}
+
+static bool get_main(
+  const cmdlinet &cmdline,
+  message_handlert &message_handler,
+  transition_systemt &transition_system)
+{
+  std::string top_module;
+
+  if(cmdline.isset("module"))
+    top_module = cmdline.get_value("module");
+  else if(cmdline.isset("top"))
+    top_module = cmdline.get_value("top");
+
+  try
+  {
+    transition_system.main_symbol =
+      &get_module(transition_system.symbol_table, top_module, message_handler);
+    transition_system.trans_expr =
+      to_trans_expr(transition_system.main_symbol->value);
+  }
+
+  catch(int e)
+  {
+    return true;
+  }
+
+  return false;
+}
+
+static void make_next_state(exprt &expr)
+{
+  for(auto &sub_expression : expr.operands())
+    make_next_state(sub_expression);
+
+  if(expr.id() == ID_symbol)
+    expr.id(ID_next_symbol);
+}
+
+std::optional<transition_systemt> verilog_ebmc_languaget::transition_system()
+{
+  messaget message(message_handler);
+
+  //
+  // preprocessing
+  //
+  if(cmdline.isset("preprocess"))
+  {
+    preprocess(cmdline, message_handler);
+    return {};
+  }
+
+  transition_systemt transition_system;
+
+  //
+  // parsing
+  //
+  ebmc_language_filest language_files;
+
+  if(parse(cmdline, language_files, message_handler))
+    throw ebmc_errort{}.with_exit_code(1);
+
+  if(cmdline.isset("show-parse"))
+  {
+    language_files.show_parse(std::cout, message_handler);
+    return {};
+  }
+
+  //
+  // type checking
+  //
+
+  message.status() << "Converting" << messaget::eom;
+
+  if(language_files.typecheck(transition_system.symbol_table, message_handler))
+  {
+    message.error() << "CONVERSION ERROR" << messaget::eom;
+    throw ebmc_errort{}.with_exit_code(2);
+  }
+
+  if(cmdline.isset("show-modules"))
+  {
+    show_modulest::from_symbol_table(transition_system.symbol_table)
+      .plain_text(std::cout);
+    return {};
+  }
+
+  if(cmdline.isset("modules-xml"))
+  {
+    auto filename = cmdline.get_value("modules-xml");
+    auto out_file = output_filet{filename};
+    show_modulest::from_symbol_table(transition_system.symbol_table)
+      .xml(out_file.stream());
+    return {};
+  }
+
+  if(cmdline.isset("json-modules"))
+  {
+    auto out_file = output_filet{cmdline.get_value("json-modules")};
+    show_modulest::from_symbol_table(transition_system.symbol_table)
+      .json(out_file.stream());
+    return {};
+  }
+
+  if(cmdline.isset("show-symbol-table"))
+  {
+    std::cout << transition_system.symbol_table;
+    return {};
+  }
+
+  // get module name
+
+  if(get_main(cmdline, message_handler, transition_system))
+    throw ebmc_errort{}.with_exit_code(1);
+
+  if(cmdline.isset("show-module-hierarchy"))
+  {
+    DATA_INVARIANT(
+      transition_system.main_symbol != nullptr, "must have main_symbol");
+    show_module_hierarchy(
+      transition_system.symbol_table,
+      *transition_system.main_symbol,
+      std::cout);
+    return {};
+  }
+
+  // --reset given?
+  if(cmdline.isset("reset"))
+  {
+    namespacet ns(transition_system.symbol_table);
+    exprt reset_constraint = to_expr(
+      ns, transition_system.main_symbol->name, cmdline.get_value("reset"));
+
+    // true in initial state
+    transt new_trans_expr = transition_system.trans_expr;
+    new_trans_expr.init() = and_exprt(new_trans_expr.init(), reset_constraint);
+
+    // and not anymore afterwards
+    exprt reset_next_state = reset_constraint;
+    make_next_state(reset_next_state);
+
+    new_trans_expr.trans() =
+      and_exprt(new_trans_expr.trans(), not_exprt(reset_next_state));
+    transition_system.trans_expr = new_trans_expr;
+  }
+
+  // done with the transition system
+  return transition_system;
+}
diff --git a/src/verilog/verilog_ebmc_language.h b/src/verilog/verilog_ebmc_language.h
new file mode 100644
index 000000000..7527386db
--- /dev/null
+++ b/src/verilog/verilog_ebmc_language.h
@@ -0,0 +1,31 @@
+/*******************************************************************\
+
+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;
+};
+
+#endif // EBMC_VERILOG_LANGUAGE_H