Skip to content

Commit f274e11

Browse files
authored
Merge pull request #927 from diffblue/bitwise_not1
aval/bval for bitwise not
2 parents cbad677 + e467b98 commit f274e11

File tree

5 files changed

+51
-0
lines changed

5 files changed

+51
-0
lines changed
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
bitwise_not1.sv
3+
--bound 0
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
module main;
2+
3+
assert final (~0 === 'hffff_ffff);
4+
assert final (~1 === 'hffff_fffe);
5+
assert final (~(-('sd1)) === 0);
6+
assert final (~3'b101 === 3'b010);
7+
assert final (~3'bxxx === 3'bxxx);
8+
assert final (~3'bzzz === 3'bxxx);
9+
assert final (~3'b10x === 3'b01x);
10+
assert final (~3'b10z === 3'b01x);
11+
12+
endmodule

src/verilog/aval_bval_encoding.cpp

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -180,6 +180,7 @@ combine_aval_bval(const exprt &aval, const exprt &bval, const typet &dest)
180180
{
181181
PRECONDITION(aval.type().id() == ID_bv);
182182
PRECONDITION(bval.type().id() == ID_bv);
183+
PRECONDITION(dest.id() == ID_bv);
183184
return concatenation_exprt{{bval, aval}, dest};
184185
}
185186

@@ -336,6 +337,24 @@ exprt aval_bval(const not_exprt &expr)
336337
return if_exprt{has_xz, x, aval_bval_conversion(not_expr, x.type())};
337338
}
338339

340+
exprt aval_bval(const bitnot_exprt &expr)
341+
{
342+
auto &type = expr.type();
343+
PRECONDITION(is_four_valued(type));
344+
PRECONDITION(is_aval_bval(expr.op()));
345+
346+
// x/z is done bit-wise.
347+
// ~z is x.
348+
auto op_aval = aval(expr.op());
349+
auto op_bval = bval(expr.op());
350+
351+
exprt aval = bitor_exprt{
352+
bitand_exprt{bitnot_exprt{op_bval}, op_bval}, // x/z case
353+
bitand_exprt{bitnot_exprt{op_aval}, bitnot_exprt{op_bval}}}; // 0/1 case
354+
355+
return combine_aval_bval(aval, op_bval, lower_to_aval_bval(expr.type()));
356+
}
357+
339358
exprt aval_bval(const power_exprt &expr)
340359
{
341360
PRECONDITION(is_four_valued(expr.type()));

src/verilog/aval_bval_encoding.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
99
#ifndef CPROVER_VERILOG_AVAL_BVAL_H
1010
#define CPROVER_VERILOG_AVAL_BVAL_H
1111

12+
#include <util/bitvector_expr.h>
1213
#include <util/bitvector_types.h>
1314
#include <util/mathematical_expr.h>
1415

@@ -46,6 +47,8 @@ exprt aval_bval(const verilog_logical_inequality_exprt &);
4647

4748
/// lowering for !
4849
exprt aval_bval(const not_exprt &);
50+
/// lowering for ~
51+
exprt aval_bval(const bitnot_exprt &);
4952
/// lowering for ==?
5053
exprt aval_bval(const verilog_wildcard_equality_exprt &);
5154
/// lowering for !=?

src/verilog/verilog_lowering.cpp

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -503,6 +503,16 @@ exprt verilog_lowering(exprt expr)
503503
else
504504
return expr; // leave as is
505505
}
506+
else if(expr.id() == ID_bitnot)
507+
{
508+
auto &bitnot_expr = to_bitnot_expr(expr);
509+
510+
// encode into aval/bval
511+
if(is_four_valued(expr.type()))
512+
return aval_bval(bitnot_expr);
513+
else
514+
return expr; // leave as is
515+
}
506516
else if(expr.id() == ID_verilog_iff)
507517
{
508518
auto &iff = to_verilog_iff_expr(expr);

0 commit comments

Comments
 (0)