Skip to content

A
abc
Commit cbb7ff86 by Alan Mishchenko
Options

Version abc80802

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