&blut caused equivalence checking failure (FIXED)

[light-tian]

Version

The latest version of ABC.

Details

&blut will detect MUX structure in GIA and create mux node in str_ntk_t, and then collect MUX-tree to do balance, to optimize delay.

But during the process of collecting MUX-tree, following two mux-trees (the part marked by the dashed line) will be hashed as the same one, then caused equivalence failure (because the original logic is very complicated, use the diagram to simplify this problem).

Solution

When hashing MUX-tree encounters boundary, need to take the complement of the boundary into consideration, then I modified the following function and the equivalence checking passed.

// src/aig/gia/giaStr.cc:333

void Str_MuxStructDump_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Str_t * vStr, int fCompl )
{
    if ( !pObj->fMark0 ) {
		if (fCompl) {
			Vec_StrPush( vStr, '!' );
		}
		return;
	}
    Vec_StrPush( vStr, '[' );
    Vec_StrPush( vStr, '(' );
    Vec_StrPrintNum( vStr, Gia_ObjFaninId2p(p, pObj) );
    Vec_StrPush( vStr, ')' );
	int inv1 = Gia_ObjFaninC2(p, pObj) ? Gia_ObjFaninC0(pObj) : Gia_ObjFaninC1(pObj);
    Str_MuxStructDump_rec( p, Gia_ObjFaninC2(p, pObj) ? Gia_ObjFanin0(pObj) : Gia_ObjFanin1(pObj), vStr, inv1);
    Vec_StrPush( vStr, '|' );
	int inv2 = Gia_ObjFaninC2(p, pObj) ? Gia_ObjFaninC1(pObj) : Gia_ObjFaninC0(pObj);
    Str_MuxStructDump_rec( p, Gia_ObjFaninC2(p, pObj) ? Gia_ObjFanin1(pObj) : Gia_ObjFanin0(pObj), vStr, inv2);
    Vec_StrPush( vStr, ']' );
}

Discussion

This case includes many muxes and is large, so I think the bug is more possible to be triggered.
The .blif is hard to provide, but the above change helped to fix the equivalence problem. Other guys who encountered the same problem may refer to it.

Finally need ABC developers to check whether this fix is needed or not, thanks!