Skip to content

Commit 80e2eee

Browse files
kroeningkroening
authored
Merge pull request #585 from diffblue/cond_for_comment
Verilog: generate property description prior to expression synthesis
2 parents c0ef1df + 08654ea commit 80e2eee

16 files changed

+208
-33
lines changed

‎regression/verilog/SVA/immediate1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
immediate1.sv
33
--bound 20
4-
^\[main\.assert\.1\] always \(main\.x == 11 \|-> main\.x & 1\): PROVED up to bound 20$
4+
^\[main\.assert\.1\] always main\.x & 1: PROVED up to bound 20$
55
^EXIT=0$
66
^SIGNAL=0$
77
--

‎regression/verilog/SVA/immediate2.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE broken-smt-backend
22
immediate2.sv
33
--bound 0
4-
^\[main\.assert\.1\] assume always \(main\.index >= 10 |-> 0\): ASSUMED$
4+
^\[main\.assume\.1\] assume always 0: ASSUMED$
55
^\[main\.assert\.2\] always main\.index < 10: PROVED up to bound 0$
66
^\[main\.assert\.3\] always 0: REFUTED$
77
^EXIT=10$

‎regression/verilog/SVA/initial2.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
initial2.sv
33
--module main --bound 1
4-
^\[main\.assert\.1\] 1 == 1: PROVED up to bound 1
4+
^\[main\.assert\.1\] main\.counter == 1: PROVED up to bound 1
55
^\[main\.assert\.2\] main\.counter == 2: PROVED up to bound 1
66
^EXIT=0$
77
^SIGNAL=0$

‎regression/verilog/SVA/named_property1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
named_property1.sv
33
--bound 0
4-
^\[main\.assert\.1\] always main\.x == 10: PROVED up to bound 0$
4+
^\[main\.assert\.1\] always main\.x_is_ten: PROVED up to bound 0$
55
^EXIT=0$
66
^SIGNAL=0$
77
--

‎regression/verilog/SVA/unbounded1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
unbounded1.sv
33
--module main --bound 1
4-
^\[main\.assert\.1\] always \(main\.a ##\[0:\$\] main.b\): REFUTED$
4+
^\[main\.assert\.1\] always \(main\.a ##\[0:main\.upper\] main.b\): REFUTED$
55
^EXIT=10$
66
^SIGNAL=0$
77
--

‎regression/verilog/enums/enum4.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,5 +3,5 @@ enum4.sv
33
--bound 0
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main\.p1\] always main.A == main.A: PROVED up to bound 0$
6+
^\[main\.p1\] always main\.A == 1: PROVED up to bound 0$
77
--

‎regression/verilog/enums/enum_base_type1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,5 +3,5 @@ enum_base_type1.sv
33
--bound 0
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[.*\] always 8 == 8: PROVED up to bound 0$
6+
^\[.*\] always \$bits\(main\.A\) == 8: PROVED up to bound 0$
77
--

‎regression/verilog/enums/enum_base_type2.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,5 +3,5 @@ enum_base_type2.sv
33
--bound 0
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[.*\] always 8 == 8: PROVED up to bound 0$
6+
^\[.*\] always \$bits\(main\.A\) == main\.p: PROVED up to bound 0$
77
--

‎regression/verilog/expressions/concatenation2.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ concatenation2.v
33
--bound 0
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main\.property\.pA\] always -1 == -1: PROVED up to bound 0$
7-
^\[main\.property\.pB\] always 15 == 15: PROVED up to bound 0$
6+
^\[main\.property\.pA\] always main\.A == -1: PROVED up to bound 0$
7+
^\[main\.property\.pB\] always main\.B == 15: PROVED up to bound 0$
88
--
99
^warning: ignoring

‎regression/verilog/expressions/static_cast1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ static_cast1.sv
33
--module main --bound 0
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main\.p0\] always 255 == 255: PROVED up to bound 0$
6+
^\[main\.p0\] always 'hFFFF == 255: PROVED up to bound 0$
77
--
88
^warning: ignoring

‎regression/verilog/modules/type_parameters1.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
22
type_parameters1.sv
33
--bound 0
4-
^\[main\.p1\] always 1 == 1: PROVED up to bound 0$
5-
^\[main\.p2\] always 32 == 32: PROVED up to bound 0$
4+
^\[main\.p1\] always \$bits\(main\.T1\) == 1: PROVED up to bound 0$
5+
^\[main\.p2\] always \$bits\(main\.T2\) == 32: PROVED up to bound 0$
66
^EXIT=0$
77
^SIGNAL=0$
88
--

‎regression/verilog/structs/structs1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
structs1.sv
33
--bound 0
4-
^\[main\.p0\] always 9 == 9: PROVED up to bound 0$
4+
^\[main\.p0\] always \$bits\(main\.s\) == 9: PROVED up to bound 0$
55
^\[main\.p1\] always main\.s\.field1 == 1: PROVED up to bound 0$
66
^\[main\.p2\] always main\.s\.field2 == 0: PROVED up to bound 0$
77
^\[main\.p3\] always main\.s\.field3 == 115: PROVED up to bound 0$

‎regression/verilog/system-functions/array_functions1.desc

Lines changed: 15 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1,21 +1,21 @@
11
CORE
22
array_functions1.sv
33
--module main --bound 0
4-
^\[main\.pP0\] always 32 == 32 && 1 == 1: PROVED up to bound 0$
5-
^\[main\.pP1\] always 0 == 0 && 31 == 31: PROVED up to bound 0$
6-
^\[main\.pP2\] always 1 == 1 && 32 == 32: PROVED up to bound 0$
7-
^\[main\.pP3\] always 0 == 0 && 31 == 31: PROVED up to bound 0$
8-
^\[main\.pP4\] always 1 == 1: PROVED up to bound 0$
9-
^\[main\.pP5\] always -1 == -1: PROVED up to bound 0$
10-
^\[main\.pU0\] always 32 == 32 && 1 == 1: PROVED up to bound 0$
11-
^\[main\.pU1\] always 0 == 0 && 31 == 31: PROVED up to bound 0$
12-
^\[main\.pU2\] always 31 == 31 && 0 == 0: PROVED up to bound 0$
13-
^\[main\.pU3\] always 1 == 1 && 32 == 32: PROVED up to bound 0$
14-
^\[main\.pU4\] always 0 == 0 && 31 == 31: PROVED up to bound 0$
15-
^\[main\.pU5\] always 0 == 0 && 31 == 31: PROVED up to bound 0$
16-
^\[main\.pU6\] always 1 == 1: PROVED up to bound 0$
17-
^\[main\.pU7\] always -1 == -1: PROVED up to bound 0$
18-
^\[main\.pU8\] always 1 == 1: PROVED up to bound 0$
4+
^\[main\.pP0\] always \$left\(main\.packed1\) == 32 && \$right\(main\.packed1\) == 1: PROVED up to bound 0$
5+
^\[main\.pP1\] always \$left\(main\.packed2\) == 0 && \$right\(main\.packed2\) == 31: PROVED up to bound 0$
6+
^\[main\.pP2\] always \$low\(main\.packed1\) == 1 && \$high\(main\.packed1\) == 32: PROVED up to bound 0$
7+
^\[main\.pP3\] always \$low\(main\.packed2\) == 0 && \$high\(main\.packed2\) == 31: PROVED up to bound 0$
8+
^\[main\.pP4\] always \$increment\(main\.packed1\) == 1: PROVED up to bound 0$
9+
^\[main\.pP5\] always \$increment\(main\.packed2\) == -1: PROVED up to bound 0$
10+
^\[main\.pU0\] always \$left\(main\.unpacked1\) == 32 && \$right\(main\.unpacked1\) == 1: PROVED up to bound 0$
11+
^\[main\.pU1\] always \$left\(main\.unpacked2\) == 0 && \$right\(main\.unpacked2\) == 31: PROVED up to bound 0$
12+
^\[main\.pU2\] always \$left\(main\.unpacked3\) == 31 && \$right\(main\.unpacked3\) == 0: PROVED up to bound 0$
13+
^\[main\.pU3\] always \$low\(main\.unpacked1\) == 1 && \$high\(main\.unpacked1\) == 32: PROVED up to bound 0$
14+
^\[main\.pU4\] always \$low\(main\.unpacked2\) == 0 && \$high\(main\.unpacked2\) == 31: PROVED up to bound 0$
15+
^\[main\.pU5\] always \$low\(main\.unpacked3\) == 0 && \$high\(main\.unpacked3\) == 31: PROVED up to bound 0$
16+
^\[main\.pU6\] always \$increment\(main\.unpacked1\) == 1: PROVED up to bound 0$
17+
^\[main\.pU7\] always \$increment\(main\.unpacked2\) == -1: PROVED up to bound 0$
18+
^\[main\.pU8\] always \$increment\(main\.unpacked3\) == 1: PROVED up to bound 0$
1919
^EXIT=0$
2020
^SIGNAL=0$
2121
--

‎src/verilog/expr2verilog.cpp

Lines changed: 113 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -647,6 +647,81 @@ std::string expr2verilogt::convert_index(
647647

648648
/*******************************************************************\
649649
650+
Function: expr2verilogt::convert_non_indexed_part_select
651+
652+
Inputs:
653+
654+
Outputs:
655+
656+
Purpose:
657+
658+
\*******************************************************************/
659+
660+
std::string expr2verilogt::convert_non_indexed_part_select(
661+
const verilog_non_indexed_part_select_exprt &src,
662+
verilog_precedencet precedence)
663+
{
664+
verilog_precedencet p;
665+
std::string op = convert(src.src(), p);
666+
667+
std::string dest;
668+
if(precedence > p)
669+
dest += '(';
670+
dest += op;
671+
if(precedence > p)
672+
dest += ')';
673+
674+
dest += '[';
675+
dest += convert(src.msb());
676+
dest += ':';
677+
dest += convert(src.lsb());
678+
dest += ']';
679+
680+
return dest;
681+
}
682+
683+
/*******************************************************************\
684+
685+
Function: expr2verilogt::convert_indexed_part_select
686+
687+
Inputs:
688+
689+
Outputs:
690+
691+
Purpose:
692+
693+
\*******************************************************************/
694+
695+
std::string expr2verilogt::convert_indexed_part_select(
696+
const verilog_indexed_part_select_plus_or_minus_exprt &src,
697+
verilog_precedencet precedence)
698+
{
699+
verilog_precedencet p;
700+
std::string op = convert(src.src(), p);
701+
702+
std::string dest;
703+
if(precedence > p)
704+
dest += '(';
705+
dest += op;
706+
if(precedence > p)
707+
dest += ')';
708+
709+
dest += '[';
710+
dest += convert(src.index());
711+
712+
if(src.id() == ID_verilog_indexed_part_select_plus)
713+
dest += '+';
714+
else
715+
dest += '-';
716+
717+
dest += convert(src.width());
718+
dest += ']';
719+
720+
return dest;
721+
}
722+
723+
/*******************************************************************\
724+
650725
Function: expr2verilogt::convert_extractbit
651726
652727
Inputs:
@@ -842,6 +917,26 @@ std::string expr2verilogt::convert_next_symbol(
842917

843918
/*******************************************************************\
844919
920+
Function: expr2verilogt::convert_hierarchical_identifier
921+
922+
Inputs:
923+
924+
Outputs:
925+
926+
Purpose:
927+
928+
\*******************************************************************/
929+
930+
std::string expr2verilogt::convert_hierarchical_identifier(
931+
const hierarchical_identifier_exprt &src,
932+
verilog_precedencet &precedence)
933+
{
934+
precedence = verilog_precedencet::MAX;
935+
return convert(src.module()) + '.' + src.item().get_string(ID_base_name);
936+
}
937+
938+
/*******************************************************************\
939+
845940
Function: expr2verilogt::convert_constant
846941
847942
Inputs:
@@ -1048,6 +1143,20 @@ expr2verilogt::convert(const exprt &src, verilog_precedencet &precedence)
10481143
return convert_index(
10491144
to_index_expr(src), precedence = verilog_precedencet::MEMBER);
10501145

1146+
else if(
1147+
src.id() == ID_verilog_indexed_part_select_plus ||
1148+
src.id() == ID_verilog_indexed_part_select_minus)
1149+
{
1150+
return convert_indexed_part_select(
1151+
to_verilog_indexed_part_select_plus_or_minus_expr(src),
1152+
precedence = verilog_precedencet::MEMBER);
1153+
}
1154+
1155+
else if(src.id() == ID_verilog_non_indexed_part_select)
1156+
return convert_non_indexed_part_select(
1157+
to_verilog_non_indexed_part_select_expr(src),
1158+
precedence = verilog_precedencet::MEMBER);
1159+
10511160
else if(src.id()==ID_extractbit)
10521161
return convert_extractbit(
10531162
to_extractbit_expr(src), precedence = verilog_precedencet::MEMBER);
@@ -1195,6 +1304,10 @@ expr2verilogt::convert(const exprt &src, verilog_precedencet &precedence)
11951304
else if(src.id()==ID_next_symbol)
11961305
return convert_next_symbol(src, precedence);
11971306

1307+
else if(src.id() == ID_hierarchical_identifier)
1308+
return convert_hierarchical_identifier(
1309+
to_hierarchical_identifier_expr(src), precedence);
1310+
11981311
else if(src.id()==ID_constant)
11991312
return convert_constant(to_constant_expr(src), precedence);
12001313

‎src/verilog/expr2verilog_class.h

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -86,6 +86,10 @@ class expr2verilogt
8686

8787
virtual std::string convert_symbol(const exprt &src, verilog_precedencet &);
8888

89+
std::string convert_hierarchical_identifier(
90+
const class hierarchical_identifier_exprt &,
91+
verilog_precedencet &precedence);
92+
8993
virtual std::string
9094
convert_nondet_symbol(const exprt &src, verilog_precedencet &);
9195

@@ -135,6 +139,14 @@ class expr2verilogt
135139

136140
virtual std::string convert_function_call(const class function_call_exprt &);
137141

142+
std::string convert_non_indexed_part_select(
143+
const class verilog_non_indexed_part_select_exprt &,
144+
verilog_precedencet precedence);
145+
146+
std::string convert_indexed_part_select(
147+
const class verilog_indexed_part_select_plus_or_minus_exprt &,
148+
verilog_precedencet precedence);
149+
138150
protected:
139151
const namespacet &ns;
140152
};

‎src/verilog/verilog_synthesis.cpp

Lines changed: 54 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2271,6 +2271,39 @@ void verilog_synthesist::synth_assert_assume_cover(
22712271
// but this is to be checked.
22722272
// Arguments to procedural concurrent assertions are complex
22732273
// (1800-2017 16.14.6.1)
2274+
{
2275+
exprt cond_for_comment = statement.condition();
2276+
2277+
// Are we in an initial or always block?
2278+
if(construct != constructt::INITIAL)
2279+
{
2280+
// one of the 'always' variants -- assertions and assumptions have an implicit 'always'
2281+
if(
2282+
statement.id() != ID_verilog_cover_property &&
2283+
statement.id() != ID_verilog_immediate_cover)
2284+
{
2285+
if(cond_for_comment.id() != ID_sva_always)
2286+
cond_for_comment = sva_always_exprt(cond_for_comment);
2287+
}
2288+
}
2289+
2290+
// mark 'assume' and 'cover' properties as such
2291+
if(
2292+
statement.id() == ID_verilog_assume_property ||
2293+
statement.id() == ID_verilog_immediate_assume ||
2294+
statement.id() == ID_verilog_smv_assume)
2295+
{
2296+
cond_for_comment = sva_assume_exprt(cond_for_comment);
2297+
}
2298+
else if(statement.id() == ID_verilog_cover_property)
2299+
{
2300+
// 'cover' properties are existential
2301+
cond_for_comment = sva_cover_exprt(cond_for_comment);
2302+
}
2303+
2304+
symbol.location.set_comment(to_string(cond_for_comment));
2305+
}
2306+
22742307
exprt cond;
22752308

22762309
// Are we in an initial or always block?
@@ -2323,8 +2356,6 @@ void verilog_synthesist::synth_assert_assume_cover(
23232356
cond = sva_cover_exprt(cond);
23242357
}
23252358

2326-
symbol.location.set_comment(to_string(cond));
2327-
23282359
symbol.value = std::move(cond);
23292360
}
23302361

@@ -2347,6 +2378,27 @@ void verilog_synthesist::synth_assert_assume_cover(
23472378
const irep_idt &identifier = module_item.identifier();
23482379
symbolt &symbol=symbol_table_lookup(identifier);
23492380

2381+
{
2382+
exprt cond_for_comment = module_item.condition();
2383+
2384+
if(
2385+
module_item.id() == ID_verilog_assert_property ||
2386+
module_item.id() == ID_verilog_assume_property)
2387+
{
2388+
// Concurrent assertions and assumptions come with an implicit 'always'
2389+
// (1800-2017 Sec 16.12.11).
2390+
if(cond_for_comment.id() != ID_sva_always)
2391+
cond_for_comment = sva_always_exprt{cond_for_comment};
2392+
}
2393+
else if(module_item.id() == ID_verilog_cover_property)
2394+
{
2395+
// 'cover' requirements are existential.
2396+
cond_for_comment = sva_cover_exprt{cond_for_comment};
2397+
}
2398+
2399+
symbol.location.set_comment(to_string(cond_for_comment));
2400+
}
2401+
23502402
construct=constructt::OTHER;
23512403

23522404
auto cond = synth_expr(module_item.condition(), symbol_statet::SYMBOL);
@@ -2376,8 +2428,6 @@ void verilog_synthesist::synth_assert_assume_cover(
23762428
else
23772429
PRECONDITION(false);
23782430

2379-
symbol.location.set_comment(to_string(cond));
2380-
23812431
symbol.value = std::move(cond);
23822432
}
23832433

0 commit comments

Comments
 (0)