Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Added proper right shift algorithm

  • Loading branch information...
commit ccf6a3eef51f6f9ef39c84c4b2370e28fcf6e232 1 parent 7a7b868
@mwolf76 authored
Showing with 43 additions and 9 deletions.
  1. +43 −9 src/model/compilers/algebra.cc
View
52 src/model/compilers/algebra.cc
@@ -352,7 +352,6 @@ void Compiler::algebraic_lshift(const Expr_ptr expr)
}
}
-/* REVIEW: http://en.wikipedia.org/wiki/Arithmetic_shift#Non-equivalence_of_arithmetic_right_shift_and_division */
void Compiler::algebraic_rshift(const Expr_ptr expr)
{
assert( is_binary_algebraic(expr) );
@@ -370,15 +369,50 @@ void Compiler::algebraic_rshift(const Expr_ptr expr)
lhs[i] = f_add_stack.back(); f_add_stack.pop_back();
}
- (*this)(em.make_ite(
- /* rhs anything beyond width? result is zero. */
- em.make_cond( em.make_ge( expr->rhs(),
- em.make_iconst(bits_per_digit * width)),
- em.make_zero()),
+ ADD tmp[width];
+ for (unsigned i = 0; i < width; ++ i) {
+ tmp[i] = lhs[i];
+ }
+
+ /* base return value, when rhs >= width * nbits */
+ ADD res[width];
+ for (unsigned i = 0; i < width; ++ i) {
+ res[i] = f_enc.zero();
+ }
- /* otherwise, div by a bounded power of 2. */
- em.make_div ( expr->lhs(),
- make_bounded_exp2(rhs, width))));
+ ADD lsb_mask = f_enc.constant(1);
+ ADD c0;
+ ADD c1;
+
+ for (unsigned k = 0; k < bits_per_digit * width; ++ k) {
+
+ /* compile selection condition */
+ (*this)(em.make_eq( expr->rhs(), em.make_iconst(k)));
+ ADD cond = f_add_stack.back(); f_add_stack.pop_back();
+ f_type_stack.pop_back(); /* adjust type stack */
+
+ c0 = f_enc.zero(); /* FIXME: rsh should *not* always introduce 0 as LSB */
+ for (unsigned i = 0; i < width; ++ i) {
+ unsigned ndx = i; /* left-to-right */
+
+ /* c' = (0 < D & MSB_MASK); */
+ c1 = f_enc.zero().LT( tmp[ndx].BWTimes( lsb_mask ));
+
+ /* accumulate */
+ res[ndx] = cond.Ite( tmp[ndx], res[ndx] );
+
+ /* x[i] = x[i] >> 1 | c0 */
+ tmp[ndx] = tmp[ndx].BWRShift().BWOr(c0);
+
+ c0 = c1;
+ }
+ }
+
+ /* push result (reversed) */
+ for (unsigned i = 0; i < width; ++ i) {
+ unsigned ndx = width - i - 1;
+ f_add_stack.push_back( res[ndx]);
+ }
}
void Compiler::algebraic_equals(const Expr_ptr expr)
Please sign in to comment.
Something went wrong with that request. Please try again.