diff --git a/src/verilog/parser.y b/src/verilog/parser.y
index 353890e80..a460ac86e 100644
--- a/src/verilog/parser.y
+++ b/src/verilog/parser.y
@@ -1447,8 +1447,7 @@ type_declaration:
 	   data_type any_identifier ';'
 		{ $$ = $2;
 		  // add to the scope as a type name
-		  auto &name = PARSER.scopes.add_name(stack_expr($4).get(ID_identifier), "", verilog_scopet::TYPEDEF);
-		  name.is_type = true;
+		  PARSER.scopes.add_name(stack_expr($4).get(ID_identifier), "", verilog_scopet::TYPEDEF);
 		  addswap($$, ID_type, $3);
 		  stack_expr($4).id(ID_declarator);
 		  mto($$, $4);
@@ -1537,7 +1536,7 @@ data_type:
 
 	          // We attach a dummy id to distinguish two syntactically
 	          // identical enum types.
-	          auto id = PARSER.scopes.current_scope->prefix + "enum-" + PARSER.get_next_id();
+	          auto id = PARSER.scopes.current_scope().prefix + "enum-" + PARSER.get_next_id();
 	          stack_expr($$).set(ID_identifier, id);
 	        }
 	| TOK_STRING
@@ -4429,7 +4428,7 @@ type_identifier: TOK_TYPE_IDENTIFIER
 		  init($$, ID_typedef_type);
 		  auto base_name = stack_expr($1).id();
 		  stack_expr($$).set(ID_base_name, base_name);
-		  stack_expr($$).set(ID_identifier, PARSER.scopes.current_scope->prefix+id2string(base_name));
+		  stack_expr($$).set(ID_identifier, PARSER.scopes.current_scope().prefix+id2string(base_name));
 		}
 	;
 
diff --git a/src/verilog/scanner.l b/src/verilog/scanner.l
index 4885bfe5a..72ec3830d 100644
--- a/src/verilog/scanner.l
+++ b/src/verilog/scanner.l
@@ -67,7 +67,7 @@ static void preprocessor()
     stack_expr(yyveriloglval).id(irep_id); \
     auto name = PARSER.scopes.lookup(irep_id); \
     return name == nullptr ? TOK_NON_TYPE_IDENTIFIER : \
-           name->is_type ?   TOK_TYPE_IDENTIFIER : \
+           name->kind == verilog_scopet::TYPEDEF ? TOK_TYPE_IDENTIFIER : \
                              TOK_NON_TYPE_IDENTIFIER; \
   }
 #define KEYWORD(s, x) \
diff --git a/src/verilog/verilog_scope.cpp b/src/verilog/verilog_scope.cpp
index 66d96e302..f343f9b73 100644
--- a/src/verilog/verilog_scope.cpp
+++ b/src/verilog/verilog_scope.cpp
@@ -8,13 +8,15 @@ Author: Daniel Kroening, dkr@amazon.com
 
 #include "verilog_scope.h"
 
-const verilog_scopet *verilog_scopest::lookup(irep_idt name) const
+#include "verilog_y.tab.h"
+
+const verilog_scopet *verilog_scopest::lookup(irep_idt base_name) const
 {
   // we start from the current scope, and walk upwards to the root
-  auto scope = current_scope;
+  auto scope = &current_scope();
   while(scope != nullptr)
   {
-    auto name_it = scope->scope_map.find(name);
+    auto name_it = scope->scope_map.find(base_name);
     if(name_it == scope->scope_map.end())
       scope = scope->parent;
     else
@@ -24,3 +26,13 @@ const verilog_scopet *verilog_scopest::lookup(irep_idt name) const
   // not found, give up
   return nullptr;
 }
+
+void verilog_scopest::enter_package_scope(irep_idt base_name)
+{
+  // look in the global scope
+  auto name_it = top_scope.scope_map.find(base_name);
+  if(name_it == top_scope.scope_map.end())
+    enter_scope(current_scope());
+  else
+    enter_scope(name_it->second); // found it
+}
diff --git a/src/verilog/verilog_scope.h b/src/verilog/verilog_scope.h
index 53de0829e..8812cb805 100644
--- a/src/verilog/verilog_scope.h
+++ b/src/verilog/verilog_scope.h
@@ -47,7 +47,6 @@ struct verilog_scopet
   }
 
   verilog_scopet *parent = nullptr;
-  bool is_type = false;
   irep_idt __base_name;
   std::string prefix;
   kindt kind;
@@ -73,42 +72,55 @@ class verilog_scopest
 public:
   using scopet = verilog_scopet;
 
-  scopet top_scope, *current_scope = &top_scope;
+  scopet top_scope;
 
   scopet &add_name(
     irep_idt _base_name,
     const std::string &separator,
     scopet::kindt kind)
   {
-    auto result = current_scope->scope_map.emplace(
-      _base_name, scopet{_base_name, separator, current_scope, kind});
+    auto result = current_scope().scope_map.emplace(
+      _base_name, scopet{_base_name, separator, &current_scope(), kind});
     return result.first->second;
   }
 
-  // Create the given sub-scope of the current scope.
+  // Scope stack
+  std::vector<scopet *> scope_stack = {&top_scope};
+
+  scopet &current_scope() const
+  {
+    // We never pop the top scope
+    PRECONDITION(!scope_stack.empty());
+    return *scope_stack.back();
+  }
+
+  // find the package scope with given base name, and enter it
+  void enter_package_scope(irep_idt base_name);
+
+  void enter_scope(scopet &scope)
+  {
+    scope_stack.push_back(&scope);
+  }
+
+  // Create the given sub-scope of the current scope, and enter it.
   void push_scope(
     irep_idt _base_name,
     const std::string &separator,
     scopet::kindt kind)
   {
-    current_scope = &add_name(_base_name, separator, kind);
+    enter_scope(add_name(_base_name, separator, kind));
   }
 
   void pop_scope()
   {
-    PRECONDITION(current_scope->parent != nullptr);
-    current_scope = current_scope->parent;
+    // We never pop the top scope
+    PRECONDITION(scope_stack.size() >= 2);
+    scope_stack.pop_back();
   }
 
   // Look up an identifier, starting from the current scope,
   // going upwards until found. Returns nullptr when not found.
   const scopet *lookup(irep_idt base_name) const;
-
-  bool is_type(irep_idt base_name) const
-  {
-    auto scope_ptr = lookup(base_name);
-    return scope_ptr == nullptr ? false : scope_ptr->is_type;
-  }
 };
 
 #endif