From 7b0a6cbb588463bc31f3c191e139d8fae546245d Mon Sep 17 00:00:00 2001 From: JingrenWang Date: Mon, 1 Jun 2026 16:23:38 +0800 Subject: [PATCH] Feat(rd_inv): Simple inv redis framework. Signed-off-by: JingrenWang --- abclib.dsp | 4 + src/base/abc/abc.h | 4 + src/base/abc/abcDfs.c | 96 ++++ src/base/abci/abc.c | 55 ++- src/base/abci/abcRmInverters.c | 853 +++++++++++++++++++++++++++++++++ src/base/abci/module.make | 1 + 6 files changed, 1012 insertions(+), 1 deletion(-) create mode 100644 src/base/abci/abcRmInverters.c diff --git a/abclib.dsp b/abclib.dsp index 2f16e849ee..4aa3a34ce5 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -443,6 +443,10 @@ SOURCE=.\src\base\abci\abcResub.c # End Source File # Begin Source File +SOURCE=.\src\base\abci\abcRmInverters.c +# End Source File +# Begin Source File + SOURCE=.\src\base\abci\abcRewrite.c # End Source File # Begin Source File diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 0b0376c47f..e490808232 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -142,6 +142,7 @@ struct Abc_Obj_t_ // 48/72 bytes (32-bits/64-bits) unsigned Level : 20; // the level of the node Vec_Int_t vFanins; // the array of fanins Vec_Int_t vFanouts; // the array of fanouts + void * pDataComp; union { void * pData; // the network specific data int iData; }; // (SOP, BDD, gate, equiv class, etc) union { void * pTemp; // temporary store for user's data @@ -620,6 +621,7 @@ extern ABC_DLL float Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fU /*=== abcDfs.c ==========================================================*/ extern ABC_DLL Vec_Ptr_t * Abc_NtkDfs( Abc_Ntk_t * pNtk, int fCollectAll ); extern ABC_DLL Vec_Ptr_t * Abc_NtkDfs2( Abc_Ntk_t * pNtk ); +extern ABC_DLL void Abc_NtkDfsSup_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Vec_Ptr_t * vSup, int iVerbose); extern ABC_DLL Vec_Ptr_t * Abc_NtkDfsNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes ); extern ABC_DLL Vec_Ptr_t * Abc_NtkDfsReverse( Abc_Ntk_t * pNtk ); extern ABC_DLL Vec_Ptr_t * Abc_NtkDfsReverseNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes ); @@ -885,6 +887,8 @@ extern ABC_DLL int Abc_NodeRef_rec( Abc_Obj_t * pNode ); extern ABC_DLL int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nMinSaved, int nConeSizeMax, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose ); /*=== abcRewrite.c ==========================================================*/ extern ABC_DLL int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose, int fVeryVerbose, int fPlaceEnable ); +/*=== abcRmInverters.c ======================================================*/ +extern ABC_DLL void Abc_NtkRmInverter(Abc_Ntk_t * pNtk, int iVerbose); /*=== abcSat.c ==========================================================*/ extern ABC_DLL int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fVerbose, ABC_INT64_T * pNumConfs, ABC_INT64_T * pNumInspects ); extern ABC_DLL void * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fAllPrimes ); diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c index 68c005a5e3..d95c8ad024 100644 --- a/src/base/abc/abcDfs.c +++ b/src/base/abc/abcDfs.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "abc.h" +#include "misc/vec/vecPtr.h" #include "proof/cec/cec.h" ABC_NAMESPACE_IMPL_START @@ -137,6 +138,101 @@ Vec_Ptr_t * Abc_NtkDfs2( Abc_Ntk_t * pNtk ) return vNodes; } +/**Function************************************************************* + + Synopsis [Collect support nodes bounded internal nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkDfsSup_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Vec_Ptr_t * vSup, int iVerbose) +{ + Abc_Obj_t * pFanin; + int i; + assert( !Abc_ObjIsNet(pNode) ); + if ( Abc_NodeIsTravIdCurrent( pNode ) ) + return; + Abc_NodeSetTravIdCurrent( pNode ); + if ( Abc_ObjIsCi(pNode) || Abc_ObjIsCo(pNode) || (Abc_NtkIsStrash(pNode->pNtk) && Abc_AigNodeIsConst(pNode)) ) + return; + if( Vec_PtrFind(vSup, pNode) >= 0 ) + { + if(iVerbose) + { + printf("Encountered vSup Node: %s\n", Abc_ObjName(pNode)); + printf("Whose fanins are:\n"); + printf(" Fanin0: %s", Abc_ObjName(Abc_ObjFanin0(pNode))); + printf(" %d on comp\n", pNode->fCompl0); + printf(" Fanin1: %s", Abc_ObjName(Abc_ObjFanin1(pNode))); + printf(" %d on comp\n", pNode->fCompl1); + } + return; + } + assert( Abc_ObjIsNode( pNode ) ); + Abc_ObjForEachFanin( pNode, pFanin, i ) + { + if(iVerbose) + { + printf(" Node %s Fanin %d: ", Abc_ObjName(pNode), i); + printf("%s", Abc_ObjName(pFanin)); + printf(" %d on comp\n", i == 0 ? pNode->fCompl0 : pNode->fCompl1); + } + Abc_NtkDfsSup_rec( Abc_ObjFanin0Ntk(pFanin), vNodes, vSup, iVerbose); + } + Vec_PtrPush( vNodes, pNode ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkDfsInvSup_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSup, int * countFlip) +{ + Abc_Obj_t * pFanin; + int i; + assert( !Abc_ObjIsNet(pNode) ); + if ( Abc_NodeIsTravIdCurrent( pNode ) ) + return; + Abc_NodeSetTravIdCurrent( pNode ); + if ( Abc_ObjIsCi(pNode) || Abc_ObjIsCo(pNode) || (Abc_NtkIsStrash(pNode->pNtk) && Abc_AigNodeIsConst(pNode)) ) + return; + if( Vec_PtrFind(vSup, pNode) >= 0 ) + { + return; + } + assert( Abc_ObjIsNode( pNode ) || Abc_ObjIsBox( pNode ) ); + + Abc_ObjForEachFanin( pNode, pFanin, i ) + { + if(Vec_PtrFind(vSup, pFanin) >= 0) + { + if(i == 0) + { + printf("Flipping edge on Node %s %d (Phase = %d)\n", Abc_ObjName(pNode), i, pFanin->fPhase ); + pNode->fCompl0 ^= 1; + } + else if(i == 1) + { + printf("Flipping edge on Node %s %d (Phase = %d)\n", Abc_ObjName(pNode),i , pFanin->fPhase); + pNode->fCompl1 ^= 1; + } + *countFlip = *countFlip + 1; + } + Abc_NtkDfsInvSup_rec( Abc_ObjFanin0Ntk(pFanin), vSup, countFlip ); + } +} + /**Function************************************************************* Synopsis [Returns the DFS ordered array of logic nodes.] diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 44ceacc880..a00315e3b4 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -149,6 +149,7 @@ static int Abc_CommandRunEco ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandRunGen ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRunScript ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRunTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandRmInverter ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1008,6 +1009,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Synthesis", "resub_unate", Abc_CommandResubUnate, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "resub_core", Abc_CommandResubCore, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "resub_check", Abc_CommandResubCheck, 0 ); + Cmd_CommandAdd( pAbc, "Synthesis", "rd_inv", Abc_CommandRmInverter, 1 ); // Cmd_CommandAdd( pAbc, "Synthesis", "rr", Abc_CommandRr, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "cascade", Abc_CommandCascade, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "lutcasdec", Abc_CommandLutCasDec, 1 ); @@ -7995,7 +7997,58 @@ int Abc_CommandRunTest( Abc_Frame_t * pAbc, int argc, char ** argv ) Synopsis [] - Description [Orchestration synthesis] + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandRmInverter( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); + Extra_UtilGetoptReset(); + int iVerbose = 0; + int c; + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + iVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + Abc_Print( -1, "Empty network.\n" ); + return 1; + } + if ( !Abc_NtkHasAig(pNtk) || !Abc_NtkIsStrash(pNtk) ) + { + Abc_Print( -1, "This command only works on AIG network.\n" ); + return 1; + } + Abc_NtkRmInverter(pNtk, iVerbose); + return 0; + +usage: + Abc_Print( -2, "usage: rd_inv\n" ); + Abc_Print( -2, "\t redistribute inverters on self-dual and self-anti-dual functions in network\n" ); + Abc_Print( -2, "\t-v : verbose output\n"); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] SideEffects [] diff --git a/src/base/abci/abcRmInverters.c b/src/base/abci/abcRmInverters.c new file mode 100644 index 0000000000..2d25d94231 --- /dev/null +++ b/src/base/abci/abcRmInverters.c @@ -0,0 +1,853 @@ +/**CFile**************************************************************** + + FileName [abcRmInverters.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Remove/Redistribute inverted edges on AIG nodes.] + + Author [Jingren Wang] + + Affiliation [HKUST(GZ)] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcRmInverters.c,v 1.00 2005/06/20 00:00:00 jingren Exp $] + +***********************************************************************/ + +#include "aig/aig/aig.h" +#include "base/abc/abc.h" +#include "misc/util/abc_global.h" +#include "misc/vec/vecInt.h" +#include "misc/vec/vecPtr.h" +#include "opt/cut/cut.h" + +ABC_NAMESPACE_IMPL_START + +#define RDINV_SIM_SIZE 100 + +static unsigned int uMask[] = { 0x1, 0x3, 0xF, 0xFF, 0xFFFF, 0xFFFFFFFF }; + +extern void Abc_NtkMarkCriticalNodes( Abc_Ntk_t * pNtk ); + +/**Function************************************************************* + + Synopsis [Collect cut leaves into a Vec_Ptr.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Vec_Ptr_t * Abc_RdInvCollectCutLeaves( Abc_Ntk_t * pNtk, Cut_Cut_t * pCut ) +{ + Vec_Ptr_t * vLeaves = Vec_PtrAlloc( pCut->nLeaves ); + for ( int li = 0; li < pCut->nLeaves; li++ ) + Vec_PtrPush( vLeaves, Abc_NtkObj(pNtk, Cut_CutReadLeaves(pCut)[li]) ); + return vLeaves; +} + +/**Function************************************************************* + + Synopsis [Detect if function is self-dual.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int AbcRmInvHasSelfDual( unsigned int uTruth, int fPhaseOri, unsigned int uTruthFlipped, int fPhaseFlipped, unsigned int uMsk ) +{ + return (uTruth == uTruthFlipped && (fPhaseOri ^ fPhaseFlipped) == 1) || + (uTruth == (~uTruthFlipped & uMsk) && fPhaseOri == fPhaseFlipped); +} + +/**Function************************************************************* + + Synopsis [Detect if function is self-anti-dual.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int AbcRmInvHasSelfAntiDual( unsigned int uTruth, int fPhaseOri, unsigned int uTruthFlipped, int fPhaseFlipped, unsigned int uMsk ) +{ + return (uTruth == uTruthFlipped && fPhaseOri == fPhaseFlipped) || + (uTruth == (~uTruthFlipped & uMsk) && (fPhaseOri ^ fPhaseFlipped) == 1); +} + +/**Function************************************************************* + + Synopsis [Collect MFFC with support variables and internal nodes.] + + Description [] + + SideEffects [] + + SeeAlso [abcMffc.c] + +***********************************************************************/ +void Abc_NodeMffcConeSuppCollect( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp, int iVerbose ) +{ + Abc_Obj_t * pObj; + int i; + Abc_NodeDeref_rec( pNode ); + Abc_NodeMffcConeSupp( pNode, vCone, vSupp ); + Abc_NodeRef_rec( pNode ); + if ( iVerbose ) + { + printf( "Node = %6s : Supp = %3d Cone = %3d (", + Abc_ObjName(pNode), Vec_PtrSize(vSupp), Vec_PtrSize(vCone) ); + Vec_PtrForEachEntry( Abc_Obj_t *, vCone, pObj, i ) + printf( " %s", Abc_ObjName(pObj) ); + printf( " )\n" ); + printf("vSupp = ("); + Vec_PtrForEachEntry( Abc_Obj_t *, vSupp, pObj, i ) + printf( " %s", Abc_ObjName(pObj) ); + printf( " )\n" ); + } +} + +/**Function************************************************************* + + Synopsis [Get inverter count on support variables for self-anti-dual case.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkRmInverterCountInvRatioSelfAntiDual( Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp, int * nLocalInv, int * nLocalInvOnCritical, int * nLocalNonInvOnCritical, int * nLocalSup ) +{ + Abc_Obj_t * pObj, * pFanin; + int i_cone, i_fanin; + Vec_PtrForEachEntry( Abc_Obj_t *, vCone, pObj, i_cone ) + { + Abc_ObjForEachFanin( pObj, pFanin, i_fanin ) + { + if ( Vec_PtrFind(vSupp, pFanin) < 0 ) + continue; + if ( (i_fanin == 0 && pObj->fCompl0) || (i_fanin == 1 && pObj->fCompl1) ) + (*nLocalInv)++; + if ( (i_fanin == 0 && pObj->fCompl0 && pFanin->fMarkA) || (i_fanin == 1 && pObj->fCompl1 && pFanin->fMarkA) ) + (*nLocalInvOnCritical)++; + if ( (i_fanin == 0 && !pObj->fCompl0 && pFanin->fMarkA) || (i_fanin == 1 && !pObj->fCompl1 && pFanin->fMarkA) ) + (*nLocalNonInvOnCritical)++; + (*nLocalSup)++; + } + } +} + +/**Function************************************************************* + + Synopsis [Get inverter count on support variables for self-dual case.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkRmInverterCountInvRatioSelfDual( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp, int * nLocalInv, int * nLocalInvOnCritical, int * nLocalNonInvOnCritical, int * nLocalSup ) +{ + Abc_Obj_t * pFanout; + int i; + Abc_NtkRmInverterCountInvRatioSelfAntiDual( vCone, vSupp, nLocalInv, nLocalInvOnCritical, nLocalNonInvOnCritical, nLocalSup ); + Abc_ObjForEachFanout( pNode, pFanout, i ) + { + int fCompl = (Abc_ObjFanin0(pFanout) == pNode) ? pFanout->fCompl0 : pFanout->fCompl1; + *nLocalInv += fCompl; + int fIsCritical = (Abc_ObjFanin0(pFanout) == pNode) + ? (Abc_ObjFanin0(pFanout)->fMarkA == 1) + : (Abc_ObjFanin1(pFanout)->fMarkA == 1); + if ( fCompl && fIsCritical ) + (*nLocalInvOnCritical)++; + else if ( !fCompl && fIsCritical ) + (*nLocalNonInvOnCritical)++; + (*nLocalSup)++; + } +} + +/**Function************************************************************* + + Synopsis [Flip inverters on self-anti-dual function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkRmInverterFlipInvSelfAntiDual( Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp ) +{ + Abc_Obj_t * pObj, * pFanin; + int i_cone, i_fanin; + Vec_PtrForEachEntry( Abc_Obj_t *, vCone, pObj, i_cone ) + { + Abc_ObjForEachFanin( pObj, pFanin, i_fanin ) + { + if ( Vec_PtrFind(vSupp, pFanin) < 0 ) + continue; + if ( i_fanin == 0 ) + pObj->fCompl0 ^= 1; + else if ( i_fanin == 1 ) + pObj->fCompl1 ^= 1; + } + } +} + +/**Function************************************************************* + + Synopsis [Flip inverters on self-dual function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkRmInverterFlipInvSelfDual( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp ) +{ + Abc_Obj_t * pFanout; + int i; + Abc_NtkRmInverterFlipInvSelfAntiDual( vCone, vSupp ); + Abc_ObjForEachFanout( pNode, pFanout, i ) + { + Abc_ObjFanin0(pFanout) == pNode ? (pFanout->fCompl0 ^= 1) : (pFanout->fCompl1 ^= 1); + } +} + +/**Function************************************************************* + + Synopsis [Simulate AIG nodes and compute truth tables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_ManResubSimulateComp( Vec_Ptr_t * vDivs, int nLeaves, Vec_Ptr_t * vSims, int nLeavesMax, int nWords ) +{ + Abc_Obj_t * pObj; + unsigned * puData0, * puData1, * puData; + int i, k; + assert( Vec_PtrSize(vDivs) - nLeaves <= Vec_PtrSize(vSims) - nLeavesMax ); + Vec_PtrForEachEntry( Abc_Obj_t *, vDivs, pObj, i ) + { + if ( i < nLeaves ) + { + pObj->pDataComp = Vec_PtrEntry( vSims, i ); + continue; + } + pObj->pDataComp = Vec_PtrEntry( vSims, i - nLeaves + nLeavesMax ); + puData = (unsigned *)pObj->pDataComp; + puData0 = (unsigned *)Abc_ObjFanin0(pObj)->pDataComp; + puData1 = (unsigned *)Abc_ObjFanin1(pObj)->pDataComp; + if ( Abc_ObjFaninC0(pObj) && Abc_ObjFaninC1(pObj) ) + for ( k = 0; k < nWords; k++ ) + puData[k] = ~puData0[k] & ~puData1[k]; + else if ( Abc_ObjFaninC0(pObj) ) + for ( k = 0; k < nWords; k++ ) + puData[k] = ~puData0[k] & puData1[k]; + else if ( Abc_ObjFaninC1(pObj) ) + for ( k = 0; k < nWords; k++ ) + puData[k] = puData0[k] & ~puData1[k]; + else + for ( k = 0; k < nWords; k++ ) + puData[k] = puData0[k] & puData1[k]; + } + Vec_PtrForEachEntry( Abc_Obj_t *, vDivs, pObj, i ) + { + puData = (unsigned *)pObj->pDataComp; + pObj->fPhase = (puData[0] & 1); + if ( pObj->fPhase ) + for ( k = 0; k < nWords; k++ ) + puData[k] = ~puData[k]; + } +} + +/**Function************************************************************* + + Synopsis [Clean pDataComp on cone nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkCleanDataComp( Vec_Ptr_t * vCone ) +{ + Abc_Obj_t * pObj; + int i; + Vec_PtrForEachEntry( Abc_Obj_t *, vCone, pObj, i ) + pObj->pDataComp = NULL; +} + +/**Function************************************************************* + + Synopsis [Simulate a cut to extract truth + phase for one polarity.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void AbcRmInvSimCuts( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, Cut_Cut_t * pCut, int nMaxLeaves, unsigned int * uNodeVal, int * fPhaseFlipped, unsigned int * pInfo, Vec_Ptr_t * vSims ) +{ + Abc_Obj_t * pObj; + int nVar = pCut->nLeaves; + int nBits = (1 << nVar); + int nWords = (nBits <= 32) ? 1 : (nBits / 32); + + Vec_Ptr_t * vCone = Vec_PtrAlloc( pCut->nLeaves + 16 ); + Vec_Ptr_t * vSup = Vec_PtrAlloc( pCut->nLeaves ); + for ( int li = 0; li < pCut->nLeaves; li++ ) + { + pObj = Abc_NtkObj( pNtk, Cut_CutReadLeaves(pCut)[li] ); + Vec_PtrPush( vSup, pObj ); + Vec_PtrPush( vCone, pObj ); + } + assert( Vec_PtrSize(vSup) == pCut->nLeaves ); + + Abc_NtkIncrementTravId( pNtk ); + Abc_NtkDfsSup_rec( pNode, vCone, vSup, 0 ); + assert( Vec_PtrSize(vCone) > pCut->nLeaves ); + + Vec_Int_t * vPh = Vec_IntAlloc( Vec_PtrSize(vCone) ); + Abc_Obj_t * pEntry; + int iPh; + Vec_PtrForEachEntry( Abc_Obj_t *, vCone, pEntry, iPh ) + Vec_IntPush( vPh, pEntry->fPhase ); + + Abc_ManResubSimulateComp( vCone, nVar, vSims, nMaxLeaves, nWords ); + unsigned int uNode = (*((unsigned int *)(pNode->pDataComp))); + *uNodeVal = uNode & uMask[nVar]; + *fPhaseFlipped = pNode->fPhase; + + Abc_NtkCleanDataComp( vCone ); + + Vec_PtrForEachEntry( Abc_Obj_t *, vCone, pEntry, iPh ) + pEntry->fPhase = Vec_IntEntry( vPh, iPh ); + + Vec_IntFree( vPh ); + Vec_PtrFree( vCone ); + Vec_PtrFree( vSup ); +} + +/**Function************************************************************* + + Synopsis [Compute original and flipped truth/phase pair for a cut.] + + Description [Allocates and frees simulation arrays internally. + Returns 1 on success, 0 if cut is too large.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void Abc_RdInvComputeTruthPair( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, Cut_Cut_t * pCut, + unsigned * uTruthOri, int * fPhaseOri, + unsigned * uTruthFlipped, int * fPhaseFlipped ) +{ + int nVar = pCut->nLeaves; + int nBits = (1 << nVar); + int nWords = (nBits <= 32) ? 1 : (nBits / 32); + int in, k; + + Vec_Ptr_t * vSims = Vec_PtrAlloc( RDINV_SIM_SIZE ); + unsigned int *pInfo = ABC_ALLOC( unsigned, nWords * (RDINV_SIM_SIZE + 1) ); + for ( in = 0; in < RDINV_SIM_SIZE; in++ ) + Vec_PtrPush( vSims, pInfo + in * nWords ); + + for ( k = 0; k < nVar; k++ ) + { + unsigned * pData = (unsigned *)vSims->pArray[k]; + Abc_InfoClear( pData, nWords ); + for ( in = 0; in < nBits; in++ ) + if ( in & (1 << k) ) + pData[in >> 5] |= (1 << (in & 31)); + } + AbcRmInvSimCuts( pNtk, pNode, pCut, 5, uTruthOri, fPhaseOri, pInfo, vSims ); + Vec_PtrFree( vSims ); + ABC_FREE( pInfo ); + + vSims = Vec_PtrAlloc( RDINV_SIM_SIZE ); + pInfo = ABC_ALLOC( unsigned, nWords * (RDINV_SIM_SIZE + 1) ); + for ( in = 0; in < RDINV_SIM_SIZE; in++ ) + Vec_PtrPush( vSims, pInfo + in * nWords ); + + for ( k = 0; k < nVar; k++ ) + { + unsigned * pData = (unsigned *)vSims->pArray[k]; + Abc_InfoClear( pData, nWords ); + for ( in = 0; in < nBits; in++ ) + if ( !(in & (1 << k)) ) + pData[in >> 5] |= (1 << (in & 31)); + } + AbcRmInvSimCuts( pNtk, pNode, pCut, 5, uTruthFlipped, fPhaseFlipped, pInfo, vSims ); + Vec_PtrFree( vSims ); + ABC_FREE( pInfo ); + + assert( (*uTruthOri & uMask[nVar]) == *uTruthOri ); + assert( (*uTruthFlipped & uMask[nVar]) == *uTruthFlipped ); +} + +/**Function************************************************************* + + Synopsis [Check if cut is self-dual.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkRmInvCutIsSelfDual( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, Cut_Cut_t * pCut ) +{ + unsigned uTruthOri, uTruthFlipped; + int fPhaseOri, fPhaseFlipped; + Abc_RdInvComputeTruthPair( pNtk, pNode, pCut, &uTruthOri, &fPhaseOri, &uTruthFlipped, &fPhaseFlipped ); + return AbcRmInvHasSelfDual( uTruthOri, fPhaseOri, uTruthFlipped, fPhaseFlipped, uMask[pCut->nLeaves] ); +} + +/**Function************************************************************* + + Synopsis [Check if cut is self-anti-dual.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkRmInvCutIsSelfAntiDual( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, Cut_Cut_t * pCut ) +{ + unsigned uTruthOri, uTruthFlipped; + int fPhaseOri, fPhaseFlipped; + Abc_RdInvComputeTruthPair( pNtk, pNode, pCut, &uTruthOri, &fPhaseOri, &uTruthFlipped, &fPhaseFlipped ); + return AbcRmInvHasSelfAntiDual( uTruthOri, fPhaseOri, uTruthFlipped, fPhaseFlipped, uMask[pCut->nLeaves] ); +} + +/**Function************************************************************* + + Synopsis [Get valid cuts of self-dual and self-anti-dual.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void AbcRmInvAvaCuts( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, Cut_Man_t * pCutMan, Vec_Ptr_t * vASDCuts, Vec_Ptr_t * vASADCuts, int iVerbose ) +{ + int nCuts = 0; + Vec_Ptr_t * vCutsPreSD = Vec_PtrAlloc( 16 ); + Vec_Ptr_t * vCutsPreSAD = Vec_PtrAlloc( 16 ); + Cut_Cut_t * pCut; + pCut = (Cut_Cut_t *)Abc_NodeGetCutsRecursive( pCutMan, pNode, 0, 1 ); + if ( pCut == NULL ) + { + printf("Warning: Abc_NodeGetCutsRecursive returned NULL for node %d\n", Abc_ObjId(pNode)); + Vec_PtrFree( vCutsPreSD ); + Vec_PtrFree( vCutsPreSAD ); + return; + } + for ( pCut = pCut->pNext; pCut; pCut = pCut->pNext ) + { + if ( Abc_NtkRmInvCutIsSelfDual(pNtk, pNode, pCut) ) + Vec_PtrPush( vCutsPreSD, pCut ); + if ( Abc_NtkRmInvCutIsSelfAntiDual(pNtk, pNode, pCut) ) + Vec_PtrPush( vCutsPreSAD, pCut ); + nCuts++; + } + Vec_PtrCopy( vASADCuts, vCutsPreSAD ); + Vec_PtrCopy( vASDCuts, vCutsPreSD ); + if ( iVerbose ) + { + printf(" %d cuts have been found and processed.\n", nCuts); + printf(" Retrieved %d(%d) of cuts in self-anti-dual and %d(%d) of cuts in self-dual.\n", + Vec_PtrSize(vASADCuts), Vec_PtrSize(vCutsPreSAD), + Vec_PtrSize(vASDCuts), Vec_PtrSize(vCutsPreSD)); + } + Vec_PtrFree( vCutsPreSD ); + Vec_PtrFree( vCutsPreSAD ); +} + +/**Function************************************************************* + + Synopsis [Show cut structure for verbose output.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_RmInvShowCutStructure( Abc_Ntk_t * pNtk, Abc_Obj_t * pRoot, Cut_Cut_t * pCut ) +{ + Vec_Ptr_t * vCone = Vec_PtrAlloc( pCut->nLeaves + 16 ); + Vec_Ptr_t * vSup = Abc_RdInvCollectCutLeaves( pNtk, pCut ); + int li; + for ( li = 0; li < pCut->nLeaves; li++ ) + Vec_PtrPush( vCone, Abc_NtkObj(pNtk, Cut_CutReadLeaves(pCut)[li]) ); + Abc_NtkIncrementTravId( pNtk ); + Abc_NtkDfsSup_rec( pRoot, vCone, vSup, 1 ); + Vec_PtrFree( vSup ); + Vec_PtrFree( vCone ); +} + +/**Function************************************************************* + + Synopsis [Retrieve max level slack.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void AbcRmInvFetchMaxLSlack( Abc_Ntk_t * pNtk, int * iLSM ) +{ + int i = 0; + Abc_Obj_t * pNode; + Vec_Int_t * vLS = Vec_IntAlloc( Abc_NtkNodeNum(pNtk) ); + Abc_NtkForEachNode( pNtk, pNode, i ) + { + int item = Abc_ObjRequiredLevel(pNode) - pNode->Level; + Vec_IntPush( vLS, item ); + } + Vec_IntSort( vLS, 1 ); + assert( Vec_IntEntry(vLS, 0) >= Vec_IntEntry(vLS, Vec_IntSize(vLS) - 1) ); + *iLSM = Vec_IntEntry( vLS, 0 ); + Vec_IntFree( vLS ); +} + +/**Function********************************************************* + + Synopsis [Retrieve critical and near-critical edges count.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void AbcRmInvCollectNCE( Abc_Ntk_t * pNtk, int iThreshold, int * iCount ) +{ + Abc_Obj_t * pNode, * pFanin, * pPo; + int i, j, k; + Abc_NtkForEachNode( pNtk, pNode, i ) + { + if ( Abc_ObjRequiredLevel(pNode) - pNode->Level <= iThreshold ) + { + Abc_ObjForEachFanin( pNode, pFanin, j ) + { + *iCount += (j == 0) ? pNode->fCompl0 : pNode->fCompl1; + } + } + } + Abc_NtkForEachPo( pNtk, pPo, k ) + { + Abc_Obj_t * pNodeToPo = Abc_ObjFanin0(pPo); + if ( pPo->fCompl0 && Abc_ObjIsNode(pNodeToPo) && (Abc_ObjRequiredLevel(pNodeToPo) - pNodeToPo->Level <= iThreshold) ) + (*iCount)++; + } +} + +/**Function************************************************************* + + Synopsis [Use markB to record level slack, markA for critical flag.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkMarkCriticalNodesScale( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pNode; + int i, Counter = 0; + Abc_NtkForEachNode( pNtk, pNode, i ) + { + if ( Abc_ObjRequiredLevel(pNode) - pNode->Level <= 1 ) + { + pNode->fMarkA = 1; + pNode->fMarkB = Abc_ObjRequiredLevel(pNode) - pNode->Level; + Counter++; + } + } + printf( "The number of nodes on the critical paths = %6d (%5.2f %%)\n", Counter, 100.0 * Counter / Abc_NtkNodeNum(pNtk) ); +} + +/**Function************************************************************* + + Synopsis [Record sum of slack with inverted edges.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkCollectInvRelatedSlack( Abc_Ntk_t * pNtk, int * invSlack ) +{ + Abc_Obj_t * pNode, * pFanin; + int i, j; + Abc_NtkForEachNode( pNtk, pNode, i ) + { + Abc_ObjForEachFanin( pNode, pFanin, j ) + { + if ( j == 0 && pNode->fCompl0 == 1 ) + (*invSlack) += pFanin->fMarkB; + if ( j == 1 && pNode->fCompl1 == 1 ) + (*invSlack) += pFanin->fMarkB; + } + } +} + +/**Function************************************************************* + + Synopsis [Process cuts: evaluate gain condition and flip if beneficial.] + + Description [Shared logic for self-anti-dual and self-dual cut processing. + fIsSelfDual=0 treats SAD; fIsSelfDual=1 treats SD.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void Abc_RdInvProcessCuts( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, + Vec_Ptr_t * vCone, Vec_Ptr_t * vCuts, int fIsSelfDual, + int * nCountCritical, int * nCountNonCritical, int * nCount, int iVerbose ) +{ + Cut_Cut_t * pCut; + int i; + Vec_PtrForEachEntry( Cut_Cut_t *, vCuts, pCut, i ) + { + int nLocalInv = 0; + int nLocalSup = 0; + int nLocalInvOnCritical = 0; + int nLocalNonInvOnCritical = 0; + + Vec_Ptr_t * vSupCuts = Abc_RdInvCollectCutLeaves( pNtk, pCut ); + + if ( fIsSelfDual ) + Abc_NtkRmInverterCountInvRatioSelfDual( pNode, vCone, vSupCuts, &nLocalInv, &nLocalInvOnCritical, &nLocalNonInvOnCritical, &nLocalSup ); + else + Abc_NtkRmInverterCountInvRatioSelfAntiDual( vCone, vSupCuts, &nLocalInv, &nLocalInvOnCritical, &nLocalNonInvOnCritical, &nLocalSup ); + + int fCheckCritical = (nLocalInvOnCritical > nLocalNonInvOnCritical); + int fCheckNonCritical = (nLocalInvOnCritical == 0 && nLocalNonInvOnCritical == 0 && nLocalSup > 0 && (float)nLocalInv / nLocalSup >= 0.5); + + if ( fCheckCritical || fCheckNonCritical ) + { + if ( fCheckCritical ) + (*nCountCritical)++; + if ( fCheckNonCritical ) + (*nCountNonCritical)++; + + if ( iVerbose ) + Abc_RmInvShowCutStructure( pNtk, pNode, pCut ); + + if ( fIsSelfDual ) + Abc_NtkRmInverterFlipInvSelfDual( pNode, vCone, vSupCuts ); + else + Abc_NtkRmInverterFlipInvSelfAntiDual( vCone, vSupCuts ); + + (*nCount)++; + } + Vec_PtrFree( vSupCuts ); + } +} + +/**Function************************************************************* + + Synopsis [Gain-based inverter removal.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkRmInverter( Abc_Ntk_t * pNtk, int iVerbose ) +{ + int i; + Abc_Obj_t * pNode, * pObj; + + if ( !Abc_NtkIsStrash(pNtk) ) + { + printf("Error: Abc_NtkRmInverter requires a strashed AIG network.\n"); + printf("Current network type: %d\n", pNtk->ntkType); + return; + } + if ( iVerbose ) + { + printf("Processing strashed AIG network with %d nodes, %d PIs, %d POs\n", + Abc_NtkNodeNum(pNtk), Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk)); + printf("Network level: %d\n", Abc_NtkLevel(pNtk)); + } + + Abc_NtkStartReverseLevels( pNtk, 0 ); + Abc_NtkMarkCriticalNodesScale( pNtk ); + + Abc_NtkForEachNode( pNtk, pNode, i ) + { + if ( Abc_AigNodeIsChoice(pNode) ) + { + Abc_Obj_t * pCurTempNode = (Abc_Obj_t *)pNode->pData; + while ( pCurTempNode != NULL ) + { + pCurTempNode->fMarkA = 1; + pCurTempNode->fMarkB = pNode->fMarkB; + pCurTempNode = (Abc_Obj_t *)pCurTempNode->pData; + } + } + } + + int iNCEBefore = 0; + int iNCEAfter = 0; + int invSlackBefore = 0; + int invSlackAfter = 0; + int iLSM = 0; + AbcRmInvFetchMaxLSlack( pNtk, &iLSM ); + int iThreshold = iLSM; + AbcRmInvCollectNCE( pNtk, iThreshold, &iNCEBefore ); + Abc_NtkCollectInvRelatedSlack( pNtk, &invSlackBefore ); + + int nCountCriticalSAD = 0; + int nCountNonCriticalSAD = 0; + int nCountSAD = 0; + int nCountCriticalSD = 0; + int nCountNonCriticalSD = 0; + int nCountSD = 0; + int nTotalNodes = Abc_NtkNodeNum(pNtk); + int nProcessed = 0; + + { + Cut_Man_t * pCutMan; + Cut_Params_t Params, * pParams = &Params; + memset( pParams, 0, sizeof(Cut_Params_t) ); + pParams->nVarsMax = 5; + pParams->nKeepMax = 250; + pParams->fTruth = 1; + pParams->fFilter = 1; + pParams->fSeq = 0; + pParams->fLocal = 0; + pParams->fGlobal = 0; + pParams->fTree = 1; + pParams->fDrop = 0; + pParams->fVerbose = 1; + pParams->nIdsMax = Abc_NtkObjNumMax( pNtk ); + pCutMan = Cut_ManStart( pParams ); + + int j_ci; + Abc_NtkForEachCi( pNtk, pObj, j_ci ) + if ( Abc_ObjFanoutNum(pObj) > 0 ) + Cut_NodeSetTriv( pCutMan, pObj->Id ); + + Abc_NtkForEachNode( pNtk, pNode, i ) + { + if ( Abc_ObjFanoutNum(pNode) == 1 && pNode->pData != NULL ) + continue; + + Vec_Ptr_t * vCone = Vec_PtrAlloc( 16 ); + Vec_Ptr_t * vSupp = Vec_PtrAlloc( 16 ); + + if ( iVerbose ) + printf("\n\n\n"); + + Abc_NodeMffcConeSuppCollect( pNode, vCone, vSupp, iVerbose ); + + int i_sup; + Vec_PtrForEachEntryReverse( Abc_Obj_t *, vSupp, pObj, i_sup ) + Vec_PtrInsert( vCone, 0, pObj ); + + if ( iVerbose ) + printf("Support var size %d, internal node size %d\n", Vec_PtrSize(vSupp), Vec_PtrSize(vCone)); + + Vec_Ptr_t * vASDCuts = Vec_PtrAlloc( 16 ); + Vec_Ptr_t * vASADCuts = Vec_PtrAlloc( 16 ); + + AbcRmInvAvaCuts( pNtk, pNode, pCutMan, vASDCuts, vASADCuts, iVerbose ); + + int nSADBefore = nCountSAD; + Abc_RdInvProcessCuts( pNtk, pNode, vCone, vASADCuts, 0, + &nCountCriticalSAD, &nCountNonCriticalSAD, &nCountSAD, iVerbose ); + + int nSDBefore = nCountSD; + Abc_RdInvProcessCuts( pNtk, pNode, vCone, vASDCuts, 1, + &nCountCriticalSD, &nCountNonCriticalSD, &nCountSD, iVerbose ); + + if ( nCountSAD > nSADBefore || nCountSD > nSDBefore ) + nProcessed++; + + Vec_PtrFree( vASADCuts ); + Vec_PtrFree( vASDCuts ); + Vec_PtrFree( vCone ); + Vec_PtrFree( vSupp ); + } + Cut_ManStop( pCutMan ); + } + + AbcRmInvCollectNCE( pNtk, iThreshold, &iNCEAfter ); + Abc_NtkCollectInvRelatedSlack( pNtk, &invSlackAfter ); + + if ( iVerbose ) + { + printf("=====Statistics about invNum with Threshold %d=====\n", iThreshold); + printf("Before %d After %d Gain %d \n", iNCEBefore, iNCEAfter, iNCEBefore - iNCEAfter); + if ( iNCEAfter > 0 || iNCEBefore > 0 ) + printf("=====Statistics about edges that ease on slack=====\n" + "Ease Gain %f \n", (float)invSlackAfter / (iNCEAfter ? iNCEAfter : 1) - (float)invSlackBefore / (iNCEBefore ? iNCEBefore : 1)); + } + + Abc_NtkStopReverseLevels( pNtk ); + Abc_NtkCleanMarkAB( pNtk ); + + assert( nCountCriticalSAD + nCountNonCriticalSAD == nCountSAD ); + assert( nCountCriticalSD + nCountNonCriticalSD == nCountSD ); + + printf("Total %d self-anti-dual functions", nCountSAD); + if ( nCountSAD > 0 ) + printf(", Critical(%f), Non-critical(%f)", (float)nCountCriticalSAD / nCountSAD, (float)nCountNonCriticalSAD / nCountSAD); + printf(" / %d self-dual are modified", nCountSD); + if ( nCountSD > 0 ) + printf(", Critical(%f), Non-critical(%f)", (float)nCountCriticalSD / nCountSD, (float)nCountNonCriticalSD / nCountSD); + printf(". Total process rate %f\n", nTotalNodes > 0 ? (float)nProcessed / nTotalNodes : 0.0f); +} + +ABC_NAMESPACE_IMPL_END diff --git a/src/base/abci/module.make b/src/base/abci/module.make index fe063a42ae..5891071dd8 100644 --- a/src/base/abci/module.make +++ b/src/base/abci/module.make @@ -49,6 +49,7 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcProve.c \ src/base/abci/abcQbf.c \ src/base/abci/abcQuant.c \ + src/base/abci/abcRmInverters.c \ src/base/abci/abcRec3.c \ src/base/abci/abcReconv.c \ src/base/abci/abcReach.c \