ebmc: add --system-verilog command-line option

This adds the command-line option --system-verilog to ebmc, which switches
the Verilog front-end to recognize SystemVerilog.

Author: kroening

regression/verilog/force-system-verilog/main1.desc

@@ -0,0 +1,8 @@
+CORE
+main1.v
+--system-verilog
+^EXIT=10$
+^SIGNAL=0$
+^no properties$
+--
+^warning: ignoring

regression/verilog/force-system-verilog/main1.v

@@ -0,0 +1,5 @@
+module main;
+  // 'logic' is a SystemVerilog keyword
+  logic some_logic;
+  initial some_logic = 1;
+endmodule

src/ebmc/ebmc_parse_options.cpp

@@ -363,6 +363,7 @@ void ebmc_parse_optionst::help()
     " {y--show-properties}           \t list the properties in the model\n"
     " {y--property} {uid}            \t check the property with given ID\n"
     " {y-I} {upath}                  \t set include path\n"
+    " {y--system-verilog}            \t force SystemVerilog instead of Verilog\n"
     " {y--reset} {uexpr}             \t set up module reset\n"
     " {y--liveness-to-safety}        \t translate liveness properties to safety properties\n"
     "\n"

src/ebmc/ebmc_parse_options.h

@@ -46,7 +46,7 @@ class ebmc_parse_optionst:public parse_options_baset
         "(random-traces)(trace-steps):(random-seed):(number-of-traces):"
         "(random-trace)(random-waveform)"
         "(liveness-to-safety)"
-        "I:(preprocess)",
+        "I:(preprocess)(system-verilog)",
         argc,
         argv,
         std::string("EBMC ") + EBMC_VERSION),

src/ebmc/transition_system.cpp

@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 #include <langapi/mode.h>
 #include <trans-word-level/show_module_hierarchy.h>
 #include <trans-word-level/show_modules.h>
+#include <verilog/verilog_language.h>
 
 #include "ebmc_error.h"
 #include "ebmc_version.h"
@@ -221,6 +222,10 @@ int get_transition_system(
   if(cmdline.isset('I'))
     config.verilog.include_paths = cmdline.get_values('I');
 
+  // do --system-verilog
+  if(cmdline.isset("system-verilog"))
+    verilog_languaget::force_systemverilog = true;
+
   if(cmdline.isset("preprocess"))
     return preprocess(cmdline, message_handler);
 

src/verilog/verilog_language.cpp

@@ -18,6 +18,8 @@ Author: Daniel Kroening, [email protected]
 #include "verilog_parser.h"
 #include "verilog_preprocessor.h"
 
+bool verilog_languaget::force_systemverilog = false;
+
 /*******************************************************************\
 
 Function: verilog_languaget::parse
@@ -46,8 +48,8 @@ bool verilog_languaget::parse(
   verilog_parser.in=&str;
   verilog_parser.log.set_message_handler(message_handler);
   verilog_parser.grammar=verilog_parsert::LANGUAGE;
-  
-  if(has_suffix(path, ".sv"))
+
+  if(has_suffix(path, ".sv") || force_systemverilog)
     verilog_parser.mode=verilog_parsert::SYSTEM_VERILOG;
 
   verilog_scanner_init();

src/verilog/verilog_language.h

@@ -91,6 +91,9 @@ class verilog_languaget:public languaget
     options.set_option("flatten_hierarchy", true);
   }
 
+  // static configuration, gobal
+  static bool force_systemverilog;
+
 protected:
   verilog_parse_treet parse_tree;
 };