Skip to content

Commit 07b13f0

Browse files
tautschnigtautschnig
authored
Merge pull request #574 from diffblue/bv-to-struct-conversion
Verilog: implement bit-vector to struct conversion
2 parents 459b5f8 + 0cef873 commit 07b13f0

File tree

4 files changed

+176
-17
lines changed

4 files changed

+176
-17
lines changed

‎regression/verilog/structs/structs1.desc‎

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,10 @@
1-
KNOWNBUG
1+
CORE
22
structs1.sv
33
--bound 0
4+
^\[main\.property\.p0\] always 9 == 9: PROVED up to bound 0$
5+
^\[main\.property\.p1\] always main\.s\.field1 == 1: PROVED up to bound 0$
6+
^\[main\.property\.p2\] always main\.s\.field2 == 0: PROVED up to bound 0$
7+
^\[main\.property\.p3\] always main\.s\.field3 == 115: PROVED up to bound 0$
48
^EXIT=0$
59
^SIGNAL=0$
610
--
7-
--
8-
cast bitvector to struct missing

‎regression/verilog/structs/structs1.sv‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,12 +7,12 @@ module main;
77
} s;
88

99
// bit-vectors can be converted without cast to packed structs
10-
initial s = 8'b1011111;
10+
initial s = 'b1_0_1110011;
1111

1212
// Expected to pass.
1313
p0: assert property ($bits(s) == 9);
1414
p1: assert property (s.field1 == 1);
1515
p2: assert property (s.field2 == 0);
16-
p3: assert property (s.field3 == 'b111111);
16+
p3: assert property (s.field3 == 'b1110011);
1717

1818
endmodule

‎src/verilog/verilog_synthesis.cpp‎

Lines changed: 164 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,136 @@ Author: Daniel Kroening, kroening@kroening.com
3030

3131
/*******************************************************************\
3232
33+
Function: verilog_synthesist::extract
34+
35+
Inputs:
36+
37+
Outputs:
38+
39+
Purpose:
40+
41+
\*******************************************************************/
42+
43+
exprt verilog_synthesist::extract(
44+
const exprt &src,
45+
const mp_integer &offset,
46+
const typet &dest_type)
47+
{
48+
auto src_width = to_bitvector_type(src.type()).get_width();
49+
auto dest_width = get_width(dest_type);
50+
51+
// first add padding, if src is too small
52+
exprt padded_src;
53+
auto padding_width = dest_width + offset - src_width;
54+
55+
if(padding_width > 0)
56+
{
57+
auto padded_width_int =
58+
numeric_cast_v<std::size_t>(src_width + padding_width);
59+
padded_src = concatenation_exprt{
60+
{unsignedbv_typet{numeric_cast_v<std::size_t>(padding_width)}.zero_expr(),
61+
src},
62+
bv_typet{padded_width_int}};
63+
}
64+
else // large enough
65+
padded_src = src;
66+
67+
// now extract
68+
if(dest_type.id() == ID_bool)
69+
{
70+
return extractbit_exprt{padded_src, from_integer(offset, integer_typet{})};
71+
}
72+
else
73+
{
74+
return extractbits_exprt{
75+
padded_src, from_integer(offset, integer_typet{}), dest_type};
76+
}
77+
}
78+
79+
/*******************************************************************\
80+
81+
Function: verilog_synthesist::from_bitvector
82+
83+
Inputs:
84+
85+
Outputs:
86+
87+
Purpose:
88+
89+
\*******************************************************************/
90+
91+
exprt verilog_synthesist::from_bitvector(
92+
const exprt &src,
93+
const mp_integer &offset,
94+
const typet &dest)
95+
{
96+
if(dest.id() == ID_struct)
97+
{
98+
const auto &struct_type = to_struct_type(dest);
99+
exprt::operandst field_values;
100+
field_values.reserve(struct_type.components().size());
101+
102+
// start from the top; the first field is the most significant
103+
mp_integer component_offset = get_width(dest);
104+
105+
for(auto &component : struct_type.components())
106+
{
107+
auto width = get_width(component.type());
108+
component_offset -= width;
109+
// rec. call
110+
field_values.push_back(
111+
from_bitvector(src, offset + component_offset, component.type()));
112+
}
113+
114+
return struct_exprt{std::move(field_values), struct_type};
115+
}
116+
else
117+
{
118+
return extract(src, offset, dest);
119+
}
120+
}
121+
122+
/*******************************************************************\
123+
124+
Function: verilog_synthesist::to_bitvector
125+
126+
Inputs:
127+
128+
Outputs:
129+
130+
Purpose:
131+
132+
\*******************************************************************/
133+
134+
exprt verilog_synthesist::to_bitvector(const exprt &src)
135+
{
136+
const auto &src_type = src.type();
137+
138+
if(src_type.id() == ID_struct)
139+
{
140+
const auto &struct_type = to_struct_type(src_type);
141+
exprt::operandst field_values;
142+
field_values.reserve(struct_type.components().size());
143+
144+
// the first struct member is the most significant
145+
for(auto &component : struct_type.components())
146+
{
147+
auto member = member_exprt{src, component};
148+
auto field_value = to_bitvector(member); // rec. call
149+
field_values.push_back(std::move(field_value));
150+
}
151+
152+
auto width_int = numeric_cast_v<std::size_t>(get_width(src));
153+
return concatenation_exprt{std::move(field_values), bv_typet{width_int}};
154+
}
155+
else
156+
{
157+
return src;
158+
}
159+
}
160+
161+
/*******************************************************************\
162+
33163
Function: verilog_synthesist::synth_expr
34164
35165
Inputs:
@@ -100,23 +230,45 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state)
100230
}
101231
else if(expr.id()==ID_typecast)
102232
{
103-
auto &typecast_expr = to_typecast_expr(expr);
104-
typecast_expr.op() = synth_expr(typecast_expr.op(), symbol_state);
233+
{
234+
auto &op = to_typecast_expr(expr).op();
235+
op = synth_expr(op, symbol_state);
105236

106-
// we perform some form of simplification for these
107-
if(typecast_expr.op().is_constant())
108-
simplify(expr, ns);
237+
// we perform some form of simplification for these
238+
if(op.is_constant())
239+
simplify(expr, ns);
240+
}
109241

110-
if(
111-
expr.type().id() == ID_verilog_unsignedbv ||
112-
expr.type().id() == ID_verilog_signedbv)
242+
if(expr.id() == ID_typecast)
113243
{
114-
auto aval_bval_type = lower_to_aval_bval(expr.type());
244+
auto &typecast_expr = to_typecast_expr(expr);
245+
typecast_expr.op() = synth_expr(typecast_expr.op(), symbol_state);
115246

116-
if(is_aval_bval(typecast_expr.op().type()))
247+
const auto &src_type = typecast_expr.op().type();
248+
const auto &dest_type = typecast_expr.type();
249+
250+
if(
251+
dest_type.id() == ID_verilog_unsignedbv ||
252+
dest_type.id() == ID_verilog_signedbv)
253+
{
254+
auto aval_bval_type = lower_to_aval_bval(dest_type);
255+
256+
if(is_aval_bval(src_type))
257+
{
258+
// separately convert aval and bval
259+
return aval_bval_conversion(typecast_expr.op(), aval_bval_type);
260+
}
261+
}
262+
else if(dest_type.id() == ID_struct)
117263
{
118-
// separately convert aval and bval
119-
return aval_bval_conversion(typecast_expr.op(), aval_bval_type);
264+
return from_bitvector(typecast_expr.op(), 0, dest_type);
265+
}
266+
else
267+
{
268+
if(src_type.id() == ID_struct)
269+
{
270+
return extract(to_bitvector(typecast_expr.op()), 0, dest_type);
271+
}
120272
}
121273
}
122274

‎src/verilog/verilog_synthesis_class.h‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -71,6 +71,11 @@ class verilog_synthesist:
7171
protected:
7272
const optionst &options;
7373

74+
static exprt extract(const exprt &, const mp_integer &offset, const typet &);
75+
static exprt
76+
from_bitvector(const exprt &, const mp_integer &offset, const typet &);
77+
static exprt to_bitvector(const exprt &);
78+
7479
// For $ND(...)
7580
std::size_t nondet_count = 0;
7681

0 commit comments

Comments
 (0)