ABC seems to output invalid BLIF files (.names using OFF-SET only)

[jpf91]

Hi there,

It seems to me that ABC seems to output invalid .blif files in some cases. It seems easily reproducible, so I'm wondering whether it's a real bug or a user error somewhere instead. To reproduce:

With this test.blif input:

.model top_or
.inputs top^a top^b
.outputs top^y2

.names top^a top^b top^BITWISE_OR~2^LOGICAL_OR~7
1- 1
-1 1

.names top^BITWISE_OR~2^LOGICAL_OR~7 top^y2
1 1

.end

the following, reduced ABC script

read test.blif;
strash;
write_blif test.abc.blif;

generates this test.abc.blif output:

# Benchmark "top_or" written by ABC on Mon Jan 22 13:46:50 2024
.model top_or
.inputs top^a top^b
.outputs top^y2
.names top^a top^b top^y2
00 0
.end

It seems to me that ABC expects this to mean "a=0, b=0 => y = 0; All other combinations result in 1". I.e. it specifies the OFF-Set and assumes the complement of the OFF-Set to be the ON set. This seems to come from abcSop.c.

The genfasm tool in VPR however reads this as "a=0, b=0 => y = 0; All other combinations result in DC". So it interpret's this as the OFF-Set with the complement of that Set being the DC-Set. It therefore returns an all-0 LUT for the OR operation.

I did some research which interpretation is correct, but the BLIF specification does not have a lot of detail for the .names directive:

.names <in-1> <in-2> ... <in-n> <output>
<single-output-cover>

[...]
single-output-cover is, formally, an n-input, 1-output PLA description of the logic function corresponding to the logic gate.
f0, 1, –g is used in the n-bit wide “input plane” and f0, 1g is used in the 1-bit wide “output plane”. The ON-set is specified with 1’s in the “output plane,” and the OFF-set is specified with 0’s in the “output plane.” The DC-set is specified for primary output nodes only, by using the construct .exdc.
[...]
For a more complete description of the PLA input format, see espresso(5)

It does not really state what happens for unspecified input combinations, but it references espresso(5), which says:

A Boolean function can be described in one of the following ways:

1. By providing the ON -set. In this case, espresso computes the OFF -set as the complement of the ON -set and the DC -set is empty. This is indicated with the keyword .type f in the input file.
2. By providing the ON -set and DC -set. In this case, espresso computes the OFF -set as the complement of the union of the ON -set and the DC -set. If any minterm belongs to both the ON -set and DC -set, then it is considered a don't care and may be removed from the ON -set during the minimization process. This is indicated with the keyword .type fd in the input file.
3. By providing the ON -set and OFF -set. In this case, espresso computes the DC -set as the complement of the union of the ON -set and the OFF -set. It is an error for any minterm to belong to both the ON -set and OFF -set. This error may not be detected during the minimization, but it can be checked with the subprogram "-Dcheck" which will check the consistency of a function. This is indicated with the keyword .type fr in the input file.
4. By providing the ON -set, OFF -set and DC -set. This is indicated with the keyword .type fdr in the input file.

So according to this, specifying only the OFF-set is case 3, with an empty ON set. All remaining inputs combinations then belong to the DC-Set and it seems VPR is correctly interpreting the BLIF format, but ABC is not.

Is that conclusion correct, or am I missing something? Maybe this is also interesting for VPR and F4GPA, @vaughnbetz and @cliffordwolf ?