You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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:
# 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:
[...] 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:
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.
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.
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.
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 ?
The text was updated successfully, but these errors were encountered:
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:the following, reduced ABC script
generates this
test.abc.blif
output: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:It does not really state what happens for unspecified input combinations, but it references espresso(5), which says:
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 ?
The text was updated successfully, but these errors were encountered: