From 9476a67b0818e1d9fa5b3e2410ec768c7ff11b4e Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 8 Aug 2024 16:39:10 -0700 Subject: [PATCH] Verilog: set defines on command line This allows setting SystemVerilog preprocessor defines on the command line with -D. --- .../verilog/preprocessor/cmdline_define1.desc | 10 ++++++++++ .../verilog/preprocessor/cmdline_define1.v | 7 +++++++ .../verilog/preprocessor/cmdline_define2.desc | 8 ++++++++ .../verilog/preprocessor/cmdline_define2.v | 3 +++ src/ebmc/ebmc_parse_options.h | 2 +- src/ebmc/transition_system.cpp | 8 ++++++++ src/verilog/verilog_language.cpp | 5 +++-- src/verilog/verilog_language.h | 4 +--- src/verilog/verilog_preprocessor.cpp | 18 ++++++++++++++++++ src/verilog/verilog_preprocessor.h | 13 +++++++++++-- src/verilog/verilog_preprocessor_tokenizer.cpp | 11 +++++++++++ src/verilog/verilog_preprocessor_tokenizer.h | 6 ++++++ 12 files changed, 87 insertions(+), 8 deletions(-) create mode 100644 regression/verilog/preprocessor/cmdline_define1.desc create mode 100644 regression/verilog/preprocessor/cmdline_define1.v create mode 100644 regression/verilog/preprocessor/cmdline_define2.desc create mode 100644 regression/verilog/preprocessor/cmdline_define2.v diff --git a/regression/verilog/preprocessor/cmdline_define1.desc b/regression/verilog/preprocessor/cmdline_define1.desc new file mode 100644 index 000000000..1871b7a70 --- /dev/null +++ b/regression/verilog/preprocessor/cmdline_define1.desc @@ -0,0 +1,10 @@ +CORE +cmdline_define1.v +--preprocess -D SOMETHING -D ELSE=foo +^A$ +^foo$ +^EXIT=0$ +^SIGNAL=0$ +-- +^B$ +^PREPROCESSING FAILED$ diff --git a/regression/verilog/preprocessor/cmdline_define1.v b/regression/verilog/preprocessor/cmdline_define1.v new file mode 100644 index 000000000..9d480ee61 --- /dev/null +++ b/regression/verilog/preprocessor/cmdline_define1.v @@ -0,0 +1,7 @@ +`ifdef SOMETHING +A +`endif +`ifdef OTHER +B +`endif +`ELSE diff --git a/regression/verilog/preprocessor/cmdline_define2.desc b/regression/verilog/preprocessor/cmdline_define2.desc new file mode 100644 index 000000000..3b9b6876d --- /dev/null +++ b/regression/verilog/preprocessor/cmdline_define2.desc @@ -0,0 +1,8 @@ +CORE +cmdline_define2.v +--show-modules -D SOME_NAME=foo +^ Name: foo$ +^EXIT=0$ +^SIGNAL=0$ +-- +^PREPROCESSING FAILED$ diff --git a/regression/verilog/preprocessor/cmdline_define2.v b/regression/verilog/preprocessor/cmdline_define2.v new file mode 100644 index 000000000..d2366f74a --- /dev/null +++ b/regression/verilog/preprocessor/cmdline_define2.v @@ -0,0 +1,3 @@ +module `SOME_NAME(); + +endmodule diff --git a/src/ebmc/ebmc_parse_options.h b/src/ebmc/ebmc_parse_options.h index 051413cf8..11f22585d 100644 --- a/src/ebmc/ebmc_parse_options.h +++ b/src/ebmc/ebmc_parse_options.h @@ -47,7 +47,7 @@ class ebmc_parse_optionst:public parse_options_baset "(random-traces)(trace-steps):(random-seed):(traces):" "(random-trace)(random-waveform)" "(liveness-to-safety)" - "I:(preprocess)(systemverilog)(vl2smv-extensions)", + "I:D:(preprocess)(systemverilog)(vl2smv-extensions)", argc, argv, std::string("EBMC ") + EBMC_VERSION), diff --git a/src/ebmc/transition_system.cpp b/src/ebmc/transition_system.cpp index 954bd07e3..ead0dbf09 100644 --- a/src/ebmc/transition_system.cpp +++ b/src/ebmc/transition_system.cpp @@ -113,6 +113,10 @@ int preprocess(const cmdlinet &cmdline, message_handlert &message_handler) options.set_option("force-systemverilog", cmdline.isset("systemverilog")); options.set_option("vl2smv-extensions", cmdline.isset("vl2smv-extensions")); + // 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)) @@ -160,6 +164,10 @@ static bool parse( options.set_option("force-systemverilog", cmdline.isset("systemverilog")); options.set_option("vl2smv-extensions", cmdline.isset("vl2smv-extensions")); + // do -D + if(cmdline.isset('D')) + options.set_option("defines", cmdline.get_values('D')); + language.set_language_options(options, message_handler); message.status() << "Parsing " << filename << messaget::eom; diff --git a/src/verilog/verilog_language.cpp b/src/verilog/verilog_language.cpp index f31872adf..d8961af9a 100644 --- a/src/verilog/verilog_language.cpp +++ b/src/verilog/verilog_language.cpp @@ -36,6 +36,7 @@ void verilog_languaget::set_language_options( { force_systemverilog = options.get_bool_option("force-systemverilog"); vl2smv_extensions = options.get_bool_option("vl2smv-extensions"); + initial_defines = options.get_list_option("defines"); } /*******************************************************************\ @@ -103,7 +104,7 @@ bool verilog_languaget::preprocess( message_handlert &message_handler) { verilog_preprocessort preprocessor( - instream, outstream, message_handler, path); + instream, outstream, message_handler, path, initial_defines); try { preprocessor.preprocessor(); } catch(int e) { return true; } @@ -186,7 +187,7 @@ bool verilog_languaget::typecheck( message.debug() << "Synthesis " << module << messaget::eom; if(verilog_synthesis( - symbol_table, module, parse_tree.standard, message_handler, options)) + symbol_table, module, parse_tree.standard, message_handler, optionst{})) return true; return false; diff --git a/src/verilog/verilog_language.h b/src/verilog/verilog_language.h index 2bea98102..d7dd5e349 100644 --- a/src/verilog/verilog_language.h +++ b/src/verilog/verilog_language.h @@ -85,17 +85,15 @@ class verilog_languaget:public languaget { return parse_tree; } - - optionst options; verilog_languaget() : parse_tree(verilog_standardt::NOT_SET) { - options.set_option("flatten_hierarchy", true); } protected: bool force_systemverilog = false; bool vl2smv_extensions = false; + std::list initial_defines; verilog_parse_treet parse_tree; }; diff --git a/src/verilog/verilog_preprocessor.cpp b/src/verilog/verilog_preprocessor.cpp index 44783ad08..d8ff5e843 100644 --- a/src/verilog/verilog_preprocessor.cpp +++ b/src/verilog/verilog_preprocessor.cpp @@ -184,6 +184,24 @@ void verilog_preprocessort::preprocessor() { try { + // set up the initial defines + for(auto &define : initial_defines) + { + std::size_t equal_pos = define.find('='); + if(equal_pos == std::string::npos) + { + defines.insert(std::pair(define, definet{})); + } + else + { + std::string key = define.substr(0, equal_pos); + std::string value = define.substr(equal_pos + 1, std::string::npos); + auto tokens = verilog_preprocessor_tokenize(value); + defines.insert( + std::pair(key, definet{std::move(tokens)})); + } + } + // the first context is the input file context_stack.emplace_back(false, &in, widen_if_needed(filename)); diff --git a/src/verilog/verilog_preprocessor.h b/src/verilog/verilog_preprocessor.h index 732ddbf59..53616c73b 100644 --- a/src/verilog/verilog_preprocessor.h +++ b/src/verilog/verilog_preprocessor.h @@ -21,8 +21,10 @@ class verilog_preprocessort:public preprocessort std::istream &_in, std::ostream &_out, message_handlert &_message_handler, - const std::string &_filename): - preprocessort(_in, _out, _message_handler, _filename) + const std::string &_filename, + const std::list &_initial_defines) + : preprocessort(_in, _out, _message_handler, _filename), + initial_defines(_initial_defines) { condition=true; } @@ -30,6 +32,9 @@ class verilog_preprocessort:public preprocessort virtual ~verilog_preprocessort() { } protected: + // from the command line + const std::list &initial_defines; + using tokent = verilog_preprocessor_token_sourcet::tokent; struct definet @@ -37,6 +42,10 @@ class verilog_preprocessort:public preprocessort using parameterst = std::vector; parameterst parameters; std::vector tokens; + definet() = default; + explicit definet(std::vector _tokens) : tokens(std::move(_tokens)) + { + } }; static std::string as_string(const std::vector &); diff --git a/src/verilog/verilog_preprocessor_tokenizer.cpp b/src/verilog/verilog_preprocessor_tokenizer.cpp index e9ae9c5bb..abba5f6d6 100644 --- a/src/verilog/verilog_preprocessor_tokenizer.cpp +++ b/src/verilog/verilog_preprocessor_tokenizer.cpp @@ -114,3 +114,14 @@ void verilog_preprocessor_tokenizert::get_token_from_stream() token.kind = static_cast( yyverilog_preprocessorlex()); } + +std::vector +verilog_preprocessor_tokenize(const std::string &text) +{ + std::istringstream instream(text); + verilog_preprocessor_tokenizert tokenizer(instream); + std::vector result; + while(!tokenizer.eof()) + result.push_back(tokenizer.next_token()); + return result; +} diff --git a/src/verilog/verilog_preprocessor_tokenizer.h b/src/verilog/verilog_preprocessor_tokenizer.h index e2d42ae58..bedc68e22 100644 --- a/src/verilog/verilog_preprocessor_tokenizer.h +++ b/src/verilog/verilog_preprocessor_tokenizer.h @@ -11,6 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "verilog_preprocessor_error.h" +#include + /// Note that the set of tokens recognised by the Verilog preprocessor /// differs from the set of tokens used by the main parser. @@ -105,4 +107,8 @@ class verilog_preprocessor_tokenizert void get_token_from_stream() override; }; +// tokenize a given string +std::vector +verilog_preprocessor_tokenize(const std::string &); + #endif // VERILOG_PREPROCESSOR_TOKENIZER_H