berkeley-abc / abc

ABC: System for Sequential Logic Synthesis and Formal Verification
Other
855 stars 525 forks source link

`read_truth` with a binary input cannot create constant functions, but hex inputs can? #214

Open MihailoIsakov opened 1 year ago

MihailoIsakov commented 1 year ago

Hi folks,

I noticed the discrepancy where:

abc -c "read_truth -x 11111111; bdd; print_kmap; print_io"

throws an error saying:

Cannot create constant function.
Segmentation fault (core dumped)

At the same time, expressing the truth table in hexadecimal such as:

abc -c "read_truth ff; bdd; print_kmap; print_io"

returns:

Truth table: ff

 c \ a b 
    0   0   1   1   
    0   1   1   0   
  +---+---+---+---+
0 | 1 | 1 | 1 | 1 |
  +---+---+---+---+
1 | 1 | 1 | 1 | 1 |
  +---+---+---+---+
Primary inputs (3):  0=a 1=b 2=c
Primary outputs (1): 0=F0
Latches (0):  

As I understand, this is not the desired behavior.

wjrforcyber commented 11 months ago

I do can reproduce what you have mentioned here, I think that since read_truth uses sop format so it uses minterms to represent, constant function indeed needs to be dealt with here.

I briefly went through the source code, bin notation does have a check on constant function while hex notation doesn't.

And, I also notice truth table in hexadecimal such as

abc -c "read_truth 00; bdd"

will abort with

Assertion failed: (0), function Abc_SopIsExorType, file abcSop.c, line 851.

So even in hex notation it can not take constant 0 since it does not cover all condition.

BTW, from a logic synthesis perspective, may I ask why you apply bdd to a constant boolean function?

MihailoIsakov commented 11 months ago

Hi, thank you for tackling this.

I've encountered this issue while working on a script that minimizes binarized neural networks (BNNs). It's quite common for BNNs to have 'dead' neurons that have a constant output, hence the issue. Of course its trivial to check whether the input circuit is constant, but I think we should avoid the segfault in any case.

wjrforcyber commented 11 months ago

@MihailoIsakov I think this issue has been taken care by @alanminko in commit c4839c9 .

UC Berkeley, ABC 1.01 (compiled Aug 18 2023 20:01:36)
abc 01> read_truth -x 11111111
abc 02> bdd
Warning: The network has only constant nodes.
abc 02>