Skip to content

Commit fbfde77

Browse files
authored
Merge pull request #410 from diffblue/force-system-verilog
ebmc: add --systemverilog command-line option
2 parents b95ce08 + c1cbce3 commit fbfde77

File tree

7 files changed

+53
-5
lines changed

7 files changed

+53
-5
lines changed
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main1.v
3+
--systemverilog
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^no properties$
7+
--
8+
^warning: ignoring
Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
module main;
2+
// 'logic' is a SystemVerilog keyword
3+
logic some_logic;
4+
initial some_logic = 1;
5+
endmodule

src/ebmc/ebmc_parse_options.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -363,6 +363,7 @@ void ebmc_parse_optionst::help()
363363
" {y--show-properties} \t list the properties in the model\n"
364364
" {y--property} {uid} \t check the property with given ID\n"
365365
" {y-I} {upath} \t set include path\n"
366+
" {y--systemverilog} \t force SystemVerilog instead of Verilog\n"
366367
" {y--reset} {uexpr} \t set up module reset\n"
367368
" {y--liveness-to-safety} \t translate liveness properties to safety properties\n"
368369
"\n"

src/ebmc/ebmc_parse_options.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ class ebmc_parse_optionst:public parse_options_baset
4646
"(random-traces)(trace-steps):(random-seed):(number-of-traces):"
4747
"(random-trace)(random-waveform)"
4848
"(liveness-to-safety)"
49-
"I:(preprocess)",
49+
"I:(preprocess)(systemverilog)",
5050
argc,
5151
argv,
5252
std::string("EBMC ") + EBMC_VERSION),

src/ebmc/transition_system.cpp

Lines changed: 14 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
1313
#include <util/get_module.h>
1414
#include <util/message.h>
1515
#include <util/namespace.h>
16+
#include <util/options.h>
1617
#include <util/unicode.h>
1718

1819
#include <langapi/language.h>
@@ -107,6 +108,11 @@ int preprocess(const cmdlinet &cmdline, message_handlert &message_handler)
107108
return 1;
108109
}
109110

111+
optionst options;
112+
options.set_option("force-systemverilog", cmdline.isset("systemverilog"));
113+
114+
language->set_language_options(options, message_handler);
115+
110116
if(language->preprocess(infile, filename, std::cout, message_handler))
111117
{
112118
message.error() << "PREPROCESSING FAILED" << messaget::eom;
@@ -116,7 +122,8 @@ int preprocess(const cmdlinet &cmdline, message_handlert &message_handler)
116122
return 0;
117123
}
118124

119-
bool parse(
125+
static bool parse(
126+
const cmdlinet &cmdline,
120127
const std::string &filename,
121128
language_filest &language_files,
122129
message_handlert &message_handler)
@@ -147,6 +154,11 @@ bool parse(
147154

148155
languaget &language = *lf.language;
149156

157+
optionst options;
158+
options.set_option("force-systemverilog", cmdline.isset("systemverilog"));
159+
160+
language.set_language_options(options, message_handler);
161+
150162
message.status() << "Parsing " << filename << messaget::eom;
151163

152164
if(language.parse(infile, filename, message_handler))
@@ -167,7 +179,7 @@ bool parse(
167179
{
168180
for(unsigned i = 0; i < cmdline.args.size(); i++)
169181
{
170-
if(parse(cmdline.args[i], language_files, message_handler))
182+
if(parse(cmdline, cmdline.args[i], language_files, message_handler))
171183
return true;
172184
}
173185
return false;

src/verilog/verilog_language.cpp

Lines changed: 21 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,25 @@ Author: Daniel Kroening, [email protected]
2020

2121
/*******************************************************************\
2222
23+
Function: verilog_languaget::set_language_options
24+
25+
Inputs:
26+
27+
Outputs:
28+
29+
Purpose:
30+
31+
\*******************************************************************/
32+
33+
void verilog_languaget::set_language_options(
34+
const optionst &options,
35+
message_handlert &message_handler)
36+
{
37+
force_systemverilog = options.get_bool_option("force-systemverilog");
38+
}
39+
40+
/*******************************************************************\
41+
2342
Function: verilog_languaget::parse
2443
2544
Inputs:
@@ -46,8 +65,8 @@ bool verilog_languaget::parse(
4665
verilog_parser.in=&str;
4766
verilog_parser.log.set_message_handler(message_handler);
4867
verilog_parser.grammar=verilog_parsert::LANGUAGE;
49-
50-
if(has_suffix(path, ".sv"))
68+
69+
if(has_suffix(path, ".sv") || force_systemverilog)
5170
verilog_parser.mode=verilog_parsert::SYSTEM_VERILOG;
5271

5372
verilog_scanner_init();

src/verilog/verilog_language.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -79,6 +79,8 @@ class verilog_languaget:public languaget
7979
return { "v", "sv" };
8080
}
8181

82+
void set_language_options(const optionst &, message_handlert &) override;
83+
8284
verilog_parse_treet &get_parse_tree()
8385
{
8486
return parse_tree;
@@ -92,6 +94,7 @@ class verilog_languaget:public languaget
9294
}
9395

9496
protected:
97+
bool force_systemverilog = false;
9598
verilog_parse_treet parse_tree;
9699
};
97100

0 commit comments

Comments
 (0)