Skip to content

Commit fb5ff54

Browse files
kroeningkroening
committed
Verilog: extract verilog_bits(...) function
This extracts the static get_width(...) method into a separate function, renaming to verilog_bits(...).
1 parent fd14e56 commit fb5ff54

File tree

8 files changed

+129
-78
lines changed

8 files changed

+129
-78
lines changed

‎lib/cbmc‎

‎src/verilog/Makefile‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
SRC = aval_bval_encoding.cpp \
22
expr2verilog.cpp \
33
sva_expr.cpp \
4+
verilog_bits.cpp \
45
verilog_elaborate.cpp \
56
verilog_elaborate_type.cpp \
67
verilog_expr.cpp \

‎src/verilog/verilog_bits.cpp‎

Lines changed: 89 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,89 @@
1+
/*******************************************************************\
2+
3+
Module: Verilog Type Width
4+
5+
Author: Daniel Kroening, dkr@amazon.com
6+
7+
\*******************************************************************/
8+
9+
#include "verilog_bits.h"
10+
11+
#include <util/arith_tools.h>
12+
13+
#include <ebmc/ebmc_error.h>
14+
15+
#include "verilog_types.h"
16+
17+
std::optional<mp_integer> verilog_bits_opt(const typet &type)
18+
{
19+
if(type.id() == ID_bool)
20+
return 1;
21+
22+
if(
23+
type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
24+
type.id() == ID_verilog_signedbv || type.id() == ID_verilog_unsignedbv)
25+
return type.get_int(ID_width);
26+
27+
if(type.id() == ID_array)
28+
{
29+
auto &array_type = to_array_type(type);
30+
auto element_width_opt = verilog_bits_opt(array_type.element_type());
31+
auto size_opt = numeric_cast<mp_integer>(array_type.size());
32+
33+
if(element_width_opt.has_value() && size_opt.has_value())
34+
{
35+
return element_width_opt.value() * size_opt.value();
36+
}
37+
else
38+
return {};
39+
}
40+
41+
if(type.id() == ID_struct)
42+
{
43+
// add them up
44+
mp_integer sum = 0;
45+
for(auto &component : to_struct_type(type).components())
46+
{
47+
auto component_width = verilog_bits_opt(component.type());
48+
if(!component_width.has_value())
49+
return {};
50+
sum += *component_width;
51+
}
52+
return sum;
53+
}
54+
55+
if(type.id() == ID_union)
56+
{
57+
// find the biggest
58+
mp_integer max = 0;
59+
for(auto &component : to_verilog_union_type(type).components())
60+
max = std::max(max, verilog_bits(component.type()));
61+
return max;
62+
}
63+
64+
if(type.id() == ID_verilog_shortint)
65+
return 16;
66+
else if(type.id() == ID_verilog_int)
67+
return 32;
68+
else if(type.id() == ID_verilog_longint)
69+
return 64;
70+
else if(type.id() == ID_verilog_integer)
71+
return 32;
72+
else if(type.id() == ID_verilog_time)
73+
return 64;
74+
75+
return {};
76+
}
77+
78+
mp_integer verilog_bits(const typet &type)
79+
{
80+
auto bits_opt = verilog_bits_opt(type);
81+
82+
if(bits_opt.has_value())
83+
return std::move(bits_opt.value());
84+
else
85+
{
86+
throw ebmc_errort() << "type `" << type.id()
87+
<< "' has unknown number of bits";
88+
}
89+
}

‎src/verilog/verilog_bits.h‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
/*******************************************************************\
2+
3+
Module: Verilog Type Width
4+
5+
Author: Daniel Kroening, dkr@amazon.com
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_VERILOG_BITS_H
10+
#define CPROVER_VERILOG_BITS_H
11+
12+
#include <util/expr.h>
13+
#include <util/mp_arith.h>
14+
15+
/// $bits -- throws an exception if no width
16+
mp_integer verilog_bits(const typet &);
17+
18+
/// $bits -- throws an exception if no width
19+
inline mp_integer verilog_bits(const exprt &expr)
20+
{
21+
return verilog_bits(expr.type());
22+
}
23+
24+
/// $bits
25+
std::optional<mp_integer> verilog_bits_opt(const typet &);
26+
27+
#endif

‎src/verilog/verilog_typecheck_base.cpp‎

Lines changed: 5 additions & 72 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
1414
#include <util/std_types.h>
1515

1616
#include "expr2verilog.h"
17+
#include "verilog_bits.h"
1718
#include "verilog_types.h"
1819

1920
/*******************************************************************\
@@ -159,74 +160,6 @@ mp_integer verilog_typecheck_baset::array_offset(const array_typet &type)
159160

160161
/*******************************************************************\
161162
162-
Function: verilog_typecheck_baset::get_width_opt
163-
164-
Inputs:
165-
166-
Outputs:
167-
168-
Purpose:
169-
170-
\*******************************************************************/
171-
172-
std::optional<mp_integer>
173-
verilog_typecheck_baset::get_width_opt(const typet &type)
174-
{
175-
if(type.id()==ID_bool)
176-
return 1;
177-
178-
if(type.id()==ID_unsignedbv || type.id()==ID_signedbv ||
179-
type.id()==ID_verilog_signedbv || type.id()==ID_verilog_unsignedbv)
180-
return type.get_int(ID_width);
181-
182-
if(type.id()==ID_array)
183-
{
184-
auto element_width = get_width_opt(to_array_type(type).element_type());
185-
if(element_width.has_value())
186-
return array_size(to_array_type(type)) * element_width.value();
187-
else
188-
return {};
189-
}
190-
191-
if(type.id() == ID_struct)
192-
{
193-
// add them up
194-
mp_integer sum = 0;
195-
for(auto &component : to_struct_type(type).components())
196-
{
197-
auto component_width = get_width_opt(component.type());
198-
if(!component_width.has_value())
199-
return {};
200-
sum += *component_width;
201-
}
202-
return sum;
203-
}
204-
205-
if(type.id() == ID_union)
206-
{
207-
// find the biggest
208-
mp_integer max = 0;
209-
for(auto &component : to_verilog_union_type(type).components())
210-
max = std::max(max, get_width(component.type()));
211-
return max;
212-
}
213-
214-
if(type.id() == ID_verilog_shortint)
215-
return 16;
216-
else if(type.id() == ID_verilog_int)
217-
return 32;
218-
else if(type.id() == ID_verilog_longint)
219-
return 64;
220-
else if(type.id() == ID_verilog_integer)
221-
return 32;
222-
else if(type.id() == ID_verilog_time)
223-
return 64;
224-
225-
return {};
226-
}
227-
228-
/*******************************************************************\
229-
230163
Function: verilog_typecheck_baset::get_width
231164
232165
Inputs:
@@ -239,13 +172,13 @@ Function: verilog_typecheck_baset::get_width
239172

240173
mp_integer verilog_typecheck_baset::get_width(const typet &type)
241174
{
242-
auto width_opt = get_width_opt(type);
175+
auto bits_opt = verilog_bits_opt(type);
243176

244-
if(width_opt.has_value())
245-
return std::move(width_opt.value());
177+
if(bits_opt.has_value())
178+
return std::move(bits_opt.value());
246179
else
247180
throw errort().with_location(type.source_location())
248-
<< "type `" << type.id() << "' has unknown width";
181+
<< "type `" << type.id() << "' has unknown number of bits";
249182
}
250183

251184
/*******************************************************************\

‎src/verilog/verilog_typecheck_base.h‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,6 @@ class verilog_typecheck_baset:public typecheckt
5151
}
5252

5353
static mp_integer get_width(const typet &);
54-
static std::optional<mp_integer> get_width_opt(const typet &);
5554
static mp_integer array_size(const array_typet &);
5655
static mp_integer array_offset(const array_typet &);
5756
static typet index_type(const array_typet &);

‎src/verilog/verilog_typecheck_expr.cpp‎

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com
2121
#include <util/string2int.h>
2222

2323
#include "expr2verilog.h"
24+
#include "verilog_bits.h"
2425
#include "verilog_expr.h"
2526
#include "verilog_types.h"
2627
#include "vtype.h"
@@ -447,15 +448,16 @@ Function: verilog_typecheck_exprt::bits
447448

448449
exprt verilog_typecheck_exprt::bits(const exprt &expr)
449450
{
450-
auto width_opt = get_width_opt(expr.type());
451+
auto bits_opt = verilog_bits_opt(expr.type());
451452

452-
if(!width_opt.has_value())
453+
if(!bits_opt.has_value())
453454
{
454455
throw errort().with_location(expr.source_location())
455456
<< "failed to determine number of bits of " << to_string(expr);
456457
}
457458

458-
return from_integer(width_opt.value(), integer_typet());
459+
return from_integer(bits_opt.value(), integer_typet())
460+
.with_source_location(expr.source_location());
459461
}
460462

461463
/*******************************************************************\

‎src/verilog/verilog_types.h‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
99
#ifndef CPROVER_VERILOG_TYPES_H
1010
#define CPROVER_VERILOG_TYPES_H
1111

12-
#include <util/std_types.h>
12+
#include <util/bitvector_types.h>
1313

1414
/// Used during elaboration only,
1515
/// to signal that a symbol is yet to be elaborated.

0 commit comments

Comments
 (0)