Skip to content

Commit 149da38

Browse files
kroeningkroening
committed
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.
1 parent 40abc2a commit 149da38

File tree

12 files changed

+110
-11
lines changed

12 files changed

+110
-11
lines changed

‎regression/verilog/vl2smv-extensions/traffic-1.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
traffic/1.v
3+
--vl2smv-extensions
4+
^file .* line 50: assignment in 'always' context without event guard$
5+
^EXIT=2$
6+
^SIGNAL=0$
7+
--

‎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)(systemverilog)",
49+
"I:(preprocess)(systemverilog)(vl2smv-extensions)",
5050
argc,
5151
argv,
5252
std::string("EBMC ") + EBMC_VERSION),

‎src/ebmc/transition_system.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -110,6 +110,7 @@ int preprocess(const cmdlinet &cmdline, message_handlert &message_handler)
110110

111111
optionst options;
112112
options.set_option("force-systemverilog", cmdline.isset("systemverilog"));
113+
options.set_option("vl2smv-extensions", cmdline.isset("vl2smv-extensions"));
113114

114115
language->set_language_options(options, message_handler);
115116

@@ -156,6 +157,7 @@ static bool parse(
156157

157158
optionst options;
158159
options.set_option("force-systemverilog", cmdline.isset("systemverilog"));
160+
options.set_option("vl2smv-extensions", cmdline.isset("vl2smv-extensions"));
159161

160162
language.set_language_options(options, message_handler);
161163

‎src/hw_cbmc_irep_ids.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -68,6 +68,8 @@ IREP_ID_ONE(deassign)
6868
IREP_ID_ONE(continuous_assign)
6969
IREP_ID_ONE(procedural_continuous_assign)
7070
IREP_ID_ONE(wait)
71+
IREP_ID_ONE(verilog_smv_eventually)
72+
IREP_ID_ONE(verilog_smv_using)
7173
IREP_ID_ONE(verilog_assert_property)
7274
IREP_ID_ONE(verilog_assume_property)
7375
IREP_ID_ONE(verilog_cover_property)

‎src/verilog/parser.y

Lines changed: 37 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -534,6 +534,10 @@ int yyverilogerror(const char *error)
534534
%token TOK_SYSIDENT // system task or function enable
535535
%token TOK_SCANNER_ERROR
536536

537+
/* VL2SMV */
538+
%token TOK_USING "using"
539+
%token TOK_PROVE "prove"
540+
537541
// Precedence of System Verilog Assertions Operators,
538542
// following System Verilog 1800-2017 Table 16-3.
539543
// Bison expects these in order of increasing precedence,
@@ -855,6 +859,8 @@ module_or_generate_item:
855859
| attribute_instance_brace module_instantiation { $$=$2; }
856860
| attribute_instance_brace concurrent_assertion_item { $$=$2; }
857861
| attribute_instance_brace assertion_item_declaration { $$=$2; }
862+
| attribute_instance_brace smv_using { $$ = $2; }
863+
| attribute_instance_brace smv_assume { $$ = $2; }
858864
| attribute_instance_brace module_common_item { $$=$2; }
859865
;
860866

@@ -1910,20 +1916,49 @@ concurrent_assertion_statement:
19101916

19111917
/* This one mimicks functionality in Cadence SMV */
19121918
smv_assertion_statement:
1913-
TOK_ASSERT property_identifier TOK_COLON expression ';'
1919+
TOK_ASSERT property_identifier TOK_COLON smv_property ';'
19141920
{ init($$, ID_verilog_smv_assert); stack_expr($$).operands().resize(2);
19151921
to_binary_expr(stack_expr($$)).op0().swap(stack_expr($4));
19161922
to_binary_expr(stack_expr($$)).op1().make_nil();
19171923
stack_expr($$).set(ID_identifier, stack_expr($2).id());
19181924
}
1919-
| TOK_ASSUME property_identifier TOK_COLON expression ';'
1925+
| TOK_ASSUME property_identifier TOK_COLON smv_property ';'
19201926
{ init($$, ID_verilog_smv_assume); stack_expr($$).operands().resize(2);
19211927
to_binary_expr(stack_expr($$)).op0().swap(stack_expr($4));
19221928
to_binary_expr(stack_expr($$)).op1().make_nil();
19231929
stack_expr($$).set(ID_identifier, stack_expr($2).id());
19241930
}
19251931
;
19261932

1933+
smv_property_identifier_list:
1934+
TOK_NON_TYPE_IDENTIFIER
1935+
| smv_property_identifier_list ',' TOK_NON_TYPE_IDENTIFIER
1936+
;
1937+
1938+
smv_using:
1939+
TOK_USING smv_property_identifier_list TOK_PROVE smv_property_identifier_list ';'
1940+
{ init($$, ID_verilog_smv_using); }
1941+
;
1942+
1943+
smv_assume:
1944+
TOK_ASSUME smv_property_identifier_list ';'
1945+
{ init($$, ID_verilog_smv_assume); }
1946+
;
1947+
1948+
// We use smv_property_proper vs smv_property to avoid the reduce/reduce
1949+
// conflict that arises between '(' expression ')' and '(' smv_property ')'.
1950+
smv_property:
1951+
smv_property_proper
1952+
| expression
1953+
;
1954+
1955+
smv_property_proper:
1956+
TOK_EVENTUALLY smv_property
1957+
{ init($$, ID_verilog_smv_eventually); mto($$, $2); }
1958+
| '(' smv_property_proper ')'
1959+
{ $$ = $2; }
1960+
;
1961+
19271962
assert_property_statement:
19281963
TOK_ASSERT TOK_PROPERTY '(' property_expr ')' action_block
19291964
{ init($$, ID_verilog_assert_property); mto($$, $4); mto($$, $6); }

‎src/verilog/scanner.l

Lines changed: 25 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -82,8 +82,22 @@ static void preprocessor()
8282
else \
8383
yyverilogerror(text " is a System Verilog operator"); \
8484
}
85-
#define VIS_VERILOG_KEYWORD(x) \
85+
#define VL2SMV_OR_SYSTEM_VERILOG_KEYWORD(x) \
8686
{ if(PARSER.mode==verilog_parsert::SYSTEM_VERILOG || \
87+
PARSER.mode==verilog_parsert::VL2SMV_VERILOG) \
88+
return x; \
89+
else \
90+
IDENTIFIER(yytext); \
91+
}
92+
#define VL2SMV_VERILOG_KEYWORD(x) \
93+
{ if(PARSER.mode==verilog_parsert::VL2SMV_VERILOG) \
94+
return x; \
95+
else \
96+
IDENTIFIER(yytext); \
97+
}
98+
#define VIS_OR_VL2SMV_OR_SYSTEM_VERILOG_KEYWORD(x) \
99+
{ if(PARSER.mode==verilog_parsert::SYSTEM_VERILOG || \
100+
PARSER.mode==verilog_parsert::VL2SMV_VERILOG || \
87101
PARSER.mode==verilog_parsert::VIS_VERILOG) \
88102
return x; \
89103
else \
@@ -395,8 +409,8 @@ alias { SYSTEM_VERILOG_KEYWORD(TOK_ALIAS); }
395409
always_comb { SYSTEM_VERILOG_KEYWORD(TOK_ALWAYS_COMB); }
396410
always_ff { SYSTEM_VERILOG_KEYWORD(TOK_ALWAYS_FF); }
397411
always_latch { SYSTEM_VERILOG_KEYWORD(TOK_ALWAYS_LATCH); }
398-
assert { VIS_VERILOG_KEYWORD(TOK_ASSERT); }
399-
assume { VIS_VERILOG_KEYWORD(TOK_ASSUME); }
412+
assert { VIS_OR_VL2SMV_OR_SYSTEM_VERILOG_KEYWORD(TOK_ASSERT); }
413+
assume { VL2SMV_OR_SYSTEM_VERILOG_KEYWORD(TOK_ASSUME); }
400414
before { SYSTEM_VERILOG_KEYWORD(TOK_BEFORE); }
401415
bind { SYSTEM_VERILOG_KEYWORD(TOK_BIND); }
402416
bins { SYSTEM_VERILOG_KEYWORD(TOK_BINS); }
@@ -425,7 +439,7 @@ endpackage { SYSTEM_VERILOG_KEYWORD(TOK_ENDPACKAGE); }
425439
endprogram { SYSTEM_VERILOG_KEYWORD(TOK_ENDPROGRAM); }
426440
endproperty { SYSTEM_VERILOG_KEYWORD(TOK_ENDPROPERTY); }
427441
endsequence { SYSTEM_VERILOG_KEYWORD(TOK_ENDSEQUENCE); }
428-
enum { VIS_VERILOG_KEYWORD(TOK_ENUM); }
442+
enum { VIS_OR_VL2SMV_OR_SYSTEM_VERILOG_KEYWORD(TOK_ENUM); }
429443
expect { SYSTEM_VERILOG_KEYWORD(TOK_EXPECT); }
430444
export { SYSTEM_VERILOG_KEYWORD(TOK_EXPORT); }
431445
extends { SYSTEM_VERILOG_KEYWORD(TOK_EXTENDS); }
@@ -478,7 +492,7 @@ throughout { SYSTEM_VERILOG_KEYWORD(TOK_THROUGHOUT); }
478492
timeprecision { SYSTEM_VERILOG_KEYWORD(TOK_TIMEPRECISION); }
479493
timeunit { SYSTEM_VERILOG_KEYWORD(TOK_TIMEUNIT); }
480494
type { SYSTEM_VERILOG_KEYWORD(TOK_TYPE); }
481-
typedef { VIS_VERILOG_KEYWORD(TOK_TYPEDEF); }
495+
typedef { VIS_OR_VL2SMV_OR_SYSTEM_VERILOG_KEYWORD(TOK_TYPEDEF); }
482496
union { SYSTEM_VERILOG_KEYWORD(TOK_UNION); }
483497
unique { SYSTEM_VERILOG_KEYWORD(TOK_UNIQUE); }
484498
var { SYSTEM_VERILOG_KEYWORD(TOK_VAR); }
@@ -494,7 +508,7 @@ within { SYSTEM_VERILOG_KEYWORD(TOK_WITHIN); }
494508
accept_on { SYSTEM_VERILOG_KEYWORD(TOK_ACCEPT_ON); }
495509
checker { SYSTEM_VERILOG_KEYWORD(TOK_CHECKER); }
496510
endchecker { SYSTEM_VERILOG_KEYWORD(TOK_ENDCHECKER); }
497-
eventually { SYSTEM_VERILOG_KEYWORD(TOK_EVENTUALLY); }
511+
eventually { VL2SMV_OR_SYSTEM_VERILOG_KEYWORD(TOK_EVENTUALLY); }
498512
global { SYSTEM_VERILOG_KEYWORD(TOK_GLOBAL); }
499513
implies { SYSTEM_VERILOG_KEYWORD(TOK_IMPLIES); }
500514
let { SYSTEM_VERILOG_KEYWORD(TOK_LET); }
@@ -522,6 +536,11 @@ interconnect { SYSTEM_VERILOG_KEYWORD(TOK_INTERCONNECT); }
522536
nettype { SYSTEM_VERILOG_KEYWORD(TOK_NETTYPE); }
523537
soft { SYSTEM_VERILOG_KEYWORD(TOK_SOFT); }
524538

539+
/* VL2SMV Keywords */
540+
541+
using { VL2SMV_VERILOG_KEYWORD(TOK_USING); }
542+
prove { VL2SMV_VERILOG_KEYWORD(TOK_PROVE); }
543+
525544
/* Preprocessor outputs */
526545

527546
\'line { continue; }

‎src/verilog/verilog_elaborate.cpp

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -683,6 +683,9 @@ void verilog_typecheckt::collect_symbols(const verilog_statementt &statement)
683683
else if(statement.id() == ID_procedural_continuous_assign)
684684
{
685685
}
686+
else if(statement.id() == ID_wait)
687+
{
688+
}
686689
else
687690
DATA_INVARIANT(false, "unexpected statement: " + statement.id_string());
688691
}
@@ -760,6 +763,12 @@ void verilog_typecheckt::collect_symbols(
760763
else if(module_item.id() == ID_verilog_empty_item)
761764
{
762765
}
766+
else if(module_item.id() == ID_verilog_smv_using)
767+
{
768+
}
769+
else if(module_item.id() == ID_verilog_smv_assume)
770+
{
771+
}
763772
else
764773
DATA_INVARIANT(false, "unexpected module item: " + module_item.id_string());
765774
}

‎src/verilog/verilog_interfaces.cpp

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -287,6 +287,12 @@ void verilog_typecheckt::interface_module_item(
287287
else if(module_item.id() == ID_verilog_empty_item)
288288
{
289289
}
290+
else if(module_item.id() == ID_verilog_smv_using)
291+
{
292+
}
293+
else if(module_item.id() == ID_verilog_smv_assume)
294+
{
295+
}
290296
else
291297
{
292298
DATA_INVARIANT(false, "unexpected module item: " + module_item.id_string());

‎src/verilog/verilog_language.cpp

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,7 @@ void verilog_languaget::set_language_options(
3535
message_handlert &message_handler)
3636
{
3737
force_systemverilog = options.get_bool_option("force-systemverilog");
38+
vl2smv_extensions = options.get_bool_option("vl2smv-extensions");
3839
}
3940

4041
/*******************************************************************\
@@ -68,6 +69,8 @@ bool verilog_languaget::parse(
6869

6970
if(has_suffix(path, ".sv") || force_systemverilog)
7071
verilog_parser.mode=verilog_parsert::SYSTEM_VERILOG;
72+
else if(vl2smv_extensions)
73+
verilog_parser.mode = verilog_parsert::VL2SMV_VERILOG;
7174

7275
verilog_scanner_init();
7376

‎src/verilog/verilog_language.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -95,6 +95,7 @@ class verilog_languaget:public languaget
9595

9696
protected:
9797
bool force_systemverilog = false;
98+
bool vl2smv_extensions = false;
9899
verilog_parse_treet parse_tree;
99100
};
100101

0 commit comments

Comments
 (0)