From d4d26c0230ea941f1f266c772e35d9dd66b49063 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 13 Apr 2024 10:47:09 -0400 Subject: [PATCH] Verilog: vl2smv extensions This adds support for a wider set of the extensions offered by Cadence SMV's vl2smv to the Verilog front-end. The extensions are enabled with --vl2smv-extensions. --- regression/ebmc/assume1/test.desc | 2 +- regression/verilog/vl2smv-extensions/README | 1 + .../verilog/vl2smv-extensions/traffic-1.desc | 7 ++ .../verilog/vl2smv-extensions/traffic-2.desc | 7 ++ .../verilog/vl2smv-extensions/traffic-3.desc | 7 ++ .../verilog/vl2smv-extensions/traffic/1.v | 115 +++++++++++++++++ .../verilog/vl2smv-extensions/traffic/2.v | 116 ++++++++++++++++++ .../verilog/vl2smv-extensions/traffic/3.v | 114 +++++++++++++++++ src/ebmc/ebmc_parse_options.h | 2 +- src/ebmc/transition_system.cpp | 2 + src/hw_cbmc_irep_ids.h | 2 + src/verilog/parser.y | 39 +++++- src/verilog/scanner.l | 31 ++++- src/verilog/verilog_elaborate.cpp | 9 ++ src/verilog/verilog_interfaces.cpp | 6 + src/verilog/verilog_language.cpp | 3 + src/verilog/verilog_language.h | 1 + src/verilog/verilog_parser.h | 10 +- src/verilog/verilog_typecheck.cpp | 9 ++ 19 files changed, 471 insertions(+), 12 deletions(-) create mode 100644 regression/verilog/vl2smv-extensions/README create mode 100644 regression/verilog/vl2smv-extensions/traffic-1.desc create mode 100644 regression/verilog/vl2smv-extensions/traffic-2.desc create mode 100644 regression/verilog/vl2smv-extensions/traffic-3.desc create mode 100644 regression/verilog/vl2smv-extensions/traffic/1.v create mode 100644 regression/verilog/vl2smv-extensions/traffic/2.v create mode 100644 regression/verilog/vl2smv-extensions/traffic/3.v diff --git a/regression/ebmc/assume1/test.desc b/regression/ebmc/assume1/test.desc index 18e318d54..79780cb7d 100644 --- a/regression/ebmc/assume1/test.desc +++ b/regression/ebmc/assume1/test.desc @@ -1,5 +1,5 @@ CORE main.v ---module main --bound 3 --aig +--module main --bound 3 --aig --vl2smv-extensions ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/verilog/vl2smv-extensions/README b/regression/verilog/vl2smv-extensions/README new file mode 100644 index 000000000..54f60bb37 --- /dev/null +++ b/regression/verilog/vl2smv-extensions/README @@ -0,0 +1 @@ +From the Cadence SMV distribution, doc/smv/examples/vlog. diff --git a/regression/verilog/vl2smv-extensions/traffic-1.desc b/regression/verilog/vl2smv-extensions/traffic-1.desc new file mode 100644 index 000000000..2d99701d6 --- /dev/null +++ b/regression/verilog/vl2smv-extensions/traffic-1.desc @@ -0,0 +1,7 @@ +CORE +traffic/1.v +--vl2smv-extensions +^file .* line 50: assignment in 'always' context without event guard$ +^EXIT=2$ +^SIGNAL=0$ +-- diff --git a/regression/verilog/vl2smv-extensions/traffic-2.desc b/regression/verilog/vl2smv-extensions/traffic-2.desc new file mode 100644 index 000000000..2e4fd488b --- /dev/null +++ b/regression/verilog/vl2smv-extensions/traffic-2.desc @@ -0,0 +1,7 @@ +CORE +traffic/2.v +--vl2smv-extensions +^file .* line 50: assignment in 'always' context without event guard$ +^EXIT=2$ +^SIGNAL=0$ +-- diff --git a/regression/verilog/vl2smv-extensions/traffic-3.desc b/regression/verilog/vl2smv-extensions/traffic-3.desc new file mode 100644 index 000000000..0a77b3aed --- /dev/null +++ b/regression/verilog/vl2smv-extensions/traffic-3.desc @@ -0,0 +1,7 @@ +CORE +traffic/3.v +--vl2smv-extensions +^file .* line 50: assignment in 'always' context without event guard$ +^EXIT=2$ +^SIGNAL=0$ +-- diff --git a/regression/verilog/vl2smv-extensions/traffic/1.v b/regression/verilog/vl2smv-extensions/traffic/1.v new file mode 100644 index 000000000..a9437d4d5 --- /dev/null +++ b/regression/verilog/vl2smv-extensions/traffic/1.v @@ -0,0 +1,115 @@ +module main(N_SENSE,S_SENSE,E_SENSE,N_GO,S_GO,E_GO); + +/* + This program implements a traffic light controller. + + Input signals: + N_SENSE - + When this goes high, a car from the north is waiting to cross the + intersection. (This signal does not have to remain high until + the request is granted.) Once the request has been granted, this + signal goes low to indicate that the car has finished crossing + the intersection. + S_SENSE - Same as N, except for traffic from the south. + E_SENSE - Same as N, except for traffic from the east. + + Output signals: + N_GO - If this signal is high, traffic from the north is permitted to + enter the intersection. If it is low, traffic must wait. + S_GO - Same as N_GO, except for traffic from the south. + E_GO - Same as N_GO, except for traffic from the east. + + Internal signals: + N_REQ - Since N is not required to remain high to indicate that a + car from the north wants to cross the intersection, this signal + is used to latch requests from the north. + S_REQ - Same as N_REQ, except for traffic from the south. + E_REQ - Same as N_REQ, except for traffic from the east. + NS_LOCK - This signal is set high by north/south traffic in order to + lock out traffic from the east. + EW_LOCK - This signal is set high by east traffic in order to + lock out traffic from the north/south. +*/ + + input N_SENSE, S_SENSE, E_SENSE; + output N_GO, S_GO, E_GO; + + wire N_SENSE, S_SENSE, E_SENSE; + reg N_GO, S_GO, E_GO; + reg NS_LOCK, EW_LOCK, N_REQ, S_REQ, E_REQ; + + initial begin + N_REQ = 0; S_REQ = 0; E_REQ = 0; + N_GO = 0; S_GO = 0; E_GO = 0; + NS_LOCK = 0; EW_LOCK = 0; + end + + +/* latch traffic sensor inputs */ + + always begin if (!N_REQ & N_SENSE) N_REQ = 1; end + always begin if (!S_REQ & S_SENSE) S_REQ = 1; end + always begin if (!E_REQ & E_SENSE) E_REQ = 1; end + +/* North traffic controller */ + + always begin + if (N_REQ) + begin + wait (!EW_LOCK); + NS_LOCK = 1; + N_GO = 1; + wait (!N_SENSE); + if (!S_GO) NS_LOCK = 0; + N_GO = 0; + N_REQ = 0; + end + end + +/* South traffic controller */ + + always begin + if (S_REQ) + begin + wait (!EW_LOCK); + NS_LOCK = 1; S_GO = 1; + wait (!S_SENSE); + if (!N_GO) NS_LOCK = 0; + S_GO = 0; S_REQ = 0; + end + end + +/* East traffic controller */ + + always begin + if (E_REQ) + begin + EW_LOCK = 1; + wait (!NS_LOCK); + E_GO = 1; + wait (!E_SENSE); + EW_LOCK = 0; E_GO = 0; E_REQ = 0; + end + end + +/* specifications */ + +always begin + assert mutex: !(E_GO & (S_GO | N_GO)); + if (E_SENSE) assert E_live: eventually E_GO; + if (S_SENSE) assert S_live: eventually S_GO; + if (N_SENSE) assert N_live: eventually N_GO; +end + +/* assumptions */ + +always begin + assert E_fair: eventually !(E_GO & E_SENSE); + assert S_fair: eventually !(S_GO & S_SENSE); + assert N_fair: eventually !(N_GO & N_SENSE); +end + +using E_fair, S_fair, N_fair prove E_live, S_live, N_live; +assume E_fair, S_fair, N_fair; + +endmodule \ No newline at end of file diff --git a/regression/verilog/vl2smv-extensions/traffic/2.v b/regression/verilog/vl2smv-extensions/traffic/2.v new file mode 100644 index 000000000..03ee48c15 --- /dev/null +++ b/regression/verilog/vl2smv-extensions/traffic/2.v @@ -0,0 +1,116 @@ +module main(N_SENSE,S_SENSE,E_SENSE,N_GO,S_GO,E_GO); + +/* + This program implements a traffic light controller. + + Input signals: + N_SENSE - + When this goes high, a car from the north is waiting to cross the + intersection. (This signal does not have to remain high until + the request is granted.) Once the request has been granted, this + signal goes low to indicate that the car has finished crossing + the intersection. + S_SENSE - Same as N, except for traffic from the south. + E_SENSE - Same as N, except for traffic from the east. + + Output signals: + N_GO - If this signal is high, traffic from the north is permitted to + enter the intersection. If it is low, traffic must wait. + S_GO - Same as N_GO, except for traffic from the south. + E_GO - Same as N_GO, except for traffic from the east. + + Internal signals: + N_REQ - Since N is not required to remain high to indicate that a + car from the north wants to cross the intersection, this signal + is used to latch requests from the north. + S_REQ - Same as N_REQ, except for traffic from the south. + E_REQ - Same as N_REQ, except for traffic from the east. + NS_LOCK - This signal is set high by north/south traffic in order to + lock out traffic from the east. + EW_LOCK - This signal is set high by east traffic in order to + lock out traffic from the north/south. +*/ + + input N_SENSE, S_SENSE, E_SENSE; + output N_GO, S_GO, E_GO; + + wire N_SENSE, S_SENSE, E_SENSE; + reg N_GO, S_GO, E_GO; + reg NS_LOCK, EW_LOCK, N_REQ, S_REQ, E_REQ; + + initial begin + N_REQ = 0; S_REQ = 0; E_REQ = 0; + N_GO = 0; S_GO = 0; E_GO = 0; + NS_LOCK = 0; EW_LOCK = 0; + end + + +/* latch traffic sensor inputs */ + + always begin if (!N_REQ & N_SENSE) N_REQ = 1; end + always begin if (!S_REQ & S_SENSE) S_REQ = 1; end + always begin if (!E_REQ & E_SENSE) E_REQ = 1; end + +/* North traffic controller */ + + always begin + if (N_REQ) + begin + wait (!EW_LOCK & !(S_GO & !S_SENSE)); + NS_LOCK = 1; + N_GO = 1; + wait (!N_SENSE); + if (!S_GO) NS_LOCK = 0; + N_GO = 0; + N_REQ = 0; + end + end + +/* South traffic controller */ + + always begin + if (S_REQ) + begin + wait (!EW_LOCK & !(N_GO & !N_SENSE)); + NS_LOCK = 1; S_GO = 1; + wait (!S_SENSE); + if (!N_GO) NS_LOCK = 0; + S_GO = 0; S_REQ = 0; + end + end + +/* East traffic controller */ + + always begin + if (E_REQ) + begin + EW_LOCK = 1; + wait (!NS_LOCK); + E_GO = 1; + wait (!E_SENSE); + EW_LOCK = 0; E_GO = 0; E_REQ = 0; + end + end + +/* specifications */ + +always begin + assert mutex: !(E_GO & (S_GO | N_GO)); + if (E_SENSE) assert E_live: eventually E_GO; + if (S_SENSE) assert S_live: eventually S_GO; + if (N_SENSE) assert N_live: eventually N_GO; +end + +/* assumptions */ + +always begin + assert E_fair: eventually !(E_GO & E_SENSE); + assert S_fair: eventually !(S_GO & S_SENSE); + assert N_fair: eventually !(N_GO & N_SENSE); +end + +using E_fair, S_fair, N_fair prove E_live, S_live, N_live; +assume E_fair, S_fair, N_fair; + + +endmodule \ No newline at end of file diff --git a/regression/verilog/vl2smv-extensions/traffic/3.v b/regression/verilog/vl2smv-extensions/traffic/3.v new file mode 100644 index 000000000..dac89383b --- /dev/null +++ b/regression/verilog/vl2smv-extensions/traffic/3.v @@ -0,0 +1,114 @@ +module main(N_SENSE,S_SENSE,E_SENSE,N_GO,S_GO,E_GO); + +/* + This program implements a traffic light controller. + + Input signals: + N_SENSE - + When this goes high, a car from the north is waiting to cross the + intersection. (This signal does not have to remain high until + the request is granted.) Once the request has been granted, this + signal goes low to indicate that the car has finished crossing + the intersection. + S_SENSE - Same as N, except for traffic from the south. + E_SENSE - Same as N, except for traffic from the east. + + Output signals: + N_GO - If this signal is high, traffic from the north is permitted to + enter the intersection. If it is low, traffic must wait. + S_GO - Same as N_GO, except for traffic from the south. + E_GO - Same as N_GO, except for traffic from the east. + + Internal signals: + N_REQ - Since N is not required to remain high to indicate that a + car from the north wants to cross the intersection, this signal + is used to latch requests from the north. + S_REQ - Same as N_REQ, except for traffic from the south. + E_REQ - Same as N_REQ, except for traffic from the east. + NS_LOCK - This signal is set high by north/south traffic in order to + lock out traffic from the east. + EW_LOCK - This signal is set high by east traffic in order to + lock out traffic from the north/south. +*/ + + input N_SENSE, S_SENSE, E_SENSE; + output N_GO, S_GO, E_GO; + + wire N_SENSE, S_SENSE, E_SENSE; + reg N_GO, S_GO, E_GO; + reg NS_LOCK, EW_LOCK, N_REQ, S_REQ, E_REQ; + + initial begin + N_REQ = 0; S_REQ = 0; E_REQ = 0; + N_GO = 0; S_GO = 0; E_GO = 0; + NS_LOCK = 0; EW_LOCK = 0; + end + + +/* latch traffic sensor inputs */ + + always begin if (!N_REQ & N_SENSE) N_REQ = 1; end + always begin if (!S_REQ & S_SENSE) S_REQ = 1; end + always begin if (!E_REQ & E_SENSE) E_REQ = 1; end + +/* North traffic controller */ + + always begin + if (N_REQ) + begin + wait (!EW_LOCK & !(S_GO & !S_SENSE)); + NS_LOCK = 1; N_GO = 1; + wait (!N_SENSE); + if (!S_GO | !S_SENSE) NS_LOCK = 0; + N_GO = 0; N_REQ = 0; + end + end + +/* South traffic controller */ + + always begin + if (S_REQ) + begin + wait (!EW_LOCK & !(N_GO & !N_SENSE)); + NS_LOCK = 1; S_GO = 1; + wait (!S_SENSE); + if (!N_GO | !N_SENSE) NS_LOCK = 0; + S_GO = 0; S_REQ = 0; + end + end + +/* East traffic controller */ + + always begin + if (E_REQ) + begin + EW_LOCK = 1; + wait (!NS_LOCK); + E_GO = 1; + wait (!E_SENSE); + EW_LOCK = 0; E_GO = 0; E_REQ = 0; + end + end + +/* specifications */ + +always begin + assert mutex: !(E_GO & (S_GO | N_GO)); + if (E_SENSE) assert E_live: eventually E_GO; + if (S_SENSE) assert S_live: eventually S_GO; + if (N_SENSE) assert N_live: eventually N_GO; +end + +/* assumptions */ + +always begin + assert E_fair: eventually !(E_GO & E_SENSE); + assert S_fair: eventually !(S_GO & S_SENSE); + assert N_fair: eventually !(N_GO & N_SENSE); +end + +using E_fair, S_fair, N_fair prove E_live, S_live, N_live; +assume E_fair, S_fair, N_fair; + + +endmodule \ No newline at end of file diff --git a/src/ebmc/ebmc_parse_options.h b/src/ebmc/ebmc_parse_options.h index 1a58e2563..605fa03c8 100644 --- a/src/ebmc/ebmc_parse_options.h +++ b/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)(systemverilog)", + "I:(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 ba53c9834..3ebacd496 100644 --- a/src/ebmc/transition_system.cpp +++ b/src/ebmc/transition_system.cpp @@ -110,6 +110,7 @@ int preprocess(const cmdlinet &cmdline, message_handlert &message_handler) optionst options; options.set_option("force-systemverilog", cmdline.isset("systemverilog")); + options.set_option("vl2smv-extensions", cmdline.isset("vl2smv-extensions")); language->set_language_options(options, message_handler); @@ -156,6 +157,7 @@ static bool parse( optionst options; options.set_option("force-systemverilog", cmdline.isset("systemverilog")); + options.set_option("vl2smv-extensions", cmdline.isset("vl2smv-extensions")); language.set_language_options(options, message_handler); diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 00e979018..f7a3ff5a6 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -70,6 +70,8 @@ IREP_ID_ONE(deassign) IREP_ID_ONE(continuous_assign) IREP_ID_ONE(procedural_continuous_assign) IREP_ID_ONE(wait) +IREP_ID_ONE(verilog_smv_eventually) +IREP_ID_ONE(verilog_smv_using) IREP_ID_ONE(verilog_assert_property) IREP_ID_ONE(verilog_assume_property) IREP_ID_ONE(verilog_cover_property) diff --git a/src/verilog/parser.y b/src/verilog/parser.y index e27dab48a..cced4ddb1 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -515,6 +515,10 @@ int yyverilogerror(const char *error) %token TOK_SYSIDENT // system task or function enable %token TOK_SCANNER_ERROR +/* VL2SMV */ +%token TOK_USING "using" +%token TOK_PROVE "prove" + // Precedence of System Verilog Assertions Operators, // following System Verilog 1800-2017 Table 16-3. // Bison expects these in order of increasing precedence, @@ -836,6 +840,8 @@ module_or_generate_item: | attribute_instance_brace module_instantiation { $$=$2; } | attribute_instance_brace concurrent_assertion_item { $$=$2; } | attribute_instance_brace assertion_item_declaration { $$=$2; } + | attribute_instance_brace smv_using { $$ = $2; } + | attribute_instance_brace smv_assume { $$ = $2; } | attribute_instance_brace module_common_item { $$=$2; } ; @@ -1891,13 +1897,13 @@ concurrent_assertion_statement: /* This one mimicks functionality in Cadence SMV */ smv_assertion_statement: - TOK_ASSERT property_identifier TOK_COLON expression ';' + TOK_ASSERT property_identifier TOK_COLON smv_property ';' { init($$, ID_verilog_smv_assert); stack_expr($$).operands().resize(2); to_binary_expr(stack_expr($$)).op0().swap(stack_expr($4)); to_binary_expr(stack_expr($$)).op1().make_nil(); stack_expr($$).set(ID_identifier, stack_expr($2).id()); } - | TOK_ASSUME property_identifier TOK_COLON expression ';' + | TOK_ASSUME property_identifier TOK_COLON smv_property ';' { init($$, ID_verilog_smv_assume); stack_expr($$).operands().resize(2); to_binary_expr(stack_expr($$)).op0().swap(stack_expr($4)); to_binary_expr(stack_expr($$)).op1().make_nil(); @@ -1905,6 +1911,35 @@ smv_assertion_statement: } ; +smv_property_identifier_list: + TOK_NON_TYPE_IDENTIFIER + | smv_property_identifier_list ',' TOK_NON_TYPE_IDENTIFIER + ; + +smv_using: + TOK_USING smv_property_identifier_list TOK_PROVE smv_property_identifier_list ';' + { init($$, ID_verilog_smv_using); } + ; + +smv_assume: + TOK_ASSUME smv_property_identifier_list ';' + { init($$, ID_verilog_smv_assume); } + ; + +// We use smv_property_proper vs smv_property to avoid the reduce/reduce +// conflict that arises between '(' expression ')' and '(' smv_property ')'. +smv_property: + smv_property_proper + | expression + ; + +smv_property_proper: + TOK_EVENTUALLY smv_property + { init($$, ID_verilog_smv_eventually); mto($$, $2); } + | '(' smv_property_proper ')' + { $$ = $2; } + ; + assert_property_statement: TOK_ASSERT TOK_PROPERTY '(' property_expr ')' action_block { init($$, ID_verilog_assert_property); mto($$, $4); mto($$, $6); } diff --git a/src/verilog/scanner.l b/src/verilog/scanner.l index 72ec8a1fb..31fdf017b 100644 --- a/src/verilog/scanner.l +++ b/src/verilog/scanner.l @@ -82,8 +82,22 @@ static void preprocessor() else \ yyverilogerror(text " is a System Verilog operator"); \ } -#define VIS_VERILOG_KEYWORD(x) \ +#define VL2SMV_OR_SYSTEM_VERILOG_KEYWORD(x) \ { if(PARSER.mode==verilog_parsert::SYSTEM_VERILOG || \ + PARSER.mode==verilog_parsert::VL2SMV_VERILOG) \ + return x; \ + else \ + IDENTIFIER(yytext); \ + } +#define VL2SMV_VERILOG_KEYWORD(x) \ + { if(PARSER.mode==verilog_parsert::VL2SMV_VERILOG) \ + return x; \ + else \ + IDENTIFIER(yytext); \ + } +#define VIS_OR_VL2SMV_OR_SYSTEM_VERILOG_KEYWORD(x) \ + { if(PARSER.mode==verilog_parsert::SYSTEM_VERILOG || \ + PARSER.mode==verilog_parsert::VL2SMV_VERILOG || \ PARSER.mode==verilog_parsert::VIS_VERILOG) \ return x; \ else \ @@ -395,8 +409,8 @@ alias { SYSTEM_VERILOG_KEYWORD(TOK_ALIAS); } always_comb { SYSTEM_VERILOG_KEYWORD(TOK_ALWAYS_COMB); } always_ff { SYSTEM_VERILOG_KEYWORD(TOK_ALWAYS_FF); } always_latch { SYSTEM_VERILOG_KEYWORD(TOK_ALWAYS_LATCH); } -assert { VIS_VERILOG_KEYWORD(TOK_ASSERT); } -assume { VIS_VERILOG_KEYWORD(TOK_ASSUME); } +assert { VIS_OR_VL2SMV_OR_SYSTEM_VERILOG_KEYWORD(TOK_ASSERT); } +assume { VL2SMV_OR_SYSTEM_VERILOG_KEYWORD(TOK_ASSUME); } before { SYSTEM_VERILOG_KEYWORD(TOK_BEFORE); } bind { SYSTEM_VERILOG_KEYWORD(TOK_BIND); } bins { SYSTEM_VERILOG_KEYWORD(TOK_BINS); } @@ -425,7 +439,7 @@ endpackage { SYSTEM_VERILOG_KEYWORD(TOK_ENDPACKAGE); } endprogram { SYSTEM_VERILOG_KEYWORD(TOK_ENDPROGRAM); } endproperty { SYSTEM_VERILOG_KEYWORD(TOK_ENDPROPERTY); } endsequence { SYSTEM_VERILOG_KEYWORD(TOK_ENDSEQUENCE); } -enum { VIS_VERILOG_KEYWORD(TOK_ENUM); } +enum { VIS_OR_VL2SMV_OR_SYSTEM_VERILOG_KEYWORD(TOK_ENUM); } expect { SYSTEM_VERILOG_KEYWORD(TOK_EXPECT); } export { SYSTEM_VERILOG_KEYWORD(TOK_EXPORT); } extends { SYSTEM_VERILOG_KEYWORD(TOK_EXTENDS); } @@ -478,7 +492,7 @@ throughout { SYSTEM_VERILOG_KEYWORD(TOK_THROUGHOUT); } timeprecision { SYSTEM_VERILOG_KEYWORD(TOK_TIMEPRECISION); } timeunit { SYSTEM_VERILOG_KEYWORD(TOK_TIMEUNIT); } type { SYSTEM_VERILOG_KEYWORD(TOK_TYPE); } -typedef { VIS_VERILOG_KEYWORD(TOK_TYPEDEF); } +typedef { VIS_OR_VL2SMV_OR_SYSTEM_VERILOG_KEYWORD(TOK_TYPEDEF); } union { SYSTEM_VERILOG_KEYWORD(TOK_UNION); } unique { SYSTEM_VERILOG_KEYWORD(TOK_UNIQUE); } var { SYSTEM_VERILOG_KEYWORD(TOK_VAR); } @@ -494,7 +508,7 @@ within { SYSTEM_VERILOG_KEYWORD(TOK_WITHIN); } accept_on { SYSTEM_VERILOG_KEYWORD(TOK_ACCEPT_ON); } checker { SYSTEM_VERILOG_KEYWORD(TOK_CHECKER); } endchecker { SYSTEM_VERILOG_KEYWORD(TOK_ENDCHECKER); } -eventually { SYSTEM_VERILOG_KEYWORD(TOK_EVENTUALLY); } +eventually { VL2SMV_OR_SYSTEM_VERILOG_KEYWORD(TOK_EVENTUALLY); } global { SYSTEM_VERILOG_KEYWORD(TOK_GLOBAL); } implies { SYSTEM_VERILOG_KEYWORD(TOK_IMPLIES); } let { SYSTEM_VERILOG_KEYWORD(TOK_LET); } @@ -522,6 +536,11 @@ interconnect { SYSTEM_VERILOG_KEYWORD(TOK_INTERCONNECT); } nettype { SYSTEM_VERILOG_KEYWORD(TOK_NETTYPE); } soft { SYSTEM_VERILOG_KEYWORD(TOK_SOFT); } + /* VL2SMV Keywords */ + +using { VL2SMV_VERILOG_KEYWORD(TOK_USING); } +prove { VL2SMV_VERILOG_KEYWORD(TOK_PROVE); } + /* Preprocessor outputs */ \'line { continue; } diff --git a/src/verilog/verilog_elaborate.cpp b/src/verilog/verilog_elaborate.cpp index ed7b39184..070f9f342 100644 --- a/src/verilog/verilog_elaborate.cpp +++ b/src/verilog/verilog_elaborate.cpp @@ -683,6 +683,9 @@ void verilog_typecheckt::collect_symbols(const verilog_statementt &statement) else if(statement.id() == ID_procedural_continuous_assign) { } + else if(statement.id() == ID_wait) + { + } else DATA_INVARIANT(false, "unexpected statement: " + statement.id_string()); } @@ -760,6 +763,12 @@ void verilog_typecheckt::collect_symbols( else if(module_item.id() == ID_verilog_empty_item) { } + else if(module_item.id() == ID_verilog_smv_using) + { + } + else if(module_item.id() == ID_verilog_smv_assume) + { + } else DATA_INVARIANT(false, "unexpected module item: " + module_item.id_string()); } diff --git a/src/verilog/verilog_interfaces.cpp b/src/verilog/verilog_interfaces.cpp index 194e435c6..b4e2f3fe5 100644 --- a/src/verilog/verilog_interfaces.cpp +++ b/src/verilog/verilog_interfaces.cpp @@ -287,6 +287,12 @@ void verilog_typecheckt::interface_module_item( else if(module_item.id() == ID_verilog_empty_item) { } + else if(module_item.id() == ID_verilog_smv_using) + { + } + else if(module_item.id() == ID_verilog_smv_assume) + { + } else { DATA_INVARIANT(false, "unexpected module item: " + module_item.id_string()); diff --git a/src/verilog/verilog_language.cpp b/src/verilog/verilog_language.cpp index cfda1aa52..d50bc6ae2 100644 --- a/src/verilog/verilog_language.cpp +++ b/src/verilog/verilog_language.cpp @@ -35,6 +35,7 @@ void verilog_languaget::set_language_options( message_handlert &message_handler) { force_systemverilog = options.get_bool_option("force-systemverilog"); + vl2smv_extensions = options.get_bool_option("vl2smv-extensions"); } /*******************************************************************\ @@ -68,6 +69,8 @@ bool verilog_languaget::parse( if(has_suffix(path, ".sv") || force_systemverilog) verilog_parser.mode=verilog_parsert::SYSTEM_VERILOG; + else if(vl2smv_extensions) + verilog_parser.mode = verilog_parsert::VL2SMV_VERILOG; verilog_scanner_init(); diff --git a/src/verilog/verilog_language.h b/src/verilog/verilog_language.h index 0ec5aaa60..ccedd6f50 100644 --- a/src/verilog/verilog_language.h +++ b/src/verilog/verilog_language.h @@ -95,6 +95,7 @@ class verilog_languaget:public languaget protected: bool force_systemverilog = false; + bool vl2smv_extensions = false; verilog_parse_treet parse_tree; }; diff --git a/src/verilog/verilog_parser.h b/src/verilog/verilog_parser.h index 4373b1dfe..22925109e 100644 --- a/src/verilog/verilog_parser.h +++ b/src/verilog/verilog_parser.h @@ -29,8 +29,14 @@ class verilog_parsert:public parsert typedef enum { LANGUAGE, EXPRESSION, TYPE } grammart; grammart grammar; - - typedef enum { STRICT_VERILOG, VIS_VERILOG, SYSTEM_VERILOG } modet; + + typedef enum + { + STRICT_VERILOG, + VIS_VERILOG, + VL2SMV_VERILOG, + SYSTEM_VERILOG + } modet; modet mode; virtual bool parse() diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index ca1399973..6d6702f68 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -1474,6 +1474,9 @@ void verilog_typecheckt::convert_statement( convert_force(to_verilog_force(statement)); else if(statement.id() == ID_verilog_label_statement) convert_statement(to_verilog_label_statement(statement).statement()); + else if(statement.id() == ID_wait) + { + } else { throw errort().with_location(statement.source_location()) @@ -1575,6 +1578,12 @@ void verilog_typecheckt::convert_module_item( else if(module_item.id() == ID_verilog_empty_item) { } + else if(module_item.id() == ID_verilog_smv_using) + { + } + else if(module_item.id() == ID_verilog_smv_assume) + { + } else { throw errort().with_location(module_item.source_location())