5 ms·
Minimizing Logic Expressions
- adamnemecek 7y agoThis sounds like proof normalization in linear logic.
- lidHanteyk 7y agoIn many flavors of logic, not just linear logic.
- 2rsf 7y agoCool, only a few days ago I explained my daughter about that. Does finding the minimum logic expression also implies it uses the minimum number of logical gates ?
- zozbot234 7y agoI don't think so, because CMOS circuits are not restricted to being series-parallel like, as in logic expressions. For example, one can implement, e.g. not(AB+CD+E(A+C)(B+D)) with just five gates (one per input) for each of the direct (pull-down) and complementary (pull-up) network.
- cellularmitosis 7y agoThis makes sense when comparing the instruction set to the logic circuit of the 74181! So many seemingly complex instructions for such a simple circuit :). Thank you for pointing this out!
- zozbot234 7y ago74181 is based on TTL logic not CMOS, but you're right that similar considerations can apply to a higher-level logic circuit, and that these explain how "seemingly complex" can in fact be quite simple.
- timclark 7y agoYou can minimise the number of gates but that doesn't minimise the number of transistors as that varies by the type of logical operation performed by the gate. Practically you probably care more about the number of transistors than the number of gates.
- Jaxan 7y agoDepends on which gates you allow in your design. But the SMT encoding is really flexible, so you can adjust it for your needs.
- praptak 7y agoSee also https://en.m.wikipedia.org/wiki/Karnaugh_map https://en.m.wikipedia.org/wiki/Karnaugh_map for a human-applicable algorithm to minimize logic expressions.
- yters 7y agoAlso Quine-McCluskey for an automated reduction of Karnaugh maps.
- paypalcust83 7y agoEE/CS here. Kmaps only work for 4-5 variables unless you're some sort of 4D-chess wizard. And they're meant for manual, human pattern-matching rather than automated evaluation. There are numerous, specialized bi/tri/quad boolean logic prime implicant optimization algorithms for combinational logic and expressions like QM and MQM.
- tasty_freeze 7y agoI once did the reverse karnaugh mapping on a set of expressions to minimize their complexity; the input set was 7 bits. Specifically, I created an instruction mapping on a 7b opcode space such that the decode logic for the critical paths was short (eg, branch decode). It took multiple sheets of paper, a few tries, and a couple of days, but it wasn't too bad.
- laszlokorte 7y agoFor my bachelors thesis I built a tool for playing around with and teaching KV diagrams [1] [1]: https://thesis.laszlokorte.de/demo/kvd-editor.html https://thesis.laszlokorte.de/demo/kvd-editor.html
- bear8642 7y agoNice tool! By DNF and KNF do you mean disjunctive and conjuctive normal form?
- 7y ago
- steerablesafe 7y agoOh, this is great! Some time ago I tried to hand optimize S4 group multiplication. S4 group elements are representable on 5 bits, so it is a 10 bit -> 5 bit function. Directly optimizing it on Karnaugh maps is infeasible. I managed by breaking it down to Z2, Z3 and V4. I would love to unleash a bruteforce optimization on it.
- AshamedCaptain 7y ago> Although I could use an off-the-shelf logic minimizer here (like Espresso), most logic minimizers solve a different problem: quickly translating large designs to simple netlists. However, I would like to have a complex output netlist: the ATF15xx CPLDs have a hardware XOR gate that I would like the minimizer to infer on its own. On the other hand, I don’t really care about the runtime of the minimizer as long as it’s on the order of minutes to hours This is called technology mapping and logic minimizers (like Espresso) do it all the time. Just think of it: who defines what the basic logic modules on your netlist _are_ ? What if your only module is a XOR gate?
- weinzierl 7y agoI don't think Espresso can do this. The Espresso Wikipedia talk page has this: "Espresso is a pure two-layer sum-of-products or product-of-sums minimizer without xor or factoring capabilities." There is also a paper by E. V. Dubrova et al. about finding optimal AND-OR-XOR expressions which has extensive comparisons with Espresso.
- derefr 7y agoWhen I needed to do this, I just grabbed Z3 and applied this little bit of black magic from the cookbook: (apply (then ctx-solver-simplify propagate-values (par-then (repeat (or-else split-clause skip)) propagate-ineqs))) Works pretty well for my problem (simplifying the branch condition paths for entering a given basic-block in a symbolic-execution system down to something human-readable), and best of all, it has no corner-cases requiring manual human teaching. (It's the ctx-solver-simplify bit that gets you most of that; it's a pretty powerful engine.)