Permalink
Browse files

Added proper left shift algorithm

  • Loading branch information...
1 parent 864cf6f commit 7a7b8686430215521b1e322c2e58f59b860a70e8 @mwolf76 committed Dec 31, 2012
@@ -775,6 +775,8 @@ extern DdNode * Cudd_addEvalConst (DdManager *dd, DdNode *f, DdNode *g);
extern int Cudd_addLeq (DdManager * dd, DdNode * f, DdNode * g);
extern DdNode * Cudd_addCmpl (DdManager *dd, DdNode *f);
extern DdNode * Cudd_addBWCmpl (DdManager *dd, DdNode *f);
+extern DdNode * Cudd_addBWLShift (DdManager *dd, DdNode *f);
+extern DdNode * Cudd_addBWRShift (DdManager *dd, DdNode *f);
extern DdNode * Cudd_addNegate (DdManager *dd, DdNode *f);
extern DdNode * Cudd_addRoundOff (DdManager *dd, DdNode *f, int N);
extern DdNode * Cudd_addWalsh (DdManager *dd, DdNode **x, DdNode **y, int n);
@@ -1054,6 +1054,58 @@ Cudd_addBWCmpl(
} /* end of Cudd_addBWCmpl */
+
+/**Function********************************************************************
+
+ Synopsis [1 bit left shift ADD.]
+
+ Description [1 bit left shift ADD.]
+
+ SideEffects [None]
+
+ SeeAlso [Cudd_addMonadicApply]
+
+******************************************************************************/
+DdNode *
+Cudd_addBWLShift(
+ DdManager * dd,
+ DdNode * f)
+{
+ if (cuddIsConstant(f)) {
+ CUDD_VALUE_TYPE value = (cuddV(f) << 1) & 0xf;
+ DdNode *res = cuddUniqueConst(dd,value);
+ return(res);
+ }
+ return(NULL);
+
+} /* end of Cudd_addBWLShift */
+
+
+/**Function********************************************************************
+
+ Synopsis [1 bit right shift ADD.]
+
+ Description [1 bit right shift ADD.]
+
+ SideEffects [None]
+
+ SeeAlso [Cudd_addMonadicApply]
+
+******************************************************************************/
+DdNode *
+Cudd_addBWRShift(
+ DdManager * dd,
+ DdNode * f)
+{
+ if (cuddIsConstant(f)) {
+ CUDD_VALUE_TYPE value = (cuddV(f) >> 1) & 0xf;
+ DdNode *res = cuddUniqueConst(dd,value);
+ return(res);
+ }
+ return(NULL);
+
+} /* end of Cudd_addBWRShift */
+
/*---------------------------------------------------------------------------*/
/* Definition of internal functions */
/*---------------------------------------------------------------------------*/
@@ -2746,6 +2746,26 @@ ADD::Cmpl() const
} // ADD::Cmpl
+ADD
+ADD::BWLShift() const
+{
+ DdManager *mgr = p->manager;
+ DdNode *result = Cudd_addMonadicApply(mgr, Cudd_addBWLShift, node);
+ checkReturnValue(result);
+ return ADD(p, result);
+
+} // ADD::BWLShift
+
+ADD
+ADD::BWRShift() const
+{
+ DdManager *mgr = p->manager;
+ DdNode *result = Cudd_addMonadicApply(mgr, Cudd_addBWRShift, node);
+ checkReturnValue(result);
+ return ADD(p, result);
+
+} // ADD::BWRShift
+
ADD
ADD::BWCmpl() const
{
@@ -365,10 +365,15 @@ public:
ADD operator+=(const ADD& other);
// ADD operator-(const ADD& other) const;
// ADD operator-=(const ADD& other);
+
// Shift operators
ADD LShift(const ADD& other) const;
ADD RShift(const ADD& other) const;
+ // 1 bit shift operators
+ ADD BWLShift() const;
+ ADD BWRShift() const;
+
// Logical operators
ADD operator~() const;
ADD operator&(const ADD& other) const;
@@ -306,15 +306,50 @@ void Compiler::algebraic_lshift(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];
+ }
- /* othwerwise, mul with a bounded power of 2. */
- em.make_mul ( expr->lhs(),
- make_bounded_exp2(rhs, width))));
+ /* base return value, when rhs >= width * nbits */
+ ADD res[width];
+ for (unsigned i = 0; i < width; ++ i) {
+ res[i] = f_enc.zero();
+ }
+
+ ADD msb_mask = f_enc.constant(1 << (bits_per_digit - 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(); /* lsh always introduces 0 as LSB */
+ for (unsigned i = 0; i < width; ++ i) {
+ unsigned ndx = width - i - 1;
+
+ /* c' = (0 < D & MSB_MASK); */
+ c1 = f_enc.zero().LT( tmp[ndx].BWTimes( msb_mask ));
+
+ /* accumulate */
+ res[ndx] = cond.Ite( tmp[ndx], res[ndx] );
+
+ /* x[i] = x[i] << 1 | c0 */
+ tmp[ndx] = tmp[ndx].BWLShift().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]);
+ }
}
/* REVIEW: http://en.wikipedia.org/wiki/Arithmetic_shift#Non-equivalence_of_arithmetic_right_shift_and_division */

0 comments on commit 7a7b868

Please sign in to comment.