Skip to content

Commit 4b0c862

Browse files
kroeningkroening
authored
Merge pull request #837 from diffblue/chandle
SystemVerilog: `chandle` data type
2 parents feb4677 + 9aa4bd3 commit 4b0c862

15 files changed

+168
-4
lines changed

‎CHANGELOG

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@
66
* Verilog: fix for nor/nand/xnor primitive gates
77
* SystemVerilog: $bitstoreal/$bitstoshortreal, $realtobits/$shortrealtobits
88
* SystemVerilog: $itor, $rtoi
9+
* SystemVerilog: chandle
910

1011
# EBMC 5.4
1112

‎regression/verilog/data-types/chandle1.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
chandle1.sv
3+
--bound 0
4+
^\[main\.p0\] always main\.some_handle == null: PROVED up to bound 0$
5+
^\[main\.p1\] always \$typename\(main\.some_handle\) == "chandle": PROVED up to bound 0$
6+
^EXIT=0$
7+
^SIGNAL=0$
8+
--

‎regression/verilog/data-types/chandle1.sv

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
module main;
2+
3+
// IEEE 1800-2017 6.14
4+
chandle some_handle = null;
5+
6+
p0: assert final (some_handle == null);
7+
p1: assert final ($typename(some_handle) == "chandle");
8+
9+
endmodule

‎src/hw_cbmc_irep_ids.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -104,7 +104,8 @@ IREP_ID_ONE(verilog_value_range)
104104
IREP_ID_ONE(verilog_void)
105105
IREP_ID_ONE(verilog_streaming_concatenation_left_to_right)
106106
IREP_ID_ONE(verilog_streaming_concatenation_right_to_left)
107-
IREP_ID_ONE(chandle)
107+
IREP_ID_ONE(verilog_chandle)
108+
IREP_ID_ONE(verilog_null)
108109
IREP_ID_ONE(event)
109110
IREP_ID_ONE(reg)
110111
IREP_ID_ONE(macromodule)

‎src/verilog/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ SRC = aval_bval_encoding.cpp \
2626
verilog_typecheck_base.cpp \
2727
verilog_typecheck_expr.cpp \
2828
verilog_typecheck_sva.cpp \
29+
verilog_types.cpp \
2930
verilog_y.tab.cpp \
3031
vtype.cpp
3132

‎src/verilog/expr2verilog.cpp

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1260,6 +1260,15 @@ expr2verilogt::resultt expr2verilogt::convert_constant(
12601260

12611261
dest += '"';
12621262
}
1263+
else if(type.id() == ID_verilog_chandle)
1264+
{
1265+
if(src.get_value() == ID_NULL)
1266+
{
1267+
dest = "null";
1268+
}
1269+
else
1270+
return convert_norep(src, precedence);
1271+
}
12631272
else
12641273
return convert_norep(src, precedence);
12651274

@@ -2030,6 +2039,8 @@ std::string expr2verilogt::convert(const typet &type)
20302039

20312040
return dest;
20322041
}
2042+
else if(type.id() == ID_verilog_chandle)
2043+
return "chandle";
20332044
else if(type.id() == ID_verilog_genvar)
20342045
return "genvar";
20352046
else if(type.id()==ID_integer)
@@ -2040,6 +2051,8 @@ std::string expr2verilogt::convert(const typet &type)
20402051
return "real";
20412052
else if(type.id()==ID_verilog_realtime)
20422053
return "realtime";
2054+
else if(type.id() == ID_verilog_null)
2055+
return "null";
20432056
else if(type.id() == ID_verilog_enum)
20442057
{
20452058
return "enum";

‎src/verilog/parser.y

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1477,7 +1477,7 @@ data_type:
14771477
| TOK_STRING
14781478
{ init($$, ID_string); }
14791479
| TOK_CHANDLE
1480-
{ init($$, ID_chandle); }
1480+
{ init($$, ID_verilog_chandle); }
14811481
| TOK_VIRTUAL interface_opt interface_identifier
14821482
{ init($$, "virtual_interface"); }
14831483
| /*scope_opt*/ type_identifier packed_dimension_brace
@@ -4039,7 +4039,7 @@ primary: primary_literal
40394039
| cast
40404040
| assignment_pattern_expression
40414041
| streaming_concatenation
4042-
| TOK_NULL { init($$, ID_NULL); }
4042+
| TOK_NULL { init($$, ID_verilog_null); }
40434043
| TOK_THIS { init($$, ID_this); }
40444044
;
40454045

‎src/verilog/verilog_elaborate_type.cpp

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -383,6 +383,10 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src)
383383
{
384384
return src;
385385
}
386+
else if(src.id() == ID_verilog_chandle)
387+
{
388+
return src;
389+
}
386390
else
387391
{
388392
throw errort().with_location(source_location)

‎src/verilog/verilog_lowering.cpp

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
1919
#include "convert_literals.h"
2020
#include "verilog_bits.h"
2121
#include "verilog_expr.h"
22+
#include "verilog_types.h"
2223

2324
/// Lowers
2425
/// * the three Verilog real types to floatbv;
@@ -42,6 +43,10 @@ typet verilog_lowering(typet type)
4243
{
4344
return lower_to_aval_bval(type);
4445
}
46+
else if(type.id() == ID_verilog_chandle)
47+
{
48+
return to_verilog_chandle_type(type).encoding();
49+
}
4550
else
4651
return type;
4752
}
@@ -347,9 +352,26 @@ exprt verilog_lowering(exprt expr)
347352
result.add_source_location() = expr.source_location();
348353
expr = std::move(result);
349354
}
355+
else if(expr.type().id() == ID_verilog_chandle)
356+
{
357+
// this is 'null'
358+
return to_verilog_chandle_type(expr.type()).null_expr();
359+
}
350360

351361
return expr;
352362
}
363+
else if(expr.id() == ID_symbol)
364+
{
365+
auto &symbol_expr = to_symbol_expr(expr);
366+
if(expr.type().id() == ID_verilog_chandle)
367+
{
368+
auto &chandle_type = to_verilog_chandle_type(expr.type());
369+
return symbol_exprt{
370+
symbol_expr.get_identifier(), chandle_type.encoding()};
371+
}
372+
else
373+
return expr;
374+
}
353375
else if(expr.id() == ID_concatenation)
354376
{
355377
if(

‎src/verilog/verilog_synthesis.cpp

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3346,7 +3346,12 @@ void verilog_synthesist::synth_assignments(
33463346
if(!symbol.is_state_var)
33473347
post_process_wire(symbol.name, new_value);
33483348

3349-
equal_exprt equality_expr{symbol_expr(symbol, curr_or_next), new_value};
3349+
auto lhs = symbol_expr(symbol, curr_or_next);
3350+
3351+
DATA_INVARIANT(
3352+
lhs.type() == new_value.type(), "synth_assignments type consistency");
3353+
3354+
equal_exprt equality_expr{std::move(lhs), new_value};
33503355

33513356
constraints.add_to_operands(std::move(equality_expr));
33523357
}

‎src/verilog/verilog_typecheck_expr.cpp

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -753,6 +753,10 @@ exprt verilog_typecheck_exprt::typename_string(const exprt &expr)
753753
{
754754
s = "shortreal";
755755
}
756+
else if(type.id() == ID_verilog_chandle)
757+
{
758+
s = "chandle";
759+
}
756760
else
757761
s = "?";
758762

@@ -1107,6 +1111,11 @@ exprt verilog_typecheck_exprt::convert_nullary_expr(nullary_exprt expr)
11071111
throw errort().with_location(expr.source_location())
11081112
<< "'this' outside of method";
11091113
}
1114+
else if(expr.id() == ID_verilog_null)
1115+
{
1116+
return constant_exprt{ID_NULL, typet{ID_verilog_null}}.with_source_location(
1117+
expr.source_location());
1118+
}
11101119
else
11111120
{
11121121
throw errort().with_location(expr.source_location())
@@ -2041,6 +2050,17 @@ void verilog_typecheck_exprt::implicit_typecast(
20412050
return;
20422051
}
20432052
}
2053+
else if(src_type.id() == ID_verilog_null)
2054+
{
2055+
if(dest_type.id() == ID_verilog_chandle)
2056+
{
2057+
if(expr.id() == ID_constant)
2058+
{
2059+
expr.type() = dest_type;
2060+
return;
2061+
}
2062+
}
2063+
}
20442064

20452065
throw errort().with_location(expr.source_location())
20462066
<< "failed to convert `" << to_string(src_type) << "' to `"
@@ -2293,6 +2313,12 @@ typet verilog_typecheck_exprt::max_type(
22932313
vtypet vt0=vtypet(t0);
22942314
vtypet vt1=vtypet(t1);
22952315

2316+
if(vt0.is_null() || vt1.is_chandle())
2317+
return t1;
2318+
2319+
if(vt0.is_chandle() || vt1.is_null())
2320+
return t0;
2321+
22962322
if(vt0.is_other() || vt1.is_other())
22972323
return static_cast<const typet &>(get_nil_irep());
22982324

‎src/verilog/verilog_types.cpp

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
/*******************************************************************\
2+
3+
Module: Verilog Types
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include "verilog_types.h"
10+
11+
#include <util/std_expr.h>
12+
13+
constant_exprt verilog_chandle_typet::null_expr() const
14+
{
15+
return encoding().all_zeros_expr();
16+
}

‎src/verilog/verilog_types.h

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -544,4 +544,41 @@ inline verilog_union_typet &to_verilog_union_type(typet &type)
544544
return static_cast<verilog_union_typet &>(type);
545545
}
546546

547+
/// a pointer type
548+
class verilog_chandle_typet : public typet
549+
{
550+
public:
551+
inline verilog_chandle_typet() : typet(ID_verilog_chandle)
552+
{
553+
}
554+
555+
bv_typet encoding() const
556+
{
557+
return bv_typet{32};
558+
}
559+
560+
constant_exprt null_expr() const;
561+
};
562+
563+
/// \brief Cast a typet to a \ref verilog_chandle_typet
564+
///
565+
/// This is an unchecked conversion. \a type must be known to be \ref
566+
/// verilog_chandle_typet. Will fail with a precondition violation if type
567+
/// doesn't match.
568+
///
569+
/// \param type: Source type.
570+
/// \return Object of type \ref verilog_chandle_typet
571+
inline const verilog_chandle_typet &to_verilog_chandle_type(const typet &type)
572+
{
573+
PRECONDITION(type.id() == ID_verilog_chandle);
574+
return static_cast<const verilog_chandle_typet &>(type);
575+
}
576+
577+
/// \copydoc to_chandle_type(const typet &)
578+
inline verilog_chandle_typet &to_verilog_chandle_type(typet &type)
579+
{
580+
PRECONDITION(type.id() == ID_verilog_chandle);
581+
return static_cast<verilog_chandle_typet &>(type);
582+
}
583+
547584
#endif

‎src/verilog/vtype.cpp

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -73,6 +73,11 @@ vtypet::vtypet(const typet &type)
7373
vtype = VERILOG_REAL;
7474
width = 32;
7575
}
76+
else if(type.id() == ID_verilog_chandle)
77+
{
78+
vtype = CHANDLE;
79+
width = 32;
80+
}
7681
else
7782
{
7883
width=0;
@@ -117,6 +122,12 @@ std::ostream &operator << (std::ostream &out, const vtypet &vtype)
117122
case vtypet::VERILOG_REAL:
118123
return out << "real";
119124

125+
case vtypet::CHANDLE:
126+
return out << "chandle";
127+
128+
case vtypet::NULL_TYPE:
129+
return out << "null";
130+
120131
case vtypet::UNKNOWN:
121132
case vtypet::OTHER:
122133
default:

‎src/verilog/vtype.h

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,14 @@ class vtypet
3131
{
3232
return vtype == VERILOG_REAL;
3333
}
34+
bool is_chandle() const
35+
{
36+
return vtype == CHANDLE;
37+
}
38+
bool is_null() const
39+
{
40+
return vtype == NULL_TYPE;
41+
}
3442
inline bool is_other() const { return vtype==OTHER; }
3543

3644
protected:
@@ -44,6 +52,8 @@ class vtypet
4452
VERILOG_SIGNED,
4553
VERILOG_UNSIGNED,
4654
VERILOG_REAL,
55+
CHANDLE,
56+
NULL_TYPE,
4757
OTHER
4858
} _vtypet;
4959
_vtypet vtype;

0 commit comments

Comments
 (0)