CIF data-based synthesis: improve resulting predicates
The CIF data-based synthesis tool internally performs calculations on BDDs. In the resulting CIF specification, the extra guards in the supervisor, as well as a potentially added initialization predicate, CIF expressions are used. One option is to encode the BDD data structures in the CIF model, and evaluate those. Another is to convert them to 'readable' CIF expressions. There is an option to configure this.
The 'readable' CIF expressions are created by converting the BDDs to CNF and DNF format. This can be somewhat readable, especially for smaller expressions. However, it is definitely not always readable. Part of the problem is that the BDDs encode everything in binary. Another issue that the CNF/DNF representations only have two levels, not more than two.
Some ideas to improve this:
-
Convert the BDDs to MDDs and then to CIF. This idea is based on the discussion at #695 (comment 1435077):
There is one other thing in favor of MDD currently, it gives nice readable results out of the box. This was the trigger for writing MDD in the first place. In compositional coordinated synthesis (if I remember its name correctly), I needed a much preserved mapping between an automaton going into synthesis and its result. (Here we will eventually need that too, as that application has been planned to be ported to ESCET.) The data synthesis with BDDs doesn't give me that, since literally everything gets rewritten as expressions using (sometimes added) power of 2 constants.
-
Convert the BDDs to ISOPs (using ZDDs). We wanted to implement this already 10 years ago, I think. It was recently mentioned again, see #695 (comment 1435077):
You can further improve the output of BDD by implementing ISOP (with ZDDs), but I doubt it will reach the same quality as I got with the MDD implementation, where you could quite easily find that a limit on one edge was incremented as the only difference between input and output.
The algorithm for this is described in Chapter 7 of this book, named 'Multi-Level Logic Synthesis Using ZBDDs'.