Skip to content

Commit 607e2a0

Browse files
committed
aval/bval lowering for reduction operators
This adds the aval/bval encoding for four-valued reduction operators.
1 parent f334106 commit 607e2a0

File tree

5 files changed

+104
-0
lines changed

5 files changed

+104
-0
lines changed
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE broken-smt-backend
2+
reduction3.sv
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
--
Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
module main;
2+
3+
assert final ( & 4'b1001 === 'b0);
4+
assert final ( & 4'bx111 === 'bx);
5+
assert final ( & 4'bz111 === 'bx);
6+
assert final (~& 4'b1001 === 'b1);
7+
assert final (~& 4'bx001 === 'b1);
8+
assert final (~& 4'bz001 === 'b1);
9+
assert final ( | 4'b1001 === 'b1);
10+
assert final ( | 4'bx000 === 'bx);
11+
assert final ( | 4'bz000 === 'bx);
12+
assert final (~| 4'b1001 === 'b0);
13+
assert final (~| 4'bx001 === 'b0);
14+
assert final (~| 4'bz001 === 'b0);
15+
assert final ( ^ 4'b1001 === 'b0);
16+
assert final ( ^ 4'bx001 === 'bx);
17+
assert final ( ^ 4'bz001 === 'bx);
18+
assert final (~^ 4'b1001 === 'b1);
19+
assert final (~^ 4'bx001 === 'bx);
20+
assert final (~^ 4'bz001 === 'bx);
21+
22+
endmodule

src/verilog/aval_bval_encoding.cpp

Lines changed: 61 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -337,6 +337,67 @@ exprt aval_bval(const not_exprt &expr)
337337
return if_exprt{has_xz, x, aval_bval_conversion(not_expr, x.type())};
338338
}
339339

340+
exprt aval_bval_reduction(const unary_exprt &expr)
341+
{
342+
auto &type = expr.type();
343+
auto type_aval_bval = lower_to_aval_bval(type);
344+
PRECONDITION(is_four_valued(type));
345+
PRECONDITION(is_aval_bval(expr.op()));
346+
347+
auto has_xz = ::has_xz(expr.op());
348+
auto x = make_x(type);
349+
auto op_aval = aval(expr.op());
350+
auto op_bval = bval(expr.op());
351+
352+
if(expr.id() == ID_reduction_xor || expr.id() == ID_reduction_xnor)
353+
{
354+
auto reduction_expr = unary_exprt{expr.id(), op_aval, bool_typet{}};
355+
return if_exprt{has_xz, x, aval_bval_conversion(reduction_expr, x.type())};
356+
}
357+
else if(expr.id() == ID_reduction_and || expr.id() == ID_reduction_nand)
358+
{
359+
auto has_zero = notequal_exprt{
360+
bitor_exprt{op_aval, op_bval},
361+
to_bv_type(op_aval.type()).all_ones_expr()};
362+
363+
auto one = combine_aval_bval(bv_typet{1}.all_ones_expr(), bv_typet{1}.all_zeros_expr(), type_aval_bval);
364+
auto zero = combine_aval_bval(bv_typet{1}.all_zeros_expr(), bv_typet{1}.all_zeros_expr(), type_aval_bval);
365+
366+
if(expr.id() == ID_reduction_and)
367+
{
368+
return if_exprt{has_zero, zero,
369+
if_exprt{has_xz, x, one}};
370+
}
371+
else // nand
372+
{
373+
return if_exprt{has_zero, one,
374+
if_exprt{has_xz, x, zero}};
375+
}
376+
}
377+
else if(expr.id() == ID_reduction_or || expr.id() == ID_reduction_nor)
378+
{
379+
auto has_one = notequal_exprt{
380+
bitand_exprt{op_aval, bitnot_exprt{op_bval}},
381+
to_bv_type(op_aval.type()).all_zeros_expr()};
382+
383+
auto one = combine_aval_bval(bv_typet{1}.all_ones_expr(), bv_typet{1}.all_zeros_expr(), type_aval_bval);
384+
auto zero = combine_aval_bval(bv_typet{1}.all_zeros_expr(), bv_typet{1}.all_zeros_expr(), type_aval_bval);
385+
386+
if(expr.id() == ID_reduction_or)
387+
{
388+
return if_exprt{has_one, one,
389+
if_exprt{has_xz, x, zero}};
390+
}
391+
else // nor
392+
{
393+
return if_exprt{has_one, zero,
394+
if_exprt{has_xz, x, one}};
395+
}
396+
}
397+
else
398+
PRECONDITION(false);
399+
}
400+
340401
exprt aval_bval(const bitnot_exprt &expr)
341402
{
342403
auto &type = expr.type();

src/verilog/aval_bval_encoding.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -51,6 +51,8 @@ exprt aval_bval(const not_exprt &);
5151
exprt aval_bval(const bitnot_exprt &);
5252
/// lowering for &, |, ^, ^~
5353
exprt aval_bval_bitwise(const multi_ary_exprt &);
54+
/// lowering for reduction operators
55+
exprt aval_bval_reduction(const unary_exprt &);
5456
/// lowering for ==?
5557
exprt aval_bval(const verilog_wildcard_equality_exprt &);
5658
/// lowering for !=?

src/verilog/verilog_lowering.cpp

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -525,6 +525,17 @@ exprt verilog_lowering(exprt expr)
525525
else
526526
return expr; // leave as is
527527
}
528+
else if(
529+
expr.id() == ID_reduction_or || expr.id() == ID_reduction_and ||
530+
expr.id() == ID_reduction_nor || expr.id() == ID_reduction_nand ||
531+
expr.id() == ID_reduction_xor || expr.id() == ID_reduction_xnor)
532+
{
533+
// encode into aval/bval
534+
if(is_four_valued(expr.type()))
535+
return aval_bval_reduction(to_unary_expr(expr));
536+
else
537+
return expr; // leave as is
538+
}
528539
else if(expr.id() == ID_verilog_iff)
529540
{
530541
auto &iff = to_verilog_iff_expr(expr);

0 commit comments

Comments
 (0)