Skip to content

Commit c9fe05c

Browse files
kroeningkroening
authored
Merge pull request #561 from diffblue/aval_bval
Verilog: aval/bval lowering of 4-valued logic
2 parents 6d90287 + 29403fd commit c9fe05c

File tree

7 files changed

+246
-64
lines changed

7 files changed

+246
-64
lines changed

‎lib/cbmc‎

‎regression/verilog/case/case1.v‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,20 +1,20 @@
11
module main(input clk, x, y);
22

33
reg [1:0] cnt1;
4-
reg z;
4+
reg result;
55

66
initial cnt1=0;
7-
initial z=0;
7+
initial result=0;
88

99
always @(posedge clk) cnt1=cnt1+1;
1010

1111
always @(posedge clk)
1212
casex (cnt1)
1313
2'b00:;
1414
2'b01:;
15-
2'b1?: z=1;
15+
2'b1?: result=1;
1616
endcase
1717

18-
always assert p1: z==0;
18+
always assert p1: result==0;
1919

2020
endmodule

‎src/hw_cbmc_irep_ids.h‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -148,6 +148,7 @@ IREP_ID_ONE(uwire)
148148
IREP_ID_ONE(wand)
149149
IREP_ID_ONE(automatic)
150150
IREP_ID_TWO(C_verilog_type, #verilog_type)
151+
IREP_ID_TWO(C_verilog_aval_bval, #verilog_aval_bval)
151152
IREP_ID_ONE(verilog_enum)
152153
IREP_ID_ONE(verilog_packed_array)
153154
IREP_ID_ONE(verilog_type_reference)

‎src/verilog/Makefile‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
1-
SRC = expr2verilog.cpp \
1+
SRC = aval_bval_encoding.cpp \
2+
expr2verilog.cpp \
23
sva_expr.cpp \
34
verilog_elaborate.cpp \
45
verilog_expr.cpp \

‎src/verilog/aval_bval_encoding.cpp‎

Lines changed: 154 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,154 @@
1+
/*******************************************************************\
2+
3+
Module: aval/bval encoding
4+
5+
Author: Daniel Kroening, dkr@amazon.com
6+
7+
\*******************************************************************/
8+
9+
#include "aval_bval_encoding.h"
10+
11+
#include <util/arith_tools.h>
12+
#include <util/bitvector_expr.h>
13+
#include <util/bitvector_types.h>
14+
#include <util/mathematical_types.h>
15+
#include <util/std_expr.h>
16+
17+
bv_typet aval_bval_type(std::size_t width, irep_idt source_type)
18+
{
19+
PRECONDITION(!source_type.empty());
20+
auto result = bv_typet{width * 2};
21+
result.set(ID_C_verilog_aval_bval, source_type);
22+
return result;
23+
}
24+
25+
bv_typet lower_to_aval_bval(const typet &src)
26+
{
27+
PRECONDITION(
28+
src.id() == ID_verilog_unsignedbv || src.id() == ID_verilog_signedbv);
29+
return aval_bval_type(to_bitvector_type(src).get_width(), src.id());
30+
}
31+
32+
bool is_aval_bval(const typet &type)
33+
{
34+
return type.id() == ID_bv && !type.get(ID_C_verilog_aval_bval).empty();
35+
}
36+
37+
std::size_t aval_bval_width(const typet &type)
38+
{
39+
PRECONDITION(is_aval_bval(type));
40+
return to_bv_type(type).get_width() / 2;
41+
}
42+
43+
typet aval_bval_underlying(const typet &src)
44+
{
45+
auto id = src.get(ID_C_verilog_aval_bval);
46+
if(id == ID_verilog_unsignedbv)
47+
return unsignedbv_typet{aval_bval_width(src)};
48+
else if(id == ID_verilog_signedbv)
49+
return signedbv_typet{aval_bval_width(src)};
50+
else
51+
PRECONDITION(false);
52+
}
53+
54+
constant_exprt lower_to_aval_bval(const constant_exprt &src)
55+
{
56+
PRECONDITION(
57+
src.type().id() == ID_verilog_signedbv ||
58+
src.type().id() == ID_verilog_unsignedbv);
59+
60+
auto new_type = lower_to_aval_bval(src.type());
61+
auto width = aval_bval_width(new_type);
62+
auto &value = id2string(src.get_value());
63+
64+
auto bv_f = [width, value](const std::size_t dest_index) {
65+
bool bval = dest_index >= width;
66+
std::size_t src_bit_nr = bval ? dest_index - width : dest_index;
67+
68+
// bval aval | 4-state Verilog value
69+
// ----------|----------------------
70+
// 0 0 | 0
71+
// 0 1 | 1
72+
// 1 0 | X
73+
// 1 1 | Z
74+
75+
switch(value[value.size() - 1 - src_bit_nr])
76+
{
77+
case '0':
78+
return bval ? 0 : 0;
79+
case '1':
80+
return bval ? 0 : 1;
81+
case 'x':
82+
return bval ? 1 : 0;
83+
case '?':
84+
case 'z':
85+
return bval ? 1 : 1;
86+
default:
87+
INVARIANT(false, "unexpected Verilog vector bit");
88+
}
89+
};
90+
91+
return constant_exprt{make_bvrep(width * 2, bv_f), new_type};
92+
}
93+
94+
exprt aval(const exprt &src)
95+
{
96+
PRECONDITION(is_aval_bval(src.type()));
97+
auto width = aval_bval_width(src.type());
98+
return extractbits_exprt{
99+
src, from_integer(0, integer_typet()), bv_typet{width}};
100+
}
101+
102+
exprt bval(const exprt &src)
103+
{
104+
PRECONDITION(is_aval_bval(src.type()));
105+
auto width = aval_bval_width(src.type());
106+
return extractbits_exprt{
107+
src, from_integer(width, integer_typet()), bv_typet{width}};
108+
}
109+
110+
static exprt adjust_size(const exprt &src, std::size_t dest_width)
111+
{
112+
auto src_width = to_bv_type(src.type()).get_width();
113+
if(dest_width > src_width)
114+
{
115+
auto zeros = from_integer(0, bv_typet{dest_width - src_width});
116+
return concatenation_exprt{{zeros, src}, bv_typet{dest_width}};
117+
}
118+
else if(dest_width < src_width)
119+
{
120+
return extractbits_exprt{
121+
src, from_integer(0, integer_typet{}), bv_typet{dest_width}};
122+
}
123+
else
124+
return src;
125+
}
126+
127+
static exprt
128+
combine_aval_bval(const exprt &aval, const exprt &bval, const typet &dest)
129+
{
130+
PRECONDITION(aval.type().id() == ID_bv);
131+
PRECONDITION(bval.type().id() == ID_bv);
132+
return concatenation_exprt{{bval, aval}, dest};
133+
}
134+
135+
exprt aval_bval_conversion(const exprt &src, const typet &dest)
136+
{
137+
PRECONDITION(is_aval_bval(src.type()));
138+
PRECONDITION(is_aval_bval(dest));
139+
140+
auto src_width = aval_bval_width(src.type());
141+
auto dest_width = aval_bval_width(dest);
142+
143+
if(src_width == dest_width)
144+
{
145+
// same size
146+
return typecast_exprt{src, dest};
147+
}
148+
else
149+
{
150+
auto new_aval = adjust_size(aval(src), dest_width);
151+
auto new_bval = adjust_size(bval(src), dest_width);
152+
return combine_aval_bval(new_aval, new_bval, dest);
153+
}
154+
}

‎src/verilog/aval_bval_encoding.h‎

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
/*******************************************************************\
2+
3+
Module: aval/bval encoding
4+
5+
Author: Daniel Kroening, dkr@amazon.com
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_VERILOG_AVAL_BVAL_H
10+
#define CPROVER_VERILOG_AVAL_BVAL_H
11+
12+
#include <util/bitvector_types.h>
13+
#include <util/std_expr.h>
14+
15+
// bit-concoding for four-valued types
16+
//
17+
// bval aval | 4-state Verilog value
18+
// ----------|----------------------
19+
// 0 0 | 0
20+
// 0 1 | 1
21+
// 1 0 | X
22+
// 1 1 | Z
23+
24+
bool is_aval_bval(const typet &);
25+
std::size_t aval_bval_width(const typet &);
26+
typet aval_bval_underlying(const typet &);
27+
28+
bv_typet lower_to_aval_bval(const typet &);
29+
constant_exprt lower_to_aval_bval(const constant_exprt &);
30+
31+
// extract a/b vectors
32+
exprt aval(const exprt &);
33+
exprt bval(const exprt &);
34+
35+
exprt aval_bval_conversion(const exprt &, const typet &);
36+
37+
#endif

‎src/verilog/verilog_synthesis.cpp‎

Lines changed: 47 additions & 58 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
1818
#include <util/simplify_expr.h>
1919
#include <util/std_expr.h>
2020

21+
#include "aval_bval_encoding.h"
2122
#include "expr2verilog.h"
2223
#include "sva_expr.h"
2324
#include "verilog_expr.h"
@@ -74,6 +75,18 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state)
7475
UNREACHABLE;
7576
}
7677
}
78+
else if(expr.id() == ID_constant)
79+
{
80+
// encode into aval/bval
81+
if(
82+
expr.type().id() == ID_verilog_unsignedbv ||
83+
expr.type().id() == ID_verilog_signedbv)
84+
{
85+
return lower_to_aval_bval(to_constant_expr(expr));
86+
}
87+
88+
return expr;
89+
}
7790
else if(expr.id()==ID_function_call)
7891
{
7992
return expand_function_call(to_function_call_expr(expr));
@@ -94,6 +107,19 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state)
94107
if(typecast_expr.op().is_constant())
95108
simplify(expr, ns);
96109

110+
if(
111+
expr.type().id() == ID_verilog_unsignedbv ||
112+
expr.type().id() == ID_verilog_signedbv)
113+
{
114+
auto aval_bval_type = lower_to_aval_bval(expr.type());
115+
116+
if(is_aval_bval(typecast_expr.op().type()))
117+
{
118+
// separately convert aval and bval
119+
return aval_bval_conversion(typecast_expr.op(), aval_bval_type);
120+
}
121+
}
122+
97123
return expr;
98124
}
99125
else if(expr.id() == ID_verilog_non_indexed_part_select)
@@ -2260,71 +2286,34 @@ exprt verilog_synthesist::case_comparison(
22602286
const exprt &case_operand,
22612287
const exprt &pattern)
22622288
{
2263-
// we need to take case of ?, x, z in the pattern
2289+
// the pattern has the max type, not the case operand
22642290
const typet &pattern_type=pattern.type();
2265-
2266-
if(pattern_type.id()==ID_verilog_signedbv ||
2267-
pattern_type.id()==ID_verilog_unsignedbv)
2268-
{
2269-
// try to simplify the pattern
2270-
exprt tmp=pattern;
2271-
2272-
simplify(tmp, ns);
2273-
2274-
if(tmp.id()!=ID_constant)
2275-
{
2276-
warning().source_location=pattern.source_location();
2277-
warning() << "unexpected case pattern: " << to_string(tmp) << eom;
2278-
}
2279-
else
2280-
{
2281-
exprt new_case_operand=case_operand;
2282-
2283-
// the pattern has the max type
2284-
unsignedbv_typet new_type(pattern.type().get_int(ID_width));
2285-
new_case_operand = typecast_exprt{new_case_operand, new_type};
2286-
2287-
// we are using masking!
2288-
2289-
std::string new_pattern_value=
2290-
id2string(to_constant_expr(tmp).get_value());
2291-
2292-
// ?zx -> 0
2293-
for(unsigned i=0; i<new_pattern_value.size(); i++)
2294-
if(new_pattern_value[i]=='?' ||
2295-
new_pattern_value[i]=='z' ||
2296-
new_pattern_value[i]=='x')
2297-
new_pattern_value[i]='0';
2298-
2299-
auto new_pattern =
2300-
from_integer(string2integer(new_pattern_value, 2), new_type);
2301-
2302-
std::string new_mask_value=
2303-
id2string(to_constant_expr(tmp).get_value());
23042291

2305-
// ?zx -> 0, 0 -> 1
2306-
for(unsigned i=0; i<new_mask_value.size(); i++)
2307-
if(new_mask_value[i]=='?' ||
2308-
new_mask_value[i]=='z' ||
2309-
new_mask_value[i]=='x')
2310-
new_mask_value[i]='0';
2311-
else
2312-
new_mask_value[i]='1';
2313-
2314-
auto new_mask = from_integer(string2integer(new_mask_value, 2), new_type);
2292+
// we need to take case of ?, x, z in the pattern
2293+
if(is_aval_bval(pattern_type))
2294+
{
2295+
// We are using masking based on the pattern.
2296+
// The aval is the comparison value, and the
2297+
// negation of bval is the mask.
2298+
auto pattern_aval = ::aval(pattern);
2299+
auto pattern_bval = ::bval(pattern);
2300+
auto mask_expr = bitnot_exprt{pattern_bval};
23152301

2316-
exprt bitand_expr = bitand_exprt{new_case_operand, new_mask};
2302+
auto case_operand_casted = typecast_exprt{
2303+
typecast_exprt::conditional_cast(
2304+
case_operand, aval_bval_underlying(pattern_type)),
2305+
mask_expr.type()};
23172306

2318-
return equal_exprt{bitand_expr, new_pattern};
2319-
}
2307+
return equal_exprt{
2308+
bitand_exprt{case_operand_casted, mask_expr},
2309+
bitand_exprt{pattern_aval, mask_expr}};
23202310
}
23212311

2322-
if(pattern.type()==case_operand.type())
2323-
return equal_exprt(case_operand, pattern);
2312+
// 2-valued comparison
2313+
exprt case_operand_casted =
2314+
typecast_exprt::conditional_cast(case_operand, pattern_type);
23242315

2325-
// the pattern has the max type
2326-
exprt tmp_case_operand=typecast_exprt(case_operand, pattern.type());
2327-
return equal_exprt(tmp_case_operand, pattern);
2316+
return equal_exprt(case_operand_casted, pattern);
23282317
}
23292318

23302319
/*******************************************************************\

0 commit comments

Comments
 (0)