Functional reduction followed by SOP balancing fails equivalence check
Closed this issue · 2 comments
I found this a few days ago and haven't been able to figure out what's causing it. In most benchmarks there's no problem, but in mem_ctrl from the EPFL benchmark suite, if I apply functional reduction followed by SOP balancing to an AIG, then write the file, it's not equivalent to the original network. Either of them alone (or if I put a different optimization between them) seems to work fine.
mockturtle::aig_network run(mockturtle::aig_network &aig){
mockturtle::sop_rebalancing<mockturtle::aig_network> balfn;
mockturtle::balancing_params bp;
bp.cut_enumeration_ps.cut_size = 4u;
mockturtle::functional_reduction(aig);
aig = mockturtle::balancing(aig, {balfn}, bp);
return aig;
}
failing ABC cec output, in case it helps:
Verification failed for at least 62 outputs: y153 y160 y189 ...
Output y153: Value in Network1 = 0. Value in Network2 = 1.
Input pattern: x55=0 x92=0 x215=0 x221=0 x929=0 x216=0 x833=0 x332=0 x1144=0 x265=0 x228=0 x105=0 x153=0 x166=0 x152=0 x161=0 x234=0 x210=0 x137=0 x95=0 x479=0 x32=0 x225=0 x40=0 x72=0 x102=0 x50=0 x77=0 x88=0 x98=0 x81=0 x64=0 x65=0 x71=0 x83=0 x103=0 x67=0 x69=0 x66=0 x73=0 x45=0 x104=0 x49=0 x89=0 x48=0 x61=0 x76=0 x85=0 x106=0 x68=0 x84=0 x36=0 x82=0 x111=0 x63=0 x107=0 x94=0 x97=0 x108=0 x46=0 x86=0 x53=0 x60=0 x109=0 x110=0 x47=0 x58=0 x91=0 x90=0 x93=0 x70=0 x96=0 x35=0 x51=0 x1091=0 x957=0 x841=0 x829=0 x950=0 x1092=0 x1093=0 x146=0 x299=0 x39=0 x223=0 x222=0 x224=0 x142=0 x198=0 x189=0 x144=0 x174=0 x38=0 x100=0 x87=0 x252=0 x75=0 x54=0 x74=0 x56=0 x62=0 x59=0 x57=0
Any idea what may be causing this? Working around it is easy, but it's been bugging me.
functional_reduction
identifies equivalent nodes and merges them, which leads to some dangling nodes in the network. They are not automatically removed. Thus they possibly create some problem in balancing
.
Adding aig = cleanup_dangling(aig);
in between should solve the issue.
Perfect; thank you.