Skip to content

ebmc: add --systemverilog command-line option #410

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Mar 19, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 8 additions & 0 deletions regression/verilog/force-system-verilog/main1.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
main1.v
--systemverilog
^EXIT=10$
^SIGNAL=0$
^no properties$
--
^warning: ignoring
5 changes: 5 additions & 0 deletions regression/verilog/force-system-verilog/main1.v
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
module main;
// 'logic' is a SystemVerilog keyword
logic some_logic;
initial some_logic = 1;
endmodule
1 change: 1 addition & 0 deletions src/ebmc/ebmc_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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--systemverilog} \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"
Expand Down
2 changes: 1 addition & 1 deletion src/ebmc/ebmc_parse_options.h
Original file line number Diff line number Diff line change
Expand Up @@ -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)(systemverilog)",
argc,
argv,
std::string("EBMC ") + EBMC_VERSION),
Expand Down
16 changes: 14 additions & 2 deletions src/ebmc/transition_system.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
#include <util/get_module.h>
#include <util/message.h>
#include <util/namespace.h>
#include <util/options.h>
#include <util/unicode.h>

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

optionst options;
options.set_option("force-systemverilog", cmdline.isset("systemverilog"));

language->set_language_options(options, message_handler);

if(language->preprocess(infile, filename, std::cout, message_handler))
{
message.error() << "PREPROCESSING FAILED" << messaget::eom;
Expand All @@ -116,7 +122,8 @@ int preprocess(const cmdlinet &cmdline, message_handlert &message_handler)
return 0;
}

bool parse(
static bool parse(
const cmdlinet &cmdline,
const std::string &filename,
language_filest &language_files,
message_handlert &message_handler)
Expand Down Expand Up @@ -147,6 +154,11 @@ bool parse(

languaget &language = *lf.language;

optionst options;
options.set_option("force-systemverilog", cmdline.isset("systemverilog"));

language.set_language_options(options, message_handler);

message.status() << "Parsing " << filename << messaget::eom;

if(language.parse(infile, filename, message_handler))
Expand All @@ -167,7 +179,7 @@ bool parse(
{
for(unsigned i = 0; i < cmdline.args.size(); i++)
{
if(parse(cmdline.args[i], language_files, message_handler))
if(parse(cmdline, cmdline.args[i], language_files, message_handler))
return true;
}
return false;
Expand Down
23 changes: 21 additions & 2 deletions src/verilog/verilog_language.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,25 @@ Author: Daniel Kroening, [email protected]

/*******************************************************************\

Function: verilog_languaget::set_language_options

Inputs:

Outputs:

Purpose:

\*******************************************************************/

void verilog_languaget::set_language_options(
const optionst &options,
message_handlert &message_handler)
{
force_systemverilog = options.get_bool_option("force-systemverilog");
}

/*******************************************************************\

Function: verilog_languaget::parse

Inputs:
Expand All @@ -46,8 +65,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();
Expand Down
3 changes: 3 additions & 0 deletions src/verilog/verilog_language.h
Original file line number Diff line number Diff line change
Expand Up @@ -79,6 +79,8 @@ class verilog_languaget:public languaget
return { "v", "sv" };
}

void set_language_options(const optionst &, message_handlert &) override;

verilog_parse_treet &get_parse_tree()
{
return parse_tree;
Expand All @@ -92,6 +94,7 @@ class verilog_languaget:public languaget
}

protected:
bool force_systemverilog = false;
verilog_parse_treet parse_tree;
};

Expand Down