Permalink
Browse files

Minor maintenance

  • Loading branch information...
1 parent 610ed36 commit 864cf6f86878fc898bbf4a9994aba389aa2d4f97 @mwolf76 committed Dec 28, 2012
Showing with 65 additions and 46 deletions.
  1. +9 −3 src/cdefs.h
  2. +7 −1 src/enc/enc_mgr.hh
  3. +4 −4 src/model/compilers/algebra.cc
  4. +45 −38 src/model/compilers/internals.cc
View
@@ -22,13 +22,19 @@
#ifndef CDEFS_DEFINED
#define CDEFS_DEFINED
-#define DEFAULT_BITS 8
+#include <limits.h>
/* Reserved for native data type, should match machine word for
- optimal performance. This type used for the ADD leaves. */
+ optimal performance. This type will be used for the ADD leaves. */
typedef long value_t;
-/* time representation */
+/* Reserved for ADD ops error checking. */
+static const value_t error_value = LONG_MIN;
+
+/* Number of bits per digit. */
+static const value_t bits_per_digit = 4;
+
+/* Reserved for time frames representation. */
typedef unsigned step_t;
#endif
View
@@ -72,12 +72,18 @@ public:
inline ADD zero()
{ return f_cudd.addZero(); }
+ inline ADD error()
+ { return f_cudd.constant(error_value); }
+
inline ADD constant(value_t value)
- { return f_cudd.constant(value); }
+ { assert (error_value != value); return f_cudd.constant(value); }
inline bool is_constant(ADD x) const
{ return cuddIsConstant(x.getNode()); }
+ inline bool is_error(ADD x) const
+ { return cuddIsConstant(x.getNode()) && (error_value == Cudd_V(x.getNode())); }
+
inline value_t const_value(ADD x) const
{ return Cudd_V(x.getNode()); }
@@ -309,10 +309,10 @@ void Compiler::algebraic_lshift(const Expr_ptr expr)
(*this)(em.make_ite(
/* rhs anything beyond width? result is zero. */
em.make_cond( em.make_ge( expr->rhs(),
- em.make_iconst(4 * width)), // HARDCODED
+ em.make_iconst(bits_per_digit * width)),
em.make_zero()),
- /* mul with a bounded power of 2 */
+ /* othwerwise, mul with a bounded power of 2. */
em.make_mul ( expr->lhs(),
make_bounded_exp2(rhs, width))));
}
@@ -338,10 +338,10 @@ void Compiler::algebraic_rshift(const Expr_ptr expr)
(*this)(em.make_ite(
/* rhs anything beyond width? result is zero. */
em.make_cond( em.make_ge( expr->rhs(),
- em.make_iconst(4 * width)), // HARDCODED
+ em.make_iconst(bits_per_digit * width)),
em.make_zero()),
- /* div with a bounded power of 2 */
+ /* otherwise, div by a bounded power of 2. */
em.make_div ( expr->lhs(),
make_bounded_exp2(rhs, width))));
}
@@ -645,56 +645,63 @@ static inline value_t pow2(unsigned exp)
return res;
}
+/**
+ This function builds a selector of powers of 2, i.e.
+
+ f(A) := (A == 0) ? 1
+ : (A == 1) ? 2
+ : (A == 2) ? 4
+ .
+ .
+ .
+ : (A == k - 1) ? 2 ^ (k-1)
+ : ERROR
+*/
Expr_ptr Compiler::make_bounded_exp2(ADD *dds, unsigned width)
{
value_t value;
unsigned base = Cudd_V(f_enc.base().getNode());
unsigned exp2 = 0;
- ADD mpx[width]; /* multiplex */
+ ADD mpx[width]; /* multiplexer, building terminal error nodes */
for (unsigned i = 0; i < width; ++ i) {
unsigned ndx = width - i - 1;
- mpx[ndx] = (! ndx )
- ? f_enc.one()
- : f_enc.zero() ;
+ mpx[ndx] = f_enc.error();
}
while (exp2 < width) {
- ADD condition = f_enc.one();
- { /* inlined condition */
- value = exp2;
-
- /* inlined condition */
- for (unsigned i = 0; i < width; ++ i) {
- unsigned ndx = width - i - 1;
-
- condition *= dds[ndx].
- Equals(f_enc.constant(value % base));
-
- value /= base;
- }
- assert (value == 0); // not overflowing
- }
-
- ADD constant[width];
- {/* inlined power of 2 */
- value = pow2(exp2);
- for (unsigned i = 0; i < width; ++ i) {
- unsigned ndx = width - i - 1;
-
- constant[ndx] = f_enc.constant(value % base);
-
- value /= base;
- }
- assert (value == 0); // not overflowing
- }
-
- for (unsigned i = 0; i < width; ++ i) {
- mpx[i] = condition.Ite( constant[i], mpx[i] );
- }
-
- ++ exp2;
+ /* build cond 0-1 ADD, 'A == k' */
+ ADD condition = f_enc.one();
+
+ value = exp2;
+ for (unsigned i = 0; i < width; ++ i) {
+ unsigned ndx = width - i - 1;
+ condition *= dds[ndx]. // TODO: this conjuction should be optimized
+ Equals(f_enc.constant(value % base));
+
+ value /= base;
+ }
+ assert (value == 0); // not overflowing
+
+ /* build corresponding Then ADD vec, '2^value' */
+ ADD constant[width];
+
+ value = pow2(exp2);
+ for (unsigned i = 0; i < width; ++ i) {
+ unsigned ndx = width - i - 1;
+ constant[ndx] = f_enc.constant(value % base);
+
+ value /= base;
+ }
+ assert (value == 0); // not overflowing
+
+ /* ITE chaining (endianess irrelevant here)*/
+ for (unsigned i = 0; i < width; ++ i) {
+ mpx[i] = condition.Ite( constant[i], mpx[i] );
+ }
+
+ ++ exp2;
}
return make_temporary_encoding(mpx, width);

0 comments on commit 864cf6f

Please sign in to comment.