diff options
| -rw-r--r-- | abc.dsp | 20 | ||||
| -rw-r--r-- | src/aig/aig/aig.h | 7 | ||||
| -rw-r--r-- | src/aig/aig/aigPart.c | 8 | ||||
| -rw-r--r-- | src/aig/aig/aigRepr.c | 19 | ||||
| -rw-r--r-- | src/aig/aig/aigTest.c | 35 | ||||
| -rw-r--r-- | src/aig/aig/aigUtil.c | 4 | ||||
| -rw-r--r-- | src/aig/dch/dch.h | 6 | ||||
| -rw-r--r-- | src/aig/dch/dchAig.c | 76 | ||||
| -rw-r--r-- | src/aig/dch/dchChoice.c | 306 | ||||
| -rw-r--r-- | src/aig/dch/dchClass.c | 585 | ||||
| -rw-r--r-- | src/aig/dch/dchCnf.c | 277 | ||||
| -rw-r--r-- | src/aig/dch/dchCore.c | 41 | ||||
| -rw-r--r-- | src/aig/dch/dchInt.h | 108 | ||||
| -rw-r--r-- | src/aig/dch/dchMan.c | 115 | ||||
| -rw-r--r-- | src/aig/dch/dchSat.c | 101 | ||||
| -rw-r--r-- | src/aig/dch/dchSim.c | 238 | ||||
| -rw-r--r-- | src/aig/dch/dchSweep.c | 262 | ||||
| -rw-r--r-- | src/aig/dch/module.make | 6 | ||||
| -rw-r--r-- | src/aig/int/intM114.c | 2 | ||||
| -rw-r--r-- | src/aig/int/intM114p.c | 5 | ||||
| -rw-r--r-- | src/aig/ntl/ntlFraig.c | 8 | ||||
| -rw-r--r-- | src/aig/ntl/ntlWriteBlif.c | 4 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 19 | ||||
| -rw-r--r-- | src/base/abci/abcDar.c | 21 |
24 files changed, 1999 insertions, 274 deletions
@@ -2930,6 +2930,10 @@ SOURCE=.\src\aig\aig\aigTable.c # End Source File # Begin Source File +SOURCE=.\src\aig\aig\aigTest.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\aig\aigTiming.c # End Source File # Begin Source File @@ -3286,6 +3290,18 @@ SOURCE=.\src\aig\dch\dchAig.c # End Source File # Begin Source File +SOURCE=.\src\aig\dch\dchChoice.c +# End Source File +# Begin Source File + +SOURCE=.\src\aig\dch\dchClass.c +# End Source File +# Begin Source File + +SOURCE=.\src\aig\dch\dchCnf.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\dch\dchCore.c # End Source File # Begin Source File @@ -3304,6 +3320,10 @@ SOURCE=.\src\aig\dch\dchSat.c SOURCE=.\src\aig\dch\dchSim.c # End Source File +# Begin Source File + +SOURCE=.\src\aig\dch\dchSweep.c +# End Source File # End Group # End Group # End Group diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index ef821d12..baba9707 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -102,8 +102,8 @@ struct Aig_Man_t_ Aig_Obj_t * pConst1; // the constant 1 node Aig_Obj_t Ghost; // the ghost node int nRegs; // the number of registers (registers are last POs) - int nTruePis; // the number of registers (registers are last POs) - int nTruePos; // the number of registers (registers are last POs) + int nTruePis; // the number of true primary inputs + int nTruePos; // the number of true primary outputs int nAsserts; // the number of asserts among POs (asserts are first POs) // AIG node counters int nObjs[AIG_OBJ_VOID];// the number of objects by type @@ -326,8 +326,9 @@ static inline void Aig_ObjClean( Aig_Obj_t * pObj ) { memset( pObj static inline Aig_Obj_t * Aig_ObjFanout0( Aig_Man_t * p, Aig_Obj_t * pObj ) { assert(p->pFanData && pObj->Id < p->nFansAlloc); return Aig_ManObj(p, p->pFanData[5*pObj->Id] >> 1); } static inline Aig_Obj_t * Aig_ObjEquiv( Aig_Man_t * p, Aig_Obj_t * pObj ) { return p->pEquivs? p->pEquivs[pObj->Id] : NULL; } static inline Aig_Obj_t * Aig_ObjRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return p->pReprs? p->pReprs[pObj->Id] : NULL; } +static inline void Aig_ObjSetRepr( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr ) { assert(p->pReprs); p->pReprs[pObj->Id] = pRepr; } static inline Aig_Obj_t * Aig_ObjHaig( Aig_Obj_t * pObj ) { assert( Aig_Regular(pObj)->pHaig ); return Aig_NotCond( Aig_Regular(pObj)->pHaig, Aig_IsComplement(pObj) ); } -static inline int Aig_ObjPioNum( Aig_Obj_t * pObj ) { assert( !Aig_ObjIsNode(pObj) ); return (int)(PORT_PTRINT_T)pObj->pNext; } +static inline int Aig_ObjPioNum( Aig_Obj_t * pObj ) { assert( !Aig_ObjIsNode(pObj) ); return (int)(PORT_PTRINT_T)pObj->pNext; } static inline int Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin ) { if ( Aig_ObjFanin0(pObj) == pFanin ) return 0; diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c index d9ec616a..aca07bd9 100644 --- a/src/aig/aig/aigPart.c +++ b/src/aig/aig/aigPart.c @@ -259,7 +259,7 @@ Vec_Int_t * Part_ManTransferEntry( Part_One_t * p ) Synopsis [Computes supports of the POs in the multi-output AIG.] Description [Returns the array of integer arrays containing indices - of the primary inputsf or each primary output.] + of the primary inputs for each primary output.] SideEffects [Adds the integer PO number at end of each array.] @@ -1417,7 +1417,7 @@ Aig_Man_t * Aig_ManFraigPartitioned( Aig_Man_t * pAig, int nPartSize, int nConfM SeeAlso [] ***********************************************************************/ -static inline void Aig_ObjSetRepr( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 ) +static inline void Aig_ObjSetRepr_( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 ) { assert( p->pReprs != NULL ); assert( !Aig_IsComplement(pNode1) ); @@ -1481,14 +1481,14 @@ void Aig_ManChoiceConstructiveOne( Aig_Man_t * pNew, Aig_Man_t * pPrev, Aig_Man_ if ( pObj->pHaig == NULL ) continue; // pObj->pData and pObj->pHaig->pData are equivalent - Aig_ObjSetRepr( pNew, Aig_Regular(pObj->pData), Aig_Regular(pObj->pHaig->pData) ); + Aig_ObjSetRepr_( pNew, Aig_Regular(pObj->pData), Aig_Regular(pObj->pHaig->pData) ); } // set the inputs of POs as equivalent Aig_ManForEachPo( pThis, pObj, i ) { pObjNew = Aig_ObjFanin0( Aig_ManPo(pNew,i) ); // pObjNew and Aig_ObjFanin0(pObj)->pData are equivalent - Aig_ObjSetRepr( pNew, pObjNew, Aig_Regular(Aig_ObjFanin0(pObj)->pData) ); + Aig_ObjSetRepr_( pNew, pObjNew, Aig_Regular(Aig_ObjFanin0(pObj)->pData) ); } } diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c index eeca69bf..9fb9b9e6 100644 --- a/src/aig/aig/aigRepr.c +++ b/src/aig/aig/aigRepr.c @@ -99,7 +99,7 @@ void Aig_ObjCreateRepr( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 ) SeeAlso [] ***********************************************************************/ -static inline void Aig_ObjSetRepr( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 ) +static inline void Aig_ObjSetRepr_( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 ) { assert( p->pReprs != NULL ); assert( !Aig_IsComplement(pNode1) ); @@ -221,7 +221,7 @@ void Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * pOld ) // go through the nodes which have representatives Aig_ManForEachObj( pOld, pObj, k ) if ( (pRepr = Aig_ObjFindRepr(pOld, pObj)) ) - Aig_ObjSetRepr( pNew, Aig_Regular(pRepr->pData), Aig_Regular(pObj->pData) ); + Aig_ObjSetRepr_( pNew, Aig_Regular(pRepr->pData), Aig_Regular(pObj->pData) ); } /**Function************************************************************* @@ -349,7 +349,7 @@ int Aig_ManRemapRepr( Aig_Man_t * p ) if ( pRepr == NULL ) continue; assert( pRepr->Id < pObj->Id ); - Aig_ObjSetRepr( p, pObj, pRepr ); + Aig_ObjSetRepr_( p, pObj, pRepr ); nFanouts += (pObj->nRefs > 0); } return nFanouts; @@ -473,11 +473,17 @@ void Aig_ManMarkValidChoices( Aig_Man_t * p ) { Aig_Obj_t * pObj, * pRepr; int i; + int nReprs, nEquivs; + +extern int Dch_DeriveChoiceCountReprs( Aig_Man_t * pAig ); +extern int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig ); + assert( p->pReprs != NULL ); // create equivalent nodes in the manager assert( p->pEquivs == NULL ); p->pEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) ); memset( p->pEquivs, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p) ); + // make the choice nodes Aig_ManForEachNode( p, pObj, i ) { @@ -507,6 +513,11 @@ void Aig_ManMarkValidChoices( Aig_Man_t * p ) p->pEquivs[pObj->Id] = p->pEquivs[pRepr->Id]; p->pEquivs[pRepr->Id] = pObj; } + + nReprs = Dch_DeriveChoiceCountReprs( p ); + nEquivs = Dch_DeriveChoiceCountEquivs( p ); + printf( "\nReprs = %d. Equivs = %d. Choices = %d.\n", + nReprs, nEquivs, Aig_ManCountChoices(p) ); } @@ -532,7 +543,7 @@ int Aig_TransferMappedClasses( Aig_Man_t * pAig, Aig_Man_t * pPart, int * pMapBa if ( pPart->pReprs[pObj->Id] == NULL ) continue; nClasses++; - Aig_ObjSetRepr( pAig, + Aig_ObjSetRepr_( pAig, Aig_ManObj(pAig, pMapBack[pObj->Id]), Aig_ManObj(pAig, pMapBack[pPart->pReprs[pObj->Id]->Id]) ); } diff --git a/src/aig/aig/aigTest.c b/src/aig/aig/aigTest.c new file mode 100644 index 00000000..b97ffb03 --- /dev/null +++ b/src/aig/aig/aigTest.c @@ -0,0 +1,35 @@ + + +#include "aig.h" + +void Aig_ProcedureTest() +{ + Aig_Man_t * p; + Aig_Obj_t * pA, * pB, * pC; + Aig_Obj_t * pFunc; + Aig_Obj_t * pFunc2; + + p = Aig_ManStart( 1000 ); + + pA = Aig_IthVar( p, 0 ); + pB = Aig_IthVar( p, 1 ); + pC = Aig_IthVar( p, 2 ); + + pFunc = Aig_Mux( p, pA, pB, pC ); + pFunc2 = Aig_And( p, pA, pB ); + + Aig_ObjCreatePo( p, pFunc ); + Aig_ObjCreatePo( p, pFunc2 ); + + Aig_ManSetRegNum( p, 1 ); + + Aig_ManCleanup( p ); + + if ( !Aig_ManCheck( p ) ) + { + printf( "Check has failed\n" ); + } + + Aig_ManDumpBlif( p, "aig_test_file.blif", NULL, NULL ); + Aig_ManStop( p ); +}
\ No newline at end of file diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c index 211b2d9f..2aca98ac 100644 --- a/src/aig/aig/aigUtil.c +++ b/src/aig/aig/aigUtil.c @@ -130,7 +130,7 @@ void Aig_ManResetRefs( Aig_Man_t * p ) /**Function************************************************************* - Synopsis [Cleans MarkB.] + Synopsis [Cleans fMarkA.] Description [] @@ -149,7 +149,7 @@ void Aig_ManCleanMarkA( Aig_Man_t * p ) /**Function************************************************************* - Synopsis [Cleans MarkB.] + Synopsis [Cleans fMarkB.] Description [] diff --git a/src/aig/dch/dch.h b/src/aig/dch/dch.h index a9949821..9f6cfdca 100644 --- a/src/aig/dch/dch.h +++ b/src/aig/dch/dch.h @@ -44,7 +44,9 @@ struct Dch_Pars_t_ int nWords; // the number of simulation words int nBTLimit; // conflict limit at a node int nSatVarMax; // the max number of SAT variables + int fSynthesis; // set to 1 to perform synthesis int fVerbose; // verbose stats + int timeSynth; // synthesis runtime }; //////////////////////////////////////////////////////////////////////// @@ -56,8 +58,8 @@ struct Dch_Pars_t_ //////////////////////////////////////////////////////////////////////// /*=== dchCore.c ==========================================================*/ -extern void Dch_ManSetDefaultParams( Dch_Pars_t * p ); -extern Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ); +extern void Dch_ManSetDefaultParams( Dch_Pars_t * p ); +extern Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ); #ifdef __cplusplus diff --git a/src/aig/dch/dchAig.c b/src/aig/dch/dchAig.c index 31b1eea3..239ece18 100644 --- a/src/aig/dch/dchAig.c +++ b/src/aig/dch/dchAig.c @@ -96,89 +96,17 @@ Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs ) } Aig_ObjCreatePo( pAigTotal, Aig_ObjChild0Copy(pObj) ); } +/* // mark the cone of the first AIG Aig_ManIncrementTravId( pAigTotal ); Aig_ManForEachObj( pAig, pObj, i ) if ( pObj->pData ) Aig_ObjSetTravIdCurrent( pAigTotal, pObj->pData ); +*/ // cleanup should not be done return pAigTotal; } -/**Function************************************************************* - - Synopsis [Derives the AIG with choices from representatives.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dch_DeriveChoiceAig_rec( Aig_Man_t * pNew, Aig_Man_t * pOld, Aig_Obj_t * pObj ) -{ - Aig_Obj_t * pRepr, * pObjNew, * pReprNew; - if ( pObj->pData ) - return; - // construct AIG for the representative - pRepr = pOld->pReprs[pObj->Id]; - if ( pRepr != NULL ) - Dch_DeriveChoiceAig_rec( pNew, pOld, pRepr ); - // skip choices with combinatinal loops - if ( Aig_ObjCheckTfi( pOld, pObj, pRepr ) ) - { - pOld->pReprs[pObj->Id] = NULL; - return; - } - Dch_DeriveChoiceAig_rec( pNew, pOld, Aig_ObjFanin0(pObj) ); - Dch_DeriveChoiceAig_rec( pNew, pOld, Aig_ObjFanin1(pObj) ); - pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - if ( pRepr == NULL ) - return; - // add choice - assert( pObj->nRefs == 0 ); - pObjNew = pObj->pData; - pReprNew = pRepr->pData; - pNew->pEquivs[pObjNew->Id] = pNew->pEquivs[pReprNew->Id]; - pNew->pEquivs[pReprNew->Id] = pObjNew; -} - -/**Function************************************************************* - - Synopsis [Derives the AIG with choices from representatives.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig ) -{ - Aig_Man_t * pChoices; - Aig_Obj_t * pObj; - int i; - // start recording equivalences - pChoices = Aig_ManStart( Aig_ManObjNumMax(pAig) ); - pChoices->pEquivs = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) ); - // map constants and PIs - Aig_ManCleanData( pAig ); - Aig_ManConst1(pAig)->pData = Aig_ManConst1(pChoices); - Aig_ManForEachPi( pAig, pObj, i ) - pObj->pData = Aig_ObjCreatePi( pChoices ); - // construct choice nodes from the POs - assert( pAig->pReprs != NULL ); - Aig_ManForEachPo( pAig, pObj, i ) - { - Dch_DeriveChoiceAig_rec( pChoices, pAig, Aig_ObjFanin0(pObj) ); - Aig_ObjCreatePo( pChoices, Aig_ObjChild0Copy(pObj) ); - } - // there is no need for cleanup - return pChoices; -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/dch/dchChoice.c b/src/aig/dch/dchChoice.c new file mode 100644 index 00000000..fe069fef --- /dev/null +++ b/src/aig/dch/dchChoice.c @@ -0,0 +1,306 @@ +/**CFile**************************************************************** + + FileName [dchChoice.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Choice computation for tech-mapping.] + + Synopsis [Contrustion of choices.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 29, 2008.] + + Revision [$Id: dchChoice.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "dchInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Counts the number of representatives.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dch_DeriveChoiceCountReprs( Aig_Man_t * pAig ) +{ + Aig_Obj_t * pObj, * pRepr; + int i, nReprs = 0; + Aig_ManForEachObj( pAig, pObj, i ) + { + pRepr = Aig_ObjRepr( pAig, pObj ); + if ( pRepr == NULL ) + continue; + assert( pRepr->Id < pObj->Id ); + nReprs++; + } + return nReprs; +} + +/**Function************************************************************* + + Synopsis [Counts the number of equivalences.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig ) +{ + Aig_Obj_t * pObj, * pTemp; + int i, nEquivs = 0; + Aig_ManForEachObj( pAig, pObj, i ) + { + if ( !Aig_ObjIsChoice(pAig, pObj) ) + continue; + for ( pTemp = Aig_ObjEquiv(pAig, pObj); pTemp; pTemp = Aig_ObjEquiv(pAig, pTemp) ) + { + assert( pTemp->nRefs == 0 ); + nEquivs++; + } + } + return nEquivs; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the choice node of pRepr is in the TFI of pObj.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dch_ObjCheckTfi_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + // check the trivial cases + if ( pObj == NULL ) + return 0; + if ( Aig_ObjIsPi(pObj) ) + return 0; + if ( pObj->fMarkA ) + return 1; + // skip the visited node + if ( Aig_ObjIsTravIdCurrent( p, pObj ) ) + return 0; + Aig_ObjSetTravIdCurrent( p, pObj ); + // check the children + if ( Dch_ObjCheckTfi_rec( p, Aig_ObjFanin0(pObj) ) ) + return 1; + if ( Dch_ObjCheckTfi_rec( p, Aig_ObjFanin1(pObj) ) ) + return 1; + // check equivalent nodes + return Dch_ObjCheckTfi_rec( p, Aig_ObjEquiv(p, pObj) ); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the choice node of pRepr is in the TFI of pObj.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dch_ObjCheckTfi( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr ) +{ + Aig_Obj_t * pTemp; + int RetValue; + assert( !Aig_IsComplement(pObj) ); + assert( !Aig_IsComplement(pRepr) ); + // mark nodes of the choice node + for ( pTemp = pRepr; pTemp; pTemp = Aig_ObjEquiv(p, pTemp) ) + pTemp->fMarkA = 1; + // traverse the new node + Aig_ManIncrementTravId( p ); + RetValue = Dch_ObjCheckTfi_rec( p, pObj ); + // unmark nodes of the choice node + for ( pTemp = pRepr; pTemp; pTemp = Aig_ObjEquiv(p, pTemp) ) + pTemp->fMarkA = 0; + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Derives the AIG with choices from representatives.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_DeriveChoiceAig_rec( Aig_Man_t * pAigNew, Aig_Man_t * pAigOld, Aig_Obj_t * pObj ) +{ + Aig_Obj_t * pRepr, * pObjNew, * pReprNew; + if ( pObj->pData ) + return; + // construct AIG for the representative + if ( (pRepr = Aig_ObjRepr(pAigOld, pObj)) ) + Dch_DeriveChoiceAig_rec( pAigNew, pAigOld, pRepr ); + // construct AIG for the fanins + Dch_DeriveChoiceAig_rec( pAigNew, pAigOld, Aig_ObjFanin0(pObj) ); + Dch_DeriveChoiceAig_rec( pAigNew, pAigOld, Aig_ObjFanin1(pObj) ); + pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + if ( pRepr == NULL ) + return; + // get the corresponding new nodes + pObjNew = Aig_Regular(pObj->pData); + pReprNew = Aig_Regular(pRepr->pData); + if ( pObjNew == pReprNew ) + return; + assert( pObjNew->nRefs == 0 ); + // update new nodes of the object + pObj->pData = Aig_NotCond( pRepr->pData, pObj->fPhase ^ pRepr->fPhase ); + if ( !Aig_ObjIsNode(pRepr) ) + return; + // skip choices with combinational loops + if ( Dch_ObjCheckTfi( pAigNew, pObjNew, pReprNew ) ) +// if ( Aig_ObjCheckTfi( pAigNew, pObjNew, pReprNew ) ) + return; + // add choice + pAigNew->pEquivs[pObjNew->Id] = pAigNew->pEquivs[pReprNew->Id]; + pAigNew->pEquivs[pReprNew->Id] = pObjNew; +} + + +/**Function************************************************************* + + Synopsis [Returns representatives of fanin in approapriate polarity.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Aig_Obj_t * Aig_ObjGetRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + Aig_Obj_t * pRepr; + if ( (pRepr = Aig_ObjRepr(p, Aig_Regular(pObj))) ) + return Aig_NotCond( pRepr, Aig_Regular(pObj)->fPhase ^ pRepr->fPhase ^ Aig_IsComplement(pObj) ); + return pObj; +} + +static inline Aig_Obj_t * Aig_ObjChild0CopyRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjGetRepr( p, Aig_ObjChild0Copy(pObj) ); } +static inline Aig_Obj_t * Aig_ObjChild1CopyRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjGetRepr( p, Aig_ObjChild1Copy(pObj) ); } + +/**Function************************************************************* + + Synopsis [Derives the AIG with choices from representatives.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_DeriveChoiceAigNode( Aig_Man_t * pAigNew, Aig_Man_t * pAigOld, Aig_Obj_t * pObj ) +{ + Aig_Obj_t * pRepr, * pObjNew, * pReprNew; + // get the new node + pObj->pData = Aig_And( pAigNew, + Aig_ObjChild0CopyRepr(pAigNew, pObj), + Aig_ObjChild1CopyRepr(pAigNew, pObj) ); + pRepr = Aig_ObjRepr( pAigOld, pObj ); + if ( pRepr == NULL ) + return; + // get the corresponding new nodes + pObjNew = Aig_Regular(pObj->pData); + pReprNew = Aig_Regular(pRepr->pData); + if ( pObjNew == pReprNew ) + return; +// assert( pObjNew->nRefs == 0 ); + // set the representatives + Aig_ObjSetRepr( pAigNew, pObjNew, pReprNew ); + // update new nodes of the object + if ( !Aig_ObjIsNode(pRepr) ) + return; + if ( pObjNew->nRefs > 0 ) + return; + // skip choices with combinational loops + if ( Dch_ObjCheckTfi( pAigNew, pObjNew, pReprNew ) ) + return; + // add choice + pAigNew->pEquivs[pObjNew->Id] = pAigNew->pEquivs[pReprNew->Id]; + pAigNew->pEquivs[pReprNew->Id] = pObjNew; +} + +/**Function************************************************************* + + Synopsis [Derives the AIG with choices from representatives.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig ) +{ + Aig_Man_t * pChoices, * pTemp; + Aig_Obj_t * pObj; + int i; + // start recording equivalences + pChoices = Aig_ManStart( Aig_ManObjNumMax(pAig) ); + pChoices->pEquivs = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) ); + pChoices->pReprs = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) ); + // map constants and PIs + Aig_ManCleanData( pAig ); + Aig_ManConst1(pAig)->pData = Aig_ManConst1(pChoices); + Aig_ManForEachPi( pAig, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pChoices ); + // construct choice nodes from the POs + assert( pAig->pReprs != NULL ); +/* + Aig_ManForEachPo( pAig, pObj, i ) + { + Dch_DeriveChoiceAig_rec( pChoices, pAig, Aig_ObjFanin0(pObj) ); + Aig_ObjCreatePo( pChoices, Aig_ObjChild0Copy(pObj) ); + } +*/ + Aig_ManForEachNode( pAig, pObj, i ) + Dch_DeriveChoiceAigNode( pChoices, pAig, pObj ); + Aig_ManForEachPo( pAig, pObj, i ) + Aig_ObjCreatePo( pChoices, Aig_ObjChild0CopyRepr(pChoices, pObj) ); + Dch_DeriveChoiceCountEquivs( pChoices ); + // there is no need for cleanup + FREE( pChoices->pReprs ); + pChoices = Aig_ManDupDfs( pTemp = pChoices ); + Aig_ManStop( pTemp ); + return pChoices; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/dch/dchClass.c b/src/aig/dch/dchClass.c new file mode 100644 index 00000000..5d192195 --- /dev/null +++ b/src/aig/dch/dchClass.c @@ -0,0 +1,585 @@ +/**CFile**************************************************************** + + FileName [dchClass.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Choice computation for tech-mapping.] + + Synopsis [Representation of candidate equivalence classes.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 29, 2008.] + + Revision [$Id: dchClass.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "dchInt.h" + +/* + The candidate equivalence classes are stored as a vector of pointers + to the array of pointers to the nodes in each class. + The first node of the class is its representative node. + The representative has the smallest topological order among the class nodes. + The nodes inside each class are ordered according to their topological order. + The classes are ordered according to the topological order of their representatives. +*/ + +// internal representation of candidate equivalence classes +struct Dch_Cla_t_ +{ + // class information + Aig_Man_t * pAig; // original AIG manager + Aig_Obj_t *** pId2Class; // non-const classes by ID of repr node + int * pClassSizes; // sizes of each equivalence class + // statistics + int nClasses; // the total number of non-const classes + int nCands1; // the total number of const candidates + int nLits; // the number of literals in all classes + // memory + Aig_Obj_t ** pMemClasses; // memory allocated for equivalence classes + Aig_Obj_t ** pMemClassesFree; // memory allocated for equivalence classes to be used + // temporary data + Vec_Ptr_t * vClassOld; // old equivalence class after splitting + Vec_Ptr_t * vClassNew; // new equivalence class(es) after splitting + // procedures used for class refinement + void * pManData; + unsigned (*pFuncNodeHash) (void *,Aig_Obj_t *); // returns has key of the node + int (*pFuncNodeIsConst) (void *,Aig_Obj_t *); // returns 1 if the node is a constant + int (*pFuncNodesAreEqual) (void *,Aig_Obj_t *, Aig_Obj_t *); // returns 1 if nodes are equal up to a complement +}; + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline Aig_Obj_t * Dch_ObjNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj ) { return ppNexts[pObj->Id]; } +static inline void Dch_ObjSetNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj, Aig_Obj_t * pNext ) { ppNexts[pObj->Id] = pNext; } + +// iterator through the equivalence classes +#define Dch_ManForEachClass( p, ppClass, i ) \ + for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ ) \ + if ( ((ppClass) = p->pId2Class[i]) == NULL ) {} else +// iterator through the nodes in one class +#define Dch_ClassForEachNode( p, pRepr, pNode, i ) \ + for ( i = 0; i < p->pClassSizes[pRepr->Id]; i++ ) \ + if ( ((pNode) = p->pId2Class[pRepr->Id][i]) == NULL ) {} else + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates one equivalence class.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Dch_ObjAddClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, Aig_Obj_t ** pClass, int nSize ) +{ + assert( p->pId2Class[pRepr->Id] == NULL ); + p->pId2Class[pRepr->Id] = pClass; + assert( p->pClassSizes[pRepr->Id] == 0 ); + assert( nSize > 1 ); + p->pClassSizes[pRepr->Id] = nSize; + p->nClasses++; + p->nLits += nSize - 1; +} + +/**Function************************************************************* + + Synopsis [Removes one equivalence class.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Aig_Obj_t ** Dch_ObjRemoveClass( Dch_Cla_t * p, Aig_Obj_t * pRepr ) +{ + Aig_Obj_t ** pClass = p->pId2Class[pRepr->Id]; + int nSize; + assert( pClass != NULL ); + p->pId2Class[pRepr->Id] = NULL; + nSize = p->pClassSizes[pRepr->Id]; + assert( nSize > 1 ); + p->nClasses--; + p->nLits -= nSize - 1; + p->pClassSizes[pRepr->Id] = 0; + return pClass; +} + +/**Function************************************************************* + + Synopsis [Starts representation of equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dch_Cla_t * Dch_ClassesStart( Aig_Man_t * pAig ) +{ + Dch_Cla_t * p; + p = ALLOC( Dch_Cla_t, 1 ); + memset( p, 0, sizeof(Dch_Cla_t) ); + p->pAig = pAig; + p->pId2Class = CALLOC( Aig_Obj_t **, Aig_ManObjNumMax(pAig) ); + p->pClassSizes = CALLOC( int, Aig_ManObjNumMax(pAig) ); + p->vClassOld = Vec_PtrAlloc( 100 ); + p->vClassNew = Vec_PtrAlloc( 100 ); + assert( pAig->pReprs == NULL ); + Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) ); + return p; +} + +/**Function************************************************************* + + Synopsis [Starts representation of equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_ClassesSetData( Dch_Cla_t * p, void * pManData, + unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *), // returns has key of the node + int (*pFuncNodeIsConst)(void *,Aig_Obj_t *), // returns 1 if the node is a constant + int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) ) // returns 1 if nodes are equal up to a complement +{ + p->pManData = pManData; + p->pFuncNodeHash = pFuncNodeHash; + p->pFuncNodeIsConst = pFuncNodeIsConst; + p->pFuncNodesAreEqual = pFuncNodesAreEqual; +} + +/**Function************************************************************* + + Synopsis [Stop representation of equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_ClassesStop( Dch_Cla_t * p ) +{ + if ( p->vClassNew ) Vec_PtrFree( p->vClassNew ); + if ( p->vClassOld ) Vec_PtrFree( p->vClassOld ); + FREE( p->pId2Class ); + FREE( p->pClassSizes ); + FREE( p->pMemClasses ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Stop representation of equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dch_ClassesLitNum( Dch_Cla_t * p ) +{ + return p->nLits; +} + +/**Function************************************************************* + + Synopsis [Checks candidate equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_ClassesCheck( Dch_Cla_t * p ) +{ + Aig_Obj_t * pObj, * pPrev, ** ppClass; + int i, k, nLits, nClasses, nCands1; + nClasses = nLits = 0; + Dch_ManForEachClass( p, ppClass, k ) + { + pPrev = NULL; + Dch_ClassForEachNode( p, ppClass[0], pObj, i ) + { + if ( i == 0 ) + assert( Aig_ObjRepr(p->pAig, pObj) == NULL ); + else + { + assert( Aig_ObjRepr(p->pAig, pObj) == ppClass[0] ); + assert( pPrev->Id < pObj->Id ); + nLits++; + } + pPrev = pObj; + } + nClasses++; + } + nCands1 = 0; + Aig_ManForEachObj( p->pAig, pObj, i ) + nCands1 += Dch_ObjIsConst1Cand( p->pAig, pObj ); + assert( p->nLits == nLits ); + assert( p->nCands1 == nCands1 ); + assert( p->nClasses == nClasses ); +} + +/**Function************************************************************* + + Synopsis [Prints simulation classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_ClassesPrintOne( Dch_Cla_t * p, Aig_Obj_t * pRepr ) +{ + Aig_Obj_t * pObj; + int i; + printf( "{ " ); + Dch_ClassForEachNode( p, pRepr, pObj, i ) + printf( "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) ); + printf( "}\n" ); +} + +/**Function************************************************************* + + Synopsis [Prints simulation classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_ClassesPrint( Dch_Cla_t * p, int fVeryVerbose ) +{ + Aig_Obj_t ** ppClass; + Aig_Obj_t * pObj; + int i; + printf( "Equivalence classes: Const1 = %5d. Class = %5d. Lit = %5d.\n", + p->nCands1, p->nClasses, p->nLits ); + if ( !fVeryVerbose ) + return; + printf( "Constants { " ); + Aig_ManForEachObj( p->pAig, pObj, i ) + if ( Dch_ObjIsConst1Cand( p->pAig, pObj ) ) + printf( "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) ); + printf( "}\n" ); + Dch_ManForEachClass( p, ppClass, i ) + { + printf( "%3d (%3d) : ", i, p->pClassSizes[i] ); + Dch_ClassesPrintOne( p, ppClass[0] ); + } + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [Creates initial simulation classes.] + + Description [Assumes that simulation info is assigned.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_ClassesPrepare( Dch_Cla_t * p, int fLatchCorr, int nMaxLevs ) +{ + Aig_Obj_t ** ppTable, ** ppNexts, ** ppClassNew; + Aig_Obj_t * pObj, * pTemp, * pRepr; + int i, k, nTableSize, nNodes, iEntry, nEntries, nEntries2; + + // allocate the hash table hashing simulation info into nodes + nTableSize = Aig_PrimeCudd( Aig_ManObjNumMax(p->pAig)/4 ); + ppTable = CALLOC( Aig_Obj_t *, nTableSize ); + ppNexts = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) ); + + // add all the nodes to the hash table + nEntries = 0; + Aig_ManForEachObj( p->pAig, pObj, i ) + { + if ( fLatchCorr ) + { + if ( !Aig_ObjIsPi(pObj) ) + continue; + } + else + { + if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) + continue; + // skip the node with more that the given number of levels + if ( nMaxLevs && (int)pObj->Level >= nMaxLevs ) + continue; + } + // check if the node belongs to the class of constant 1 + if ( p->pFuncNodeIsConst( p->pManData, pObj ) ) + { + Dch_ObjSetConst1Cand( p->pAig, pObj ); + p->nCands1++; + continue; + } + // hash the node by its simulation info + iEntry = p->pFuncNodeHash( p->pManData, pObj ) % nTableSize; + // add the node to the class + if ( ppTable[iEntry] == NULL ) + ppTable[iEntry] = pObj; + else + { + // set the representative of this node + pRepr = ppTable[iEntry]; + Aig_ObjSetRepr( p->pAig, pObj, pRepr ); + // add node to the table + if ( Dch_ObjNext( ppNexts, pRepr ) == NULL ) + { // this will be the second entry + p->pClassSizes[pRepr->Id]++; + nEntries++; + } + // add the entry to the list + Dch_ObjSetNext( ppNexts, pObj, Dch_ObjNext( ppNexts, pRepr ) ); + Dch_ObjSetNext( ppNexts, pRepr, pObj ); + p->pClassSizes[pRepr->Id]++; + nEntries++; + } + } + + // allocate room for classes + p->pMemClasses = ALLOC( Aig_Obj_t *, nEntries + p->nCands1 ); + p->pMemClassesFree = p->pMemClasses + nEntries; + + // copy the entries into storage in the topological order + nEntries2 = 0; + Aig_ManForEachObj( p->pAig, pObj, i ) + { + if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) + continue; + nNodes = p->pClassSizes[pObj->Id]; + // skip the nodes that are not representatives of non-trivial classes + if ( nNodes == 0 ) + continue; + assert( nNodes > 1 ); + // add the nodes to the class in the topological order + ppClassNew = p->pMemClasses + nEntries2; + ppClassNew[0] = pObj; + for ( pTemp = Dch_ObjNext(ppNexts, pObj), k = 1; pTemp; + pTemp = Dch_ObjNext(ppNexts, pTemp), k++ ) + { + ppClassNew[nNodes-k] = pTemp; + } + // add the class of nodes + p->pClassSizes[pObj->Id] = 0; + Dch_ObjAddClass( p, pObj, ppClassNew, nNodes ); + // increment the number of entries + nEntries2 += nNodes; + } + assert( nEntries == nEntries2 ); + free( ppTable ); + free( ppNexts ); + // now it is time to refine the classes + Dch_ClassesRefine( p ); + Dch_ClassesCheck( p ); +} + +/**Function************************************************************* + + Synopsis [Iteratively refines the classes after simulation.] + + Description [Returns the number of refinements performed.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dch_ClassesRefineOneClass( Dch_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursive ) +{ + Aig_Obj_t ** pClassOld, ** pClassNew; + Aig_Obj_t * pObj, * pReprNew; + int i; + + // split the class + Vec_PtrClear( p->vClassOld ); + Vec_PtrClear( p->vClassNew ); + Dch_ClassForEachNode( p, pReprOld, pObj, i ) + if ( p->pFuncNodesAreEqual(p->pManData, pReprOld, pObj) ) + Vec_PtrPush( p->vClassOld, pObj ); + else + Vec_PtrPush( p->vClassNew, pObj ); + // check if splitting happened + if ( Vec_PtrSize(p->vClassNew) == 0 ) + return 0; + + // get the new representative + pReprNew = Vec_PtrEntry( p->vClassNew, 0 ); + assert( Vec_PtrSize(p->vClassOld) > 0 ); + assert( Vec_PtrSize(p->vClassNew) > 0 ); + + // create old class + pClassOld = Dch_ObjRemoveClass( p, pReprOld ); + Vec_PtrForEachEntry( p->vClassOld, pObj, i ) + { + pClassOld[i] = pObj; + Aig_ObjSetRepr( p->pAig, pObj, i? pReprOld : NULL ); + } + // create new class + pClassNew = pClassOld + i; + Vec_PtrForEachEntry( p->vClassNew, pObj, i ) + { + pClassNew[i] = pObj; + Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL ); + } + + // put classes back + if ( Vec_PtrSize(p->vClassOld) > 1 ) + Dch_ObjAddClass( p, pReprOld, pClassOld, Vec_PtrSize(p->vClassOld) ); + if ( Vec_PtrSize(p->vClassNew) > 1 ) + Dch_ObjAddClass( p, pReprNew, pClassNew, Vec_PtrSize(p->vClassNew) ); + + // skip of the class should not be recursively refined + if ( fRecursive && Vec_PtrSize(p->vClassNew) > 1 ) + return 1 + Dch_ClassesRefineOneClass( p, pReprNew, 1 ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Refines the classes after simulation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dch_ClassesRefine( Dch_Cla_t * p ) +{ + Aig_Obj_t ** ppClass; + int i, nRefis = 0; + Dch_ManForEachClass( p, ppClass, i ) + nRefis += Dch_ClassesRefineOneClass( p, ppClass[0], 0 ); + return nRefis; +} + + +/**Function************************************************************* + + Synopsis [Returns equivalence class of the given node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_ClassesCollectOneClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, Vec_Ptr_t * vRoots ) +{ + Aig_Obj_t * pObj; + int i; + Vec_PtrClear( vRoots ); + Dch_ClassForEachNode( p, pRepr, pObj, i ) + Vec_PtrPush( vRoots, pObj ); + assert( Vec_PtrSize(vRoots) > 1 ); +} + +/**Function************************************************************* + + Synopsis [Returns equivalence class of the given node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_ClassesCollectConst1Group( Dch_Cla_t * p, Aig_Obj_t * pObj, int nNodes, Vec_Ptr_t * vRoots ) +{ + int i, Limit; + Vec_PtrClear( vRoots ); + Limit = AIG_MIN( pObj->Id + nNodes, Aig_ManObjNumMax(p->pAig) ); + for ( i = pObj->Id; i < Limit; i++ ) + { + pObj = Aig_ManObj( p->pAig, i ); + if ( pObj && Dch_ObjIsConst1Cand( p->pAig, pObj ) ) + Vec_PtrPush( vRoots, pObj ); + } +} + +/**Function************************************************************* + + Synopsis [Refine the group of constant 1 nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dch_ClassesRefineConst1Group( Dch_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive ) +{ + Aig_Obj_t * pObj, * pReprNew, ** ppClassNew; + int i; + // collect the nodes to be refined + Vec_PtrClear( p->vClassNew ); + Vec_PtrForEachEntry( vRoots, pObj, i ) + if ( !p->pFuncNodeIsConst( p->pManData, pObj ) ) + Vec_PtrPush( p->vClassNew, pObj ); + // check if there is a new class + if ( Vec_PtrSize(p->vClassNew) == 0 ) + return 0; + p->nCands1 -= Vec_PtrSize(p->vClassNew); + pReprNew = Vec_PtrEntry( p->vClassNew, 0 ); + Aig_ObjSetRepr( p->pAig, pReprNew, NULL ); + if ( Vec_PtrSize(p->vClassNew) == 1 ) + return 1; + // create a new class composed of these nodes + ppClassNew = p->pMemClassesFree; + p->pMemClassesFree += Vec_PtrSize(p->vClassNew); + Vec_PtrForEachEntry( p->vClassNew, pObj, i ) + { + ppClassNew[i] = pObj; + Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL ); + } + Dch_ObjAddClass( p, pReprNew, ppClassNew, Vec_PtrSize(p->vClassNew) ); + // refine them recursively + if ( fRecursive ) + return 1 + Dch_ClassesRefineOneClass( p, pReprNew, 1 ); + return 1; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/dch/dchCnf.c b/src/aig/dch/dchCnf.c new file mode 100644 index 00000000..6533ca81 --- /dev/null +++ b/src/aig/dch/dchCnf.c @@ -0,0 +1,277 @@ +/**CFile**************************************************************** + + FileName [dchCnf.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Choice computation for tech-mapping.] + + Synopsis [Computation of CNF.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 29, 2008.] + + Revision [$Id: dchCnf.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "dchInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Addes clauses to the solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_AddClausesMux( Dch_Man_t * p, Aig_Obj_t * pNode ) +{ + Aig_Obj_t * pNodeI, * pNodeT, * pNodeE; + int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE; + + assert( !Aig_IsComplement( pNode ) ); + assert( Aig_ObjIsMuxType( pNode ) ); + // get nodes (I = if, T = then, E = else) + pNodeI = Aig_ObjRecognizeMux( pNode, &pNodeT, &pNodeE ); + // get the variable numbers + VarF = Dch_ObjSatNum(p,pNode); + VarI = Dch_ObjSatNum(p,pNodeI); + VarT = Dch_ObjSatNum(p,Aig_Regular(pNodeT)); + VarE = Dch_ObjSatNum(p,Aig_Regular(pNodeE)); + // get the complementation flags + fCompT = Aig_IsComplement(pNodeT); + fCompE = Aig_IsComplement(pNodeE); + + // f = ITE(i, t, e) + + // i' + t' + f + // i' + t + f' + // i + e' + f + // i + e + f' + + // create four clauses + pLits[0] = toLitCond(VarI, 1); + pLits[1] = toLitCond(VarT, 1^fCompT); + pLits[2] = toLitCond(VarF, 0); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); + assert( RetValue ); + pLits[0] = toLitCond(VarI, 1); + pLits[1] = toLitCond(VarT, 0^fCompT); + pLits[2] = toLitCond(VarF, 1); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); + assert( RetValue ); + pLits[0] = toLitCond(VarI, 0); + pLits[1] = toLitCond(VarE, 1^fCompE); + pLits[2] = toLitCond(VarF, 0); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); + assert( RetValue ); + pLits[0] = toLitCond(VarI, 0); + pLits[1] = toLitCond(VarE, 0^fCompE); + pLits[2] = toLitCond(VarF, 1); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); + assert( RetValue ); + + // two additional clauses + // t' & e' -> f' + // t & e -> f + + // t + e + f' + // t' + e' + f + + if ( VarT == VarE ) + { +// assert( fCompT == !fCompE ); + return; + } + + pLits[0] = toLitCond(VarT, 0^fCompT); + pLits[1] = toLitCond(VarE, 0^fCompE); + pLits[2] = toLitCond(VarF, 1); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); + assert( RetValue ); + pLits[0] = toLitCond(VarT, 1^fCompT); + pLits[1] = toLitCond(VarE, 1^fCompE); + pLits[2] = toLitCond(VarF, 0); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); + assert( RetValue ); +} + +/**Function************************************************************* + + Synopsis [Addes clauses to the solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_AddClausesSuper( Dch_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper ) +{ + Aig_Obj_t * pFanin; + int * pLits, nLits, RetValue, i; + assert( !Aig_IsComplement(pNode) ); + assert( Aig_ObjIsNode( pNode ) ); + // create storage for literals + nLits = Vec_PtrSize(vSuper) + 1; + pLits = ALLOC( int, nLits ); + // suppose AND-gate is A & B = C + // add !A => !C or A + !C + Vec_PtrForEachEntry( vSuper, pFanin, i ) + { + pLits[0] = toLitCond(Dch_ObjSatNum(p,Aig_Regular(pFanin)), Aig_IsComplement(pFanin)); + pLits[1] = toLitCond(Dch_ObjSatNum(p,pNode), 1); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); + assert( RetValue ); + } + // add A & B => C or !A + !B + C + Vec_PtrForEachEntry( vSuper, pFanin, i ) + pLits[i] = toLitCond(Dch_ObjSatNum(p,Aig_Regular(pFanin)), !Aig_IsComplement(pFanin)); + pLits[nLits-1] = toLitCond(Dch_ObjSatNum(p,pNode), 0); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits ); + assert( RetValue ); + free( pLits ); +} + +/**Function************************************************************* + + Synopsis [Collects the supergate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes ) +{ + // if the new node is complemented or a PI, another gate begins + if ( Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) || + (!fFirst && Aig_ObjRefs(pObj) > 1) || + (fUseMuxes && Aig_ObjIsMuxType(pObj)) ) + { + Vec_PtrPushUnique( vSuper, pObj ); + return; + } + // go through the branches + Dch_CollectSuper_rec( Aig_ObjChild0(pObj), vSuper, 0, fUseMuxes ); + Dch_CollectSuper_rec( Aig_ObjChild1(pObj), vSuper, 0, fUseMuxes ); +} + +/**Function************************************************************* + + Synopsis [Collects the supergate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper ) +{ + assert( !Aig_IsComplement(pObj) ); + assert( !Aig_ObjIsPi(pObj) ); + Vec_PtrClear( vSuper ); + Dch_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes ); +} + +/**Function************************************************************* + + Synopsis [Updates the solver clause database.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_ObjAddToFrontier( Dch_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontier ) +{ + assert( !Aig_IsComplement(pObj) ); + if ( Dch_ObjSatNum(p,pObj) ) + return; + assert( Dch_ObjSatNum(p,pObj) == 0 ); + if ( Aig_ObjIsConst1(pObj) ) + return; + Dch_ObjSetSatNum( p, pObj, p->nSatVars++ ); + if ( Aig_ObjIsNode(pObj) ) + Vec_PtrPush( vFrontier, pObj ); +} + +/**Function************************************************************* + + Synopsis [Updates the solver clause database.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_CnfNodeAddToSolver( Dch_Man_t * p, Aig_Obj_t * pObj ) +{ + Vec_Ptr_t * vFrontier; + Aig_Obj_t * pNode, * pFanin; + int i, k, fUseMuxes = 1; + // quit if CNF is ready + if ( Dch_ObjSatNum(p,pObj) ) + return; + // start the frontier + vFrontier = Vec_PtrAlloc( 100 ); + Dch_ObjAddToFrontier( p, pObj, vFrontier ); + // explore nodes in the frontier + Vec_PtrForEachEntry( vFrontier, pNode, i ) + { + // create the supergate + assert( Dch_ObjSatNum(p,pNode) ); + if ( fUseMuxes && Aig_ObjIsMuxType(pNode) ) + { + Vec_PtrClear( p->vFanins ); + Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin0(pNode) ) ); + Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) ); + Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) ); + Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) ); + Vec_PtrForEachEntry( p->vFanins, pFanin, k ) + Dch_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier ); + Dch_AddClausesMux( p, pNode ); + } + else + { + Dch_CollectSuper( pNode, fUseMuxes, p->vFanins ); + Vec_PtrForEachEntry( p->vFanins, pFanin, k ) + Dch_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier ); + Dch_AddClausesSuper( p, pNode, p->vFanins ); + } + assert( Vec_PtrSize(p->vFanins) > 1 ); + } + Vec_PtrFree( vFrontier ); +} + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/dch/dchCore.c b/src/aig/dch/dchCore.c index cdac853f..b73fceb3 100644 --- a/src/aig/dch/dchCore.c +++ b/src/aig/dch/dchCore.c @@ -43,8 +43,9 @@ void Dch_ManSetDefaultParams( Dch_Pars_t * p ) { memset( p, 0, sizeof(Dch_Pars_t) ); p->nWords = 4; // the number of simulation words - p->nBTLimit = 1000; // conflict limit at a node - p->nSatVarMax = 5000; // the max number of SAT variables + p->nBTLimit = 100; // conflict limit at a node + p->nSatVarMax = 10000; // the max number of SAT variables + p->fSynthesis = 1; // derives three snapshots p->fVerbose = 1; // verbose stats } @@ -63,30 +64,30 @@ Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ) { Dch_Man_t * p; Aig_Man_t * pResult; - int i; - + int clk, clkTotal = clock(); assert( Vec_PtrSize(vAigs) > 0 ); - - printf( "AIGs considered for choicing:\n" ); - Vec_PtrForEachEntry( vAigs, pResult, i ) - { - Aig_ManPrintStats( pResult ); - } - // start the choicing manager p = Dch_ManCreate( vAigs, pPars ); // compute candidate equivalence classes +clk = clock(); p->ppClasses = Dch_CreateCandEquivClasses( p->pAigTotal, pPars->nWords, pPars->fVerbose ); - - - - - +p->timeSimInit = clock() - clk; +// Dch_ClassesPrint( p->ppClasses, 0 ); + p->nLits = Dch_ClassesLitNum( p->ppClasses ); + // perform SAT sweeping + Dch_ManSweep( p ); + // count the number of representatives + p->nReprs = Dch_DeriveChoiceCountReprs( p->pAigTotal ); // create choices -// pResult = Dch_DeriveChoiceAig( p->pAigTotal ); - Aig_ManCleanup( p->pAigTotal ); - pResult = Aig_ManDupSimpleDfs( p->pAigTotal ); - +clk = clock(); + pResult = Dch_DeriveChoiceAig( p->pAigTotal ); +p->timeChoice = clock() - clk; +// Aig_ManCleanup( p->pAigTotal ); +// pResult = Aig_ManDupSimpleDfs( p->pAigTotal ); + // count the number of equivalences and choices + p->nEquivs = Dch_DeriveChoiceCountEquivs( pResult ); + p->nChoices = Aig_ManCountChoices( pResult ); +p->timeTotal = clock() - clkTotal; Dch_ManStop( p ); return pResult; } diff --git a/src/aig/dch/dchInt.h b/src/aig/dch/dchInt.h index e35f8111..a71cba69 100644 --- a/src/aig/dch/dchInt.h +++ b/src/aig/dch/dchInt.h @@ -43,52 +43,108 @@ extern "C" { // equivalence classes typedef struct Dch_Cla_t_ Dch_Cla_t; -struct Dch_Cla_t_ -{ - int nNodes; // the number of nodes in the class - int pNodes[0]; // the nodes of the class -}; // choicing manager typedef struct Dch_Man_t_ Dch_Man_t; struct Dch_Man_t_ { // parameters - Dch_Pars_t * pPars; + Dch_Pars_t * pPars; // choicing parameters // AIGs used in the package - Vec_Ptr_t * vAigs; // user-given AIGs - Aig_Man_t * pAigTotal; // intermediate AIG - Aig_Man_t * pAigFraig; // final AIG + Vec_Ptr_t * vAigs; // user-given AIGs + Aig_Man_t * pAigTotal; // intermediate AIG + Aig_Man_t * pAigFraig; // final AIG // equivalence classes - Dch_Cla_t ** ppClasses; // classes for representative nodes + Dch_Cla_t * ppClasses; // equivalence classes of nodes + Aig_Obj_t ** pReprsProved; // equivalences proved // SAT solving - sat_solver * pSat; // recyclable SAT solver - Vec_Int_t ** ppSatVars; // SAT variables for used nodes - Vec_Ptr_t * vUsedNodes; // nodes whose SAT vars are assigned + sat_solver * pSat; // recyclable SAT solver + int nSatVars; // the counter of SAT variables + int * pSatVars; // mapping of each node into its SAT var + Vec_Ptr_t * vUsedNodes; // nodes whose SAT vars are assigned + int nRecycles; // the number of times SAT solver was recycled + Vec_Ptr_t * vFanins; // fanins of the CNF node + Vec_Ptr_t * vRoots; // the roots of the current equiv class + // solver cone size + int nConeThis; + int nConeMax; + // SAT calls statistics + int nSatCalls; // the number of SAT calls + int nSatProof; // the number of proofs + int nSatFailsReal; // the number of timeouts + int nSatCallsUnsat; // the number of unsat SAT calls + int nSatCallsSat; // the number of sat SAT calls + // choice node statistics + int nLits; // the number of lits in the cand equiv classes + int nReprs; // the number of proved equivalent pairs + int nEquivs; // the number of final equivalences + int nChoices; // the number of final choice nodes // runtime stats + int timeSimInit; // simulation and class computation + int timeSimSat; // simulation of the counter-examples + int timeSat; // solving SAT + int timeSatSat; // sat + int timeSatUnsat; // unsat + int timeSatUndec; // undecided + int timeChoice; // choice computation + int timeOther; // other runtime + int timeTotal; // total runtime }; //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +static inline int Dch_ObjIsConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) +{ + return Aig_ObjRepr(pAig, pObj) == Aig_ManConst1(pAig); +} +static inline void Dch_ObjSetConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) +{ + assert( !Dch_ObjIsConst1Cand( pAig, pObj ) ); + Aig_ObjSetRepr( pAig, pObj, Aig_ManConst1(pAig) ); +} + +static inline int Dch_ObjSatNum( Dch_Man_t * p, Aig_Obj_t * pObj ) { return p->pSatVars[pObj->Id]; } +static inline void Dch_ObjSetSatNum( Dch_Man_t * p, Aig_Obj_t * pObj, int Num ) { p->pSatVars[pObj->Id] = Num; } + //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -/*=== dchAig.c =====================================================*/ -extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs ); -extern Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig ); - -/*=== dchMan.c =====================================================*/ -extern Dch_Man_t * Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ); -extern void Dch_ManStop( Dch_Man_t * p ); - -/*=== dchSat.c =====================================================*/ - -/*=== dchSim.c =====================================================*/ -extern Dch_Cla_t ** Dch_CreateCandEquivClasses( Aig_Man_t * pAig, int nWords, int fVerbose ); - +/*=== dchAig.c ===================================================*/ +extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs ); +/*=== dchChoice.c ===================================================*/ +extern int Dch_DeriveChoiceCountReprs( Aig_Man_t * pAig ); +extern int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig ); +extern Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig ); +/*=== dchClass.c =================================================*/ +extern Dch_Cla_t * Dch_ClassesStart( Aig_Man_t * pAig ); +extern void Dch_ClassesSetData( Dch_Cla_t * p, void * pManData, + unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *), + int (*pFuncNodeIsConst)(void *,Aig_Obj_t *), + int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) ); +extern void Dch_ClassesStop( Dch_Cla_t * p ); +extern int Dch_ClassesLitNum( Dch_Cla_t * p ); +extern void Dch_ClassesPrint( Dch_Cla_t * p, int fVeryVerbose ); +extern void Dch_ClassesPrepare( Dch_Cla_t * p, int fLatchCorr, int nMaxLevs ); +extern int Dch_ClassesRefine( Dch_Cla_t * p ); +extern int Dch_ClassesRefineOneClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive ); +extern void Dch_ClassesCollectOneClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, Vec_Ptr_t * vRoots ); +extern void Dch_ClassesCollectConst1Group( Dch_Cla_t * p, Aig_Obj_t * pObj, int nNodes, Vec_Ptr_t * vRoots ); +extern int Dch_ClassesRefineConst1Group( Dch_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive ); +/*=== dchCnf.c ===================================================*/ +extern void Dch_CnfNodeAddToSolver( Dch_Man_t * p, Aig_Obj_t * pObj ); +/*=== dchMan.c ===================================================*/ +extern Dch_Man_t * Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ); +extern void Dch_ManStop( Dch_Man_t * p ); +extern void Dch_ManSatSolverRecycle( Dch_Man_t * p ); +/*=== dchSat.c ===================================================*/ +extern int Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 ); +/*=== dchSim.c ===================================================*/ +extern Dch_Cla_t * Dch_CreateCandEquivClasses( Aig_Man_t * pAig, int nWords, int fVerbose ); +/*=== dchSim.c ===================================================*/ +extern void Dch_ManSweep( Dch_Man_t * p ); #ifdef __cplusplus } diff --git a/src/aig/dch/dchMan.c b/src/aig/dch/dchMan.c index 2fc739f1..6a0eecfe 100644 --- a/src/aig/dch/dchMan.c +++ b/src/aig/dch/dchMan.c @@ -30,7 +30,7 @@ /**Function************************************************************* - Synopsis [Creates the interpolation manager.] + Synopsis [Creates the manager.] Description [] @@ -46,20 +46,71 @@ Dch_Man_t * Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ) p = ALLOC( Dch_Man_t, 1 ); memset( p, 0, sizeof(Dch_Man_t) ); p->pPars = pPars; - // AIGs p->vAigs = vAigs; p->pAigTotal = Dch_DeriveTotalAig( vAigs ); - // equivalence classes - Aig_ManReprStart( p->pAigTotal, Aig_ManObjNumMax(p->pAigTotal) ); // SAT solving - p->ppSatVars = CALLOC( Vec_Int_t *, Aig_ManObjNumMax(p->pAigTotal) ); + p->nSatVars = 1; + p->pSatVars = CALLOC( int, Aig_ManObjNumMax(p->pAigTotal) ); p->vUsedNodes = Vec_PtrAlloc( 1000 ); + p->vFanins = Vec_PtrAlloc( 100 ); + p->vRoots = Vec_PtrAlloc( 1000 ); + // equivalences proved + p->pReprsProved = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAigTotal) ); return p; } /**Function************************************************************* - Synopsis [Frees the interpolation manager.] + Synopsis [Prints stats of the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_ManPrintStats( Dch_Man_t * p ) +{ +// Aig_Man_t * pAig; + int i; + for ( i = 0; i < 85; i++ ) + printf( " " ); + printf( "\r" ); +// printf( "Choicing will be performed with %d AIGs:\n", Vec_PtrSize(p->vAigs) ); +// Vec_PtrForEachEntry( p->vAigs, pAig, i ) +// Aig_ManPrintStats( pAig ); + printf( "Parameters: Sim words = %d. Conf limit = %d. SAT var max = %d.\n", + p->pPars->nWords, p->pPars->nBTLimit, p->pPars->nSatVarMax ); + printf( "AIG nodes : Total = %6d. Dangling = %6d. Main = %6d. (%6.2f %%)\n", + Aig_ManNodeNum(p->pAigTotal), + Aig_ManNodeNum(p->pAigTotal)-Aig_ManNodeNum(Vec_PtrEntry(p->vAigs,0)), + Aig_ManNodeNum(Vec_PtrEntry(p->vAigs,0)), + 100.0 * Aig_ManNodeNum(Vec_PtrEntry(p->vAigs,0))/Aig_ManNodeNum(p->pAigTotal) ); + printf( "SAT solver: Vars = %d. Max cone = %d. Recycles = %d.\n", + p->nSatVars, p->nConeMax, p->nRecycles ); + printf( "SAT calls : All = %6d. Unsat = %6d. Sat = %6d. Fail = %6d.\n", + p->nSatCalls, p->nSatCalls-p->nSatCallsSat-p->nSatFailsReal, + p->nSatCallsSat, p->nSatFailsReal ); + printf( "Choices : Lits = %6d. Reprs = %5d. Equivs = %5d. Choices = %5d.\n", + p->nLits, p->nReprs, p->nEquivs, p->nChoices ); + printf( "Runtime statistics:\n" ); + p->timeOther = p->timeTotal-p->timeSimInit-p->timeSimSat-p->timeSat-p->timeChoice; + PRTP( "Sim init ", p->timeSimInit, p->timeTotal ); + PRTP( "Sim SAT ", p->timeSimSat, p->timeTotal ); + PRTP( "SAT solving", p->timeSat, p->timeTotal ); + PRTP( " sat ", p->timeSatSat, p->timeTotal ); + PRTP( " unsat ", p->timeSatUnsat, p->timeTotal ); + PRTP( " undecided", p->timeSatUndec, p->timeTotal ); + PRTP( "Choice ", p->timeChoice, p->timeTotal ); + PRTP( "Other ", p->timeOther, p->timeTotal ); + PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); + PRT( "Synthesis ", p->pPars->timeSynth ); +} + +/**Function************************************************************* + + Synopsis [Frees the manager.] Description [] @@ -71,29 +122,51 @@ Dch_Man_t * Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ) void Dch_ManStop( Dch_Man_t * p ) { if ( p->pPars->fVerbose ) - { -/* - p->timeOther = p->timeTotal-p->timeRwr-p->timeCnf-p->timeSat-p->timeInt-p->timeEqu; - printf( "Runtime statistics:\n" ); - PRTP( "Rewriting ", p->timeRwr, p->timeTotal ); - PRTP( "CNF mapping", p->timeCnf, p->timeTotal ); - PRTP( "SAT solving", p->timeSat, p->timeTotal ); - PRTP( "Interpol ", p->timeInt, p->timeTotal ); - PRTP( "Containment", p->timeEqu, p->timeTotal ); - PRTP( "Other ", p->timeOther, p->timeTotal ); - PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); -*/ - } + Dch_ManPrintStats( p ); if ( p->pAigTotal ) Aig_ManStop( p->pAigTotal ); if ( p->pAigFraig ) Aig_ManStop( p->pAigFraig ); - FREE( p->ppClasses ); - FREE( p->ppSatVars ); + if ( p->ppClasses ) + Dch_ClassesStop( p->ppClasses ); + if ( p->pSat ) + sat_solver_delete( p->pSat ); Vec_PtrFree( p->vUsedNodes ); + Vec_PtrFree( p->vFanins ); + Vec_PtrFree( p->vRoots ); + FREE( p->pReprsProved ); + FREE( p->pSatVars ); free( p ); } +/**Function************************************************************* + + Synopsis [Recycles the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_ManSatSolverRecycle( Dch_Man_t * p ) +{ + int Lit; + if ( p->pSat ) + { + sat_solver_delete( p->pSat ); + memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAigTotal) ); + } + p->pSat = sat_solver_new(); + sat_solver_setnvars( p->pSat, 1000 ); + // var 0 is reserved for const1 node - add the clause + Lit = toLit( 0 ); + sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); + p->nSatVars = 1; + p->nRecycles++; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/dch/dchSat.c b/src/aig/dch/dchSat.c index 0d81991f..19aaffee 100644 --- a/src/aig/dch/dchSat.c +++ b/src/aig/dch/dchSat.c @@ -30,7 +30,7 @@ /**Function************************************************************* - Synopsis [] + Synopsis [Runs equivalence test for the two nodes.] Description [] @@ -39,6 +39,105 @@ SeeAlso [] ***********************************************************************/ +int Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) +{ + int nBTLimit = p->pPars->nBTLimit; + int pLits[2], RetValue, RetValue1, status, clk; + p->nSatCalls++; + + // sanity checks + assert( !Aig_IsComplement(pNew) ); + assert( !Aig_IsComplement(pOld) ); + assert( pNew != pOld ); + + // check if SAT solver needs recycling + if ( p->pSat == NULL || (p->pPars->nSatVarMax && p->nSatVars > p->pPars->nSatVarMax) ) + Dch_ManSatSolverRecycle( p ); + + // if the nodes do not have SAT variables, allocate them + Dch_CnfNodeAddToSolver( p, pOld ); + Dch_CnfNodeAddToSolver( p, pNew ); + + // propage unit clauses + if ( p->pSat->qtail != p->pSat->qhead ) + { + status = sat_solver_simplify(p->pSat); + assert( status != 0 ); + assert( p->pSat->qtail == p->pSat->qhead ); + } + + // solve under assumptions + // A = 1; B = 0 OR A = 1; B = 1 + pLits[0] = toLitCond( Dch_ObjSatNum(p,pOld), 0 ); + pLits[1] = toLitCond( Dch_ObjSatNum(p,pNew), pOld->fPhase == pNew->fPhase ); +//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 ); +clk = clock(); + RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, + (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); +p->timeSat += clock() - clk; + if ( RetValue1 == l_False ) + { +p->timeSatUnsat += clock() - clk; + pLits[0] = lit_neg( pLits[0] ); + pLits[1] = lit_neg( pLits[1] ); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); + assert( RetValue ); + p->nSatCallsUnsat++; + } + else if ( RetValue1 == l_True ) + { +p->timeSatSat += clock() - clk; + p->nSatCallsSat++; + return 0; + } + else // if ( RetValue1 == l_Undef ) + { +p->timeSatUndec += clock() - clk; + p->nSatFailsReal++; + return -1; + } + + // if the old node was constant 0, we already know the answer + if ( pOld == Aig_ManConst1(p->pAigFraig) ) + { + p->nSatProof++; + return 1; + } + + // solve under assumptions + // A = 0; B = 1 OR A = 0; B = 0 + pLits[0] = toLitCond( Dch_ObjSatNum(p,pOld), 1 ); + pLits[1] = toLitCond( Dch_ObjSatNum(p,pNew), pOld->fPhase ^ pNew->fPhase ); +clk = clock(); + RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, + (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); +p->timeSat += clock() - clk; + if ( RetValue1 == l_False ) + { +p->timeSatUnsat += clock() - clk; + pLits[0] = lit_neg( pLits[0] ); + pLits[1] = lit_neg( pLits[1] ); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); + assert( RetValue ); + p->nSatCallsUnsat++; + } + else if ( RetValue1 == l_True ) + { +p->timeSatSat += clock() - clk; + p->nSatCallsSat++; + return 0; + } + else // if ( RetValue1 == l_Undef ) + { +p->timeSatUndec += clock() - clk; + p->nSatFailsReal++; + return -1; + } + // return SAT proof + p->nSatProof++; + return 1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/dch/dchSim.c b/src/aig/dch/dchSim.c index f11b701f..9882dd05 100644 --- a/src/aig/dch/dchSim.c +++ b/src/aig/dch/dchSim.c @@ -39,6 +39,121 @@ static inline unsigned Dch_ObjRandomSim() /**Function************************************************************* + Synopsis [Computes hash value of the node using its simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Dch_NodeHash( void * p, Aig_Obj_t * pObj ) +{ + Vec_Ptr_t * vSims = p; + static int s_FPrimes[128] = { + 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, + 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, + 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, + 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, + 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, + 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, + 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, + 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, + 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, + 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, + 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, + 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, + 8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147 + }; + unsigned * pSim; + unsigned uHash; + int k, nWords; + nWords = (unsigned *)Vec_PtrEntry(vSims, 1) - (unsigned *)Vec_PtrEntry(vSims, 0); + uHash = 0; + pSim = Dch_ObjSim( vSims, pObj ); + if ( pObj->fPhase ) + { + for ( k = 0; k < nWords; k++ ) + uHash ^= ~pSim[k] * s_FPrimes[k & 0x7F]; + } + else + { + for ( k = 0; k < nWords; k++ ) + uHash ^= pSim[k] * s_FPrimes[k & 0x7F]; + } + return uHash; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if simulation info is composed of all zeros.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dch_NodeIsConst( void * p, Aig_Obj_t * pObj ) +{ + Vec_Ptr_t * vSims = p; + unsigned * pSim; + int k, nWords; + nWords = (unsigned *)Vec_PtrEntry(vSims, 1) - (unsigned *)Vec_PtrEntry(vSims, 0); + pSim = Dch_ObjSim( vSims, pObj ); + if ( pObj->fPhase ) + { + for ( k = 0; k < nWords; k++ ) + if ( ~pSim[k] ) + return 0; + } + else + { + for ( k = 0; k < nWords; k++ ) + if ( pSim[k] ) + return 0; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if simulation infos are equal.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dch_NodesAreEqual( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) +{ + Vec_Ptr_t * vSims = p; + unsigned * pSim0, * pSim1; + int k, nWords; + nWords = (unsigned *)Vec_PtrEntry(vSims, 1) - (unsigned *)Vec_PtrEntry(vSims, 0); + pSim0 = Dch_ObjSim( vSims, pObj0 ); + pSim1 = Dch_ObjSim( vSims, pObj1 ); + if ( pObj0->fPhase != pObj1->fPhase ) + { + for ( k = 0; k < nWords; k++ ) + if ( pSim0[k] != ~pSim1[k] ) + return 0; + } + else + { + for ( k = 0; k < nWords; k++ ) + if ( pSim0[k] != pSim1[k] ) + return 0; + } + return 1; +} + +/**Function************************************************************* + Synopsis [Perform random simulation.] Description [] @@ -48,11 +163,12 @@ static inline unsigned Dch_ObjRandomSim() SeeAlso [] ***********************************************************************/ -void Dch_PerformRandomSimulation( Aig_Man_t * pAig, Vec_Ptr_t * vSims, int nWords ) +void Dch_PerformRandomSimulation( Aig_Man_t * pAig, Vec_Ptr_t * vSims ) { unsigned * pSim, * pSim0, * pSim1; Aig_Obj_t * pObj; - int i, k; + int i, k, nWords; + nWords = (unsigned *)Vec_PtrEntry(vSims, 1) - (unsigned *)Vec_PtrEntry(vSims, 0); // assign const 1 sim info pObj = Aig_ManConst1(pAig); @@ -65,6 +181,7 @@ void Dch_PerformRandomSimulation( Aig_Man_t * pAig, Vec_Ptr_t * vSims, int nWord pSim = Dch_ObjSim( vSims, pObj ); for ( k = 0; k < nWords; k++ ) pSim[k] = Dch_ObjRandomSim(); + pSim[0] <<= 1; } // simulate AIG in the topological order @@ -95,92 +212,11 @@ void Dch_PerformRandomSimulation( Aig_Man_t * pAig, Vec_Ptr_t * vSims, int nWord pSim[k] = pSim0[k] & pSim1[k]; } } - // get simulation information for primary outputs } /**Function************************************************************* - Synopsis [Hashing nodes by sim info.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dch_HashNodesBySimulationInfo( Aig_Man_t * pAig, Vec_Ptr_t * vSims, int nWords ) -{ - unsigned * pSim0, * pSim1; - Aig_Obj_t * pObj, * pUnique; - int i, k, j, nodeId, Counter, c, CountNodes; - - Vec_Int_t * vUniqueNodes, * vNodeCounters; - - vUniqueNodes = Vec_IntAlloc( 1000 ); - vNodeCounters = Vec_IntStart( Aig_ManObjNumMax(pAig) ); - - Aig_ManForEachObj( pAig, pObj, i ) - { - if ( Aig_ObjIsPo(pObj) ) - continue; - - // node's sim info - pSim0 = Dch_ObjSim( vSims, pObj ); - - Vec_IntForEachEntry( vUniqueNodes, nodeId, j ) - { - pUnique = Aig_ManObj( pAig, nodeId ); - // unique node's sim info - pSim1 = Dch_ObjSim( vSims, pUnique ); - - for ( k = 0; k < nWords; k++ ) - if ( pSim0[k] != pSim1[k] ) - break; - if ( k == nWords ) // sim info is same as this node - { - Counter = Vec_IntEntry( vNodeCounters, nodeId ); - Vec_IntWriteEntry( vNodeCounters, nodeId, Counter+1 ); - break; - } - } - - if ( j == Vec_IntSize(vUniqueNodes) ) // sim info of pObj is unique - { - Vec_IntPush( vUniqueNodes, pObj->Id ); - - Counter = Vec_IntEntry( vNodeCounters, pObj->Id ); - assert( Counter == 0 ); - Vec_IntWriteEntry( vNodeCounters, pObj->Id, Counter+1 ); - } - } - - Counter = 0; - Vec_IntForEachEntry( vNodeCounters, c, k ) - if ( c > 1 ) - Counter++; - - - printf( "Detected %d non-trivial candidate equivalence classes for %d nodes.\n", - Counter, Vec_IntSize(vUniqueNodes) ); - - CountNodes = 0; - Vec_IntForEachEntry( vUniqueNodes, nodeId, k ) - { - if ( Vec_IntEntry( vNodeCounters, nodeId ) == 1 ) - continue; -// printf( "%d ", Vec_IntEntry( vNodeCounters, nodeId ) ); - CountNodes += Vec_IntEntry( vNodeCounters, nodeId ); - } -// printf( "\n" ); - printf( "Nodes participating in non-trivial classes = %d.\n", CountNodes ); - - -} - -/**Function************************************************************* - Synopsis [Derives candidate equivalence classes of AIG nodes.] Description [] @@ -190,32 +226,30 @@ void Dch_HashNodesBySimulationInfo( Aig_Man_t * pAig, Vec_Ptr_t * vSims, int nWo SeeAlso [] ***********************************************************************/ -Dch_Cla_t ** Dch_CreateCandEquivClasses( Aig_Man_t * pAig, int nWords, int fVerbose ) +Dch_Cla_t * Dch_CreateCandEquivClasses( Aig_Man_t * pAig, int nWords, int fVerbose ) { - Dch_Cla_t ** ppClasses; // place for equivalence classes - Aig_MmFlex_t * pMemCla; // memory for equivalence classes + Dch_Cla_t * pClasses; Vec_Ptr_t * vSims; - - // start storage for equivalence classes - ppClasses = CALLOC( Dch_Cla_t *, Aig_ManObjNumMax(pAig) ); - pMemCla = Aig_MmFlexStart(); - + int i; // allocate simulation information vSims = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(pAig), nWords ); - - // run simulation - Dch_PerformRandomSimulation( pAig, vSims, nWords ); - + // run random simulation from the primary inputs + Dch_PerformRandomSimulation( pAig, vSims ); + // start storage for equivalence classes + pClasses = Dch_ClassesStart( pAig ); + Dch_ClassesSetData( pClasses, vSims, Dch_NodeHash, Dch_NodeIsConst, Dch_NodesAreEqual ); // hash nodes by sim info - Dch_HashNodesBySimulationInfo( pAig, vSims, nWords ); - - // collect equivalence classes -// ppClasses = NULL; - + Dch_ClassesPrepare( pClasses, 0, 0 ); + // iterate random simulation + for ( i = 0; i < 3; i++ ) + { + Dch_PerformRandomSimulation( pAig, vSims ); + Dch_ClassesRefine( pClasses ); + } // clean up and return - Aig_MmFlexStop( pMemCla, 0 ); + Dch_ClassesSetData( pClasses, NULL, NULL, NULL, NULL ); Vec_PtrFree( vSims ); - return ppClasses; + return pClasses; } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/dch/dchSweep.c b/src/aig/dch/dchSweep.c new file mode 100644 index 00000000..305e19ee --- /dev/null +++ b/src/aig/dch/dchSweep.c @@ -0,0 +1,262 @@ +/**CFile**************************************************************** + + FileName [dchSat.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Choice computation for tech-mapping.] + + Synopsis [Calls to the SAT solver.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 29, 2008.] + + Revision [$Id: dchSat.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "dchInt.h" +#include "bar.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline Aig_Obj_t * Dch_ObjFraig( Aig_Obj_t * pObj ) { return pObj->pData; } +static inline void Dch_ObjSetFraig( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { pObj->pData = pNode; } + +static inline Aig_Obj_t * Dch_ObjChild0Fra( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Dch_ObjFraig(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj)) : NULL; } +static inline Aig_Obj_t * Dch_ObjChild1Fra( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Dch_ObjFraig(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj)) : NULL; } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns 1 if the node appears to be constant 1 candidate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dch_NodeIsConstCex( void * p, Aig_Obj_t * pObj ) +{ + return pObj->fPhase == pObj->fMarkB; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the nodes appear equal.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dch_NodesAreEqualCex( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) +{ + return (pObj0->fPhase == pObj1->fPhase) == (pObj0->fMarkB == pObj1->fMarkB); +} + +/**Function************************************************************* + + Synopsis [Resimulates the cone of influence of the solved nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_ManResimulateSolved_rec( Dch_Man_t * p, Aig_Obj_t * pObj ) +{ + if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) ) + return; + Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj); + if ( Aig_ObjIsPi(pObj) ) + { + // get the value from the SAT solver + assert( p->pSatVars[pObj->Id] > 0 ); + pObj->fMarkB = sat_solver_var_value( p->pSat, p->pSatVars[pObj->Id] ); + return; + } + Dch_ManResimulateSolved_rec( p, Aig_ObjFanin0(pObj) ); + Dch_ManResimulateSolved_rec( p, Aig_ObjFanin1(pObj) ); + pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ) + & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) ); + // count the cone size + if ( Dch_ObjSatNum( p, Aig_Regular(Dch_ObjFraig(pObj)) ) > 0 ) + p->nConeThis++; +} + +/**Function************************************************************* + + Synopsis [Resimulates the cone of influence of the other nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_ManResimulateOther_rec( Dch_Man_t * p, Aig_Obj_t * pObj ) +{ + if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) ) + return; + Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj); + if ( Aig_ObjIsPi(pObj) ) + { + // set random value + pObj->fMarkB = Aig_ManRandom(0) & 1; + return; + } + Dch_ManResimulateOther_rec( p, Aig_ObjFanin0(pObj) ); + Dch_ManResimulateOther_rec( p, Aig_ObjFanin1(pObj) ); + pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ) + & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Handle the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_ManSweepResimulate( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr ) +{ + Aig_Obj_t * pRoot; + int i, RetValue, clk = clock(); + // get the equivalence class + if ( Dch_ObjIsConst1Cand(p->pAigTotal, pObj) ) + Dch_ClassesCollectConst1Group( p->ppClasses, pObj, 500, p->vRoots ); + else + Dch_ClassesCollectOneClass( p->ppClasses, pRepr, p->vRoots ); + // resimulate the cone of influence of the solved nodes + p->nConeThis = 0; + Aig_ManIncrementTravId( p->pAigTotal ); + Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) ); + Dch_ManResimulateSolved_rec( p, pObj ); + Dch_ManResimulateSolved_rec( p, pRepr ); + p->nConeMax = AIG_MAX( p->nConeMax, p->nConeThis ); + // resimulate the cone of influence of the other nodes + Vec_PtrForEachEntry( p->vRoots, pRoot, i ) + Dch_ManResimulateOther_rec( p, pRoot ); + // refine this class + if ( Dch_ObjIsConst1Cand(p->pAigTotal, pObj) ) + RetValue = Dch_ClassesRefineConst1Group( p->ppClasses, p->vRoots, 0 ); + else + RetValue = Dch_ClassesRefineOneClass( p->ppClasses, pRepr, 0 ); + assert( RetValue ); +p->timeSimSat += clock() - clk; +} + +/**Function************************************************************* + + Synopsis [Performs fraiging for one node.] + + Description [Returns the fraiged node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_ManSweepNode( Dch_Man_t * p, Aig_Obj_t * pObj ) +{ + Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig; + int RetValue; + // get representative of this class + pObjRepr = Aig_ObjRepr( p->pAigTotal, pObj ); + if ( pObjRepr == NULL ) + return; + // get the fraiged node + pObjFraig = Dch_ObjFraig( pObj ); + // get the fraiged representative + pObjReprFraig = Dch_ObjFraig( pObjRepr ); + // if the fraiged nodes are the same, return + if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) ) + { + // remember the proved equivalence + p->pReprsProved[ pObj->Id ] = pObjRepr; + return; + } + assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pAigFraig) ); + RetValue = Dch_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) ); + if ( RetValue == -1 ) // timed out + return; + if ( RetValue == 1 ) // proved equivalent + { + pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase ); + Dch_ObjSetFraig( pObj, pObjFraig2 ); + // remember the proved equivalence + p->pReprsProved[ pObj->Id ] = pObjRepr; + return; + } + // disproved the equivalence + Dch_ManSweepResimulate( p, pObj, pObjRepr ); +} + +/**Function************************************************************* + + Synopsis [Performs fraiging for the internal nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_ManSweep( Dch_Man_t * p ) +{ + Bar_Progress_t * pProgress = NULL; + Aig_Obj_t * pObj, * pObjNew; + int i; + // map constants and PIs + p->pAigFraig = Aig_ManStart( Aig_ManObjNumMax(p->pAigTotal) ); + Aig_ManCleanData( p->pAigTotal ); + Aig_ManConst1(p->pAigTotal)->pData = Aig_ManConst1(p->pAigFraig); + Aig_ManForEachPi( p->pAigTotal, pObj, i ) + pObj->pData = Aig_ObjCreatePi( p->pAigFraig ); + // prepare class refinement procedures + Dch_ClassesSetData( p->ppClasses, NULL, NULL, Dch_NodeIsConstCex, Dch_NodesAreEqualCex ); + // sweep internal nodes + pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAigTotal) ); + Aig_ManForEachNode( p->pAigTotal, pObj, i ) + { + Bar_ProgressUpdate( pProgress, i, NULL ); + pObjNew = Aig_And( p->pAigFraig, Dch_ObjChild0Fra(pObj), Dch_ObjChild1Fra(pObj) ); + if ( pObjNew == NULL ) + continue; + Dch_ObjSetFraig( pObj, pObjNew ); + Dch_ManSweepNode( p, pObj ); + } + // update the representatives of the nodes (makes classes invalid) + FREE( p->pAigTotal->pReprs ); + p->pAigTotal->pReprs = p->pReprsProved; + p->pReprsProved = NULL; + // clean the mark + Aig_ManCleanMarkB( p->pAigTotal ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/dch/module.make b/src/aig/dch/module.make index ebe1ba7f..08d5a555 100644 --- a/src/aig/dch/module.make +++ b/src/aig/dch/module.make @@ -1,5 +1,9 @@ SRC += src/aig/dch/dchAig.c \ + src/aig/dch/dchChoice.c \ + src/aig/dch/dchClass.c \ + src/aig/dch/dchCnf.c \ src/aig/dch/dchCore.c \ src/aig/dch/dchMan.c \ src/aig/dch/dchSat.c \ - src/aig/dch/dchSim.c + src/aig/dch/dchSim.c \ + src/aig/dch/dchSweep.c diff --git a/src/aig/int/intM114.c b/src/aig/int/intM114.c index f92ba179..dbf078e2 100644 --- a/src/aig/int/intM114.c +++ b/src/aig/int/intM114.c @@ -206,7 +206,7 @@ int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward ) int * pGlobalVars; int clk, status, RetValue; int i, Var; - assert( p->pInterNew == NULL ); +// assert( p->pInterNew == NULL ); // derive the SAT solver pSat = Inter_ManDeriveSatSolver( p->pInter, p->pCnfInter, p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames, p->vVarsAB, fUseBackward ); diff --git a/src/aig/int/intM114p.c b/src/aig/int/intM114p.c index 69c643ae..77776f7e 100644 --- a/src/aig/int/intM114p.c +++ b/src/aig/int/intM114p.c @@ -322,6 +322,9 @@ Aig_Man_t * Inter_ManpInterpolateM114( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Ptr_t * vInters; int * pLits, * pClauses, * pVars; int nLits, nVars, i, k, iVar; + int nClauses; + + nClauses = M114p_SolverProofClauseNum(s); assert( M114p_SolverProofIsReady(s) ); @@ -346,7 +349,7 @@ Aig_Man_t * Inter_ManpInterpolateM114( M114p_Solver_t s, Vec_Int_t * vMapRoots, } } Vec_PtrPush( vInters, pInter ); - } + } // assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) ); // process learned clauses diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c index 1f6a28ef..0a991fff 100644 --- a/src/aig/ntl/ntlFraig.c +++ b/src/aig/ntl/ntlFraig.c @@ -97,8 +97,12 @@ void Ntl_ManUpdateNoMergeReprs( Aig_Man_t * pAig, Aig_Obj_t ** pReprs ) continue; } // remap the representative - assert( pObj->Id > pRepresNew->Id ); - pReprs[ pObj->Id ] = pRepresNew; +// assert( pObj->Id > pRepresNew->Id ); +// pReprs[ pObj->Id ] = pRepresNew; + if ( pObj->Id > pRepresNew->Id ) + pReprs[ pObj->Id ] = pRepresNew; + else + pReprs[ pObj->Id ] = NULL; } free( pReprsNew ); } diff --git a/src/aig/ntl/ntlWriteBlif.c b/src/aig/ntl/ntlWriteBlif.c index 9c8d55ae..6b7f0996 100644 --- a/src/aig/ntl/ntlWriteBlif.c +++ b/src/aig/ntl/ntlWriteBlif.c @@ -316,6 +316,8 @@ void Ioa_WriteBlifModelGz( gzFile pFile, Ntl_Mod_t * pModel, int fMain ) // gzprintf( pFile, " %s", pModel->attrKeep? "keep" : "sweep" ); gzprintf( pFile, "\n" ); } + if ( pModel->attrNoMerge ) + gzprintf( pFile, ".no_merge\n" ); gzprintf( pFile, ".inputs" ); Ntl_ModelForEachPi( pModel, pObj, i ) gzprintf( pFile, " %s", Ntl_ObjFanout0(pObj)->pName ); @@ -491,6 +493,8 @@ void Ioa_WriteBlifModelBz2( bz2file * b, Ntl_Mod_t * pModel, int fMain ) // fprintfBz2( b, " %s", pModel->attrKeep? "keep" : "sweep" ); fprintfBz2( b, "\n" ); } + if ( pModel->attrNoMerge ) + fprintfBz2( b, ".no_merge\n" ); fprintfBz2( b, ".inputs" ); Ntl_ModelForEachPi( pModel, pObj, i ) fprintfBz2( b, " %s", Ntl_ObjFanout0(pObj)->pName ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 45510e62..5e65d636 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -5860,7 +5860,7 @@ int Abc_CommandMuxes( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: fprintf( pErr, "usage: muxes [-h]\n" ); - fprintf( pErr, "\t converts the current network by a network derived by\n" ); + fprintf( pErr, "\t converts the current network into a network derived by\n" ); fprintf( pErr, "\t replacing all nodes by DAGs isomorphic to the local BDDs\n" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -7683,7 +7683,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) int nLevels; int fVerbose; int fVeryVerbose; - char * pFileName; +// char * pFileName; // extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk ); // extern Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk ); @@ -7703,6 +7703,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) // extern Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk, If_Lib_t * pLutLib ); extern Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose ); extern void Abc_NtkDarTest( Abc_Ntk_t * pNtk ); + extern void Aig_ProcedureTest(); pNtk = Abc_FrameReadNtk(pAbc); @@ -7902,11 +7903,15 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) } // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); -*/ +*//* + if ( argc != globalUtilOptind + 1 ) goto usage; pFileName = argv[globalUtilOptind]; Nwk_ManLutMergeGraphTest( pFileName ); +*/ + Aig_ProcedureTest(); + return 0; usage: fprintf( pErr, "usage: test [-h] <file_name>\n" ); @@ -8962,7 +8967,7 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults Dch_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WCSvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsvh" ) ) != EOF ) { switch ( c ) { @@ -8999,6 +9004,9 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nSatVarMax < 0 ) goto usage; break; + case 's': + pPars->fSynthesis ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -9029,11 +9037,12 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: dch [-WCS num] [-vh]\n" ); + fprintf( pErr, "usage: dch [-WCS num] [-svh]\n" ); fprintf( pErr, "\t performs computation of structural choices\n" ); fprintf( pErr, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords ); fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); fprintf( pErr, "\t-S num : the max number of SAT variables [default = %d]\n", pPars->nSatVarMax ); + fprintf( pErr, "\t-s : toggle synthesizing three snapshots [default = %s]\n", pPars->fSynthesis? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index c7e0df30..16215a64 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -834,16 +834,27 @@ Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars ) Vec_Ptr_t * vAigs; Aig_Man_t * pMan, * pTemp; Abc_Ntk_t * pNtkAig; - int i; + int i, clk; assert( Abc_NtkIsStrash(pNtk) ); pMan = Abc_NtkToDar( pNtk, 0, 0 ); if ( pMan == NULL ) return NULL; - vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, pPars->fVerbose ); - Aig_ManStop( pMan ); +clk = clock(); + if ( pPars->fSynthesis ) + { +// vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, pPars->fVerbose ); + vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, 0 ); + Aig_ManStop( pMan ); + } + else + { + vAigs = Vec_PtrAlloc( 1 ); + Vec_PtrPush( vAigs, pMan ); + } +pPars->timeSynth = clock() - clk; pMan = Dch_ComputeChoices( vAigs, pPars ); -// pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan ); - pNtkAig = Abc_NtkFromDar( pNtk, pMan ); + pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan ); +// pNtkAig = Abc_NtkFromDar( pNtk, pMan ); Aig_ManStop( pMan ); // cleanup Vec_PtrForEachEntry( vAigs, pTemp, i ) |