lsils/mockturtle

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.