diff --git a/regression/smv/define/define2.desc b/regression/smv/define/define2.desc
index 4fa0eea60..dfb4457cf 100644
--- a/regression/smv/define/define2.desc
+++ b/regression/smv/define/define2.desc
@@ -1,7 +1,7 @@
 CORE
 define2.smv
 
-^file .* line 6: variable `x' already declared.*$
+^file .* line 6: identifier x already used as variable$
 ^EXIT=2$
 ^SIGNAL=0$
 --
diff --git a/regression/smv/define/define3.desc b/regression/smv/define/define3.desc
index a69176ac9..79214d15d 100644
--- a/regression/smv/define/define3.desc
+++ b/regression/smv/define/define3.desc
@@ -1,7 +1,7 @@
 CORE
 define3.smv
 
-^file .* line 6: variable x already declared, at file .* line 3$
+^file .* line 6: identifier x already used as define$
 ^EXIT=2$
 ^SIGNAL=0$
 --
diff --git a/regression/smv/enums/name_collision1.desc b/regression/smv/enums/name_collision1.desc
index fa029e06d..4537a9f2f 100644
--- a/regression/smv/enums/name_collision1.desc
+++ b/regression/smv/enums/name_collision1.desc
@@ -1,9 +1,9 @@
-KNOWNBUG
+CORE
 name_collision1.smv
 
-^EXIT=0$
+^file .* line 6: identifier red already used as enum$
+^EXIT=2$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This crashes.
diff --git a/regression/smv/enums/name_collision2.desc b/regression/smv/enums/name_collision2.desc
index 7bc17f348..7a2eb1393 100644
--- a/regression/smv/enums/name_collision2.desc
+++ b/regression/smv/enums/name_collision2.desc
@@ -1,7 +1,7 @@
 CORE
 name_collision2.smv
 
-^file .* line 8: enum red already declared, at file .* line 3$
+^file .* line 8: identifier red already used as variable$
 ^EXIT=2$
 ^SIGNAL=0$
 --
diff --git a/regression/smv/enums/name_collision3.desc b/regression/smv/enums/name_collision3.desc
index 91c3ea2f6..8ae3e5f34 100644
--- a/regression/smv/enums/name_collision3.desc
+++ b/regression/smv/enums/name_collision3.desc
@@ -1,9 +1,9 @@
-KNOWNBUG
+CORE
 name_collision3.smv
 
-^EXIT=0$
+^file .* line 8: identifier red already used as enum$
+^EXIT=2$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This crashes.
diff --git a/regression/smv/modules/parameters2.desc b/regression/smv/modules/parameters2.desc
index 18158a51a..2288ee0fa 100644
--- a/regression/smv/modules/parameters2.desc
+++ b/regression/smv/modules/parameters2.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 parameters2.smv
 
 ^EXIT=10$
@@ -6,4 +6,3 @@ parameters2.smv
 --
 ^warning: ignoring
 --
-This yields a type-checking error.
diff --git a/regression/smv/var/already_declared1.desc b/regression/smv/var/already_declared1.desc
index 0910f0f55..8d5b4a1c4 100644
--- a/regression/smv/var/already_declared1.desc
+++ b/regression/smv/var/already_declared1.desc
@@ -1,7 +1,7 @@
 CORE
 already_declared1.smv
 
-^file .* line 6: variable x already declared, at file .* line 3$
+^file .* line 6: identifier x already used as variable$
 ^EXIT=2$
 ^SIGNAL=0$
 --
diff --git a/regression/smv/var/already_declared2.desc b/regression/smv/var/already_declared2.desc
index cfacd32a3..51fdcee66 100644
--- a/regression/smv/var/already_declared2.desc
+++ b/regression/smv/var/already_declared2.desc
@@ -1,7 +1,7 @@
 CORE
 already_declared2.smv
 
-^file .* line 6: variable x already declared, at file .* line 3$
+^file .* line 6: identifier x already used as define$
 ^EXIT=2$
 ^SIGNAL=0$
 --
diff --git a/regression/smv/var/already_declared3.desc b/regression/smv/var/already_declared3.desc
index 22e8c3575..33afc32cb 100644
--- a/regression/smv/var/already_declared3.desc
+++ b/regression/smv/var/already_declared3.desc
@@ -1,7 +1,7 @@
 CORE
 already_declared3.smv
 
-^file .* line 8: variable x already declared, at file .* line 5$
+^file .* line 8: identifier x already used as variable$
 ^EXIT=2$
 ^SIGNAL=0$
 --
diff --git a/src/ebmc/build_transition_system.cpp b/src/ebmc/build_transition_system.cpp
index 1471e2a1f..f14dc10b6 100644
--- a/src/ebmc/build_transition_system.cpp
+++ b/src/ebmc/build_transition_system.cpp
@@ -18,6 +18,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #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 <trans-word-level/show_modules.h>
 
@@ -335,39 +336,76 @@ int show_symbol_table(
     cmdline, message_handler, dummy_transition_system);
 }
 
-std::optional<transition_systemt> ebmc_languagest::transition_system()
+static std::set<std::string> file_extensions(const cmdlinet::argst &args)
 {
-  if(cmdline.isset("preprocess"))
-  {
-    preprocess(cmdline, message_handler);
-    return {};
-  }
+  std::set<std::string> result;
 
-  if(cmdline.isset("show-parse"))
+  for(auto &arg : args)
   {
-    show_parse(cmdline, message_handler);
-    return {};
+    std::size_t ext_pos = arg.rfind('.');
+
+    if(ext_pos != std::string::npos)
+    {
+      auto ext = std::string(arg, ext_pos + 1, std::string::npos);
+      result.insert(ext);
+    }
   }
 
-  if(
-    cmdline.isset("show-modules") || cmdline.isset("modules-xml") ||
-    cmdline.isset("json-modules"))
+  return result;
+}
+
+std::optional<transition_systemt> ebmc_languagest::transition_system()
+{
+  auto extensions = file_extensions(cmdline.args);
+  auto ext_used = [&extensions](const char *ext)
+  { return extensions.find(ext) != extensions.end(); };
+
+  bool have_smv = ext_used("smv");
+  bool have_verilog = ext_used("v") || ext_used("sv");
+
+  if(have_smv && have_verilog)
   {
-    show_modules(cmdline, message_handler);
-    return {};
+    throw ebmc_errort{} << "no support for mixed-language models";
   }
 
-  if(cmdline.isset("show-module-hierarchy"))
+  if(have_smv)
   {
-    show_module_hierarchy(cmdline, message_handler);
-    return {};
+    return smv_ebmc_languaget{cmdline, message_handler}.transition_system();
   }
-
-  if(cmdline.isset("show-symbol-table"))
+  else
   {
-    show_symbol_table(cmdline, message_handler);
-    return {};
+    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);
   }
-
-  return get_transition_system(cmdline, message_handler);
 }
diff --git a/src/smvlang/Makefile b/src/smvlang/Makefile
index 248dced76..30b6e6505 100644
--- a/src/smvlang/Makefile
+++ b/src/smvlang/Makefile
@@ -1,4 +1,5 @@
-SRC = smv_expr.cpp \
+SRC = smv_ebmc_language.cpp \
+      smv_expr.cpp \
       smv_language.cpp \
       smv_parser.cpp \
       smv_typecheck.cpp \
diff --git a/src/smvlang/smv_ebmc_language.cpp b/src/smvlang/smv_ebmc_language.cpp
new file mode 100644
index 000000000..2177c062a
--- /dev/null
+++ b/src/smvlang/smv_ebmc_language.cpp
@@ -0,0 +1,109 @@
+/*******************************************************************\
+
+Module: SMV Language Interface
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+/// \file
+/// SMV Language Interface
+
+#include "smv_ebmc_language.h"
+
+#include <util/cmdline.h>
+#include <util/get_module.h>
+#include <util/unicode.h>
+
+#include <ebmc/ebmc_error.h>
+#include <ebmc/transition_system.h>
+
+#include "smv_parser.h"
+#include "smv_typecheck.h"
+
+#include <fstream>
+#include <iostream>
+
+std::string smv_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) << "SMV only uses a single file";
+
+  return cmdline.args.front();
+}
+
+smv_parse_treet smv_ebmc_languaget::parse()
+{
+  smv_parsert smv_parser{message_handler};
+
+  auto file_name = smv_file_name(cmdline);
+
+  std::ifstream infile{widen_if_needed(file_name)};
+
+  if(!infile)
+    throw ebmc_errort{}.with_exit_code(1) << "failed to open " << file_name;
+
+  smv_parser.set_file(file_name);
+  smv_parser.in = &infile;
+
+  if(smv_parser.parse())
+    throw ebmc_errort{}.with_exit_code(1);
+
+  return std::move(smv_parser.parse_tree);
+}
+
+std::optional<transition_systemt> smv_ebmc_languaget::transition_system()
+{
+  if(cmdline.isset("preprocess"))
+  {
+    throw ebmc_errort{}.with_exit_code(1) << "SMV does not use preprocessing";
+  }
+
+  auto parse_tree = parse();
+
+  if(cmdline.isset("show-parse"))
+  {
+    parse_tree.show(std::cout);
+    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 {};
+  }
+
+  transition_systemt result;
+
+  if(smv_typecheck(
+       parse_tree, result.symbol_table, "smv::main", message_handler))
+  {
+    messaget message{message_handler};
+    message.error() << "CONVERSION ERROR" << messaget::eom;
+    throw ebmc_errort{}.with_exit_code(2);
+  }
+
+  if(cmdline.isset("show-symbol-table"))
+  {
+    std::cout << result.symbol_table;
+    return {};
+  }
+
+  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/smvlang/smv_ebmc_language.h b/src/smvlang/smv_ebmc_language.h
new file mode 100644
index 000000000..72ab3ef35
--- /dev/null
+++ b/src/smvlang/smv_ebmc_language.h
@@ -0,0 +1,34 @@
+/*******************************************************************\
+
+Module: SMV Language Interface
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+/// \file
+/// SMV Language Interface
+
+#ifndef EBMC_SMV_LANGUAGE_H
+#define EBMC_SMV_LANGUAGE_H
+
+#include <ebmc/ebmc_language.h>
+
+class smv_parse_treet;
+
+class smv_ebmc_languaget : public ebmc_languaget
+{
+public:
+  smv_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:
+  smv_parse_treet parse();
+};
+
+#endif // EBMC_SMV_LANGUAGE_H
diff --git a/src/smvlang/smv_parse_tree.h b/src/smvlang/smv_parse_tree.h
index 5dc88bcd7..9a2d04a64 100644
--- a/src/smvlang/smv_parse_tree.h
+++ b/src/smvlang/smv_parse_tree.h
@@ -24,7 +24,7 @@ class smv_parse_treet
   struct modulet
   {
     irep_idt name, base_name;
-    std::list<irep_idt> parameters;
+    std::vector<irep_idt> parameters;
 
     struct elementt
     {
diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp
index 95f7edd62..c3af84554 100644
--- a/src/smvlang/smv_typecheck.cpp
+++ b/src/smvlang/smv_typecheck.cpp
@@ -60,9 +60,8 @@ class smv_typecheckt:public typecheckt
   } modet;
 
   void convert(smv_parse_treet::modulet &);
-  void create_var_symbols(
-    const smv_parse_treet::modulet::element_listt &,
-    const std::list<irep_idt> &module_parameters);
+
+  void create_var_symbols(const smv_parse_treet::modulet::element_listt &);
 
   void collect_define(const equal_exprt &);
   void convert_defines(exprt::operandst &invar);
@@ -88,6 +87,8 @@ class smv_typecheckt:public typecheckt
   void check_type(typet &);
   smv_ranget convert_type(const typet &);
 
+  void variable_checks(const smv_parse_treet::modulet &);
+
   void convert(smv_parse_treet::modulet::elementt &);
   void typecheck(smv_parse_treet::modulet::elementt &);
   void typecheck_expr_rec(exprt &, modet);
@@ -104,7 +105,7 @@ class smv_typecheckt:public typecheckt
     smv_parse_treet::modulet &,
     const irep_idt &identifier,
     const irep_idt &instance,
-    const exprt::operandst &operands,
+    const exprt::operandst &arguments,
     const source_locationt &);
 
   typet
@@ -196,8 +197,14 @@ Function: smv_typecheckt::flatten_hierarchy
 
 void smv_typecheckt::flatten_hierarchy(smv_parse_treet::modulet &smv_module)
 {
-  for(auto &element : smv_module.elements)
+  // Not using ranged for since we will append to the list we are
+  // iterating over! This avoids recursion.
+  for(auto element_it = smv_module.elements.begin();
+      element_it != smv_module.elements.end();
+      ++element_it)
   {
+    auto &element = *element_it;
+
     if(element.is_var() && element.expr.type().id() == ID_smv_submodule)
     {
       exprt &inst =
@@ -235,145 +242,67 @@ void smv_typecheckt::instantiate(
   smv_parse_treet::modulet &smv_module,
   const irep_idt &identifier,
   const irep_idt &instance,
-  const exprt::operandst &operands,
+  const exprt::operandst &arguments,
   const source_locationt &location)
 {
-  symbol_table_baset::symbolst::const_iterator s_it =
-    symbol_table.symbols.find(identifier);
+  // Find the module
+  auto module_it = smv_parse_tree.modules.find(identifier);
 
-  if(s_it==symbol_table.symbols.end())
+  if(module_it == smv_parse_tree.modules.end())
   {
     throw errort().with_location(location)
       << "submodule `" << identifier << "' not found";
   }
 
-  if(s_it->second.type.id()!=ID_module)
-  {
-    throw errort().with_location(location)
-      << "submodule `" << identifier << "' not a module";
-  }
-
-  const irept::subt &ports=s_it->second.type.find(ID_ports).get_sub();
-
-  // do the arguments/ports
+  const auto &instantiated_module = module_it->second;
+  const auto &parameters = instantiated_module.parameters;
 
-  if(ports.size()!=operands.size())
+  // map the arguments to parameters
+  if(parameters.size() != arguments.size())
   {
     throw errort().with_location(location)
       << "submodule `" << identifier << "' has wrong number of arguments";
   }
 
-  std::set<irep_idt> port_identifiers;
-  rename_mapt rename_map;
+  rename_mapt parameter_map;
 
-  for(std::size_t i = 0; i < ports.size(); i++)
+  for(std::size_t i = 0; i < parameters.size(); i++)
   {
-    const irep_idt &identifier=ports[i].get(ID_identifier);
-    rename_map.insert(std::pair<irep_idt, exprt>(identifier, operands[i]));
-    port_identifiers.insert(identifier);
+    parameter_map.emplace(parameters[i], arguments[i]);
   }
 
-  // do the variables
-
-  std::string new_prefix=
-    id2string(smv_module.name)+"::var::"+id2string(instance)+".";
+  const std::string prefix = id2string(instance) + '.';
 
-  std::set<irep_idt> var_identifiers;
-
-  for(auto v_it=symbol_table.symbol_module_map.lower_bound(identifier);
-      v_it!=symbol_table.symbol_module_map.upper_bound(identifier);
-      v_it++)
+  // copy the parse tree elements
+  for(auto &src_element : instantiated_module.elements)
   {
-    symbol_table_baset::symbolst::const_iterator s_it2 =
-      symbol_table.symbols.find(v_it->second);
-
-    if(s_it2==symbol_table.symbols.end())
-    {
-      throw errort() << "symbol `" << v_it->second << "' not found";
-    }
-
-    if(port_identifiers.find(s_it2->first) != port_identifiers.end())
-    {
-    }
-    else if(s_it2->second.type.id() == ID_module)
-    {
-    }
-    else
-    {
-      symbolt symbol(s_it2->second);
+    auto copy = src_element;
 
-      symbol.name=new_prefix+id2string(symbol.base_name);
-      symbol.module=smv_module.name;
-
-      if(smv_module.name == "smv::main")
+    // replace the parameter identifiers,
+    // and add the prefix to non-parameter identifiers
+    copy.expr.visit_post(
+      [&parameter_map, &prefix](exprt &expr)
       {
-        symbol.pretty_name =
-          id2string(instance) + '.' + id2string(symbol.base_name);
-      }
-      else
-      {
-        symbol.pretty_name = strip_smv_prefix(symbol.name);
-      }
-
-      rename_map.insert(
-          std::pair<irep_idt, exprt>(s_it2->first, symbol.symbol_expr()));
-
-      var_identifiers.insert(symbol.name);
-
-      symbol_table.add(symbol);
-    }
-  }
-
-  // fix values (macros)
-
-  for(const auto &v_id : var_identifiers)
-  {
-    auto s_it2 = symbol_table.get_writeable(v_id);
-
-    if(s_it2==nullptr)
-    {
-      throw errort() << "symbol `" << v_id << "' not found";
-    }
-
-    symbolt &symbol=*s_it2;
-
-    if(!symbol.value.is_nil())
-    {
-      instantiate_rename(symbol.value, rename_map);
-      typecheck(symbol.value, OTHER);
-      convert_expr_to(symbol.value, symbol.type);
-    }
-  }
-
-  // get the transition system
-
-  const transt &trans=to_trans_expr(s_it->second.value);
-
-  std::string old_prefix=id2string(s_it->first)+"::var::";
-
-  // do the transition system
+        if(expr.id() == ID_smv_identifier)
+        {
+          auto identifier = to_smv_identifier_expr(expr).identifier();
+          auto parameter_it = parameter_map.find(identifier);
+          if(parameter_it != parameter_map.end())
+          {
+            expr = parameter_it->second;
+          }
+          else
+          {
+            // add the prefix
+            to_smv_identifier_expr(expr).identifier(
+              prefix + id2string(identifier));
+          }
+        }
+      });
 
-  if(!trans.invar().is_true())
-  {
-    exprt tmp(trans.invar());
-    instantiate_rename(tmp, rename_map);
-    smv_module.add_invar(tmp);
-  }
-    
-  if(!trans.init().is_true())
-  {
-    exprt tmp(trans.init());
-    instantiate_rename(tmp, rename_map);
-    smv_module.add_init(tmp);
-  }
-    
-  if(!trans.trans().is_true())
-  {
-    exprt tmp(trans.trans());
-    instantiate_rename(tmp, rename_map);
-    smv_module.add_trans(tmp);
+    // add to main parse tree
+    smv_module.elements.push_back(copy);
   }
-
 }
 
 /*******************************************************************\
@@ -2126,7 +2055,7 @@ void smv_typecheckt::convert(smv_parse_treet::modulet::elementt &element)
 
 /*******************************************************************\
 
-Function: smv_typecheckt::create_var_symbols
+Function: smv_typecheckt::variable_checks
 
   Inputs:
 
@@ -2136,42 +2065,141 @@ Function: smv_typecheckt::create_var_symbols
 
 \*******************************************************************/
 
-void smv_typecheckt::create_var_symbols(
-  const smv_parse_treet::modulet::element_listt &elements,
-  const std::list<irep_idt> &module_parameters)
+void smv_typecheckt::variable_checks(const smv_parse_treet::modulet &module)
 {
-  const irep_idt mode = "SMV";
-
-  // to catch variables that have the same name as enums
-  std::unordered_set<irep_idt, irep_id_hash> enums;
+  std::unordered_set<irep_idt, irep_id_hash> enums, defines, vars, parameters;
 
-  // to catch re-use of parameter identifiers
-  std::unordered_set<irep_idt, irep_id_hash> parameters;
-
-  for(const auto &parameter : module_parameters)
+  for(const auto &parameter : module.parameters)
     parameters.insert(parameter);
 
-  for(const auto &element : elements)
+  for(const auto &element : module.elements)
   {
     if(element.is_var() || element.is_ivar())
     {
-      irep_idt base_name = to_smv_identifier_expr(element.expr).identifier();
-      irep_idt identifier = module + "::var::" + id2string(base_name);
+      const auto &identifier_expr = to_smv_identifier_expr(element.expr);
+      irep_idt base_name = identifier_expr.identifier();
 
       // already used as enum?
       if(enums.find(base_name) != enums.end())
       {
-        throw errort{}.with_location(element.expr.source_location())
+        throw errort{}.with_location(identifier_expr.source_location())
           << "identifier " << base_name << " already used as enum";
       }
 
       // already used as a parameter?
       if(parameters.find(base_name) != parameters.end())
       {
-        throw errort{}.with_location(element.expr.source_location())
+        throw errort{}.with_location(identifier_expr.source_location())
           << "identifier " << base_name << " already used as a parameter";
       }
 
+      // already used as variable?
+      if(vars.find(base_name) != vars.end())
+      {
+        throw errort{}.with_location(identifier_expr.source_location())
+          << "identifier " << base_name << " already used as variable";
+      }
+
+      // already used as define?
+      if(defines.find(base_name) != defines.end())
+      {
+        throw errort{}.with_location(identifier_expr.source_location())
+          << "identifier " << base_name << " already used as define";
+      }
+
+      vars.insert(base_name);
+    }
+    else if(element.is_define())
+    {
+      const auto &identifier_expr =
+        to_smv_identifier_expr(to_equal_expr(element.expr).lhs());
+      irep_idt base_name = identifier_expr.identifier();
+
+      // already used as enum?
+      if(enums.find(base_name) != enums.end())
+      {
+        throw errort{}.with_location(identifier_expr.source_location())
+          << "identifier " << base_name << " already used as enum";
+      }
+
+      // already used as a parameter?
+      if(parameters.find(base_name) != parameters.end())
+      {
+        throw errort{}.with_location(identifier_expr.source_location())
+          << "identifier " << base_name << " already used as a parameter";
+      }
+
+      // already used as variable?
+      if(vars.find(base_name) != vars.end())
+      {
+        throw errort{}.with_location(identifier_expr.source_location())
+          << "identifier " << base_name << " already used as variable";
+      }
+
+      // already used as define?
+      if(defines.find(base_name) != defines.end())
+      {
+        throw errort{}.with_location(identifier_expr.source_location())
+          << "identifier " << base_name << " already used as define";
+      }
+
+      defines.insert(base_name);
+    }
+    else if(element.is_enum())
+    {
+      const auto &identifier_expr = to_smv_identifier_expr(element.expr);
+      irep_idt base_name = identifier_expr.identifier();
+
+      // already used as a parameter?
+      if(parameters.find(base_name) != parameters.end())
+      {
+        throw errort{}.with_location(identifier_expr.source_location())
+          << "identifier " << base_name << " already used as a parameter";
+      }
+
+      // already used as variable?
+      if(vars.find(base_name) != vars.end())
+      {
+        throw errort{}.with_location(identifier_expr.source_location())
+          << "identifier " << base_name << " already used as variable";
+      }
+
+      // already used as define?
+      if(defines.find(base_name) != defines.end())
+      {
+        throw errort{}.with_location(identifier_expr.source_location())
+          << "identifier " << base_name << " already used as define";
+      }
+
+      enums.insert(base_name);
+    }
+  }
+}
+
+/*******************************************************************\
+
+Function: smv_typecheckt::create_var_symbols
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_typecheckt::create_var_symbols(
+  const smv_parse_treet::modulet::element_listt &elements)
+{
+  const irep_idt mode = "SMV";
+
+  for(const auto &element : elements)
+  {
+    if(element.is_var() || element.is_ivar())
+    {
+      irep_idt base_name = to_smv_identifier_expr(element.expr).identifier();
+      irep_idt identifier = module + "::var::" + id2string(base_name);
+
       auto symbol_ptr = symbol_table.lookup(identifier);
       if(symbol_ptr != nullptr)
       {
@@ -2213,20 +2241,6 @@ void smv_typecheckt::create_var_symbols(
       irep_idt base_name = identifier_expr.identifier();
       irep_idt identifier = module + "::var::" + id2string(base_name);
 
-      // already used as enum?
-      if(enums.find(base_name) != enums.end())
-      {
-        throw errort{}.with_location(identifier_expr.source_location())
-          << "identifier " << base_name << " already used as enum";
-      }
-
-      // already used as a parameter?
-      if(parameters.find(base_name) != parameters.end())
-      {
-        throw errort{}.with_location(identifier_expr.source_location())
-          << "identifier " << base_name << " already used as a parameter";
-      }
-
       auto symbol_ptr = symbol_table.lookup(identifier);
       if(symbol_ptr != nullptr)
       {
@@ -2261,13 +2275,6 @@ void smv_typecheckt::create_var_symbols(
       irep_idt base_name = to_smv_identifier_expr(element.expr).identifier();
       irep_idt identifier = module + "::var::" + id2string(base_name);
 
-      // already used as a parameter?
-      if(parameters.find(base_name) != parameters.end())
-      {
-        throw errort{}.with_location(element.expr.source_location())
-          << "identifier " << base_name << " already used as a parameter";
-      }
-
       auto symbol_ptr = symbol_table.lookup(identifier);
       if(symbol_ptr != nullptr)
       {
@@ -2275,8 +2282,6 @@ void smv_typecheckt::create_var_symbols(
           << "enum " << base_name << " already declared, at "
           << symbol_ptr->location;
       }
-
-      enums.insert(base_name);
     }
   }
 }
@@ -2421,8 +2426,11 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
 
   define_map.clear();
 
-  // variables/defines first, can be used before their declaration
-  create_var_symbols(smv_module.elements, smv_module.parameters);
+  // expand the module hierarchy
+  flatten_hierarchy(smv_module);
+
+  // Now do variables/defines, which can be used before their declaration
+  create_var_symbols(smv_module.elements);
 
   // transition relation
 
@@ -2445,8 +2453,6 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
       if(!element.is_var() && !element.is_ivar())
         convert(element);
 
-    flatten_hierarchy(smv_module);
-
     // we first need to collect all the defines
 
     for(auto &element : smv_module.elements)
@@ -2552,6 +2558,13 @@ Function: smv_typecheckt::typecheck
 
 void smv_typecheckt::typecheck()
 {
+  if(module != "smv::main")
+    return;
+
+  // check all modules for duplicate identifiers
+  for(auto &module_it : smv_parse_tree.modules)
+    variable_checks(module_it.second);
+
   smv_parse_treet::modulest::iterator it=smv_parse_tree.modules.find(module);
 
   if(it==smv_parse_tree.modules.end())
diff --git a/src/verilog/verilog_ebmc_language.cpp b/src/verilog/verilog_ebmc_language.cpp
new file mode 100644
index 000000000..9b6df71dd
--- /dev/null
+++ b/src/verilog/verilog_ebmc_language.cpp
@@ -0,0 +1,64 @@
+/*******************************************************************\
+
+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/unicode.h>
+
+#include <ebmc/ebmc_error.h>
+#include <ebmc/transition_system.h>
+
+#include "verilog_parser.h"
+#include "verilog_typecheck.h"
+
+#include <fstream>
+
+verilog_parse_treet verilog_ebmc_languaget::parse()
+{
+  verilog_standardt standard;
+
+  verilog_parsert verilog_parser{standard, message_handler};
+
+  auto file_name = verilog_file_name(cmdline);
+
+  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