diff options
Diffstat (limited to 'src/proof/dch')
| -rw-r--r-- | src/proof/dch/dch.h | 90 | ||||
| -rw-r--r-- | src/proof/dch/dchAig.c | 119 | ||||
| -rw-r--r-- | src/proof/dch/dchChoice.c | 508 | ||||
| -rw-r--r-- | src/proof/dch/dchClass.c | 611 | ||||
| -rw-r--r-- | src/proof/dch/dchCnf.c | 334 | ||||
| -rw-r--r-- | src/proof/dch/dchCore.c | 158 | ||||
| -rw-r--r-- | src/proof/dch/dchInt.h | 170 | ||||
| -rw-r--r-- | src/proof/dch/dchMan.c | 191 | ||||
| -rw-r--r-- | src/proof/dch/dchSat.c | 166 | ||||
| -rw-r--r-- | src/proof/dch/dchSim.c | 297 | ||||
| -rw-r--r-- | src/proof/dch/dchSimSat.c | 258 | ||||
| -rw-r--r-- | src/proof/dch/dchSweep.c | 146 | ||||
| -rw-r--r-- | src/proof/dch/module.make | 10 |
13 files changed, 3058 insertions, 0 deletions
diff --git a/src/proof/dch/dch.h b/src/proof/dch/dch.h new file mode 100644 index 00000000..731eb776 --- /dev/null +++ b/src/proof/dch/dch.h @@ -0,0 +1,90 @@ +/**CFile**************************************************************** + + FileName [dch.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Choice computation for tech-mapping.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 29, 2008.] + + Revision [$Id: dch.h,v 1.00 2008/07/29 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef ABC__aig__dch__dch_h +#define ABC__aig__dch__dch_h + + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + + + +ABC_NAMESPACE_HEADER_START + + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +// choicing parameters +typedef struct Dch_Pars_t_ Dch_Pars_t; +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 fPolarFlip; // uses polarity adjustment + int fSimulateTfo; // uses simulation of TFO classes + int fPower; // uses power-aware rewriting + int fUseGia; // uses GIA package + int fUseCSat; // uses circuit-based solver + int fLightSynth; // uses lighter version of synthesis + int fVerbose; // verbose stats + int timeSynth; // synthesis runtime + int nNodesAhead; // the lookahead in terms of nodes + int nCallsRecycle; // calls to perform before recycling SAT solver +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== dchAig.c ==========================================================*/ +extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs ); +/*=== dchCore.c ==========================================================*/ +extern void Dch_ManSetDefaultParams( Dch_Pars_t * p ); +extern int Dch_ManReadVerbose( Dch_Pars_t * p ); +extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars ); +extern void Dch_ComputeEquivalences( Aig_Man_t * pAig, Dch_Pars_t * pPars ); +/*=== dchScript.c ==========================================================*/ +extern Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars ); + + +ABC_NAMESPACE_HEADER_END + + + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/proof/dch/dchAig.c b/src/proof/dch/dchAig.c new file mode 100644 index 00000000..91a00c63 --- /dev/null +++ b/src/proof/dch/dchAig.c @@ -0,0 +1,119 @@ +/**CFile**************************************************************** + + FileName [dchAig.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Choice computation for tech-mapping.] + + Synopsis [AIG manipulation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 29, 2008.] + + Revision [$Id: dchAig.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "dchInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Derives the cumulative AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_DeriveTotalAig_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + if ( pObj->pData ) + return; + Dch_DeriveTotalAig_rec( p, Aig_ObjFanin0(pObj) ); + Dch_DeriveTotalAig_rec( p, Aig_ObjFanin1(pObj) ); + pObj->pData = Aig_And( p, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Derives the cumulative AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs ) +{ + Aig_Man_t * pAig, * pAig2, * pAigTotal; + Aig_Obj_t * pObj, * pObjPi, * pObjPo; + int i, k, nNodes; + assert( Vec_PtrSize(vAigs) > 0 ); + // make sure they have the same number of PIs/POs + nNodes = 0; + pAig = (Aig_Man_t *)Vec_PtrEntry( vAigs, 0 ); + Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, i ) + { + assert( Aig_ManPiNum(pAig) == Aig_ManPiNum(pAig2) ); + assert( Aig_ManPoNum(pAig) == Aig_ManPoNum(pAig2) ); + nNodes += Aig_ManNodeNum(pAig2); + Aig_ManCleanData( pAig2 ); + } + // map constant nodes + pAigTotal = Aig_ManStart( nNodes ); + Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k ) + Aig_ManConst1(pAig2)->pData = Aig_ManConst1(pAigTotal); + // map primary inputs + Aig_ManForEachPi( pAig, pObj, i ) + { + pObjPi = Aig_ObjCreatePi( pAigTotal ); + Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k ) + Aig_ManPi( pAig2, i )->pData = pObjPi; + } + // construct the AIG in the order of POs + Aig_ManForEachPo( pAig, pObj, i ) + { + Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k ) + { + pObjPo = Aig_ManPo( pAig2, i ); + Dch_DeriveTotalAig_rec( pAigTotal, Aig_ObjFanin0(pObjPo) ); + } + 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; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/dch/dchChoice.c b/src/proof/dch/dchChoice.c new file mode 100644 index 00000000..1772f8aa --- /dev/null +++ b/src/proof/dch/dchChoice.c @@ -0,0 +1,508 @@ +/**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" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// 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, * pPrev; + int i, nEquivs = 0, Counter = 0; + Aig_ManForEachObj( pAig, pObj, i ) + { + if ( !Aig_ObjIsChoice(pAig, pObj) ) + continue; + for ( pPrev = pObj, pTemp = Aig_ObjEquiv(pAig, pObj); pTemp; + pPrev = pTemp, pTemp = Aig_ObjEquiv(pAig, pTemp) ) + { + if ( pTemp->nRefs > 0 ) + { + // remove referenced node from equivalence class + assert( pAig->pEquivs[pPrev->Id] == pTemp ); + pAig->pEquivs[pPrev->Id] = pAig->pEquivs[pTemp->Id]; + pAig->pEquivs[pTemp->Id] = NULL; + // how about the need to continue iterating over the list? + // pPrev = pTemp ??? + Counter++; + } + nEquivs++; + } + } +// printf( "Removed %d classes.\n", Counter ); + + if ( Counter ) + Dch_DeriveChoiceCountEquivs( pAig ); +// if ( Counter ) +// printf( "Removed %d equiv nodes because of non-zero ref counter.\n", Counter ); + 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 [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((Aig_Obj_t *)pObj->pData); + pReprNew = Aig_Regular((Aig_Obj_t *)pRepr->pData); + if ( pObjNew == pReprNew ) + return; + // skip the earlier nodes + if ( pReprNew->Id > pObjNew->Id ) + return; + assert( pReprNew->Id < pObjNew->Id ); + // set the representatives + Aig_ObjSetRepr( pAigNew, pObjNew, pReprNew ); + // skip used nodes + if ( pObjNew->nRefs > 0 ) + return; + assert( pObjNew->nRefs == 0 ); + // update new nodes of the object + if ( !Aig_ObjIsNode(pRepr) ) + 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_old( 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 = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) ); + pChoices->pReprs = ABC_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 choices for the internal nodes + assert( pAig->pReprs != NULL ); + 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 + ABC_FREE( pChoices->pReprs ); + pChoices = Aig_ManDupDfs( pTemp = pChoices ); + Aig_ManStop( pTemp ); + return pChoices; +} + + + + +/**Function************************************************************* + + Synopsis [Checks for combinational loops in the AIG.] + + Description [Returns 1 if combinational loop is detected.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManCheckAcyclic_rec( Aig_Man_t * p, Aig_Obj_t * pNode, int fVerbose ) +{ + Aig_Obj_t * pFanin; + int fAcyclic; + if ( Aig_ObjIsPi(pNode) || Aig_ObjIsConst1(pNode) ) + return 1; + assert( Aig_ObjIsNode(pNode) ); + // make sure the node is not visited + assert( !Aig_ObjIsTravIdPrevious(p, pNode) ); + // check if the node is part of the combinational loop + if ( Aig_ObjIsTravIdCurrent(p, pNode) ) + { + if ( fVerbose ) + Abc_Print( 1, "Network \"%s\" contains combinational loop!\n", p->pSpec? p->pSpec : NULL ); + if ( fVerbose ) + Abc_Print( 1, "Node \"%d\" is encountered twice on the following path to the COs:\n", Aig_ObjId(pNode) ); + return 0; + } + // mark this node as a node on the current path + Aig_ObjSetTravIdCurrent( p, pNode ); + + // visit the transitive fanin + pFanin = Aig_ObjFanin0(pNode); + // check if the fanin is visited + if ( !Aig_ObjIsTravIdPrevious(p, pFanin) ) + { + // traverse the fanin's cone searching for the loop + if ( !(fAcyclic = Aig_ManCheckAcyclic_rec(p, pFanin, fVerbose)) ) + { + // return as soon as the loop is detected + if ( fVerbose ) + Abc_Print( 1, " %d ->", Aig_ObjId(pFanin) ); + return 0; + } + } + + // visit the transitive fanin + pFanin = Aig_ObjFanin1(pNode); + // check if the fanin is visited + if ( !Aig_ObjIsTravIdPrevious(p, pFanin) ) + { + // traverse the fanin's cone searching for the loop + if ( !(fAcyclic = Aig_ManCheckAcyclic_rec(p, pFanin, fVerbose)) ) + { + // return as soon as the loop is detected + if ( fVerbose ) + Abc_Print( 1, " %d ->", Aig_ObjId(pFanin) ); + return 0; + } + } + + // visit choices + if ( Aig_ObjRepr(p, pNode) == NULL && Aig_ObjEquiv(p, pNode) != NULL ) + { + for ( pFanin = Aig_ObjEquiv(p, pNode); pFanin; pFanin = Aig_ObjEquiv(p, pFanin) ) + { + // check if the fanin is visited + if ( Aig_ObjIsTravIdPrevious(p, pFanin) ) + continue; + // traverse the fanin's cone searching for the loop + if ( (fAcyclic = Aig_ManCheckAcyclic_rec(p, pFanin, fVerbose)) ) + continue; + // return as soon as the loop is detected + if ( fVerbose ) + Abc_Print( 1, " %d", Aig_ObjId(pFanin) ); + if ( fVerbose ) + Abc_Print( 1, " (choice of %d) -> ", Aig_ObjId(pNode) ); + return 0; + } + } + // mark this node as a visited node + Aig_ObjSetTravIdPrevious( p, pNode ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Checks for combinational loops in the AIG.] + + Description [Returns 1 if there is no combinational loops.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManCheckAcyclic( Aig_Man_t * p, int fVerbose ) +{ + Aig_Obj_t * pNode; + int fAcyclic; + int i; + // set the traversal ID for this DFS ordering + Aig_ManIncrementTravId( p ); + Aig_ManIncrementTravId( p ); + // pNode->TravId == pNet->nTravIds means "pNode is on the path" + // pNode->TravId == pNet->nTravIds - 1 means "pNode is visited but is not on the path" + // pNode->TravId < pNet->nTravIds - 1 means "pNode is not visited" + // traverse the network to detect cycles + fAcyclic = 1; + Aig_ManForEachPo( p, pNode, i ) + { + pNode = Aig_ObjFanin0(pNode); + if ( Aig_ObjIsTravIdPrevious(p, pNode) ) + continue; + // traverse the output logic cone + if ( (fAcyclic = Aig_ManCheckAcyclic_rec(p, pNode, fVerbose)) ) + continue; + // stop as soon as the first loop is detected + if ( fVerbose ) + Abc_Print( 1, " CO %d\n", i ); + break; + } + return fAcyclic; +} + +/**Function************************************************************* + + Synopsis [Removes combinational loop.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManFixLoopProblem( Aig_Man_t * p, int fVerbose ) +{ + Aig_Obj_t * pObj; + int i, Counter = 0, Counter2 = 0; + Aig_ManForEachObj( p, pObj, i ) + { + if ( !Aig_ObjIsTravIdCurrent(p, pObj) ) + continue; + Counter2++; + if ( Aig_ObjRepr(p, pObj) == NULL && Aig_ObjEquiv(p, pObj) != NULL ) + { + Aig_ObjSetEquiv(p, pObj, NULL); + Counter++; + } + } + if ( fVerbose ) + Abc_Print( 1, "Fixed %d choice nodes on the path with %d objects.\n", Counter, Counter2 ); +} + + +/**Function************************************************************* + + Synopsis [Derives the AIG with choices from representatives.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Dch_DeriveChoiceAigInt( 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 = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) ); + pChoices->pReprs = ABC_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 choices for the internal nodes + assert( pAig->pReprs != NULL ); + 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 ); + Aig_ManSetRegNum( pChoices, Aig_ManRegNum(pAig) ); + return pChoices; +} + +/**Function************************************************************* + + Synopsis [Derives the AIG with choices from representatives.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig ) +{ + extern int Aig_ManCheckAcyclic( Aig_Man_t * pAig, int fVerbose ); + Aig_Man_t * pChoices, * pTemp; + int fVerbose = 0; + pChoices = Dch_DeriveChoiceAigInt( pAig ); +// pChoices = Dch_DeriveChoiceAigInt( pTemp = pChoices ); +// Aig_ManStop( pTemp ); + // there is no need for cleanup + ABC_FREE( pChoices->pReprs ); + while ( !Aig_ManCheckAcyclic( pChoices, fVerbose ) ) + { + if ( fVerbose ) + Abc_Print( 1, "There is a loop!\n" ); + Aig_ManFixLoopProblem( pChoices, fVerbose ); + } + pChoices = Aig_ManDupDfs( pTemp = pChoices ); + Aig_ManStop( pTemp ); + return pChoices; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/dch/dchClass.c b/src/proof/dch/dchClass.c new file mode 100644 index 00000000..24476309 --- /dev/null +++ b/src/proof/dch/dchClass.c @@ -0,0 +1,611 @@ +/**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" + +ABC_NAMESPACE_IMPL_START + + +/* + 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 topo 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 hash 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 = ABC_ALLOC( Dch_Cla_t, 1 ); + memset( p, 0, sizeof(Dch_Cla_t) ); + p->pAig = pAig; + p->pId2Class = ABC_CALLOC( Aig_Obj_t **, Aig_ManObjNumMax(pAig) ); + p->pClassSizes = ABC_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 hash 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 ); + ABC_FREE( p->pId2Class ); + ABC_FREE( p->pClassSizes ); + ABC_FREE( p->pMemClasses ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Stop representation of equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dch_ClassesLitNum( Dch_Cla_t * p ) +{ + return p->nLits; +} + +/**Function************************************************************* + + Synopsis [Stop representation of equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t ** Dch_ClassesReadClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize ) +{ + assert( p->pId2Class[pRepr->Id] != NULL ); + assert( p->pClassSizes[pRepr->Id] > 1 ); + *pnSize = p->pClassSizes[pRepr->Id]; + return p->pId2Class[pRepr->Id]; +} + +/**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; + Abc_Print( 1, "{ " ); + Dch_ClassForEachNode( p, pRepr, pObj, i ) + Abc_Print( 1, "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) ); + Abc_Print( 1, "}\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; + Abc_Print( 1, "Equivalence classes: Const1 = %5d. Class = %5d. Lit = %5d.\n", + p->nCands1, p->nClasses, p->nLits ); + if ( !fVeryVerbose ) + return; + Abc_Print( 1, "Constants { " ); + Aig_ManForEachObj( p->pAig, pObj, i ) + if ( Dch_ObjIsConst1Cand( p->pAig, pObj ) ) + Abc_Print( 1, "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) ); + Abc_Print( 1, "}\n" ); + Dch_ManForEachClass( p, ppClass, i ) + { + Abc_Print( 1, "%3d (%3d) : ", i, p->pClassSizes[i] ); + Dch_ClassesPrintOne( p, ppClass[0] ); + } + Abc_Print( 1, "\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 = Abc_PrimeCudd( Aig_ManObjNumMax(p->pAig)/4 ); + ppTable = ABC_CALLOC( Aig_Obj_t *, nTableSize ); + ppNexts = ABC_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 = ABC_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 ); + ABC_FREE( ppTable ); + ABC_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 = (Aig_Obj_t *)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( Aig_Obj_t *, p->vClassOld, pObj, i ) + { + pClassOld[i] = pObj; + Aig_ObjSetRepr( p->pAig, pObj, i? pReprOld : NULL ); + } + // create new class + pClassNew = pClassOld + i; + Vec_PtrForEachEntry( Aig_Obj_t *, 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) ); + + // check if the class should 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 = Abc_MinInt( 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; + if ( Vec_PtrSize(vRoots) == 0 ) + return 0; + // collect the nodes to be refined + Vec_PtrClear( p->vClassNew ); + Vec_PtrForEachEntry( Aig_Obj_t *, 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 = (Aig_Obj_t *)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( Aig_Obj_t *, 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 /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/dch/dchCnf.c b/src/proof/dch/dchCnf.c new file mode 100644 index 00000000..4175a123 --- /dev/null +++ b/src/proof/dch/dchCnf.c @@ -0,0 +1,334 @@ +/**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" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// 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); + if ( p->pPars->fPolarFlip ) + { + if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] ); + if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] ); + if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] ); + } + 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); + if ( p->pPars->fPolarFlip ) + { + if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] ); + if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] ); + if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] ); + } + 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); + if ( p->pPars->fPolarFlip ) + { + if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] ); + if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] ); + if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] ); + } + 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); + if ( p->pPars->fPolarFlip ) + { + if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] ); + if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] ); + if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] ); + } + 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); + if ( p->pPars->fPolarFlip ) + { + if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] ); + if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] ); + if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] ); + } + 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); + if ( p->pPars->fPolarFlip ) + { + if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] ); + if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] ); + if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] ); + } + 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 = ABC_ALLOC( int, nLits ); + // suppose AND-gate is A & B = C + // add !A => !C or A + !C + Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i ) + { + pLits[0] = toLitCond(Dch_ObjSatNum(p,Aig_Regular(pFanin)), Aig_IsComplement(pFanin)); + pLits[1] = toLitCond(Dch_ObjSatNum(p,pNode), 1); + if ( p->pPars->fPolarFlip ) + { + if ( Aig_Regular(pFanin)->fPhase ) pLits[0] = lit_neg( pLits[0] ); + if ( pNode->fPhase ) pLits[1] = lit_neg( pLits[1] ); + } + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); + assert( RetValue ); + } + // add A & B => C or !A + !B + C + Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i ) + { + pLits[i] = toLitCond(Dch_ObjSatNum(p,Aig_Regular(pFanin)), !Aig_IsComplement(pFanin)); + if ( p->pPars->fPolarFlip ) + { + if ( Aig_Regular(pFanin)->fPhase ) pLits[i] = lit_neg( pLits[i] ); + } + } + pLits[nLits-1] = toLitCond(Dch_ObjSatNum(p,pNode), 0); + if ( p->pPars->fPolarFlip ) + { + if ( pNode->fPhase ) pLits[nLits-1] = lit_neg( pLits[nLits-1] ); + } + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits ); + assert( RetValue ); + ABC_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; + Vec_PtrPush( p->vUsedNodes, pObj ); + 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( Aig_Obj_t *, 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( Aig_Obj_t *, p->vFanins, pFanin, k ) + Dch_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier ); + Dch_AddClausesMux( p, pNode ); + } + else + { + Dch_CollectSuper( pNode, fUseMuxes, p->vFanins ); + Vec_PtrForEachEntry( Aig_Obj_t *, 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 /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/dch/dchCore.c b/src/proof/dch/dchCore.c new file mode 100644 index 00000000..bc78682b --- /dev/null +++ b/src/proof/dch/dchCore.c @@ -0,0 +1,158 @@ +/**CFile**************************************************************** + + FileName [dchCore.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Choice computation for tech-mapping.] + + Synopsis [The core procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 29, 2008.] + + Revision [$Id: dchCore.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "dchInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [This procedure sets default parameters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_ManSetDefaultParams( Dch_Pars_t * p ) +{ + memset( p, 0, sizeof(Dch_Pars_t) ); + p->nWords = 8; // the number of simulation words + p->nBTLimit = 1000; // conflict limit at a node + p->nSatVarMax = 5000; // the max number of SAT variables + p->fSynthesis = 1; // derives three snapshots + p->fPolarFlip = 1; // uses polarity adjustment + p->fSimulateTfo = 1; // simulate TFO + p->fPower = 0; // power-aware rewriting + p->fLightSynth = 0; // uses lighter version of synthesis + p->fVerbose = 0; // verbose stats + p->nNodesAhead = 1000; // the lookahead in terms of nodes + p->nCallsRecycle = 100; // calls to perform before recycling SAT solver +} + +/**Function************************************************************* + + Synopsis [Returns verbose parameter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dch_ManReadVerbose( Dch_Pars_t * p ) +{ + return p->fVerbose; +} + +/**Function************************************************************* + + Synopsis [Performs computation of AIGs with choices.] + + Description [Takes several AIGs and performs choicing.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars ) +{ + Dch_Man_t * p; + Aig_Man_t * pResult; + int clk, clkTotal = clock(); + // reset random numbers + Aig_ManRandom(1); + // start the choicing manager + p = Dch_ManCreate( pAig, pPars ); + // compute candidate equivalence classes +clk = clock(); + p->ppClasses = Dch_CreateCandEquivClasses( pAig, 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 ); + // free memory ahead of time +p->timeTotal = clock() - clkTotal; + Dch_ManStop( p ); + // create choices + ABC_FREE( pAig->pTable ); + pResult = Dch_DeriveChoiceAig( pAig ); + // count the number of representatives + if ( pPars->fVerbose ) + Abc_Print( 1, "STATS: Reprs = %6d. Equivs = %6d. Choices = %6d.\n", + Dch_DeriveChoiceCountReprs( pAig ), + Dch_DeriveChoiceCountEquivs( pResult ), + Aig_ManChoiceNum( pResult ) ); + return pResult; +} + +/**Function************************************************************* + + Synopsis [Performs computation of AIGs with choices.] + + Description [Takes several AIGs and performs choicing.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_ComputeEquivalences( Aig_Man_t * pAig, Dch_Pars_t * pPars ) +{ + Dch_Man_t * p; + int clk, clkTotal = clock(); + // reset random numbers + Aig_ManRandom(1); + // start the choicing manager + p = Dch_ManCreate( pAig, pPars ); + // compute candidate equivalence classes +clk = clock(); + p->ppClasses = Dch_CreateCandEquivClasses( pAig, 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 ); + // free memory ahead of time +p->timeTotal = clock() - clkTotal; + Dch_ManStop( p ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/dch/dchInt.h b/src/proof/dch/dchInt.h new file mode 100644 index 00000000..c9f2f4f6 --- /dev/null +++ b/src/proof/dch/dchInt.h @@ -0,0 +1,170 @@ +/**CFile**************************************************************** + + FileName [dchInt.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Choice computation for tech-mapping.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 29, 2008.] + + Revision [$Id: dchInt.h,v 1.00 2008/07/29 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef ABC__aig__dch__dchInt_h +#define ABC__aig__dch__dchInt_h + + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include "src/aig/aig/aig.h" +#include "src/sat/bsat/satSolver.h" +#include "dch.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + + + +ABC_NAMESPACE_HEADER_START + + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +// equivalence classes +typedef struct Dch_Cla_t_ Dch_Cla_t; + +// choicing manager +typedef struct Dch_Man_t_ Dch_Man_t; +struct Dch_Man_t_ +{ + // parameters + 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 + // equivalence classes + Dch_Cla_t * ppClasses; // equivalence classes of nodes + Aig_Obj_t ** pReprsProved; // equivalences proved + // SAT solving + 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 + int nCallsSince; // the number of calls since the last recycle + Vec_Ptr_t * vFanins; // fanins of the CNF node + Vec_Ptr_t * vSimRoots; // the roots of cand const 1 nodes to simulate + Vec_Ptr_t * vSimClasses; // the roots of cand equiv classes to simulate + // 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_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; } + +static inline Aig_Obj_t * Dch_ObjFraig( Aig_Obj_t * pObj ) { return (Aig_Obj_t *)pObj->pData; } +static inline void Dch_ObjSetFraig( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { pObj->pData = pNode; } + +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) ); +} + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== dchAig.c ===================================================*/ +/*=== 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 Aig_Obj_t ** Dch_ClassesReadClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize ); +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( Aig_Man_t * pAig, 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 ); +/*=== dchSimSat.c ===================================================*/ +extern void Dch_ManResimulateCex( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr ); +extern void Dch_ManResimulateCex2( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr ); +/*=== dchSweep.c ===================================================*/ +extern void Dch_ManSweep( Dch_Man_t * p ); + + + +ABC_NAMESPACE_HEADER_END + + + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/proof/dch/dchMan.c b/src/proof/dch/dchMan.c new file mode 100644 index 00000000..dc856309 --- /dev/null +++ b/src/proof/dch/dchMan.c @@ -0,0 +1,191 @@ +/**CFile**************************************************************** + + FileName [dchMan.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: dchMan.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "dchInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dch_Man_t * Dch_ManCreate( Aig_Man_t * pAig, Dch_Pars_t * pPars ) +{ + Dch_Man_t * p; + // create interpolation manager + p = ABC_ALLOC( Dch_Man_t, 1 ); + memset( p, 0, sizeof(Dch_Man_t) ); + p->pPars = pPars; + p->pAigTotal = pAig; //Dch_DeriveTotalAig( vAigs ); + Aig_ManFanoutStart( p->pAigTotal ); + // SAT solving + p->nSatVars = 1; + p->pSatVars = ABC_CALLOC( int, Aig_ManObjNumMax(p->pAigTotal) ); + p->vUsedNodes = Vec_PtrAlloc( 1000 ); + p->vFanins = Vec_PtrAlloc( 100 ); + p->vSimRoots = Vec_PtrAlloc( 1000 ); + p->vSimClasses = Vec_PtrAlloc( 1000 ); + // equivalences proved + p->pReprsProved = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAigTotal) ); + return p; +} + +/**Function************************************************************* + + Synopsis [Prints stats of the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_ManPrintStats( Dch_Man_t * p ) +{ + int nNodeNum = Aig_ManNodeNum(p->pAigTotal) / 3; + Abc_Print( 1, "Parameters: Sim words = %d. Conf limit = %d. SAT var max = %d.\n", + p->pPars->nWords, p->pPars->nBTLimit, p->pPars->nSatVarMax ); + Abc_Print( 1, "AIG nodes : Total = %6d. Dangling = %6d. Main = %6d. (%6.2f %%)\n", + Aig_ManNodeNum(p->pAigTotal), + Aig_ManNodeNum(p->pAigTotal)-nNodeNum, + nNodeNum, + 100.0 * nNodeNum/Aig_ManNodeNum(p->pAigTotal) ); + Abc_Print( 1, "SAT solver: Vars = %d. Max cone = %d. Recycles = %d.\n", + p->nSatVars, p->nConeMax, p->nRecycles ); + Abc_Print( 1, "SAT calls : All = %6d. Unsat = %6d. Sat = %6d. Fail = %6d.\n", + p->nSatCalls, p->nSatCalls-p->nSatCallsSat-p->nSatFailsReal, + p->nSatCallsSat, p->nSatFailsReal ); + Abc_Print( 1, "Choices : Lits = %6d. Reprs = %5d. Equivs = %5d. Choices = %5d.\n", + p->nLits, p->nReprs, p->nEquivs, p->nChoices ); + Abc_Print( 1, "Choicing runtime statistics:\n" ); + p->timeOther = p->timeTotal-p->timeSimInit-p->timeSimSat-p->timeSat-p->timeChoice; + Abc_PrintTimeP( 1, "Sim init ", p->timeSimInit, p->timeTotal ); + Abc_PrintTimeP( 1, "Sim SAT ", p->timeSimSat, p->timeTotal ); + Abc_PrintTimeP( 1, "SAT solving", p->timeSat, p->timeTotal ); + Abc_PrintTimeP( 1, " sat ", p->timeSatSat, p->timeTotal ); + Abc_PrintTimeP( 1, " unsat ", p->timeSatUnsat, p->timeTotal ); + Abc_PrintTimeP( 1, " undecided", p->timeSatUndec, p->timeTotal ); + Abc_PrintTimeP( 1, "Choice ", p->timeChoice, p->timeTotal ); + Abc_PrintTimeP( 1, "Other ", p->timeOther, p->timeTotal ); + Abc_PrintTimeP( 1, "TOTAL ", p->timeTotal, p->timeTotal ); + if ( p->pPars->timeSynth ) + { + Abc_PrintTime( 1, "Synthesis ", p->pPars->timeSynth ); + } +} + +/**Function************************************************************* + + Synopsis [Frees the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_ManStop( Dch_Man_t * p ) +{ + Aig_ManFanoutStop( p->pAigTotal ); + if ( p->pPars->fVerbose ) + Dch_ManPrintStats( p ); + if ( p->pAigFraig ) + Aig_ManStop( p->pAigFraig ); + 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->vSimRoots ); + Vec_PtrFree( p->vSimClasses ); + ABC_FREE( p->pReprsProved ); + ABC_FREE( p->pSatVars ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Recycles the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_ManSatSolverRecycle( Dch_Man_t * p ) +{ + int Lit; + if ( p->pSat ) + { + Aig_Obj_t * pObj; + int i; + Vec_PtrForEachEntry( Aig_Obj_t *, p->vUsedNodes, pObj, i ) + Dch_ObjSetSatNum( p, pObj, 0 ); + Vec_PtrClear( p->vUsedNodes ); +// memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAigTotal) ); + sat_solver_delete( p->pSat ); + } + p->pSat = sat_solver_new(); + sat_solver_setnvars( p->pSat, 1000 ); + // var 0 is not used + // var 1 is reserved for const1 node - add the clause + p->nSatVars = 1; +// p->nSatVars = 0; + Lit = toLit( p->nSatVars ); + if ( p->pPars->fPolarFlip ) + Lit = lit_neg( Lit ); + sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); + Dch_ObjSetSatNum( p, Aig_ManConst1(p->pAigFraig), p->nSatVars++ ); + + p->nRecycles++; + p->nCallsSince = 0; +} + + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/dch/dchSat.c b/src/proof/dch/dchSat.c new file mode 100644 index 00000000..f5e346ef --- /dev/null +++ b/src/proof/dch/dchSat.c @@ -0,0 +1,166 @@ +/**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" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Runs equivalence test for the two nodes.] + + Description [] + + SideEffects [] + + 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 ); + + p->nCallsSince++; // experiment with this!!! + + // check if SAT solver needs recycling + if ( p->pSat == NULL || + (p->pPars->nSatVarMax && + p->nSatVars > p->pPars->nSatVarMax && + p->nCallsSince > p->pPars->nCallsRecycle) ) + 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 ); + if ( p->pPars->fPolarFlip ) + { + if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] ); + if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] ); + } +//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 ); +clk = clock(); + RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, + (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)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 ); + if ( p->pPars->fPolarFlip ) + { + if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] ); + if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] ); + } +clk = clock(); + RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, + (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)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 /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/dch/dchSim.c b/src/proof/dch/dchSim.c new file mode 100644 index 00000000..b2d24761 --- /dev/null +++ b/src/proof/dch/dchSim.c @@ -0,0 +1,297 @@ +/**CFile**************************************************************** + + FileName [dchSim.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Choice computation for tech-mapping.] + + Synopsis [Performs random simulation at the beginning.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 29, 2008.] + + Revision [$Id: dchSim.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "dchInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline unsigned * Dch_ObjSim( Vec_Ptr_t * vSims, Aig_Obj_t * pObj ) +{ + return (unsigned *)Vec_PtrEntry( vSims, pObj->Id ); +} +static inline unsigned Dch_ObjRandomSim() +{ + return Aig_ManRandom(0); +} + +//////////////////////////////////////////////////////////////////////// +/// 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 [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 = (Vec_Ptr_t *)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 = (Vec_Ptr_t *)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 = (Vec_Ptr_t *)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 [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_PerformRandomSimulation( Aig_Man_t * pAig, Vec_Ptr_t * vSims ) +{ + unsigned * pSim, * pSim0, * pSim1; + Aig_Obj_t * pObj; + int i, k, nWords; + nWords = (unsigned *)Vec_PtrEntry(vSims, 1) - (unsigned *)Vec_PtrEntry(vSims, 0); + + // assign const 1 sim info + pObj = Aig_ManConst1(pAig); + pSim = Dch_ObjSim( vSims, pObj ); + memset( pSim, 0xff, sizeof(unsigned) * nWords ); + + // assign primary input random sim info + Aig_ManForEachPi( pAig, pObj, i ) + { + pSim = Dch_ObjSim( vSims, pObj ); + for ( k = 0; k < nWords; k++ ) + pSim[k] = Dch_ObjRandomSim(); + pSim[0] <<= 1; + } + + // simulate AIG in the topological order + Aig_ManForEachNode( pAig, pObj, i ) + { + pSim0 = Dch_ObjSim( vSims, Aig_ObjFanin0(pObj) ); + pSim1 = Dch_ObjSim( vSims, Aig_ObjFanin1(pObj) ); + pSim = Dch_ObjSim( vSims, pObj ); + + if ( Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) ) // both are compls + { + for ( k = 0; k < nWords; k++ ) + pSim[k] = ~pSim0[k] & ~pSim1[k]; + } + else if ( Aig_ObjFaninC0(pObj) && !Aig_ObjFaninC1(pObj) ) // first one is compl + { + for ( k = 0; k < nWords; k++ ) + pSim[k] = ~pSim0[k] & pSim1[k]; + } + else if ( !Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) ) // second one is compl + { + for ( k = 0; k < nWords; k++ ) + pSim[k] = pSim0[k] & ~pSim1[k]; + } + else // if ( Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) ) // none is compl + { + for ( k = 0; k < nWords; k++ ) + pSim[k] = pSim0[k] & pSim1[k]; + } + } + // get simulation information for primary outputs +} + +/**Function************************************************************* + + Synopsis [Derives candidate equivalence classes of AIG nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dch_Cla_t * Dch_CreateCandEquivClasses( Aig_Man_t * pAig, int nWords, int fVerbose ) +{ + Dch_Cla_t * pClasses; + Vec_Ptr_t * vSims; + int i; + // allocate simulation information + vSims = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(pAig), 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_ClassesPrepare( pClasses, 0, 0 ); + // iterate random simulation + for ( i = 0; i < 7; i++ ) + { + Dch_PerformRandomSimulation( pAig, vSims ); + Dch_ClassesRefine( pClasses ); + } + // clean up and return + Vec_PtrFree( vSims ); + // prepare class refinement procedures + Dch_ClassesSetData( pClasses, NULL, NULL, Dch_NodeIsConstCex, Dch_NodesAreEqualCex ); + return pClasses; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/dch/dchSimSat.c b/src/proof/dch/dchSimSat.c new file mode 100644 index 00000000..808e754a --- /dev/null +++ b/src/proof/dch/dchSimSat.c @@ -0,0 +1,258 @@ +/**CFile**************************************************************** + + FileName [dchSimSat.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Choice computation for tech-mapping.] + + Synopsis [Performs resimulation using counter-examples.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 29, 2008.] + + Revision [$Id: dchSimSat.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "dchInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Collects internal nodes in the reverse DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_ManCollectTfoCands_rec( Dch_Man_t * p, Aig_Obj_t * pObj ) +{ + Aig_Obj_t * pFanout, * pRepr; + int iFanout = -1, i; + assert( !Aig_IsComplement(pObj) ); + if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) ) + return; + Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj); + // traverse the fanouts + Aig_ObjForEachFanout( p->pAigTotal, pObj, pFanout, iFanout, i ) + Dch_ManCollectTfoCands_rec( p, pFanout ); + // check if the given node has a representative + pRepr = Aig_ObjRepr( p->pAigTotal, pObj ); + if ( pRepr == NULL ) + return; + // pRepr is the constant 1 node + if ( pRepr == Aig_ManConst1(p->pAigTotal) ) + { + Vec_PtrPush( p->vSimRoots, pObj ); + return; + } + // pRepr is the representative of an equivalence class + if ( pRepr->fMarkA ) + return; + pRepr->fMarkA = 1; + Vec_PtrPush( p->vSimClasses, pRepr ); +} + +/**Function************************************************************* + + Synopsis [Collect equivalence classes and const1 cands in the TFO.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_ManCollectTfoCands( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 ) +{ + Aig_Obj_t * pObj; + int i; + Vec_PtrClear( p->vSimRoots ); + Vec_PtrClear( p->vSimClasses ); + Aig_ManIncrementTravId( p->pAigTotal ); + Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) ); + Dch_ManCollectTfoCands_rec( p, pObj1 ); + Dch_ManCollectTfoCands_rec( p, pObj2 ); + Vec_PtrSort( p->vSimRoots, (int (*)(void))Aig_ObjCompareIdIncrease ); + Vec_PtrSort( p->vSimClasses, (int (*)(void))Aig_ObjCompareIdIncrease ); + Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimClasses, pObj, i ) + pObj->fMarkA = 0; +} + +/**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) ) + { + Aig_Obj_t * pObjFraig; + int nVarNum; + pObjFraig = Dch_ObjFraig( pObj ); + assert( !Aig_IsComplement(pObjFraig) ); + nVarNum = Dch_ObjSatNum( p, pObjFraig ); + // get the value from the SAT solver + // (account for the fact that some vars may be minimized away) + pObj->fMarkB = !nVarNum? 0 : sat_solver_var_value( p->pSat, nVarNum ); +// pObj->fMarkB = !nVarNum? Aig_ManRandom(0) & 1 : sat_solver_var_value( p->pSat, nVarNum ); + 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_ManResimulateCex( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr ) +{ + Aig_Obj_t * pRoot, ** ppClass; + int i, k, nSize, RetValue1, RetValue2, clk = clock(); + // get the equivalence classes + Dch_ManCollectTfoCands( p, pObj, pRepr ); + // 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 = Abc_MaxInt( p->nConeMax, p->nConeThis ); + // resimulate the cone of influence of the other nodes + Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimRoots, pRoot, i ) + Dch_ManResimulateOther_rec( p, pRoot ); + // refine these nodes + RetValue1 = Dch_ClassesRefineConst1Group( p->ppClasses, p->vSimRoots, 0 ); + // resimulate the cone of influence of the cand classes + RetValue2 = 0; + Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimClasses, pRoot, i ) + { + ppClass = Dch_ClassesReadClass( p->ppClasses, pRoot, &nSize ); + for ( k = 0; k < nSize; k++ ) + Dch_ManResimulateOther_rec( p, ppClass[k] ); + // refine this class + RetValue2 += Dch_ClassesRefineOneClass( p->ppClasses, pRoot, 0 ); + } + // make sure refinement happened + if ( Aig_ObjIsConst1(pRepr) ) + assert( RetValue1 ); + else + assert( RetValue2 ); +p->timeSimSat += clock() - clk; +} + +/**Function************************************************************* + + Synopsis [Handle the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_ManResimulateCex2( 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->vSimRoots ); + else + Dch_ClassesCollectOneClass( p->ppClasses, pRepr, p->vSimRoots ); + // 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 = Abc_MaxInt( p->nConeMax, p->nConeThis ); + // resimulate the cone of influence of the other nodes + Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimRoots, pRoot, i ) + Dch_ManResimulateOther_rec( p, pRoot ); + // refine this class + if ( Dch_ObjIsConst1Cand(p->pAigTotal, pObj) ) + RetValue = Dch_ClassesRefineConst1Group( p->ppClasses, p->vSimRoots, 0 ); + else + RetValue = Dch_ClassesRefineOneClass( p->ppClasses, pRepr, 0 ); + assert( RetValue ); +p->timeSimSat += clock() - clk; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/dch/dchSweep.c b/src/proof/dch/dchSweep.c new file mode 100644 index 00000000..a1c4f79b --- /dev/null +++ b/src/proof/dch/dchSweep.c @@ -0,0 +1,146 @@ +/**CFile**************************************************************** + + FileName [dchSweep.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Choice computation for tech-mapping.] + + Synopsis [One round of SAT sweeping.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 29, 2008.] + + Revision [$Id: dchSweep.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "dchInt.h" +#include "src/misc/bar/bar.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +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 [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 ); + if ( pObjFraig == NULL ) + return; + // get the fraiged representative + pObjReprFraig = Dch_ObjFraig( pObjRepr ); + if ( pObjReprFraig == NULL ) + return; + // 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 + { + Dch_ObjSetFraig( pObj, NULL ); + 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 + if ( p->pPars->fSimulateTfo ) + Dch_ManResimulateCex( p, pObj, pObjRepr ); + else + Dch_ManResimulateCex2( p, pObj, pObjRepr ); + assert( Aig_ObjRepr( p->pAigTotal, 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 ); + // sweep internal nodes + pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAigTotal) ); + Aig_ManForEachNode( p->pAigTotal, pObj, i ) + { + Bar_ProgressUpdate( pProgress, i, NULL ); + if ( Dch_ObjFraig(Aig_ObjFanin0(pObj)) == NULL || + Dch_ObjFraig(Aig_ObjFanin1(pObj)) == NULL ) + continue; + pObjNew = Aig_And( p->pAigFraig, Dch_ObjChild0Fra(pObj), Dch_ObjChild1Fra(pObj) ); + if ( pObjNew == NULL ) + continue; + Dch_ObjSetFraig( pObj, pObjNew ); + Dch_ManSweepNode( p, pObj ); + } + Bar_ProgressStop( pProgress ); + // update the representatives of the nodes (makes classes invalid) + ABC_FREE( p->pAigTotal->pReprs ); + p->pAigTotal->pReprs = p->pReprsProved; + p->pReprsProved = NULL; + // clean the mark + Aig_ManCleanMarkB( p->pAigTotal ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/dch/module.make b/src/proof/dch/module.make new file mode 100644 index 00000000..11163cef --- /dev/null +++ b/src/proof/dch/module.make @@ -0,0 +1,10 @@ +SRC += src/proof/dch/dchAig.c \ + src/proof/dch/dchChoice.c \ + src/proof/dch/dchClass.c \ + src/proof/dch/dchCnf.c \ + src/proof/dch/dchCore.c \ + src/proof/dch/dchMan.c \ + src/proof/dch/dchSat.c \ + src/proof/dch/dchSim.c \ + src/proof/dch/dchSimSat.c \ + src/proof/dch/dchSweep.c |