TLSF bus variable names are different in syfco output, so also in synthesized AIGER

[johnyf]

Bus naming in AIGER

The SYNTCOMP rules (bullet 4 under Sec. "Technical") say:

"In the synthesis categories, tools must produce outputs in AIGER format (if the specification is realizable). As a syntactical restriction, the sets of inputs and outputs of the TLSF file must be identical to the sets of inputs and outputs of the AIGER solution. Additionally, solutions will be model checked with existing LTL model checking tools (details tbd)."

TLSF defines Boolean vectors as x[1]. The first value in TLSF is referred to with x[0]. However, AIGER takes Boolean variables as inputs. It seems that the requirement would be to use in the synthesized AIGER circuit the string x[0] as name for the first signal of that bus, in the symbol table of the AIGER file. In the SYNTCOMP 2014 report, Sec.3.1, p.12 says "This is followed by an arbitrary string that names the variable.". This suggests that x[0] is admissible as AIGER signal name.

From the above, SYNTCOMP would expect x[0] to appear inside synthesized AIGER. For tools that read TLSF as input, the name x[0] is available directly. However, for tools that read as input some output format of syfco (for example structured Slugs), the bus names are changed to x_0 etc. So, the same check would fail, i.e., the synthesized AIGER would include the Boolean variable x_0, not x[0].

Will SYNTCOMP take this into account, and distinguish what (bus) variable names are expected in the AIGER files synthesized by each tool, depending on what input the tool was given?

This would modify the above rule to "the sets of inputs and outputs of the input file to the tool", instead of TLSF.

Integer variable naming

Note that if there are no integer variables in TLSF and so syfco output (#10), then the current issue need not consider the names of bitvectors that represent integers. Otherwise, bitvectors have to be accounted for too, with similar naming concerns as above, with respect to the associated integer.

In this case, the difference is that a bus (bitvector) x[3] becomes the bits x_0, x_1, x_2 in AIGER, whereas an integer j in 0..15 becomes the bits j_0, j_1, j_2, j_3 (assuming a similar convention for naming the bitvector). Bit numbering is another issue in this case.

[kleinreact]

The variable names used for the AIGER output are pure boolean ones, as they appear for example in the basic output. Hence, the full TLSF input file does not specifiy a direct list of input variables, but more an indirect one, which still has to be concretized by the context (we will make this clearer in the description for next year). The same applies for example to the new smv output, which is then used by the model checker verifying your solution. Thereby, syfco takes care the naming for both outputs is consistent.

If you change the default names via the corresponding command line arguments, we will take this into accout. However, clearly it helps, if the change is made in a transparent way such that we can easily adapt all other tools correspondingly.