cjdrake / pyeda Goto Github PK

Recently looked at using weakref.WeakValueDictionary for the Expression.restrict cache, but it didn't work b/c it cannot be used to store integers. Unfortunately, when doing expression simplification, I am using the actual integer 0 and 1 values, which are not of the same type as of expression arguments.

I think maybe it's time to revert back to having an expression Constant implementation. The ZERO and ONE objects should be singletons. I think the reason I got rid of this in the past was that I wanted the actual return value to be an integer, not some weird expression object that the user wouldn't know what to do with. In other words, "x * -x" should just return 0, not ExpressionConstantZero or whatever.

To solve the problem, similar to BDD, expression functions should "exprify" their inputs, and "constify" their outputs. This leads to a very interesting possibility of actually parsing much more elaborate expressions written using strings, rather than just 0 and 1.

This would have the added benefit of making the type of all expression objects consistent, and uniform. I doubt PyPy or some other JIT would approve of using integers the way I'm using them.

Using a 64-bit word has some nice benefits.

I skipped this during BDD implementation, but it's required to prevent very expensive duplicate calculation during recursion.

The identity didn't occur to me originally:

f = s * a + -s * b
-f = s * -a + -s * -b

Only dependency that is currently misbehaving is pylint, which flakes out at some Python 3.3 stuff.

Similar to pyeda.parsing.boolexpr, the DIMACS formats shouldn't directly return Expression instances. CNF should return a tuple of tuple of ints, and SAT should return an AST.

With information about:

• ripple-carry
• Brent-Kung
  *Kogge-Stone

Misread the orientation of 0/1 from a book. Turns out that zero is 1<<0 (1), and one is 1<<1 (2). They are reversed in table.py.

Just realized that I put the reduce implementation in the Variable class, but it was supposed to go in the Expression class. Herp-derp.

There are a few assert statements here and there that should probably raise either TypeError or ValueError.

Profiling shows that expression construction does lots of redundant computation simplifying expressions. Need to enable a method to construct the entire tree, then run a simplify operation once in a top-down manner.

First thought is that if you have And(..., simplify=True) as the default, then that will be good for interactive use, but you can use And(..., simplify=False) to just save simplification for later by calling F.simplify() or simplify(F).

In Expression, checking the inputs looks for boolfunc.Function. Should be Expression. The unate methods are not implemented by Table representations.

The table implementation of this method seems straight-forward. Not sure if the expression algorithm of using min/max terms makes any sense. Need to look this one up.

Current code puts d0 on the d1 edge, and vice-versa.

It's possible to do the entire CNF file with one regular expression, but for some reason I'm sharing the SAT format lexer with CNF format.

Found this while testing out formal equivalence with ITE. Currently commented out.

I'm definitely mixing several unrelated things in the current repository structure.

Possible future organization:

pyeda/
    __init__.py
    util.py
    boolalg/
        __init__.py
        alphas.py
        bdd.py
        boolfunc.py
        expr.py
        nfexpr.py
        table.py
        vexpr.py
    logic/
        __init__.py
        addition.py
        floatingpoint.py
        graycode.py
        multiplication.py
        sudoku.py
        ...
    parsing/
        dimacs.py
        verilog.py
        ...

Some notes:

• Not sure where to put satisfiability. Might make sense in boolalg, but that's a lot of nesting, and I think SAT can stand on its own--it's so important. Would be nice to integrate several SAT algorithms.
• After integrating some fast SAT solvers written in C/C++, I think the nfexpr type can go away. It's a neat function representation, but cannot possibly implement the full boofunc interface.

There's no reason for other Function implementations to use an Expression as the Variable implementation.

A table implementation of a variable is just a one-bit table with a label. A BDD implementation of a variable is just a Node with low=0 and high=1. And so on...

The binop.apply2 method behaves unexpectedly as a result of this (among other things).

Probably expr.py, table.py, bdd.py, etc will each require their own "Variable" class. Considering we already duplicate that name between boolfunc.py and expr.py, probably a good idea to change the class name to ExprVariable, TableVariable, BDDVariable, etc.

Recently saw a problem with this in pyeda/__init__.py:

from pyeda.expr import (..., expr, ...)

Unfortunately, that actually replaces the pyeda.expr module with the pyeda.expr.expr function.

So probably the best solution is to just drop almost all imports, and require users to just import stuff explicitly.

Currently returns a mutable set type

There are a few iterators that could make use of the cool yield from syntax introduced in Python 3.3. Need to deprecate Python 3.2.

In "Synthesis and Optimization of Digital Circuits" by DeMicheli, page 80 he defines the top variable as "the first variable in the support set".

In "Logic Synthesis and Verification Algorithms" by Hatchel/Somenzi, on page 234 they define the top variable as "the variable with the lowest index".

In the last release I used the last variable in the ordered support, so that appears to have been a mistake. Maybe if there's a top variable, there can also be a bottom as well.

Would be pretty easy to add these. Need to change And.invert to Nand, and Or.invert to Nor. DeMorgan would be implemented in Nor/Nand factor.

Should standardize the format of runtime input argument errors. Should be something like:

expected {type or value description} [, got {type or value description} ]

The 'got' part of the statement can be a bit annoying to produce sometimes, so optional.

Python namedtuple cannot be the value in a WeakValueDictionary. Easier to just drop namedtuple usage altogether.

For modeling timing-aware design elements such as flip-flops.

After thinking about this, there isn't really any value to maintaining a truth table that uses only 0/1, and one that uses positional cube notation. The space savings is only 2x, and since truth tables are already exponential in size it seems a bit silly to maintain this for its compression purposes alone.

Better to expend more time thinking about and implementing an ImplicantTable implementation.

So get rid of TruthTable, and replace the PCTable with TruthTable.

Related to issue #24, it would be extremely useful to implement a general-purpose logic expression parser that can handle variable names in the form x.y.z[1][2][3], unary '-', and all the usual infix operators: '+', '-', '*', 'xor' , '=', '->'.

This is already implemented in the example code. Just need to update docs.

Only need a single function which determines whether the expression input is in DNF/CNF form, and then do the proper conversion automatically. The actual conversion is from "Expression" to "NormalFormExpression". Too easy to mistake cnf/dnf for an actual type, rather than just a format.

Currently, the Table.str method assumes you want your table to be printed in Espresso format. A better implementation will make the str(F) method return a generic table, maybe something like RestructuredText. Then need another method that takes a 'fmt' parameter. Using fmt=None should return the generic string.

An if-then-else expression would be pretty awesome. Might have some practical use in the implementation of BDDs.

Looks like my package metadata is missing something from either MANIFEST.in or setup.py.