Issues with equivalence checking, when working with XAGs

[hibenj]

1. When reading a file in AIGER format with &read and creating the XAG with &st -m -L 1 then the command &cec will return not equivalent. But when strashing it again with &st the equivalence is given again. I though this migh be due to the internal representation of XOR gates after using the &st -m -L 1 command.
2. This would not be a big issue, but when using optimization commands on XAGs like &b after &st -m -L 1 and then using &st again, the &cec will still give not equivalent.

The issues can be tested by just executing the provided shell script in the base of an ABC repo with built abc executable:

!/bin/bash

echo "Executing command 1" ./abc -c "&read i10.aig; &st -m -L 1; &cec; &st; &cec" echo "Executing command 2" ./abc -c "&read i10.aig; &st -m -L 1; &b; &st; &cec"

Output: Executing command 1 ABC command line: "&read i10.aig; &st -m -L 1; &cec; &st; &cec".

Generated AND/XOR/MUX graph. Networks are NOT EQUIVALENT. Output 144 trivially differs (different phase). Time = 0.00 sec Generated AIG from AND/XOR/MUX graph. Networks are equivalent. Time = 0.03 sec Executing command 2 ABC command line: "&read i10.aig; &st -m -L 1; &b; &st; &cec".

Generated AND/XOR/MUX graph. Networks are NOT EQUIVALENT. Output 144 trivially differs (different phase). Time = 0.00 sec

[alanminko]

Thank you for the report. Please note that when we use "&b" (as opposed to "&b -a"), it will internally convert the circuit to AND/XOR/MUX, and perform balancing with these gates. There is no need to run "&st -m -L 1" before "&b" or any other optimization command. The reason "&st -m -L 1" is available, is for experiments with various transformations involving XOR/MUX gates. Those who use it for these experiments are aware that the intermediate result does not verify.

[alanminko]

In general, If ABC is used as a black box, the only legitimate use of "&st -m -L 1" is to count the number of XOR gates present in the AIG. If ABC is used for programming new optimization engines, "&st -m -L 1" can be used to transform AIG into XAIG, followed by applying desired optimizations. In the end, we can use &st, to convert XAIG into AIG, before equivalence checking.

[wjrforcyber]

In general, If ABC is used as a black box, the only legitimate use of "&st -m -L 1" is to count the number of XOR gates present in the AIG. If ABC is used for programming new optimization engines, "&st -m -L 1" can be used to transform AIG into XAIG, followed by applying desired optimizations. In the end, we can use &st, to convert XAIG into AIG, before equivalence checking.

It seems that since AIG is not canonical, the &st right after &st -m -L 1 could not 100% recover the network(even after &st at the beginning), for those who use &st -m -L 1 for structure analyse, is duplicate the original AIG the only way to save the original one?

abc 01> &r i10.aig 
abc 01> &st
abc 01> &ps 
i10      : i/o =    257/    224  and =    2675  lev =   50 (15.54)  mem = 0.04 MB
abc 01> &ps -m
i10      : i/o =    257/    224  and =    2675  lev =   50 (15.54)  mem = 0.04 MB
XOR/MUX stats:  xor =     154  17.27 %   mux =     157  17.61 %   and =    1742  65.12 %   obj =    2675
abc 01> &st -m -L 1
Generated AND/XOR/MUX graph.
abc 01> &ps -m
i10      : i/o =    257/    224  nod =    2386  lev =   50 (15.54)  mem = 0.04 MB
XOR/MUX stats:  xor =     151  16.85 %   mux =       0   0.00 %   and =    2235  83.15 %   obj =    2386  
abc 01> &st
Generated AIG from AND/XOR/MUX graph.
abc 01> &ps -m
i10      : i/o =    257/    224  and =    2674  lev =   50 (15.54)  mem = 0.04 MB
XOR/MUX stats:  xor =     151  16.94 %   mux =     157  17.61 %   and =    1750  65.45 %   obj =    2674
abc 01> &cec
Networks are equivalent.  Time =     0.04 sec
abc 01>