luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Version abc90714 

committer: Baruch Sterin <baruchs@gmail.com>
This commit is contained in:
Alan Mishchenko 2015-06-22 23:04:53 -07:00
parent 70697f868a
commit 0398ced824
67 changed files with 2536 additions and 456 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

68
abclib.dsp
View File

@ -231,6 +231,10 @@ SOURCE=.\src\base\abci\abcDelay.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcDprove2.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcDress.c
# End Source File
# Begin Source File
@ -2269,6 +2273,14 @@ SOURCE=.\src\misc\util\abc_global.h
SOURCE=.\src\misc\util\util_hack.h
# End Source File
# Begin Source File
SOURCE=.\src\misc\util\utilMem.c
# End Source File
# Begin Source File
SOURCE=.\src\misc\util\utilMem.h
# End Source File
# End Group
# Begin Group "nm"
@ -3107,6 +3119,10 @@ SOURCE=.\src\aig\ntl\ntlMap.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ntl\ntlNames.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ntl\ntlObj.c
# End Source File
# Begin Source File
@ -3669,46 +3685,6 @@ SOURCE=.\src\aig\cgt\cgtSat.c
# Begin Group "nal"
# PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\aig\nal090422\nal.h
# End Source File
# Begin Source File
SOURCE=.\src\aig\nal090422\nalCore.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\nal090422\nalFlop.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\nal090422\nalFunc.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\nal090422\nalInt.h
# End Source File
# Begin Source File
SOURCE=.\src\aig\nal090422\nalMan.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\nal090422\nalModels.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\nal090422\nalRead.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\nal090422\nalUtil.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\nal090422\nalWrite.c
# End Source File
# End Group
# Begin Group "gia"
@ -3747,6 +3723,10 @@ SOURCE=.\src\aig\gia\giaCSatOld.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaCTas.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaDfs.c
# End Source File
# Begin Source File
@ -3787,6 +3767,10 @@ SOURCE=.\src\aig\gia\giaFront.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaGiarf.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaGlitch.c
# End Source File
# Begin Source File
@ -3795,6 +3779,10 @@ SOURCE=.\src\aig\gia\giaHash.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaHcd.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaMan.c
# End Source File
# Begin Source File

5
src/aig/aig/aig.h
View File

@ -481,13 +481,16 @@ extern Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupTrim( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Aig_Man_t * pGuide );
extern Vec_Ptr_t * Aig_ManOrderPios( Aig_Man_t * p, Aig_Man_t * pOrder );
extern Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Vec_Ptr_t * vPios );
extern Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupRepres( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupRepresDfs( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int fImpl );
extern Aig_Man_t * Aig_ManDupOrpos( Aig_Man_t * p, int fAddRegs );
extern Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum, int fAddRegs );
extern Aig_Man_t * Aig_ManDupUnsolvedOutputs( Aig_Man_t * p, int fAddRegs );
/*=== aigFanout.c ==========================================================*/
extern void Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
extern void Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );

104
src/aig/aig/aigDup.c
View File

@ -602,9 +602,8 @@ Aig_Obj_t * Aig_ManDupDfsGuided_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Aig_Man_t * pGuide )
Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Vec_Ptr_t * vPios )
{
Vec_Ptr_t * vPios;
Aig_Man_t * pNew;
Aig_Obj_t * pObj, * pObjNew;
int i, nNodes;
@ -631,7 +630,6 @@ Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Aig_Man_t * pGuide )
// duplicate internal nodes
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
vPios = Aig_ManOrderPios( p, pGuide );
Vec_PtrForEachEntry( vPios, pObj, i )
{
if ( Aig_ObjIsPi(pObj) )
@ -650,7 +648,6 @@ Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Aig_Man_t * pGuide )
pObj->pData = pObjNew;
}
}
Vec_PtrFree( vPios );
// assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
if ( p->pEquivs == NULL && p->pReprs == NULL && (nNodes = Aig_ManCleanup( pNew )) )
printf( "Aig_ManDupDfs(): Cleanup after AIG duplication removed %d nodes.\n", nNodes );
@ -971,6 +968,54 @@ Aig_Man_t * Aig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper )
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates AIG with only one primary output.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_ManDupOrpos( Aig_Man_t * p, int fAddRegs )
{
Aig_Man_t * pNew;
Aig_Obj_t * pObj, * pMiter;
int i;
assert( Aig_ManRegNum(p) > 0 );
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Aig_ManForEachPi( p, pObj, i )
pObj->pData = Aig_ObjCreatePi( pNew );
// set registers
pNew->nRegs = fAddRegs? p->nRegs : 0;
pNew->nTruePis = fAddRegs? p->nTruePis : p->nTruePis + p->nRegs;
pNew->nTruePos = 1;
// duplicate internal nodes
Aig_ManForEachNode( p, pObj, i )
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
// create the PO
pMiter = Aig_ManConst0(pNew);
Aig_ManForEachPoSeq( p, pObj, i )
pMiter = Aig_Or( pNew, pMiter, Aig_ObjChild0Copy(pObj) );
Aig_ObjCreatePo( pNew, pMiter );
// create register inputs with MUXes
if ( fAddRegs )
{
Aig_ManForEachLiSeq( p, pObj, i )
Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
}
Aig_ManCleanup( pNew );
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates AIG with only one primary output.]
@ -1018,6 +1063,57 @@ Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum, int fAddRegs )
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates AIG with only one primary output.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_ManDupUnsolvedOutputs( Aig_Man_t * p, int fAddRegs )
{
Aig_Man_t * pNew;
Aig_Obj_t * pObj;
int i, nOuts = 0;
assert( Aig_ManRegNum(p) > 0 );
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Aig_ManForEachPi( p, pObj, i )
pObj->pData = Aig_ObjCreatePi( pNew );
// create the POs
nOuts = 0;
Aig_ManForEachPoSeq( p, pObj, i )
nOuts += ( Aig_ObjFanin0(pObj) != Aig_ManConst1(p) );
// set registers
pNew->nRegs = fAddRegs? p->nRegs : 0;
pNew->nTruePis = fAddRegs? p->nTruePis : p->nTruePis + p->nRegs;
pNew->nTruePos = nOuts;
// duplicate internal nodes
Aig_ManForEachNode( p, pObj, i )
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
// create the PO
Aig_ManForEachPoSeq( p, pObj, i )
if ( Aig_ObjFanin0(pObj) != Aig_ManConst1(p) )
Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
// create register inputs with MUXes
if ( fAddRegs )
{
Aig_ManForEachLiSeq( p, pObj, i )
Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
}
Aig_ManCleanup( pNew );
return pNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

4
src/aig/aig/aigMan.c
View File

@ -373,8 +373,8 @@ void Aig_ManPrintStats( Aig_Man_t * p )
{
int nChoices = Aig_ManChoiceNum(p);
printf( "%-15s : ", p->pName );
printf( "pi = %5d ", Aig_ManPiNum(p) );
printf( "po = %5d ", Aig_ManPoNum(p) );
printf( "pi = %5d ", Aig_ManPiNum(p)-Aig_ManRegNum(p) );
printf( "po = %5d ", Aig_ManPoNum(p)-Aig_ManRegNum(p) );
if ( Aig_ManRegNum(p) )
printf( "lat = %5d ", Aig_ManRegNum(p) );
printf( "and = %7d ", Aig_ManAndNum(p) );

16
src/aig/aig/aigPart.c
View File

@ -1223,6 +1223,7 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nCon
// extern void * Abc_FrameGetGlobalFrame();
extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax, int nLevelMax );
Vec_Ptr_t * vPios;
Vec_Ptr_t * vOutsTotal, * vOuts;
Aig_Man_t * pAigTotal, * pAigPart, * pAig, * pTemp;
Vec_Int_t * vPart, * vPartSupp;
@ -1323,8 +1324,10 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nCon
// create the equivalent nodes lists
Aig_ManMarkValidChoices( pAig );
// reconstruct the network
pAig = Aig_ManDupDfsGuided( pTemp = pAig, Vec_PtrEntry(vAigs,0) );
vPios = Aig_ManOrderPios( pAig, Vec_PtrEntry(vAigs,0) );
pAig = Aig_ManDupDfsGuided( pTemp = pAig, vPios );
Aig_ManStop( pTemp );
Vec_PtrFree( vPios );
// duplicate the timing manager
pTemp = Vec_PtrEntry( vAigs, 0 );
if ( pTemp->pManTime )
@ -1541,6 +1544,7 @@ void Aig_ManChoiceEval( Aig_Man_t * p )
***********************************************************************/
Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose )
{
Vec_Ptr_t * vPios;
Aig_Man_t * pNew, * pThis, * pPrev, * pTemp;
int i;
// start AIG with choices
@ -1562,8 +1566,10 @@ Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose )
// create the equivalent nodes lists
Aig_ManMarkValidChoices( pNew );
// reconstruct the network
pNew = Aig_ManDupDfsGuided( pTemp = pNew, Vec_PtrEntry( vAigs, 0 ) );
vPios = Aig_ManOrderPios( pNew, Vec_PtrEntry( vAigs, 0 ) );
pNew = Aig_ManDupDfsGuided( pTemp = pNew, vPios );
Aig_ManStop( pTemp );
Vec_PtrFree( vPios );
// duplicate the timing manager
pTemp = Vec_PtrEntry( vAigs, 0 );
if ( pTemp->pManTime )
@ -1573,6 +1579,12 @@ Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose )
return pNew;
}
/*
Vec_Ptr_t * vPios;
vPios = Aig_ManOrderPios( pMan, pAig );
Vec_PtrFree( vPios );
*/
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

127
src/aig/aig/aigUtil.c
View File

@ -1278,6 +1278,133 @@ void Aig_NodeIntersectLists( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * v
assert( vArr->nSize <= vArr2->nSize );
}
#include "fra.h"
#include "saig.h"
extern void Aig_ManCounterExampleValueStart( Aig_Man_t * pAig, Fra_Cex_t * pCex );
extern void Aig_ManCounterExampleValueStop( Aig_Man_t * pAig );
extern int Aig_ManCounterExampleValueLookup( Aig_Man_t * pAig, int Id, int iFrame );
/**Function*************************************************************
Synopsis [Starts the process of retuning values for internal nodes.]
Description [Should be called when pCex is available, before probing
any object for its value using Aig_ManCounterExampleValueLookup().]
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManCounterExampleValueStart( Aig_Man_t * pAig, Fra_Cex_t * pCex )
{
Aig_Obj_t * pObj, * pObjRi, * pObjRo;
int Val0, Val1, nObjs, i, k, iBit = 0;
assert( Aig_ManRegNum(pAig) > 0 ); // makes sense only for sequential AIGs
assert( pAig->pData2 == NULL ); // if this fail, there may be a memory leak
// allocate memory to store simulation bits for internal nodes
pAig->pData2 = ABC_CALLOC( unsigned, Aig_BitWordNum( (pCex->iFrame + 1) * Aig_ManObjNum(pAig) ) );
// the register values in the counter-example should be zero
Saig_ManForEachLo( pAig, pObj, k )
assert( Aig_InfoHasBit(pCex->pData, iBit++) == 0 );
// iterate through the timeframes
nObjs = Aig_ManObjNum(pAig);
for ( i = 0; i <= pCex->iFrame; i++ )
{
// set constant 1 node
Aig_InfoSetBit( pAig->pData2, nObjs * i + 0 );
// set primary inputs according to the counter-example
Saig_ManForEachPi( pAig, pObj, k )
if ( Aig_InfoHasBit(pCex->pData, iBit++) )
Aig_InfoSetBit( pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
// compute values for each node
Aig_ManForEachNode( pAig, pObj, k )
{
Val0 = Aig_InfoHasBit( pAig->pData2, nObjs * i + Aig_ObjFaninId0(pObj) );
Val1 = Aig_InfoHasBit( pAig->pData2, nObjs * i + Aig_ObjFaninId1(pObj) );
if ( (Val0 ^ Aig_ObjFaninC0(pObj)) & (Val1 ^ Aig_ObjFaninC1(pObj)) )
Aig_InfoSetBit( pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
}
// derive values for combinational outputs
Aig_ManForEachPo( pAig, pObj, k )
{
Val0 = Aig_InfoHasBit( pAig->pData2, nObjs * i + Aig_ObjFaninId0(pObj) );
if ( Val0 ^ Aig_ObjFaninC0(pObj) )
Aig_InfoSetBit( pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
}
if ( i == pCex->iFrame )
continue;
// transfer values to the register output of the next frame
Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
if ( Aig_InfoHasBit( pAig->pData2, nObjs * i + Aig_ObjId(pObjRi) ) )
Aig_InfoSetBit( pAig->pData2, nObjs * (i+1) + Aig_ObjId(pObjRo) );
}
assert( iBit == pCex->nBits );
// check that the counter-example is correct, that is, the corresponding output is asserted
assert( Aig_InfoHasBit( pAig->pData2, nObjs * pCex->iFrame + Aig_ObjId(Aig_ManPo(pAig, pCex->iPo)) ) );
}
/**Function*************************************************************
Synopsis [Stops the process of retuning values for internal nodes.]
Description [Should be called when probing is no longer needed]
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManCounterExampleValueStop( Aig_Man_t * pAig )
{
assert( pAig->pData2 != NULL ); // if this fail, we try to call this procedure more than once
free( pAig->pData2 );
pAig->pData2 = NULL;
}
/**Function*************************************************************
Synopsis [Returns the value of the given object in the given timeframe.]
Description [Should be called to probe the value of an object with
the given ID (iFrame is a 0-based number of a time frame - should not
exceed the number of timeframes in the original counter-example).]
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManCounterExampleValueLookup( Aig_Man_t * pAig, int Id, int iFrame )
{
assert( Id >= 0 && Id < Aig_ManObjNum(pAig) );
return Aig_InfoHasBit( pAig->pData2, Aig_ManObjNum(pAig) * iFrame + Id );
}
/**Function*************************************************************
Synopsis [Procedure to test the above code.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManCounterExampleValueTest( Aig_Man_t * pAig, Fra_Cex_t * pCex )
{
Aig_Obj_t * pObj = Aig_ManObj( pAig, Aig_ManObjNum(pAig)/2 );
int iFrame = ABC_MAX( 0, pCex->iFrame - 1 );
printf( "\nUsing counter-example, which asserts output %d in frame %d.\n", pCex->iPo, pCex->iFrame );
Aig_ManCounterExampleValueStart( pAig, pCex );
printf( "Value of object %d in frame %d is %d.\n", Aig_ObjId(pObj), iFrame,
Aig_ManCounterExampleValueLookup(pAig, Aig_ObjId(pObj), iFrame) );
Aig_ManCounterExampleValueStop( pAig );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

4
src/aig/bbr/bbr.h
View File

@ -57,7 +57,7 @@ typedef struct Bbr_ImageTree_t_ Bbr_ImageTree_t;
extern Bbr_ImageTree_t * Bbr_bddImageStart(
DdManager * dd, DdNode * bCare,
int nParts, DdNode ** pbParts,
int nVars, DdNode ** pbVars, int fVerbose );
int nVars, DdNode ** pbVars, int nBddMax, int fVerbose );
extern DdNode * Bbr_bddImageCompute( Bbr_ImageTree_t * pTree, DdNode * bCare );
extern void Bbr_bddImageTreeDelete( Bbr_ImageTree_t * pTree );
extern DdNode * Bbr_bddImageRead( Bbr_ImageTree_t * pTree );
@ -74,7 +74,7 @@ extern void Aig_ManFreeGlobalBdds( Aig_Man_t * p, DdManager * dd );
extern int Aig_ManSizeOfGlobalBdds( Aig_Man_t * p );
extern DdManager * Aig_ManComputeGlobalBdds( Aig_Man_t * p, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose );
/*=== bbrReach.c ==========================================================*/
extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent );
extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent );
#ifdef __cplusplus
}

2
src/aig/bbr/bbrCex.c
View File

@ -63,7 +63,7 @@ Ssw_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd,
// create the cube of NS variables
bCubeNs = Bbr_bddComputeRangeCube( dd, Saig_ManCiNum(p), Saig_ManCiNum(p)+Saig_ManRegNum(p) ); Cudd_Ref( bCubeNs );
pTree = Bbr_bddImageStart( dd, bCubeNs, Saig_ManRegNum(p), pbParts, Saig_ManCiNum(p), dd->vars, fVerbose );
pTree = Bbr_bddImageStart( dd, bCubeNs, Saig_ManRegNum(p), pbParts, Saig_ManCiNum(p), dd->vars, 100000000, fVerbose );
Cudd_RecursiveDeref( dd, bCubeNs );
if ( pTree == NULL )
{

18
src/aig/bbr/bbrImage.c
View File

@ -27,7 +27,7 @@
Helmut Veith, Dong Wang. Non-linear Quantification Scheduling in
Image Computation. ICCAD, 2001.
*/
/*---------------------------------------------------------------------------*/
/* Constant declarations */
/*---------------------------------------------------------------------------*/
@ -49,6 +49,7 @@ struct Bbr_ImageTree_t_
int nNodesMax; // the max number of nodes in one iter
int nNodesMaxT; // the overall max number of nodes
int nIter; // the number of iterations with this tree
int nBddMax; // the number of node to stop
};
struct Bbr_ImageNode_t_
@ -89,8 +90,6 @@ struct Bbr_ImageVar_t_
/* Macro declarations */
/*---------------------------------------------------------------------------*/
#define BDD_BLOW_UP 2000000
#define b0 Cudd_Not((dd)->one)
#define b1 (dd)->one
@ -116,7 +115,7 @@ static Bbr_ImageNode_t ** Bbr_CreateNodes( DdManager * dd,
static void Bbr_DeleteParts_rec( Bbr_ImageNode_t * pNode );
static int Bbr_BuildTreeNode( DdManager * dd,
int nNodes, Bbr_ImageNode_t ** pNodes,
int nVars, Bbr_ImageVar_t ** pVars, int * pfStop );
int nVars, Bbr_ImageVar_t ** pVars, int * pfStop, int nBddMax );
static Bbr_ImageNode_t * Bbr_MergeTopNodes( DdManager * dd,
int nNodes, Bbr_ImageNode_t ** pNodes );
static void Bbr_bddImageTreeDelete_rec( Bbr_ImageNode_t * pNode );
@ -166,7 +165,7 @@ static void Bbr_bddPrint( DdManager * dd, DdNode * F );
Bbr_ImageTree_t * Bbr_bddImageStart(
DdManager * dd, DdNode * bCare, // the care set
int nParts, DdNode ** pbParts, // the partitions for image computation
int nVars, DdNode ** pbVars, int fVerbose ) // the NS and parameter variables (not quantified!)
int nVars, DdNode ** pbVars, int nBddMax, int fVerbose ) // the NS and parameter variables (not quantified!)
{
Bbr_ImageTree_t * pTree;
Bbr_ImagePart_t ** pParts;
@ -184,7 +183,7 @@ Bbr_ImageTree_t * Bbr_bddImageStart(
pCare = pNodes[nParts];
// process the nodes
while ( Bbr_BuildTreeNode( dd, nParts + 1, pNodes, dd->size, pVars, &fStop ) );
while ( Bbr_BuildTreeNode( dd, nParts + 1, pNodes, dd->size, pVars, &fStop, nBddMax ) );
// consider the case of BDD node blowup
if ( fStop )
@ -213,6 +212,7 @@ Bbr_ImageTree_t * Bbr_bddImageStart(
pTree = ABC_ALLOC( Bbr_ImageTree_t, 1 );
memset( pTree, 0, sizeof(Bbr_ImageTree_t) );
pTree->pCare = pCare;
pTree->nBddMax = nBddMax;
pTree->fVerbose = fVerbose;
// merge the topmost nodes
@ -698,7 +698,7 @@ int Bbr_bddImageCompute_rec( Bbr_ImageTree_t * pTree, Bbr_ImageNode_t * pNode )
if ( pTree->nNodesMax < nNodes )
pTree->nNodesMax = nNodes;
}
if ( dd->keys-dd->dead > BDD_BLOW_UP )
if ( dd->keys-dd->dead > (unsigned)pTree->nBddMax )
return 0;
return 1;
}
@ -716,7 +716,7 @@ int Bbr_bddImageCompute_rec( Bbr_ImageTree_t * pTree, Bbr_ImageNode_t * pNode )
***********************************************************************/
int Bbr_BuildTreeNode( DdManager * dd,
int nNodes, Bbr_ImageNode_t ** pNodes,
int nVars, Bbr_ImageVar_t ** pVars, int * pfStop )
int nVars, Bbr_ImageVar_t ** pVars, int * pfStop, int nBddMax )
{
Bbr_ImageNode_t * pNode1, * pNode2;
Bbr_ImageVar_t * pVar;
@ -808,7 +808,7 @@ int Bbr_BuildTreeNode( DdManager * dd,
}
*pfStop = 0;
if ( dd->keys-dd->dead > BDD_BLOW_UP )
if ( dd->keys-dd->dead > (unsigned)nBddMax )
{
*pfStop = 1;
return 0;

24
src/aig/bbr/bbrReach.c
View File

@ -220,11 +220,16 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
int i, nIters, nBddSize;
int nThreshold = 10000;
Vec_Ptr_t * vOnionRings;
int status, method;
status = Cudd_ReorderingStatus( dd, &method );
if ( status )
Cudd_AutodynDisable( dd );
// start the image computation
bCubeCs = Bbr_bddComputeRangeCube( dd, Saig_ManPiNum(p), Saig_ManCiNum(p) ); Cudd_Ref( bCubeCs );
if ( fPartition )
pTree = Bbr_bddImageStart( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), fVerbose );
pTree = Bbr_bddImageStart( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), nBddMax, fVerbose );
else
pTree2 = Bbr_bddImageStart2( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), fVerbose );
Cudd_RecursiveDeref( dd, bCubeCs );
@ -235,6 +240,9 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
return -1;
}
if ( status )
Cudd_AutodynEnable( dd, method );
// start the onion rings
vOnionRings = Vec_PtrAlloc( 1000 );
@ -360,11 +368,11 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent )
int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent )
{
DdManager * dd;
DdNode ** pbParts, ** pbOutputs;
@ -397,6 +405,10 @@ int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, int nBddMax, int nIterMax, int fP
// create the initial state and the variable map
bInitial = Aig_ManInitStateVarMap( dd, p, fVerbose ); Cudd_Ref( bInitial );
// set reordering
if ( fReorderImage )
Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
// check the result
RetValue = -1;
for ( i = 0; i < Saig_ManPoNum(p); i++ )
@ -456,7 +468,7 @@ int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, int nBddMax, int nIterMax, int fP
SeeAlso []
***********************************************************************/
int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent )
int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent )
{
Ssw_Cex_t * pCexOld, * pCexNew;
Aig_Man_t * p;
@ -468,12 +480,12 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, int nBddMax, int nIterMax, int fP
if ( Aig_ObjRefs(pObj) == 0 )
break;
if ( i == Saig_ManPiNum(pInit) )
return Aig_ManVerifyUsingBdds_int( pInit, nBddMax, nIterMax, fPartition, fReorder, fVerbose, fSilent );
return Aig_ManVerifyUsingBdds_int( pInit, nBddMax, nIterMax, fPartition, fReorder, fReorderImage, fVerbose, fSilent );
// create new AIG
p = Aig_ManDupTrim( pInit );
assert( Aig_ManPiNum(p) < Aig_ManPiNum(pInit) );
assert( Aig_ManRegNum(p) == Aig_ManRegNum(pInit) );
RetValue = Aig_ManVerifyUsingBdds_int( p, nBddMax, nIterMax, fPartition, fReorder, fVerbose, fSilent );
RetValue = Aig_ManVerifyUsingBdds_int( p, nBddMax, nIterMax, fPartition, fReorder, fReorderImage, fVerbose, fSilent );
if ( RetValue != 0 )
{
Aig_ManStop( p );

1
src/aig/cec/cec.h
View File

@ -48,6 +48,7 @@ struct Cec_ParSat_t_
int fPolarFlip; // flops polarity of variables
int fCheckMiter; // the circuit is the miter
int fFirstStop; // stop on the first sat output
int fLearnCls; // perform clause learning
int fVerbose; // verbose stats
};

35
src/aig/cec/cecChoice.c
View File

@ -380,17 +380,17 @@ Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias )
SeeAlso []
***********************************************************************/
Gia_Man_t * Cec_ManChoiceComputationVec( Vec_Ptr_t * vGias, Cec_ParChc_t * pPars )
Gia_Man_t * Cec_ManChoiceComputationVec( Gia_Man_t * pGia, int nGias, Cec_ParChc_t * pPars )
{
Gia_Man_t * pMiter, * pNew;
Gia_Man_t * pNew;
int RetValue;
// compute equivalences of the miter
pMiter = Gia_ManChoiceMiter( vGias );
RetValue = Cec_ManChoiceComputation_int( pMiter, pPars );
// pMiter = Gia_ManChoiceMiter( vGias );
RetValue = Cec_ManChoiceComputation_int( pGia, pPars );
// derive AIG with choices
pNew = Gia_ManEquivToChoices( pMiter, Vec_PtrSize(vGias) );
pNew = Gia_ManEquivToChoices( pGia, nGias );
Gia_ManHasChoices( pNew );
Gia_ManStop( pMiter );
// Gia_ManStop( pMiter );
// report the results
if ( pPars->fVerbose )
{
@ -422,11 +422,7 @@ Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pParsChc
Gia_Man_t * pGia;
if ( 0 )
{
Vec_Ptr_t * vGias;
vGias = Vec_PtrAlloc( 1 );
Vec_PtrPush( vGias, pAig );
pGia = Cec_ManChoiceComputationVec( vGias, pParsChc );
Vec_PtrFree( vGias );
pGia = Cec_ManChoiceComputationVec( pAig, 3, pParsChc );
}
else
{
@ -439,7 +435,7 @@ Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pParsChc
pManNew = Dar_ManChoiceNew( pMan, pPars );
pGia = Gia_ManFromAig( pManNew );
Aig_ManStop( pManNew );
Aig_ManStop( pMan );
// Aig_ManStop( pMan );
}
return pGia;
}
@ -455,13 +451,10 @@ Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pParsChc
SeeAlso []
***********************************************************************/
Aig_Man_t * Cec_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars )
{
Cec_ParChc_t ParsChc, * pParsChc = &ParsChc;
Vec_Ptr_t * vGias;
Gia_Man_t * pGia;
Aig_Man_t * pAig;
int i;
if ( pPars->fVerbose )
ABC_PRT( "Synthesis time", pPars->timeSynth );
Cec_ManChcSetDefaultParams( pParsChc );
@ -470,14 +463,8 @@ Aig_Man_t * Cec_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
if ( pParsChc->fUseCSat && pParsChc->nBTLimit > 100 )
pParsChc->nBTLimit = 100;
pParsChc->fVerbose = pPars->fVerbose;
vGias = Vec_PtrAlloc( 10 );
Vec_PtrForEachEntry( vAigs, pAig, i )
Vec_PtrPush( vGias, Gia_ManFromAig(pAig) );
pGia = Cec_ManChoiceComputationVec( vGias, pParsChc );
Gia_ManSetRegNum( pGia, Gia_ManRegNum(Vec_PtrEntry(vGias, 0)) );
Vec_PtrForEachEntry( vGias, pAig, i )
Gia_ManStop( (Gia_Man_t *)pAig );
Vec_PtrFree( vGias );
pGia = Cec_ManChoiceComputationVec( pGia, 3, pParsChc );
Gia_ManSetRegNum( pGia, Gia_ManRegNum(pGia) );
pAig = Gia_ManToAig( pGia, 1 );
Gia_ManStop( pGia );
return pAig;

1
src/aig/cec/cecCore.c
View File

@ -49,6 +49,7 @@ void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p )
p->fPolarFlip = 1; // flops polarity of variables
p->fCheckMiter = 0; // the circuit is the miter
p->fFirstStop = 0; // stop on the first sat output
p->fLearnCls = 0; // perform clause learning
p->fVerbose = 0; // verbose stats
}

14
src/aig/cec/cecCorr.c
View File

@ -797,7 +797,7 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
}
pParsSat->nBTLimit *= 10;
if ( pPars->fUseCSat )
vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
vCexStore = Tas_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
else
vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
// refine classes with these counter-examples
@ -831,8 +831,9 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
***********************************************************************/
int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
{
int nIterMax = 100000;
int nAddFrames = 1; // additional timeframes to simulate
int nIterMax = 100000;
int nAddFrames = 1; // additional timeframes to simulate
int fRunBmcFirst = 0;
Vec_Str_t * vStatus;
Vec_Int_t * vOutputs;
Vec_Int_t * vCexStore;
@ -875,8 +876,8 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
Cec_ManRefinedClassPrintStats( pAig, NULL, 0, clock() - clk );
}
// check the base case
if ( !pPars->fLatchCorr || pPars->nFrames > 1 )
Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 );
if ( fRunBmcFirst && (!pPars->fLatchCorr || pPars->nFrames > 1) )
Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 );
// perform refinement of equivalence classes
for ( r = 0; r < nIterMax; r++ )
{
@ -926,6 +927,9 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
if ( r == nIterMax )
printf( "The refinement was not finished. The result may be incorrect.\n" );
Cec_ManSimStop( pSim );
// check the base case
if ( !fRunBmcFirst && (!pPars->fLatchCorr || pPars->nFrames > 1) )
Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 );
clkTotal = clock() - clkTotal;
// report the results
if ( pPars->fVerbose )

4
src/aig/cec/cecInt.h
View File

@ -199,6 +199,10 @@ extern int Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pO
extern void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars );
extern Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats );
extern Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Str_t ** pvStatus );
extern int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj );
extern int Cec_ManSatCheckNodeTwo( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 );
extern void Cec_ManSavePattern( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 );
extern Vec_Int_t * Cec_ManSatReadCex( Cec_ManSat_t * p );
/*=== ceFraeep.c ============================================================*/
extern Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p );
extern int Cec_ManFraClassesUpdate( Cec_ManFra_t * p, Cec_ManSim_t * pSim, Cec_ManPat_t * pPat, Gia_Man_t * pNew );

190
src/aig/cec/cecSolve.c
View File

@ -404,9 +404,9 @@ void Cec_SetActivityFactors_rec( Cec_ManSat_t * p, Gia_Obj_t * pObj, int LevelMi
float dActConeBumpMax = 20.0;
int iVar;
// skip visited variables
if ( Gia_ObjIsTravIdCurrent(p->pAig, pObj) )
if ( Gia_ObjIsTravIdCurrentArray(p->pAig, pObj) )
return;
Gia_ObjSetTravIdCurrent(p->pAig, pObj);
Gia_ObjSetTravIdCurrentArray(p->pAig, pObj);
// add the PI to the list
if ( Gia_ObjLevel(p->pAig, pObj) <= LevelMin || Gia_ObjIsCi(pObj) )
return;
@ -440,7 +440,7 @@ int Cec_SetActivityFactors( Cec_ManSat_t * p, Gia_Obj_t * pObj )
// reset the active variables
veci_resize(&p->pSat->act_vars, 0);
// prepare for traversal
Gia_ManIncrementTravId( p->pAig );
Gia_ManIncrementTravIdArray( p->pAig );
// determine the min and max level to visit
assert( dActConeRatio > 0 && dActConeRatio < 1 );
LevelMax = Gia_ObjLevel(p->pAig,pObj);
@ -465,9 +465,18 @@ int Cec_SetActivityFactors( Cec_ManSat_t * p, Gia_Obj_t * pObj )
***********************************************************************/
int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj )
{
Gia_Obj_t * pObjR = Gia_Regular(pObj);
int nBTLimit = p->pPars->nBTLimit;
int Lit, RetValue, status, clk, clk2, nConflicts;
if ( pObj == Gia_ManConst0(p->pAig) )
return 1;
if ( pObj == Gia_ManConst1(p->pAig) )
{
assert( 0 );
return 0;
}
p->nCallsSince++; // experiment with this!!!
p->nSatTotal++;
@ -480,12 +489,12 @@ int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj )
// if the nodes do not have SAT variables, allocate them
clk2 = clock();
Cec_CnfNodeAddToSolver( p, Gia_ObjFanin0(pObj) );
Cec_CnfNodeAddToSolver( p, pObjR );
//ABC_PRT( "cnf", clock() - clk2 );
//printf( "%d \n", p->pSat->size );
clk2 = clock();
// Cec_SetActivityFactors( p, Gia_ObjFanin0(pObj) );
// Cec_SetActivityFactors( p, pObjR );
//ABC_PRT( "act", clock() - clk2 );
// propage unit clauses
@ -498,10 +507,10 @@ clk2 = clock();
// solve under assumptions
// A = 1; B = 0 OR A = 1; B = 1
Lit = toLitCond( Cec_ObjSatNum(p,Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
Lit = toLitCond( Cec_ObjSatNum(p,pObjR), Gia_IsComplement(pObj) );
if ( p->pPars->fPolarFlip )
{
if ( Gia_ObjFanin0(pObj)->fPhase ) Lit = lit_neg( Lit );
if ( pObjR->fPhase ) Lit = lit_neg( Lit );
}
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
clk = clock();
@ -541,6 +550,110 @@ p->timeSatUndec += clock() - clk;
}
}
/**Function*************************************************************
Synopsis [Runs equivalence test for the two nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cec_ManSatCheckNodeTwo( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 )
{
Gia_Obj_t * pObjR1 = Gia_Regular(pObj1);
Gia_Obj_t * pObjR2 = Gia_Regular(pObj2);
int nBTLimit = p->pPars->nBTLimit;
int Lits[2], RetValue, status, clk, clk2, nConflicts;
if ( pObj1 == Gia_ManConst0(p->pAig) || pObj2 == Gia_ManConst0(p->pAig) || pObj1 == Gia_Not(pObj2) )
return 1;
if ( pObj1 == Gia_ManConst1(p->pAig) && (pObj2 == NULL || pObj2 == Gia_ManConst1(p->pAig)) )
{
assert( 0 );
return 0;
}
p->nCallsSince++; // experiment with this!!!
p->nSatTotal++;
// check if SAT solver needs recycling
if ( p->pSat == NULL ||
(p->pPars->nSatVarMax &&
p->nSatVars > p->pPars->nSatVarMax &&
p->nCallsSince > p->pPars->nCallsRecycle) )
Cec_ManSatSolverRecycle( p );
// if the nodes do not have SAT variables, allocate them
clk2 = clock();
Cec_CnfNodeAddToSolver( p, pObjR1 );
Cec_CnfNodeAddToSolver( p, pObjR2 );
//ABC_PRT( "cnf", clock() - clk2 );
//printf( "%d \n", p->pSat->size );
clk2 = clock();
// Cec_SetActivityFactors( p, pObjR1 );
// Cec_SetActivityFactors( p, pObjR2 );
//ABC_PRT( "act", clock() - clk2 );
// 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
Lits[0] = toLitCond( Cec_ObjSatNum(p,pObjR1), Gia_IsComplement(pObj1) );
Lits[1] = toLitCond( Cec_ObjSatNum(p,pObjR2), Gia_IsComplement(pObj2) );
if ( p->pPars->fPolarFlip )
{
if ( pObjR1->fPhase ) Lits[0] = lit_neg( Lits[0] );
if ( pObjR2->fPhase ) Lits[1] = lit_neg( Lits[1] );
}
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
clk = clock();
nConflicts = p->pSat->stats.conflicts;
clk2 = clock();
RetValue = sat_solver_solve( p->pSat, Lits, Lits + 2,
(ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
//ABC_PRT( "sat", clock() - clk2 );
if ( RetValue == l_False )
{
p->timeSatUnsat += clock() - clk;
Lits[0] = lit_neg( Lits[0] );
Lits[1] = lit_neg( Lits[1] );
RetValue = sat_solver_addclause( p->pSat, Lits, Lits + 2 );
assert( RetValue );
p->nSatUnsat++;
p->nConfUnsat += p->pSat->stats.conflicts - nConflicts;
//printf( "UNSAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
return 1;
}
else if ( RetValue == l_True )
{
p->timeSatSat += clock() - clk;
p->nSatSat++;
p->nConfSat += p->pSat->stats.conflicts - nConflicts;
//printf( "SAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
return 0;
}
else // if ( RetValue == l_Undef )
{
p->timeSatUndec += clock() - clk;
p->nSatUndec++;
p->nConfUndec += p->pSat->stats.conflicts - nConflicts;
//printf( "UNDEC after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
return -1;
}
}
/**Function*************************************************************
@ -570,7 +683,7 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar
}
Gia_ManSetPhase( pAig );
Gia_ManLevelNum( pAig );
Gia_ManResetTravId( pAig );
Gia_ManResetTravIdArray( pAig );
p = Cec_ManSatCreate( pAig, pPars );
pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) );
Gia_ManForEachCo( pAig, pObj, i )
@ -583,7 +696,7 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar
}
Bar_ProgressUpdate( pProgress, i, "SAT..." );
clk2 = clock();
status = Cec_ManSatCheckNode( p, pObj );
status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) );
pObj->fMark0 = (status == 0);
pObj->fMark1 = (status == 1);
/*
@ -617,6 +730,22 @@ clk2 = clock();
/**Function*************************************************************
Synopsis [Returns the pattern stored.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Cec_ManSatReadCex( Cec_ManSat_t * pSat )
{
return pSat->vCex;
}
/**Function*************************************************************
Synopsis [Save values in the cone of influence.]
@ -630,9 +759,9 @@ clk2 = clock();
***********************************************************************/
void Cec_ManSatSolveSeq_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vInfo, int iPat, int nRegs )
{
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
if ( Gia_ObjIsTravIdCurrentArray(p, pObj) )
return;
Gia_ObjSetTravIdCurrent(p, pObj);
Gia_ObjSetTravIdCurrentArray(p, pObj);
if ( Gia_ObjIsCi(pObj) )
{
unsigned * pInfo = Vec_PtrEntry( vInfo, nRegs + Gia_ObjCioId(pObj) );
@ -670,7 +799,7 @@ Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat
nPatsInit = nPats = 32 * Vec_PtrReadWordsSimInfo(vPatts);
Gia_ManSetPhase( pAig );
Gia_ManLevelNum( pAig );
Gia_ManResetTravId( pAig );
Gia_ManResetTravIdArray( pAig );
p = Cec_ManSatCreate( pAig, pPars );
vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) );
@ -691,7 +820,7 @@ Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat
}
continue;
}
status = Cec_ManSatCheckNode( p, pObj );
status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) );
//printf( "output %d status = %d\n", i, status );
Vec_StrPush( vStatus, (char)status );
if ( status != 0 )
@ -707,7 +836,7 @@ Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat
if ( iPat % nPatsInit == 0 )
iPat++;
// save the pattern
Gia_ManIncrementTravId( pAig );
Gia_ManIncrementTravIdArray( pAig );
// Vec_IntClear( p->vCex );
Cec_ManSatSolveSeq_rec( p, pAig, Gia_ObjFanin0(pObj), vPatts, iPat++, nRegs );
// Gia_SatVerifyPattern( pAig, pObj, p->vCex, p->vVisits );
@ -771,9 +900,9 @@ void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out )
***********************************************************************/
void Cec_ManSatSolveMiter_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pObj )
{
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
if ( Gia_ObjIsTravIdCurrentArray(p, pObj) )
return;
Gia_ObjSetTravIdCurrent(p, pObj);
Gia_ObjSetTravIdCurrentArray(p, pObj);
if ( Gia_ObjIsCi(pObj) )
{
pSat->nCexLits++;
@ -785,6 +914,26 @@ void Cec_ManSatSolveMiter_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * p
Cec_ManSatSolveMiter_rec( pSat, p, Gia_ObjFanin1(pObj) );
}
/**Function*************************************************************
Synopsis [Save patterns.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cec_ManSavePattern( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 )
{
Vec_IntClear( p->vCex );
Gia_ManIncrementTravIdArray( p->pAig );
Cec_ManSatSolveMiter_rec( p, p->pAig, Gia_Regular(pObj1) );
if ( pObj2 )
Cec_ManSatSolveMiter_rec( p, p->pAig, Gia_Regular(pObj2) );
}
/**Function*************************************************************
Synopsis [Performs one round of solving for the POs of the AIG.]
@ -808,7 +957,7 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St
// prepare AIG
Gia_ManSetPhase( pAig );
Gia_ManLevelNum( pAig );
Gia_ManResetTravId( pAig );
Gia_ManResetTravIdArray( pAig );
// create resulting data-structures
vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
vCexStore = Vec_IntAlloc( 10000 );
@ -834,7 +983,7 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St
}
continue;
}
status = Cec_ManSatCheckNode( p, pObj );
status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) );
Vec_StrPush( vStatus, (char)status );
if ( status == -1 )
{
@ -845,8 +994,9 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St
continue;
assert( status == 0 );
// save the pattern
Gia_ManIncrementTravId( pAig );
Cec_ManSatSolveMiter_rec( p, pAig, Gia_ObjFanin0(pObj) );
// Gia_ManIncrementTravIdArray( pAig );
// Cec_ManSatSolveMiter_rec( p, pAig, Gia_ObjFanin0(pObj) );
Cec_ManSavePattern( p, Gia_ObjFanin0(pObj), NULL );
// Gia_SatVerifyPattern( pAig, pObj, p->vCex, p->vVisits );
Cec_ManSatAddToStore( vCexStore, p->vCex, i );
}

459
src/aig/dar/darScript.c
View File

@ -19,12 +19,16 @@
***********************************************************************/
#include "darInt.h"
//#include "ioa.h"
#include "dch.h"
#include "gia.h"
#include "giaAig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
extern void * Tim_ManDup( void * p, int fDiscrete );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@ -419,7 +423,146 @@ ABC_PRT( "Choicing time ", clock() - clk );
// return NULL;
}
#include "dch.h"
/**Function*************************************************************
Synopsis [Duplicates the AIG in the DFS order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Dar_ManChoiceMiter_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
{
if ( ~pObj->Value )
return pObj->Value;
Dar_ManChoiceMiter_rec( pNew, p, Gia_ObjFanin0(pObj) );
if ( Gia_ObjIsCo(pObj) )
return pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Dar_ManChoiceMiter_rec( pNew, p, Gia_ObjFanin1(pObj) );
return pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
/**Function*************************************************************
Synopsis [Derives the miter of several AIGs for choice computation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Dar_ManChoiceMiter( Vec_Ptr_t * vGias )
{
Gia_Man_t * pNew, * pGia, * pGia0;
int i, k, iNode, nNodes;
// make sure they have equal parameters
assert( Vec_PtrSize(vGias) > 0 );
pGia0 = Vec_PtrEntry( vGias, 0 );
Vec_PtrForEachEntry( vGias, pGia, i )
{
assert( Gia_ManCiNum(pGia) == Gia_ManCiNum(pGia0) );
assert( Gia_ManCoNum(pGia) == Gia_ManCoNum(pGia0) );
assert( Gia_ManRegNum(pGia) == Gia_ManRegNum(pGia0) );
Gia_ManFillValue( pGia );
Gia_ManConst0(pGia)->Value = 0;
}
// start the new manager
pNew = Gia_ManStart( Vec_PtrSize(vGias) * Gia_ManObjNum(pGia0) );
pNew->pName = Gia_UtilStrsav( pGia0->pName );
// create new CIs and assign them to the old manager CIs
for ( k = 0; k < Gia_ManCiNum(pGia0); k++ )
{
iNode = Gia_ManAppendCi(pNew);
Vec_PtrForEachEntry( vGias, pGia, i )
Gia_ManCi( pGia, k )->Value = iNode;
}
// create internal nodes
Gia_ManHashAlloc( pNew );
for ( k = 0; k < Gia_ManCoNum(pGia0); k++ )
{
Vec_PtrForEachEntry( vGias, pGia, i )
Dar_ManChoiceMiter_rec( pNew, pGia, Gia_ManCo( pGia, k ) );
}
Gia_ManHashStop( pNew );
// check the presence of dangling nodes
nNodes = Gia_ManHasDandling( pNew );
assert( nNodes == 0 );
// finalize
Gia_ManSetRegNum( pNew, Gia_ManRegNum(pGia0) );
return pNew;
}
/**Function*************************************************************
Synopsis [Reproduces script "compress".]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Dar_NewCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose )
//alias compress2 "b -l; rw -l; rwz -l; b -l; rwz -l; b -l"
{
Aig_Man_t * pTemp;
Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
Dar_ManDefaultRwrParams( pParsRwr );
Dar_ManDefaultRefParams( pParsRef );
pParsRwr->fUpdateLevel = fUpdateLevel;
pParsRef->fUpdateLevel = fUpdateLevel;
pParsRwr->fPower = fPower;
pParsRwr->fVerbose = 0;//fVerbose;
pParsRef->fVerbose = 0;//fVerbose;
// pAig = Aig_ManDupDfs( pAig );
if ( fVerbose ) Aig_ManPrintStats( pAig );
// rewrite
Dar_ManRewrite( pAig, pParsRwr );
pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
// refactor
Dar_ManRefactor( pAig, pParsRef );
pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
// balance
if ( fBalance )
{
pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
}
pParsRwr->fUseZeros = 1;
pParsRef->fUseZeros = 1;
// rewrite
Dar_ManRewrite( pAig, pParsRwr );
pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
return pAig;
}
/**Function*************************************************************
@ -432,6 +575,174 @@ ABC_PRT( "Choicing time ", clock() - clk );
SeeAlso []
***********************************************************************/
Aig_Man_t * Dar_NewCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fLightSynth, int fVerbose )
//alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
{
Aig_Man_t * pTemp;
Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
Dar_ManDefaultRwrParams( pParsRwr );
Dar_ManDefaultRefParams( pParsRef );
pParsRwr->fUpdateLevel = fUpdateLevel;
pParsRef->fUpdateLevel = fUpdateLevel;
pParsRwr->fFanout = fFanout;
pParsRwr->fPower = fPower;
pParsRwr->fVerbose = 0;//fVerbose;
pParsRef->fVerbose = 0;//fVerbose;
// pAig = Aig_ManDupDfs( pAig );
if ( fVerbose ) Aig_ManPrintStats( pAig );
// skip if lighter synthesis is requested
if ( !fLightSynth )
{
// rewrite
Dar_ManRewrite( pAig, pParsRwr );
pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
// refactor
Dar_ManRefactor( pAig, pParsRef );
pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
}
// balance
pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
// skip if lighter synthesis is requested
if ( !fLightSynth )
{
// rewrite
Dar_ManRewrite( pAig, pParsRwr );
pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
}
pParsRwr->fUseZeros = 1;
pParsRef->fUseZeros = 1;
// rewrite
Dar_ManRewrite( pAig, pParsRwr );
pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
// skip if lighter synthesis is requested
if ( !fLightSynth )
{
// balance
if ( fBalance )
{
pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
}
}
// refactor
Dar_ManRefactor( pAig, pParsRef );
pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
// skip if lighter synthesis is requested
if ( !fLightSynth )
{
// rewrite
Dar_ManRewrite( pAig, pParsRwr );
pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
}
// balance
if ( fBalance )
{
pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
}
return pAig;
}
/**Function*************************************************************
Synopsis [Reproduces script "compress2".]
Description [Takes AIG manager, consumes it, and produces GIA manager.]
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Dar_NewChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fLightSynth, int fVerbose )
//alias resyn "b; rw; rwz; b; rwz; b"
//alias resyn2 "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"
{
Vec_Ptr_t * vGias;
Gia_Man_t * pGia, * pTemp;
int i;
vGias = Vec_PtrAlloc( 3 );
pGia = Gia_ManFromAig(pAig);
Vec_PtrPush( vGias, pGia );
pAig = Dar_NewCompress( pAig, fBalance, fUpdateLevel, fPower, fVerbose );
pGia = Gia_ManFromAig(pAig);
Vec_PtrPush( vGias, pGia );
//Aig_ManPrintStats( pAig );
pAig = Dar_NewCompress2( pAig, fBalance, fUpdateLevel, 1, fPower, fLightSynth, fVerbose );
pGia = Gia_ManFromAig(pAig);
Vec_PtrPush( vGias, pGia );
//Aig_ManPrintStats( pAig );
Aig_ManStop( pAig );
// swap around the first and the last
pTemp = Vec_PtrPop( vGias );
Vec_PtrPush( vGias, Vec_PtrEntry(vGias,0) );
Vec_PtrWriteEntry( vGias, 0, pTemp );
// Aig_Man_t * pAig;
// int i;
// printf( "Choicing will be performed with %d AIGs:\n", Vec_PtrSize(p->vAigs) );
// Vec_PtrForEachEntry( p->vAigs, pAig, i )
// Aig_ManPrintStats( pAig );
// derive the miter
pGia = Dar_ManChoiceMiter( vGias );
// cleanup
Vec_PtrForEachEntry( vGias, pTemp, i )
Gia_ManStop( pTemp );
Vec_PtrFree( vGias );
return pGia;
}
/**Function*************************************************************
Synopsis [Reproduces script "compress2".]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
/*
Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
{
extern Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars );
@ -465,12 +776,6 @@ if ( fVerbose )
pPars->timeSynth = clock() - clk;
clk = clock();
/*
if ( fConstruct )
pMan = Aig_ManChoiceConstructive( vAigs, fVerbose );
else
pMan = Aig_ManChoicePartitioned( vAigs, 300, nConfMax, nLevelMax, fVerbose );
*/
// perform choice computation
if ( pPars->fUseGia )
pMan = Cec_ComputeChoices( vAigs, pPars );
@ -506,6 +811,144 @@ if ( fVerbose )
return pMan;
// return NULL;
}
*/
/**Function*************************************************************
Synopsis [Reproduces script "compress2".]
Description [Consumes the input AIG to reduce memory usage.]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Dar_ManChoiceNewAig( Aig_Man_t * pAig, Dch_Pars_t * pPars )
{
extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs );
extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars );
int fVerbose = pPars->fVerbose;
Aig_Man_t * pMan, * pTemp;
Vec_Ptr_t * vAigs;
Vec_Ptr_t * vPios;
void * pManTime;
char * pName, * pSpec;
int i, clk;
clk = clock();
vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, pPars->fPower, fVerbose );
pPars->timeSynth = clock() - clk;
// swap the first and last network
// this should lead to the primary choice being "better" because of synthesis
// (it is also important when constructing choices)
pMan = Vec_PtrPop( vAigs );
Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
Vec_PtrWriteEntry( vAigs, 0, pMan );
// derive the total AIG
pMan = Dch_DeriveTotalAig( vAigs );
// cleanup
Vec_PtrForEachEntry( vAigs, pTemp, i )
Aig_ManStop( pTemp );
Vec_PtrFree( vAigs );
// compute choices
pMan = Dch_ComputeChoices( pTemp = pMan, pPars );
Aig_ManStop( pTemp );
// save useful things
pManTime = pAig->pManTime; pAig->pManTime = NULL;
pName = Aig_UtilStrsav( pAig->pName );
pSpec = Aig_UtilStrsav( pAig->pSpec );
// create guidence
vPios = Aig_ManOrderPios( pMan, pAig );
Aig_ManStop( pAig );
// reconstruct the network
pMan = Aig_ManDupDfsGuided( pTemp = pMan, vPios );
Aig_ManStop( pTemp );
Vec_PtrFree( vPios );
// reset levels
pMan->pManTime = pManTime;
Aig_ManChoiceLevel( pMan );
// copy names
ABC_FREE( pMan->pName );
ABC_FREE( pMan->pSpec );
pMan->pName = pName;
pMan->pSpec = pSpec;
return pMan;
}
/**Function*************************************************************
Synopsis [Reproduces script "compress2".]
Description [Consumes the input AIG to reduce memory usage.]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
{
extern Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars );
extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs );
extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars );
int fVerbose = pPars->fVerbose;
Aig_Man_t * pMan, * pTemp;
Gia_Man_t * pGia;
Vec_Ptr_t * vPios;
void * pManTime;
char * pName, * pSpec;
int clk;
// save useful things
pManTime = pAig->pManTime; pAig->pManTime = NULL;
pName = Aig_UtilStrsav( pAig->pName );
pSpec = Aig_UtilStrsav( pAig->pSpec );
// perform synthesis
clk = clock();
pGia = Dar_NewChoiceSynthesis( Aig_ManDupDfs(pAig), 1, 1, pPars->fPower, pPars->fLightSynth, 0 );
pPars->timeSynth = clock() - clk;
// perform choice computation
if ( pPars->fUseGia )
pMan = Cec_ComputeChoices( pGia, pPars );
else
{
pMan = Gia_ManToAigSkip( pGia, 3 );
Gia_ManStop( pGia );
pMan = Dch_ComputeChoices( pTemp = pMan, pPars );
Aig_ManStop( pTemp );
}
// create guidence
vPios = Aig_ManOrderPios( pMan, pAig );
Aig_ManStop( pAig );
// reconstruct the network
pMan = Aig_ManDupDfsGuided( pTemp = pMan, vPios );
Aig_ManStop( pTemp );
Vec_PtrFree( vPios );
// reset levels
pMan->pManTime = pManTime;
Aig_ManChoiceLevel( pMan );
// copy names
ABC_FREE( pMan->pName );
ABC_FREE( pMan->pSpec );
pMan->pName = pName;
pMan->pSpec = pSpec;
return pMan;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

3
src/aig/dch/dch.h
View File

@ -50,6 +50,7 @@ struct Dch_Pars_t_
int fPower; // uses power-aware rewriting
int fUseGia; // uses GIA package
int fUseCSat; // uses circuit-based solver
int fLightSynth; // uses lighter version of synthesis
int fVerbose; // verbose stats
int timeSynth; // synthesis runtime
int nNodesAhead; // the lookahead in terms of nodes
@ -66,7 +67,7 @@ struct Dch_Pars_t_
/*=== dchCore.c ==========================================================*/
extern void Dch_ManSetDefaultParams( Dch_Pars_t * p );
extern Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars );
extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars );
#ifdef __cplusplus

29
src/aig/dch/dchCore.c
View File

@ -49,6 +49,7 @@ void Dch_ManSetDefaultParams( Dch_Pars_t * p )
p->fPolarFlip = 1; // uses polarity adjustment
p->fSimulateTfo = 1; // simulate TFO
p->fPower = 0; // power-aware rewriting
p->fLightSynth = 0; // uses lighter version of synthesis
p->fVerbose = 0; // verbose stats
p->nNodesAhead = 1000; // the lookahead in terms of nodes
p->nCallsRecycle = 100; // calls to perform before recycling SAT solver
@ -65,37 +66,35 @@ void Dch_ManSetDefaultParams( Dch_Pars_t * p )
SeeAlso []
***********************************************************************/
Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars )
{
Dch_Man_t * p;
Aig_Man_t * pResult;
int clk, clkTotal = clock();
assert( Vec_PtrSize(vAigs) > 0 );
// reset random numbers
Aig_ManRandom(1);
// start the choicing manager
p = Dch_ManCreate( vAigs, pPars );
p = Dch_ManCreate( pAig, pPars );
// compute candidate equivalence classes
clk = clock();
p->ppClasses = Dch_CreateCandEquivClasses( p->pAigTotal, pPars->nWords, pPars->fVerbose );
p->ppClasses = Dch_CreateCandEquivClasses( pAig, pPars->nWords, pPars->fVerbose );
p->timeSimInit = clock() - clk;
// Dch_ClassesPrint( p->ppClasses, 0 );
p->nLits = Dch_ClassesLitNum( p->ppClasses );
// perform SAT sweeping
Dch_ManSweep( p );
// count the number of representatives
p->nReprs = Dch_DeriveChoiceCountReprs( p->pAigTotal );
// create choices
clk = clock();
pResult = Dch_DeriveChoiceAig( p->pAigTotal );
p->timeChoice = clock() - clk;
// Aig_ManCleanup( p->pAigTotal );
// pResult = Aig_ManDupSimpleDfs( p->pAigTotal );
// count the number of equivalences and choices
p->nEquivs = Dch_DeriveChoiceCountEquivs( pResult );
p->nChoices = Aig_ManChoiceNum( pResult );
// free memory ahead of time
p->timeTotal = clock() - clkTotal;
Dch_ManStop( p );
// create choices
ABC_FREE( pAig->pTable );
pResult = Dch_DeriveChoiceAig( pAig );
// count the number of representatives
if ( pPars->fVerbose )
printf( "STATS: Reprs = %6d. Equivs = %6d. Choices = %6d.\n",
Dch_DeriveChoiceCountReprs( pAig ),
Dch_DeriveChoiceCountEquivs( pResult ),
Aig_ManChoiceNum( pResult ) );
return pResult;
}

4
src/aig/dch/dchInt.h
View File

@ -51,7 +51,7 @@ struct Dch_Man_t_
// parameters
Dch_Pars_t * pPars; // choicing parameters
// 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 * pAigFraig; // final AIG
// equivalence classes
@ -142,7 +142,7 @@ extern int Dch_ClassesRefineConst1Group( Dch_Cla_t * p, Vec_Ptr_t * vR
/*=== 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( Aig_Man_t * pAig, Dch_Pars_t * pPars );
extern void Dch_ManStop( Dch_Man_t * p );
extern void Dch_ManSatSolverRecycle( Dch_Man_t * p );
/*=== dchSat.c ===================================================*/

22
src/aig/dch/dchMan.c
View File

@ -39,15 +39,14 @@
SeeAlso []
***********************************************************************/
Dch_Man_t * Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
Dch_Man_t * Dch_ManCreate( Aig_Man_t * pAig, Dch_Pars_t * pPars )
{
Dch_Man_t * p;
// create interpolation manager
p = ABC_ALLOC( Dch_Man_t, 1 );
memset( p, 0, sizeof(Dch_Man_t) );
p->pPars = pPars;
p->vAigs = vAigs;
p->pAigTotal = Dch_DeriveTotalAig( vAigs );
p->pAigTotal = pAig; //Dch_DeriveTotalAig( vAigs );
Aig_ManFanoutStart( p->pAigTotal );
// SAT solving
p->nSatVars = 1;
@ -74,18 +73,14 @@ Dch_Man_t * Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
***********************************************************************/
void Dch_ManPrintStats( Dch_Man_t * p )
{
// Aig_Man_t * pAig;
// int i;
// printf( "Choicing will be performed with %d AIGs:\n", Vec_PtrSize(p->vAigs) );
// Vec_PtrForEachEntry( p->vAigs, pAig, i )
// Aig_ManPrintStats( pAig );
int nNodeNum = Aig_ManNodeNum(p->pAigTotal) / 3;
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) );
Aig_ManNodeNum(p->pAigTotal)-nNodeNum,
nNodeNum,
100.0 * nNodeNum/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",
@ -108,7 +103,7 @@ void Dch_ManPrintStats( Dch_Man_t * p )
{
ABC_PRT( "Synthesis ", p->pPars->timeSynth );
}
}
}
/**Function*************************************************************
@ -123,10 +118,9 @@ void Dch_ManPrintStats( Dch_Man_t * p )
***********************************************************************/
void Dch_ManStop( Dch_Man_t * p )
{
Aig_ManFanoutStop( p->pAigTotal );
if ( p->pPars->fVerbose )
Dch_ManPrintStats( p );
if ( p->pAigTotal )
Aig_ManStop( p->pAigTotal );
if ( p->pAigFraig )
Aig_ManStop( p->pAigFraig );
if ( p->ppClasses )

4
src/aig/fra/fra.h
View File

@ -128,13 +128,17 @@ struct Fra_Sec_t_
int fFraiging; // enables fraiging at the beginning
int fInduction; // enable the use of induction
int fInterpolation; // enables interpolation
int fInterSeparate; // enables interpolation for each outputs separately
int fReachability; // enables BDD based reachability
int fReorderImage; // enables BDD reordering during image computation
int fStopOnFirstFail; // enables stopping after first output of a miter has failed to prove
int fUseNewProver; // the new prover
int fSilent; // disables all output
int fVerbose; // enables verbose reporting of statistics
int fVeryVerbose; // enables very verbose reporting
int TimeLimit; // enables the timeout
int fReadUnsolved; // inserts the unsolved model back
int nSMnumber; // the number of model written
// internal parameters
int fRecursive; // set to 1 when SEC is called recursively
int fReportSolution; // enables report solution in a special form

72
src/aig/fra/fraSec.c
View File

@ -61,7 +61,9 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p )
p->fFraiging = 1; // enables fraiging at the beginning
p->fInduction = 1; // enables the use of induction (signal correspondence)
p->fInterpolation = 1; // enables interpolation
p->fInterSeparate = 0; // enables interpolation for each outputs separately
p->fReachability = 1; // enables BDD based reachability
p->fReorderImage = 0; // enables variable reordering during image computation
p->fStopOnFirstFail = 1; // enables stopping after first output of a miter has failed to prove
p->fUseNewProver = 0; // enables new prover
p->fSilent = 0; // disables all output
@ -93,6 +95,7 @@ int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec, Aig_Man_t ** ppResult )
int TimeOut = 0;
int fLatchCorr = 0;
float TimeLeft = 0.0;
pParSec->nSMnumber = -1;
// try the miter before solving
pNew = Aig_ManDupSimple( p );
@ -466,14 +469,68 @@ clk = clock();
{
Inter_ManParams_t Pars, * pPars = &Pars;
int Depth;
ABC_FREE( pNew->pSeqModel );
Inter_ManSetDefaultParams( pPars );
// pPars->nBTLimit = 100;
pPars->nBTLimit = pParSec->nBTLimitInter;
pPars->fVerbose = pParSec->fVeryVerbose;
if ( Saig_ManPoNum(pNew) == 1 )
{
RetValue = Inter_ManPerformInterpolation( pNew, pPars, &Depth );
}
else if ( pParSec->fInterSeparate )
{
Aig_Man_t * pTemp, * pAux;
Aig_Obj_t * pObjPo;
int i, Counter = 0;
Saig_ManForEachPo( pNew, pObjPo, i )
{
if ( Aig_ObjFanin0(pObjPo) == Aig_ManConst1(pNew) )
continue;
pTemp = Aig_ManDupOneOutput( pNew, i, 1 );
pTemp = Aig_ManScl( pAux = pTemp, 1, 1, 0 );
Aig_ManStop( pAux );
if ( Saig_ManRegNum(pTemp) > 0 )
{
RetValue = Inter_ManPerformInterpolation( pTemp, pPars, &Depth );
if ( pTemp->pSeqModel )
{
Ssw_Cex_t * pCex;
pCex = pNew->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
pCex->iPo = i;
Aig_ManStop( pTemp );
break;
}
// if solved, remove the output
if ( RetValue == 1 )
{
Aig_ObjPatchFanin0( pNew, pObjPo, Aig_ManConst0(pNew) );
// printf( "Output %3d : Solved ", i );
}
else
{
Counter++;
// printf( "Output %3d : Undec ", i );
}
}
else
Counter++;
// Aig_ManPrintStats( pTemp );
Aig_ManStop( pTemp );
printf( "Solving output %3d (out of %3d) using interpolation.\r", i, Saig_ManPoNum(pNew) );
}
Aig_ManCleanup( pNew );
if ( pNew->pSeqModel == NULL )
{
printf( "Interpolation left %d (out of %d) outputs unsolved \n", Counter, Saig_ManPoNum(pNew) );
if ( Counter )
RetValue = -1;
}
pNew = Aig_ManDupUnsolvedOutputs( pTemp = pNew, 1 );
Aig_ManStop( pTemp );
pNew = Aig_ManScl( pTemp = pNew, 1, 1, 0 );
Aig_ManStop( pTemp );
}
else
{
Aig_Man_t * pNewOrpos = Said_ManDupOrpos( pNew );
@ -481,7 +538,6 @@ clk = clock();
if ( pNewOrpos->pSeqModel )
{
Ssw_Cex_t * pCex;
ABC_FREE( pNew->pSeqModel );
pCex = pNew->pSeqModel = pNewOrpos->pSeqModel; pNewOrpos->pSeqModel = NULL;
pCex->iPo = Ssw_SmlFindOutputCounterExample( pNew, pNew->pSeqModel );
}
@ -505,10 +561,10 @@ ABC_PRT( "Time", clock() - clk );
// try reachability analysis
if ( pParSec->fReachability && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManRegNum(pNew) < pParSec->nBddVarsMax )
{
extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent );
extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent );
pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew);
pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew);
RetValue = Aig_ManVerifyUsingBdds( pNew, pParSec->nBddMax, pParSec->nBddIterMax, 1, 1, 0, pParSec->fSilent );
RetValue = Aig_ManVerifyUsingBdds( pNew, pParSec->nBddMax, pParSec->nBddIterMax, 1, 1, pParSec->fReorderImage, 0, pParSec->fSilent );
}
finish:
@ -541,6 +597,11 @@ ABC_PRT( "Time", clock() - clkTotal );
}
else
{
///////////////////////////////////
// save intermediate result
extern void Abc_FrameSetSave1( void * pAig );
Abc_FrameSetSave1( Aig_ManDupSimple(pNew) );
///////////////////////////////////
if ( !pParSec->fSilent )
{
printf( "Networks are UNDECIDED. " );
@ -555,7 +616,8 @@ ABC_PRT( "Time", clock() - clkTotal );
{
static int Counter = 1;
char pFileName[1000];
sprintf( pFileName, "sm%03d.aig", Counter++ );
pParSec->nSMnumber = Counter;
sprintf( pFileName, "sm%02d.aig", Counter++ );
Ioa_WriteAiger( pNew, pFileName, 0, 0 );
printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName );
}

46
src/aig/gia/gia.h
View File

@ -82,7 +82,7 @@ struct Gia_Obj_t_
unsigned Value; // application-specific value
};
// Value is currently use to store several types of information
// Value is currently used to store several types of information
// - pointer to the next node in the hash table during structural hashing
// - pointer to the node copy during duplication
// - traversal ID of the node during traversal
@ -135,6 +135,7 @@ struct Gia_Man_t_
Vec_Int_t * vFlopClasses; // classes of flops for retiming/merging/etc
unsigned char* pSwitching; // switching activity for each object
Gia_Plc_t * pPlacement; // placement of the objects
int * pTravIds; // separate traversal ID representation
};
@ -309,13 +310,22 @@ static inline void Gia_ObjRefFanin1Inc(Gia_Man_t * p, Gia_Obj_t * pObj){
static inline void Gia_ObjRefFanin0Dec(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefDec(p, Gia_ObjFanin0(pObj)); }
static inline void Gia_ObjRefFanin1Dec(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefDec(p, Gia_ObjFanin1(pObj)); }
static inline void Gia_ManResetTravId( Gia_Man_t * p ) { extern void Gia_ManCleanValue( Gia_Man_t * p ); Gia_ManCleanValue( p ); p->nTravIds = 1; }
static inline void Gia_ManIncrementTravId( Gia_Man_t * p ) { p->nTravIds++; }
static inline void Gia_ObjSetTravId( Gia_Obj_t * pObj, int TravId ) { pObj->Value = TravId; }
static inline void Gia_ObjSetTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj ) { pObj->Value = p->nTravIds; }
static inline void Gia_ObjSetTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { pObj->Value = p->nTravIds - 1; }
static inline int Gia_ObjIsTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj ) { return ((int)pObj->Value == p->nTravIds); }
static inline int Gia_ObjIsTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { return ((int)pObj->Value == p->nTravIds - 1); }
static inline void Gia_ManResetTravId( Gia_Man_t * p ) { extern void Gia_ManCleanValue( Gia_Man_t * p ); Gia_ManCleanValue( p ); p->nTravIds = 1; }
static inline void Gia_ManIncrementTravId( Gia_Man_t * p ) { p->nTravIds++; }
static inline void Gia_ObjSetTravId( Gia_Obj_t * pObj, int TravId ) { pObj->Value = TravId; }
static inline void Gia_ObjSetTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj ) { pObj->Value = p->nTravIds; }
static inline void Gia_ObjSetTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { pObj->Value = p->nTravIds - 1; }
static inline int Gia_ObjIsTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj ) { return ((int)pObj->Value == p->nTravIds); }
static inline int Gia_ObjIsTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { return ((int)pObj->Value == p->nTravIds - 1); }
static inline void Gia_ManResetTravIdArray( Gia_Man_t * p ) { ABC_FREE( p->pTravIds ); p->pTravIds = ABC_CALLOC( int, Gia_ManObjNum(p) ); p->nTravIds = 1; }
static inline void Gia_ManIncrementTravIdArray( Gia_Man_t * p ) { p->nTravIds++; }
static inline void Gia_ObjSetTravIdCurrentArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { p->pTravIds[Gia_ObjId(p, pObj)] = p->nTravIds; }
static inline void Gia_ObjSetTravIdPreviousArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { p->pTravIds[Gia_ObjId(p, pObj)] = p->nTravIds - 1; }
static inline int Gia_ObjIsTravIdCurrentArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds); }
static inline int Gia_ObjIsTravIdPreviousArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds - 1); }
static inline void Gia_ObjSetTravIdCurrentArrayId( Gia_Man_t * p, int Id ) { p->pTravIds[Id] = p->nTravIds; }
static inline int Gia_ObjIsTravIdCurrentArrayId( Gia_Man_t * p, int Id ) { return (p->pTravIds[Id] == p->nTravIds); }
// AIG construction
extern void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout );
@ -402,6 +412,7 @@ static inline int Gia_XsimAndCond( int Value0, int fCompl0, int Value1, int fCom
static inline Gia_Obj_t * Gia_ObjReprObj( Gia_Man_t * p, int Id ) { return p->pReprs[Id].iRepr == GIA_VOID ? NULL : Gia_ManObj( p, p->pReprs[Id].iRepr ); }
static inline int Gia_ObjRepr( Gia_Man_t * p, int Id ) { return p->pReprs[Id].iRepr; }
static inline void Gia_ObjSetRepr( Gia_Man_t * p, int Id, int Num ) { p->pReprs[Id].iRepr = Num; }
static inline void Gia_ObjUnsetRepr( Gia_Man_t * p, int Id ) { p->pReprs[Id].iRepr = GIA_VOID; }
static inline int Gia_ObjProved( Gia_Man_t * p, int Id ) { return p->pReprs[Id].fProved; }
static inline void Gia_ObjSetProved( Gia_Man_t * p, int Id ) { p->pReprs[Id].fProved = 1; }
@ -423,12 +434,15 @@ static inline int Gia_ObjNext( Gia_Man_t * p, int Id ) { r
static inline void Gia_ObjSetNext( Gia_Man_t * p, int Id, int Num ) { p->pNexts[Id] = Num; }
static inline int Gia_ObjIsConst( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == 0; }
static inline int Gia_ObjIsUsed( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) != GIA_VOID && Gia_ObjNext(p, Id) > 0; }
static inline int Gia_ObjIsHead( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) > 0; }
static inline int Gia_ObjIsNone( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) == 0; }
static inline int Gia_ObjIsTail( Gia_Man_t * p, int Id ) { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) && Gia_ObjNext(p, Id) == 0; }
static inline int Gia_ObjIsClass( Gia_Man_t * p, int Id ) { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) || Gia_ObjNext(p, Id) > 0; }
static inline int Gia_ObjHasSameRepr( Gia_Man_t * p, int i, int k ) { assert( k ); return i? (Gia_ObjRepr(p, i) == Gia_ObjRepr(p, k) && Gia_ObjRepr(p, i) != GIA_VOID) : Gia_ObjRepr(p, k) == 0; }
static inline int Gia_ObjIsFailedPair( Gia_Man_t * p, int i, int k ) { assert( k ); return i? (Gia_ObjFailed(p, i) || Gia_ObjFailed(p, k)) : Gia_ObjFailed(p, k); }
static inline int Gia_ClassIsPair( Gia_Man_t * p, int i ) { assert( Gia_ObjIsHead(p, i) ); assert( Gia_ObjNext(p, i) ); return Gia_ObjNext(p, Gia_ObjNext(p, i)) == 0; }
static inline void Gia_ClassUndoPair( Gia_Man_t * p, int i ) { assert( Gia_ClassIsPair(p,i) ); Gia_ObjSetRepr(p, Gia_ObjNext(p, i), GIA_VOID); Gia_ObjSetNext(p, i, 0); }
#define Gia_ManForEachConst( p, i ) \
for ( i = 1; i < Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsConst(p, i) ) {} else
@ -466,7 +480,9 @@ static inline int * Gia_ObjGateFanins( Gia_Man_t * p, int Id ) { re
#define Gia_ManForEachObjReverse( p, pObj, i ) \
for ( i = p->nObjs - 1; (i > 0) && ((pObj) = Gia_ManObj(p, i)); i-- )
#define Gia_ManForEachAnd( p, pObj, i ) \
for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ ) if ( !Gia_ObjIsAnd(pObj) ) {} else
for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ ) if ( !Gia_ObjIsAnd(pObj) ) {} else
#define Gia_ManForEachAndReverse( p, pObj, i ) \
for ( i = p->nObjs - 1; (i > 0) && ((pObj) = Gia_ManObj(p, i)); i-- ) if ( !Gia_ObjIsAnd(pObj) ) {} else
#define Gia_ManForEachCi( p, pObj, i ) \
for ( i = 0; (i < Vec_IntSize(p->vCis)) && ((pObj) = Gia_ManCi(p, i)); i++ )
#define Gia_ManForEachCo( p, pObj, i ) \
@ -498,6 +514,8 @@ extern void Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int
extern Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
/*=== giaCsat.c ============================================================*/
extern Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
/*=== giaCTas.c ============================================================*/
extern Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
/*=== giaCof.c =============================================================*/
extern void Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes );
extern Gia_Man_t * Gia_ManDupCof( Gia_Man_t * p, int iVar );
@ -508,6 +526,7 @@ extern void Gia_ManCollectCis( Gia_Man_t * p, int * pNodes, int n
extern void Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vNodes );
extern int Gia_ManSuppSize( Gia_Man_t * p, int * pNodes, int nNodes );
extern int Gia_ManConeSize( Gia_Man_t * p, int * pNodes, int nNodes );
extern Vec_Vec_t * Gia_ManLevelize( Gia_Man_t * p );
/*=== giaDup.c ============================================================*/
extern Gia_Man_t * Gia_ManDupOrderDfs( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupOrderDfsReverse( Gia_Man_t * p );
@ -620,6 +639,7 @@ extern void Gia_ManCheckMark1( Gia_Man_t * p );
extern void Gia_ManCleanValue( Gia_Man_t * p );
extern void Gia_ManFillValue( Gia_Man_t * p );
extern void Gia_ManSetPhase( Gia_Man_t * p );
extern void Gia_ManCleanPhase( Gia_Man_t * p );
extern int Gia_ManLevelNum( Gia_Man_t * p );
extern void Gia_ManSetRefs( Gia_Man_t * p );
extern int * Gia_ManCreateMuxRefs( Gia_Man_t * p );
@ -636,6 +656,14 @@ extern void Gia_ManPrintCounterExample( Gia_Cex_t * p );
extern int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode );
extern int Gia_ManHasChoices( Gia_Man_t * p );
extern int Gia_ManHasDandling( Gia_Man_t * p );
/*=== giaUtil.c ===========================================================*/
typedef struct Tas_Man_t_ Tas_Man_t;
extern Tas_Man_t * Tas_ManAlloc( Gia_Man_t * pAig, int nBTLimit );
extern void Tas_ManStop( Tas_Man_t * p );
extern Vec_Int_t * Tas_ReadModel( Tas_Man_t * p );
extern void Tas_ManSatPrintStats( Tas_Man_t * p );
extern int Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 );
#ifdef __cplusplus
}

41
src/aig/gia/giaAig.c
View File

@ -260,6 +260,47 @@ Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices )
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates AIG in the DFS order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Gia_ManToAigSkip( Gia_Man_t * p, int nOutDelta )
{
Aig_Man_t * pNew;
Aig_Obj_t ** ppNodes;
Gia_Obj_t * pObj;
int i;
assert( p->pNexts == NULL && p->pReprs == NULL );
assert( nOutDelta > 0 && Gia_ManCoNum(p) % nOutDelta == 0 );
// create the new manager
pNew = Aig_ManStart( Gia_ManAndNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
// pNew->pSpec = Gia_UtilStrsav( p->pName );
// create the PIs
ppNodes = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
ppNodes[0] = Aig_ManConst0(pNew);
Gia_ManForEachCi( p, pObj, i )
ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePi( pNew );
// add logic for the POs
Gia_ManForEachCo( p, pObj, i )
{
Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) );
if ( i % nOutDelta != 0 )
continue;
ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePo( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
}
Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) );
ABC_FREE( ppNodes );
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates AIG in the DFS order.]

1
src/aig/gia/giaAig.h
View File

@ -50,6 +50,7 @@ extern Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p );
extern Gia_Man_t * Gia_ManFromAigSimple( Aig_Man_t * p );
extern Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p );
extern Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices );
extern Aig_Man_t * Gia_ManToAigSkip( Gia_Man_t * p, int nOutDelta );
extern void Gia_ManReprToAigRepr( Aig_Man_t * p, Gia_Man_t * pGia );
#ifdef __cplusplus

2
src/aig/gia/giaCSat.c
View File

@ -1020,6 +1020,8 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
// solve for each output
Gia_ManForEachCo( pAig, pRoot, i )
{
// printf( "\n" );
Vec_IntClear( vCex );
if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) )
{

27
src/aig/gia/giaDfs.c
View File

@ -264,6 +264,33 @@ int Gia_ManConeSize( Gia_Man_t * p, int * pNodes, int nNodes )
return Counter;
}
/**Function*************************************************************
Synopsis [Levelizes the nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Vec_t * Gia_ManLevelize( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
Vec_Vec_t * vLevels;
int nLevels, Level, i;
nLevels = Gia_ManLevelNum( p );
vLevels = Vec_VecStart( nLevels + 1 );
Gia_ManForEachAnd( p, pObj, i )
{
Level = Gia_ObjLevel( p, pObj );
assert( Level <= nLevels );
Vec_VecPush( vLevels, Level, pObj );
}
return vLevels;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

33
src/aig/gia/giaEquiv.c
View File

@ -277,6 +277,8 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
assert( Gia_ManEquivCheckLits( p, nLits ) );
if ( fVerbose )
{
int Ent;
/*
printf( "Const0 = " );
Gia_ManForEachConst( p, i )
printf( "%d ", i );
@ -284,6 +286,18 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
Counter = 0;
Gia_ManForEachClass( p, i )
Gia_ManEquivPrintOne( p, i, ++Counter );
*/
Gia_ManLevelNum( p );
Gia_ManForEachClass( p, i )
if ( i % 100 == 0 )
{
// printf( "%d ", Gia_ManEquivCountOne(p, i) );
Gia_ClassForEachObj( p, i, Ent )
{
printf( "%d ", Gia_ObjLevel( p, Gia_ManObj(p, Ent) ) );
}
printf( "\n" );
}
}
}
@ -370,6 +384,15 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fV
printf( "Gia_ManEquivReduce(): Dual-output miter should have even number of POs.\n" );
return NULL;
}
// check if there are any equivalences defined
Gia_ManForEachObj( p, pObj, i )
if ( Gia_ObjReprObj(p, i) != NULL )
break;
if ( i == Gia_ManObjNum(p) )
{
printf( "Gia_ManEquivReduce(): There are no equivalences to reduce.\n" );
return NULL;
}
/*
if ( !Gia_ManCheckTopoOrder( p ) )
{
@ -720,6 +743,16 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose )
printf( "Gia_ManSpecReduce(): Dual-output miter should have even number of POs.\n" );
return NULL;
}
// check if there are any equivalences defined
Gia_ManForEachObj( p, pObj, i )
if ( Gia_ObjReprObj(p, i) != NULL )
break;
if ( i == Gia_ManObjNum(p) )
{
printf( "Gia_ManSpecReduce(): There are no equivalences to reduce.\n" );
return NULL;
}
/*
if ( !Gia_ManCheckTopoOrder( p ) )
{

5
src/aig/gia/giaMan.c
View File

@ -70,6 +70,7 @@ void Gia_ManStop( Gia_Man_t * p )
Vec_IntFree( p->vFlopClasses );
Vec_IntFree( p->vCis );
Vec_IntFree( p->vCos );
ABC_FREE( p->pTravIds );
ABC_FREE( p->pPlacement );
ABC_FREE( p->pSwitching );
ABC_FREE( p->pCexSeq );
@ -203,10 +204,10 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fSwitch )
void Gia_ManPrintStatsShort( Gia_Man_t * p )
{
printf( "i/o =%7d/%7d ", Gia_ManPiNum(p), Gia_ManPoNum(p) );
// printf( "ff =%7d ", Gia_ManRegNum(p) );
printf( "ff =%7d ", Gia_ManRegNum(p) );
printf( "and =%8d ", Gia_ManAndNum(p) );
printf( "lev =%5d ", Gia_ManLevelNum(p) );
printf( "mem =%5.2f Mb", 12.0*Gia_ManObjNum(p)/(1<<20) );
// printf( "mem =%5.2f Mb", 12.0*Gia_ManObjNum(p)/(1<<20) );
printf( "\n" );
}

42
src/aig/gia/giaUtil.c
View File

@ -315,6 +315,25 @@ void Gia_ManSetPhase( Gia_Man_t * p )
}
}
/**Function*************************************************************
Synopsis [Sets phases of the internal nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManCleanPhase( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i;
Gia_ManForEachObj( p, pObj, i )
pObj->fPhase = 0;
}
/**Function*************************************************************
Synopsis [Assigns levels.]
@ -883,17 +902,32 @@ int Gia_ManHasChoices( Gia_Man_t * p )
Gia_ManForEachObj( p, pObj, i )
{
if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) )
{
// printf( "%d ", i );
Counter1++;
if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) )
Counter2++;
}
// if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) )
// Counter2++;
}
// printf( "\n" );
Gia_ManForEachObj( p, pObj, i )
{
// if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) )
// Counter1++;
if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) )
{
// printf( "%d ", i );
Counter2++;
}
}
// printf( "\n" );
if ( Counter1 == 0 )
{
printf( "Warning: AIG has repr data-strucure but not reprs.\n" );
return 0;
}
// printf( "%d nodes have reprs.\n", Counter1 );
// printf( "%d nodes have nexts.\n", Counter2 );
printf( "%d nodes have reprs.\n", Counter1 );
printf( "%d nodes have nexts.\n", Counter2 );
// check if there are any internal nodes without fanout
// make sure all nodes without fanout have representatives
// make sure all nodes with fanout have no representatives

1
src/aig/gia/module.make
View File

@ -4,6 +4,7 @@ SRC += src/aig/gia/gia.c \
src/aig/gia/giaCof.c \
src/aig/gia/giaCSatOld.c \
src/aig/gia/giaCSat.c \
src/aig/gia/giaCTas.c \
src/aig/gia/giaDfs.c \
src/aig/gia/giaDup.c \
src/aig/gia/giaEmbed.c \

1
src/aig/int/int.h
View File

@ -57,6 +57,7 @@ struct Inter_ManParams_t_
int fCheckKstep; // check using K-step induction
int fUseBias; // bias decisions to global variables
int fUseBackward; // perform backward interpolation
int fUseSeparate; // solve each output separately
int fVerbose; // print verbose statistics
};

1
src/aig/int/intCore.c
View File

@ -53,6 +53,7 @@ void Inter_ManSetDefaultParams( Inter_ManParams_t * p )
p->fCheckKstep = 1; // check using K-step induction
p->fUseBias = 0; // bias decisions to global variables
p->fUseBackward = 0; // perform backward interpolation
p->fUseSeparate = 0; // solve each output separately
p->fVerbose = 0; // print verbose statistics
}

1
src/aig/ntl/module.make
View File

@ -6,6 +6,7 @@ SRC += src/aig/ntl/ntlCheck.c \
src/aig/ntl/ntlInsert.c \
src/aig/ntl/ntlMan.c \
src/aig/ntl/ntlMap.c \
src/aig/ntl/ntlNames.c \
src/aig/ntl/ntlObj.c \
src/aig/ntl/ntlReadBlif.c \
src/aig/ntl/ntlSweep.c \

20
src/aig/ntl/ntl.h
View File

@ -76,6 +76,7 @@ struct Ntl_Man_t_
Vec_Ptr_t * vVisNodes; // the nodes of the abstracted part
Vec_Int_t * vBox1Cios; // the first COs of the boxes
Vec_Int_t * vRegClasses; // the classes of registers in the AIG
Vec_Int_t * vRstClasses; // the classes of reset registers in the AIG
Aig_Man_t * pAig; // the extracted AIG
Tim_Man_t * pManTime; // the timing manager
int iLastCi; // the last true CI
@ -83,6 +84,7 @@ struct Ntl_Man_t_
void (*pNalF)(void *); // additional data
void (*pNalD)(void *,void *); // additional data
void (*pNalW)(void *,void *); // additional data
void (*pNalR)(void *); // additional data
// hashing names into models
Ntl_Mod_t ** pModTable; // the hash table of names into models
int nModTableSize; // the allocated table size
@ -112,6 +114,9 @@ struct Ntl_Mod_t_
// clocks of the model
Vec_Ptr_t * vClocks; // the clock signals
Vec_Vec_t * vClockFlops; // the flops of each clock
// resets of the model
Vec_Ptr_t * vResets; // the reset signals
Vec_Vec_t * vResetFlops; // the ASYNC flops of each reset
// delay information
Vec_Int_t * vDelays;
Vec_Int_t * vTimeInputs;
@ -121,7 +126,7 @@ struct Ntl_Mod_t_
Ntl_Mod_t * pNext;
void * pCopy;
int nUsed, nRems;
};
};
struct Ntl_Reg_t_
{
@ -139,6 +144,7 @@ struct Ntl_Obj_t_
unsigned Id : 28; // object ID
int nFanins; // the number of fanins
int nFanouts; // the number of fanouts
int Reset; // reset of the flop
union { // functionality
Ntl_Mod_t * pImplem; // model (for boxes)
char * pSop; // SOP (for logic nodes)
@ -162,9 +168,10 @@ struct Ntl_Net_t_
int iTemp; // other data
};
Ntl_Obj_t * pDriver; // driver of the net
unsigned NetId : 28; // unique ID of the net
unsigned NetId : 27; // unique ID of the net
unsigned nVisits : 2; // the number of times the net is visted
unsigned fMark : 1; // temporary mark
unsigned fMark2 : 1; // temporary mark
unsigned fFixed : 1; // the fixed net
char pName[0]; // the name of this net
};
@ -329,11 +336,18 @@ extern ABC_DLL void Ntl_ManFree( Ntl_Man_t * p );
extern ABC_DLL void Ntl_ManPrintStats( Ntl_Man_t * p );
extern ABC_DLL Tim_Man_t * Ntl_ManReadTimeMan( Ntl_Man_t * p );
extern ABC_DLL void Ntl_ManPrintTypes( Ntl_Man_t * p );
extern ABC_DLL int Ntl_ManCompareClockClasses( Vec_Ptr_t ** pp1, Vec_Ptr_t ** pp2 );
extern ABC_DLL void Ntl_ManPrintClocks( Ntl_Man_t * p );
extern ABC_DLL void Ntl_ManPrintResets( Ntl_Man_t * p );
extern ABC_DLL Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName );
extern ABC_DLL Ntl_Mod_t * Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld );
extern ABC_DLL Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld );
extern ABC_DLL void Ntl_ModelFree( Ntl_Mod_t * p );
extern ABC_DLL Ntl_Mod_t * Ntl_ManCreateLatchModel( Ntl_Man_t * pMan, int Init );
extern ABC_DLL int Ntl_ModelCountLut0( Ntl_Mod_t * p );
extern ABC_DLL int Ntl_ModelCountLut1( Ntl_Mod_t * p );
extern ABC_DLL int Ntl_ModelCountBuf( Ntl_Mod_t * p );
extern ABC_DLL int Ntl_ModelCountInv( Ntl_Mod_t * p );
/*=== ntlMap.c ============================================================*/
extern ABC_DLL Vec_Ptr_t * Ntl_MappingAlloc( int nLuts, int nVars );
extern ABC_DLL Vec_Ptr_t * Ntl_MappingFromAig( Aig_Man_t * p );
@ -350,6 +364,7 @@ extern ABC_DLL Ntl_Obj_t * Ntl_ModelCreatePiWithName( Ntl_Mod_t * pModel, ch
extern ABC_DLL char * Ntl_ManStoreName( Ntl_Man_t * p, char * pName );
extern ABC_DLL char * Ntl_ManStoreSop( Aig_MmFlex_t * pMan, char * pSop );
extern ABC_DLL char * Ntl_ManStoreFileName( Ntl_Man_t * p, char * pFileName );
extern ABC_DLL int Ntl_ManObjWhichFanout( Ntl_Obj_t * pNode, Ntl_Net_t * pFanout );
/*=== ntlSweep.c ==========================================================*/
extern ABC_DLL int Ntl_ManSweep( Ntl_Man_t * p, int fVerbose );
/*=== ntlTable.c ==========================================================*/
@ -374,7 +389,6 @@ extern ABC_DLL Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck );
extern ABC_DLL void Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName );
extern ABC_DLL void Ioa_WriteBlifLogic( Nwk_Man_t * pNtk, Ntl_Man_t * p, char * pFileName );
/*=== ntlUtil.c ==========================================================*/
extern ABC_DLL int Ntl_ModelCountLut1( Ntl_Mod_t * pRoot );
extern ABC_DLL int Ntl_ModelGetFaninMax( Ntl_Mod_t * pRoot );
extern ABC_DLL Ntl_Net_t * Ntl_ModelFindSimpleNet( Ntl_Net_t * pNetCo );
extern ABC_DLL int Ntl_ManCountSimpleCoDrivers( Ntl_Man_t * p );

3
src/aig/ntl/ntlExtract.c
View File

@ -371,6 +371,7 @@ int Ntl_ManCollapseBoxSeq1_rec( Ntl_Man_t * p, Ntl_Obj_t * pBox, int fSeq )
pNet->nVisits = 2;
// remember the class of this register
Vec_IntPush( p->vRegClasses, p->pNal ? pBox->iTemp : pObj->LatchId.regClass );
Vec_IntPush( p->vRstClasses, p->pNal ? pBox->Reset : -1 );
}
// compute AIG for the internal nodes
Ntl_ModelForEachPo( pModel, pObj, i )
@ -505,6 +506,7 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq )
assert( Vec_PtrSize(p->vCos) != 0 );
Vec_IntClear( p->vBox1Cios );
Vec_IntClear( p->vRegClasses );
Vec_IntClear( p->vRstClasses );
// clear net visited flags
pRoot = Ntl_ManRootModel(p);
assert( Ntl_ModelLatchNum(pRoot) == 0 );
@ -797,6 +799,7 @@ Nwk_Man_t * Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig, Tim_Man_t * pMan
{
pNet->pCopy2 = Ntl_ManExtractNwk_rec( p, pNet, pNtk, vCover, vMemory );
Nwk_ObjAddFanin( pNode, pNet->pCopy2 );
pNode->fInvert = (Nwk_ObjFanin0(pNode)->pFunc == Hop_ManConst0(pNtk->pManHop)); // fixed on June 7, 2009
}
}
}

220
src/aig/ntl/ntlFraig.c
View File

@ -421,6 +421,171 @@ Ntl_Man_t * Ntl_ManFraig( Ntl_Man_t * p, int nPartSize, int nConfLimit, int nLev
return pNew;
}
/**Function*************************************************************
Synopsis [Counts the number of resets.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ManAigCountResets( Ntl_Man_t * pNtl )
{
Ntl_Mod_t * pModel = Ntl_ManRootModel(pNtl);
Ntl_Obj_t * pBox;
int i, Counter = -1;
Ntl_ModelForEachObj( pModel, pBox, i )
Counter = ABC_MAX( Counter, pBox->Reset );
return Counter + 1;
}
/**Function*************************************************************
Synopsis [Transforms sequential AIG to allow for async reset.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Ntl_ManAigToRst( Ntl_Man_t * pNtl, Aig_Man_t * p )
{
Ntl_Mod_t * pModel = Ntl_ManRootModel(pNtl);
Aig_Man_t * pNew;
Aig_Obj_t * pObj;
int i, iRegNum, iRstNum, Counter = 0;
int nResets = Ntl_ManAigCountResets( pNtl );
assert( pNtl->pNal != NULL );
assert( Aig_ManRegNum(p) > 0 );
assert( Vec_IntSize(pNtl->vRstClasses) == Aig_ManRegNum(p) );
//printf( "Number of resets before synthesis = %d.\n", nResets );
// create the PIs
Aig_ManCleanData( p );
Aig_ManSetPioNumbers( p );
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
// create special PIs
for ( i = 0; i < nResets; i++ )
Aig_ObjCreatePi( pNew );
// duplicate internal nodes
Aig_ManForEachPi( p, pObj, i )
pObj->pData = Aig_ObjCreatePi( pNew );
Aig_ManForEachObj( p, pObj, i )
{
if ( Aig_ObjIsNode(pObj) )
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
else if ( Aig_ObjIsPo(pObj) )
pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
else if ( Aig_ObjIsPi(pObj) )
{
// pObj->pData = Aig_ObjCreatePi( pNew );
iRegNum = Aig_ObjPioNum(pObj) - (Aig_ManPiNum(p) - Aig_ManRegNum(p));
if ( iRegNum < 0 )
continue;
iRstNum = Vec_IntEntry(pNtl->vRstClasses, iRegNum);
if ( iRstNum < 0 )
continue;
assert( iRstNum < nResets );
pObj->pData = Aig_And( pNew, pObj->pData, Aig_ManPi(pNew, iRstNum) ); // could be NOT(pi)
Counter++;
}
else if ( Aig_ObjIsConst1(pObj) )
pObj->pData = Aig_ManConst1(pNew);
else
assert( 0 );
}
assert( Aig_ManNodeNum(p) + Counter == Aig_ManNodeNum(pNew) );
if ( (Counter = Aig_ManCleanup( pNew )) )
printf( "Aig_ManDupOrdered(): Cleanup after AIG duplication removed %d nodes.\n", Counter );
Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
return pNew;
}
/**Function*************************************************************
Synopsis [Remaps equivalence classes from the new nodes to the old ones.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ntl_ManRemapClassesLcorr( Ntl_Man_t * pNtl, Aig_Man_t * p, Aig_Man_t * pNew )
{
Ntl_Mod_t * pModel = Ntl_ManRootModel(pNtl);
Aig_Obj_t * pObj, * pObjRepr, * pObjNew, * pObjNewRepr;
int i, nResets = Ntl_ManAigCountResets( pNtl );
int nTruePis = Aig_ManPiNum(p) - Aig_ManRegNum(p);
assert( pNew->pReprs != NULL );
assert( nResets == Aig_ManPiNum(pNew) - Aig_ManPiNum(p) );
Aig_ManReprStart( p, Aig_ManObjNumMax(p) );
Aig_ManForEachLoSeq( pNew, pObjNew, i )
{
pObj = Aig_ManPi( p, i - nResets );
pObjNewRepr = pNew->pReprs[pObjNew->Id];
if ( pObjNewRepr == NULL )
continue;
if ( pObjNewRepr == Aig_ManConst1(pNew) )
{
Aig_ObjCreateRepr( p, Aig_ManConst1(p), pObj );
continue;
}
assert( Aig_ObjIsPi(pObjNewRepr) );
// find the corresponding representative node
pObjRepr = Aig_ManPi( p, Aig_ObjPioNum(pObjNewRepr) - nResets );
// if they belong to different domains, quit
if ( Vec_IntEntry( pNtl->vRstClasses, Aig_ObjPioNum(pObj) - nTruePis ) !=
Vec_IntEntry( pNtl->vRstClasses, Aig_ObjPioNum(pObjRepr) - nTruePis ) )
continue;
Aig_ObjCreateRepr( p, pObjRepr, pObj );
}
}
/**Function*************************************************************
Synopsis [Remaps equivalence classes from the new nodes to the old ones.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ntl_ManRemapClassesScorr( Ntl_Man_t * pNtl, Aig_Man_t * p, Aig_Man_t * pNew )
{
Aig_Obj_t * pObj, * pObjRepr, * pObjNew, * pObjNewRepr;
int i;
// map things back
Aig_ManForEachObj( p, pObj, i )
{
pObjNew = pObj->pData;
assert( pObjNew != NULL && !Aig_IsComplement(pObjNew) );
pObjNew->pData = pObj;
}
// remap the classes
Aig_ManForEachObj( pNew, pObjNew, i )
{
pObjNewRepr = pNew->pReprs[pObjNew->Id];
if ( pObjNewRepr == NULL )
continue;
pObj = pObjNew->pData;
pObjRepr = pObjNewRepr->pData;
assert( Aig_ObjId(pObjRepr) < Aig_ObjId(pObj) );
Aig_ObjCreateRepr( p, pObjRepr, pObj );
}
}
/**Function*************************************************************
Synopsis [Performs sequential cleanup.]
@ -451,9 +616,21 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe
//Ntl_ManPrintStats( pNew );
//Aig_ManPrintStats( pAigCol );
// perform SCL for the given design
pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, fVerbose );
Aig_ManStop( pTemp );
// perform SCL
if ( p->pNal )
{
Aig_Man_t * pAigRst;
pAigRst = Ntl_ManAigToRst( pNew, pAigCol );
pTemp = Aig_ManScl( pAigRst, fLatchConst, fLatchEqual, fVerbose );
Aig_ManStop( pTemp );
Ntl_ManRemapClassesLcorr( pNew, pAigCol, pAigRst );
Aig_ManStop( pAigRst );
}
else
{
pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, fVerbose );
Aig_ManStop( pTemp );
}
// finalize the transformation
pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose );
@ -493,11 +670,23 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fScorrGia, int fUseCS
return pNew;
}
// perform LCORR for the given design
// perform LCORR
pPars->fScorrGia = fScorrGia;
pPars->fUseCSat = fUseCSat;
pTemp = Ssw_LatchCorrespondence( pAigCol, pPars );
Aig_ManStop( pTemp );
if ( p->pNal )
{
Aig_Man_t * pAigRst;
pAigRst = Ntl_ManAigToRst( pNew, pAigCol );
pTemp = Ssw_LatchCorrespondence( pAigRst, pPars );
Aig_ManStop( pTemp );
Ntl_ManRemapClassesLcorr( pNew, pAigCol, pAigRst );
Aig_ManStop( pAigRst );
}
else
{
pTemp = Ssw_LatchCorrespondence( pAigCol, pPars );
Aig_ManStop( pTemp );
}
// finalize the transformation
pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose );
@ -522,6 +711,7 @@ Ntl_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Fra_Ssw_t * pPars )
{
Ntl_Man_t * pNew, * pAux;
Aig_Man_t * pAig, * pAigCol, * pTemp;
assert( 0 ); // not updated for nal
// collapse the AIG
pAig = Ntl_ManExtract( p );
@ -571,9 +761,21 @@ Ntl_Man_t * Ntl_ManScorr( Ntl_Man_t * p, Ssw_Pars_t * pPars )
return pNew;
}
// perform SCL for the given design
pTemp = Ssw_SignalCorrespondence( pAigCol, pPars );
Aig_ManStop( pTemp );
// perform SCL
if ( p->pNal )
{
Aig_Man_t * pAigRst;
pAigRst = Ntl_ManAigToRst( pNew, pAigCol );
pTemp = Ssw_SignalCorrespondence( pAigRst, pPars );
Aig_ManStop( pTemp );
Ntl_ManRemapClassesLcorr( pNew, pAigCol, pAigRst );
Aig_ManStop( pAigRst );
}
else
{
pTemp = Ssw_SignalCorrespondence( pAigCol, pPars );
Aig_ManStop( pTemp );
}
// finalize the transformation
pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, pPars->fVerbose );

185
src/aig/ntl/ntlInsert.c
View File

@ -279,6 +279,190 @@ void Ntl_ManFindDriver( Ntl_Man_t * p, char * pName )
pNode->Id, Ntl_ObjFaninNum(pNode), Ntl_ObjFanoutNum(pNode), Ntl_ObjFanout(pNode,0)->pName );
}
/**Function*************************************************************
Synopsis [Inserts the given mapping into the netlist.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ntl_Man_t * Ntl_ManInsertNtk2( Ntl_Man_t * p, Nwk_Man_t * pNtk )
{
int fWriteConstants = 1;
char Buffer[1000];
Vec_Ptr_t * vObjs;
Vec_Int_t * vTruth;
Vec_Int_t * vCover;
Ntl_Mod_t * pRoot;
Ntl_Obj_t * pNode;
Ntl_Net_t * pNet, * pNetCo;
Nwk_Obj_t * pObj, * pFanin;
int i, k, nDigits;
unsigned * pTruth;
assert( Vec_PtrSize(p->vCis) == Nwk_ManCiNum(pNtk) );
assert( Vec_PtrSize(p->vCos) == Nwk_ManCoNum(pNtk) );
p = Ntl_ManStartFrom( p );
pRoot = Ntl_ManRootModel( p );
assert( Ntl_ModelNodeNum(pRoot) == 0 );
// set the correspondence between the PI/PO nodes
Ntl_ManForEachCiNet( p, pNet, i )
Nwk_ManCi( pNtk, i )->pCopy = pNet;
// create a new node for each LUT
vTruth = Vec_IntAlloc( 1 << 16 );
vCover = Vec_IntAlloc( 1 << 16 );
nDigits = Aig_Base10Log( Nwk_ManNodeNum(pNtk) );
// go through the nodes in the topological order
vObjs = Nwk_ManDfs( pNtk );
Vec_PtrForEachEntry( vObjs, pObj, i )
{
if ( !Nwk_ObjIsNode(pObj) )
continue;
/*
if ( fWriteConstants && Nwk_ObjFaninNum(pObj) == 0 )
{
pObj->pCopy = NULL;
continue;
}
*/
// skip constant drivers if they only drive COs
if ( fWriteConstants && Nwk_ObjFaninNum(pObj) == 0 )
{
Nwk_Obj_t * pFanout;
int i;
Nwk_ObjForEachFanout( pObj, pFanout, i )
if ( Nwk_ObjIsNode(pFanout) )
break;
if ( i == Nwk_ObjFanoutNum(pObj) )
{
pObj->pCopy = NULL;
continue;
}
}
pNode = Ntl_ModelCreateNode( pRoot, Nwk_ObjFaninNum(pObj) );
pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, Hop_Regular(pObj->pFunc), Nwk_ObjFaninNum(pObj), vTruth, 0 );
if ( Hop_IsComplement(pObj->pFunc) )
Kit_TruthNot( pTruth, pTruth, Nwk_ObjFaninNum(pObj) );
if ( !Kit_TruthIsConst0(pTruth, Nwk_ObjFaninNum(pObj)) && !Kit_TruthIsConst1(pTruth, Nwk_ObjFaninNum(pObj)) )
{
Nwk_ObjForEachFanin( pObj, pFanin, k )
{
pNet = pFanin->pCopy;
if ( pNet == NULL )
{
printf( "Ntl_ManInsertNtk(): Internal error: Net not found.\n" );
return 0;
}
Ntl_ObjSetFanin( pNode, pNet, k );
}
}
else if ( Kit_TruthIsConst0(pTruth, Nwk_ObjFaninNum(pObj)) )
{
pObj->pFunc = Hop_ManConst0(pNtk->pManHop);
pNode->nFanins = 0;
}
else if ( Kit_TruthIsConst1(pTruth, Nwk_ObjFaninNum(pObj)) )
{
pObj->pFunc = Hop_ManConst1(pNtk->pManHop);
pNode->nFanins = 0;
}
pNode->pSop = Kit_PlaFromTruth( p->pMemSops, pTruth, Nwk_ObjFaninNum(pObj), vCover );
sprintf( Buffer, "lut%0*d", nDigits, i );
if ( (pNet = Ntl_ModelFindNet( pRoot, Buffer )) )
{
printf( "Ntl_ManInsertNtk(): Internal error: Intermediate net name is not unique.\n" );
return 0;
}
pNet = Ntl_ModelFindOrCreateNet( pRoot, Buffer );
if ( !Ntl_ModelSetNetDriver( pNode, pNet ) )
{
printf( "Ntl_ManInsertNtk(): Internal error: Net has more than one fanin.\n" );
return 0;
}
pObj->pCopy = pNet;
}
Vec_PtrFree( vObjs );
Vec_IntFree( vCover );
Vec_IntFree( vTruth );
// mark the nets driving special boxes
if ( p->pNalR )
p->pNalR( p );
// mark CIs and outputs of the registers
Ntl_ManForEachCiNet( p, pNetCo, i )
pNetCo->fMark = 1;
// update the CO pointers
Ntl_ManForEachCoNet( p, pNetCo, i )
{
if ( pNetCo->fMark )
continue;
pNetCo->fMark = 1;
// get the corresponding PO and its driver
pObj = Nwk_ManCo( pNtk, i );
pFanin = Nwk_ObjFanin0( pObj );
// get the net driving this PO
pNet = pFanin->pCopy;
if ( pNet == NULL ) // constant net
{
assert( fWriteConstants );
pNode = Ntl_ModelCreateNode( pRoot, 0 );
pNode->pSop = pObj->fInvert? Ntl_ManStoreSop( p->pMemSops, " 0\n" ) : Ntl_ManStoreSop( p->pMemSops, " 1\n" );
}
else
if ( Nwk_ObjFanoutNum(pFanin) == 1 && Ntl_ObjIsNode(pNet->pDriver) && !pNet->fMark2 )
{
pNode = pNet->pDriver;
if ( !Ntl_ModelClearNetDriver( pNode, pNet ) )
{
printf( "Ntl_ManInsertNtk(): Internal error! Net already has no driver.\n" );
return NULL;
}
// remove this net
Ntl_ModelDeleteNet( pRoot, pNet );
Vec_PtrWriteEntry( pRoot->vNets, pNet->NetId, NULL );
// update node's function
if ( pObj->fInvert )
Kit_PlaComplement( pNode->pSop );
}
else
{
/*
if ( fWriteConstants && Ntl_ObjFaninNum(pNet->pDriver) == 0 )
{
pNode = Ntl_ModelCreateNode( pRoot, 0 );
pNode->pSop = pObj->fInvert? Ntl_ManStoreSop( p->pMemSops, " 0\n" ) : Ntl_ManStoreSop( p->pMemSops, " 1\n" );
}
else
*/
{
// assert( Ntl_ObjFaninNum(pNet->pDriver) != 0 );
pNode = Ntl_ModelCreateNode( pRoot, 1 );
pNode->pSop = pObj->fInvert? Ntl_ManStoreSop( p->pMemSops, "0 1\n" ) : Ntl_ManStoreSop( p->pMemSops, "1 1\n" );
Ntl_ObjSetFanin( pNode, pNet, 0 );
}
}
// update the CO driver net
assert( pNetCo->pDriver == NULL );
if ( !Ntl_ModelSetNetDriver( pNode, pNetCo ) )
{
printf( "Ntl_ManInsertNtk(): Internal error: PO net has more than one fanin.\n" );
return NULL;
}
}
// clean CI/CO marks
Ntl_ManUnmarkCiCoNets( p );
if ( !Ntl_ManCheck( p ) )
{
printf( "Ntl_ManInsertNtk: The check has failed for design %s.\n", p->pName );
return NULL;
}
return p;
}
/**Function*************************************************************
Synopsis [Inserts the given mapping into the netlist.]
@ -418,7 +602,6 @@ Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
return p;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

212
src/aig/ntl/ntlMan.c
View File

@ -51,6 +51,7 @@ Ntl_Man_t * Ntl_ManAlloc()
p->vVisNodes = Vec_PtrAlloc( 1000 );
p->vBox1Cios = Vec_IntAlloc( 1000 );
p->vRegClasses = Vec_IntAlloc( 1000 );
p->vRstClasses = Vec_IntAlloc( 1000 );
// start the manager
p->pMemObjs = Aig_MmFlexStart();
p->pMemSops = Aig_MmFlexStart();
@ -123,6 +124,7 @@ Ntl_Man_t * Ntl_ManStartFrom( Ntl_Man_t * pOld )
{
((Ntl_Obj_t *)pBox->pCopy)->pImplem = pBox->pImplem->pCopy;
((Ntl_Obj_t *)pBox->pCopy)->iTemp = pBox->iTemp;
((Ntl_Obj_t *)pBox->pCopy)->Reset = pBox->Reset;
}
Ntl_ManForEachCiNet( pOld, pNet, i )
Vec_PtrPush( pNew->vCis, pNet->pCopy );
@ -197,6 +199,7 @@ void Ntl_ManFree( Ntl_Man_t * p )
if ( p->vCos ) Vec_PtrFree( p->vCos );
if ( p->vVisNodes ) Vec_PtrFree( p->vVisNodes );
if ( p->vRegClasses) Vec_IntFree( p->vRegClasses );
if ( p->vRstClasses) Vec_IntFree( p->vRstClasses );
if ( p->vBox1Cios ) Vec_IntFree( p->vBox1Cios );
if ( p->pMemObjs ) Aig_MmFlexStop( p->pMemObjs, 0 );
if ( p->pMemSops ) Aig_MmFlexStop( p->pMemSops, 0 );
@ -294,18 +297,34 @@ void Nwk_ManPrintStatsShort( Ntl_Man_t * p, Aig_Man_t * pAig, Nwk_Man_t * pNtk )
SeeAlso []
***********************************************************************/
int Nwk_ManStatsRegs( Ntl_Man_t * p )
int Ntl_ManStatsRegs( Ntl_Man_t * p )
{
Ntl_Mod_t * pRoot;
Ntl_Obj_t * pObj;
int i, Counter = 0;
pRoot = Ntl_ManRootModel( p );
Ntl_ModelForEachBox( pRoot, pObj, i )
if ( strcmp(pObj->pImplem->pName, "dff") == 0 )
if ( strcmp(pObj->pImplem->pName, "m_dff") == 0 )
Counter++;
return Counter;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ManStatsLuts( Ntl_Man_t * p )
{
return Ntl_ModelLut1Num( Ntl_ManRootModel(p) ) + Ntl_ModelNodeNum( Ntl_ManRootModel(p) );
}
/**Function*************************************************************
Synopsis []
@ -353,13 +372,13 @@ int Nwk_ManStatsLevs( Nwk_Man_t * pNtk )
void Nwk_ManPrintStatsUpdate( Ntl_Man_t * p, Aig_Man_t * pAig, Nwk_Man_t * pNtk,
int nRegInit, int nLutInit, int nLevInit, int Time )
{
printf( "FF =%7d (%4.1f%%) ", Nwk_ManStatsRegs(p), 100.0*(nRegInit-Nwk_ManStatsRegs(p))/nRegInit );
printf( "FF =%7d (%5.1f%%) ", Ntl_ManStatsRegs(p), nRegInit ? (100.0*(nRegInit-Ntl_ManStatsRegs(p))/nRegInit) : 0.0 );
if ( pNtk == NULL )
printf( "Mapping is not available. " );
printf( "Mapping is not available. " );
else
{
printf( "Lut =%7d (%4.1f%%) ", Nwk_ManStatsLuts(pNtk), 100.0*(nLutInit-Nwk_ManStatsLuts(pNtk))/nLutInit );
printf( "Lev =%4d (%4.1f%%) ", Nwk_ManStatsLevs(pNtk), 100.0*(nLevInit-Nwk_ManStatsLevs(pNtk))/nLevInit );
printf( "Lut =%7d (%5.1f%%) ", Ntl_ManStatsLuts(p), nLutInit ? (100.0*(nLutInit-Ntl_ManStatsLuts(p))/nLutInit) : 0.0 );
printf( "Lev =%4d (%5.1f%%) ", Nwk_ManStatsLevs(pNtk), nLevInit ? (100.0*(nLevInit-Nwk_ManStatsLevs(pNtk))/nLevInit) : 0.0 );
}
ABC_PRT( "Time", clock() - Time );
}
@ -459,6 +478,101 @@ void Ntl_ManPrintTypes( Ntl_Man_t * p )
printf( "\n" );
}
/**Function*************************************************************
Synopsis [Procedure used for sorting the nodes in decreasing order of levels.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ManCompareClockClasses( Vec_Ptr_t ** pp1, Vec_Ptr_t ** pp2 )
{
int Diff = Vec_PtrSize(*pp1) - Vec_PtrSize(*pp2);
if ( Diff > 0 )
return -1;
if ( Diff < 0 )
return 1;
return 0;
}
/**Function*************************************************************
Synopsis [Saves the model type.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ntl_ManPrintClocks( Ntl_Man_t * p )
{
Vec_Ptr_t * vFlops;
Ntl_Net_t * pNet;
Ntl_Mod_t * pModel;
int i;
pModel = Ntl_ManRootModel( p );
if ( Ntl_ModelBoxNum(pModel) == 0 )
return;
if ( pModel->vClockFlops )
{
printf( "CLOCK STATISTICS:\n" );
Vec_VecForEachLevel( pModel->vClockFlops, vFlops, i )
{
pNet = Vec_PtrEntry( pModel->vClocks, i );
printf( "Clock %2d : Name = %30s Flops = %6d.\n", i+1, pNet->pName, Vec_PtrSize(vFlops) );
if ( i == 10 )
{
printf( "Skipping... (the total is %d)\n", Vec_VecSize(pModel->vClockFlops) );
break;
}
}
}
// printf( "\n" );
}
/**Function*************************************************************
Synopsis [Saves the model type.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ntl_ManPrintResets( Ntl_Man_t * p )
{
Vec_Ptr_t * vFlops;
Ntl_Net_t * pNet;
Ntl_Mod_t * pModel;
int i;
pModel = Ntl_ManRootModel( p );
if ( Ntl_ModelBoxNum(pModel) == 0 )
return;
if ( pModel->vResetFlops )
{
printf( "RESET STATISTICS:\n" );
Vec_VecForEachLevel( pModel->vResetFlops, vFlops, i )
{
pNet = Vec_PtrEntry( pModel->vResets, i );
printf( "Reset %2d : Name = %30s Flops = %6d.\n", i+1, pNet->pName, Vec_PtrSize(vFlops) );
if ( i == 10 )
{
printf( "Skipping... (the total is %d)\n", Vec_VecSize(pModel->vResetFlops) );
break;
}
}
}
// printf( "\n" );
}
/**Function*************************************************************
Synopsis [Allocates the model.]
@ -643,6 +757,8 @@ void Ntl_ModelFree( Ntl_Mod_t * p )
if ( p->vDelays ) Vec_IntFree( p->vDelays );
if ( p->vClocks ) Vec_PtrFree( p->vClocks );
if ( p->vClockFlops ) Vec_VecFree( p->vClockFlops );
if ( p->vResets ) Vec_PtrFree( p->vResets );
if ( p->vResetFlops ) Vec_VecFree( p->vResetFlops );
Vec_PtrFree( p->vNets );
Vec_PtrFree( p->vObjs );
Vec_PtrFree( p->vPis );
@ -699,6 +815,90 @@ Ntl_Mod_t * Ntl_ManCreateLatchModel( Ntl_Man_t * pMan, int Init )
}
/**Function*************************************************************
Synopsis [Count constant nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ModelCountLut0( Ntl_Mod_t * p )
{
Ntl_Obj_t * pNode;
int i, Counter = 0;
Ntl_ModelForEachNode( p, pNode, i )
if ( Ntl_ObjFaninNum(pNode) == 0 )
Counter++;
return Counter;
}
/**Function*************************************************************
Synopsis [Count single-output nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ModelCountLut1( Ntl_Mod_t * p )
{
Ntl_Obj_t * pNode;
int i, Counter = 0;
Ntl_ModelForEachNode( p, pNode, i )
if ( Ntl_ObjFaninNum(pNode) == 1 )
Counter++;
return Counter;
}
/**Function*************************************************************
Synopsis [Count buffers]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ModelCountBuf( Ntl_Mod_t * p )
{
Ntl_Obj_t * pNode;
int i, Counter = 0;
Ntl_ModelForEachNode( p, pNode, i )
if ( Ntl_ObjFaninNum(pNode) == 1 && pNode->pSop[0] == '1' )
Counter++;
return Counter;
}
/**Function*************************************************************
Synopsis [Count inverters.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ModelCountInv( Ntl_Mod_t * p )
{
Ntl_Obj_t * pNode;
int i, Counter = 0;
Ntl_ModelForEachNode( p, pNode, i )
if ( Ntl_ObjFaninNum(pNode) == 1 && pNode->pSop[0] == '0' )
Counter++;
return Counter;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

22
src/aig/ntl/ntlObj.c
View File

@ -160,6 +160,7 @@ Ntl_Obj_t * Ntl_ModelCreateBox( Ntl_Mod_t * pModel, int nFanins, int nFanouts )
p->Type = NTL_OBJ_BOX;
p->nFanins = nFanins;
p->nFanouts = nFanouts;
p->Reset = -1;
pModel->nObjs[NTL_OBJ_BOX]++;
return p;
}
@ -285,6 +286,27 @@ char * Ntl_ManStoreFileName( Ntl_Man_t * p, char * pFileName )
}
/**Function*************************************************************
Synopsis [Returns the index of the fanin in the fanin list of the fanout.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ManObjWhichFanout( Ntl_Obj_t * pNode, Ntl_Net_t * pFanout )
{
Ntl_Net_t * pObj;
int i;
Ntl_ObjForEachFanout( pNode, pObj, i )
if ( pObj == pFanout )
return i;
return -1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

22
src/aig/ntl/ntlUtil.c
View File

@ -28,27 +28,6 @@
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Counts COs that are connected to the internal nodes through invs/bufs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ModelCountLut1( Ntl_Mod_t * pRoot )
{
Ntl_Obj_t * pObj;
int i, Counter = 0;
Ntl_ModelForEachNode( pRoot, pObj, i )
if ( Ntl_ObjFaninNum(pObj) == 1 )
Counter++;
return Counter;
}
/**Function*************************************************************
Synopsis [Reads the maximum number of fanins.]
@ -370,6 +349,7 @@ Vec_Vec_t * Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVer
if ( Vec_IntSize(pMan->vRegClasses) == 0 )
{
printf( "Ntl_ManReportRegClasses(): Register classes are not defined.\n" );
// return (Vec_Vec_t *)Vec_PtrAlloc(0);
return NULL;
}
// find the largest class

2
src/aig/nwk/nwkMap.c
View File

@ -321,6 +321,7 @@ Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p, Vec_Ptr_t * vAigToI
pObjNew = Nwk_ManCreateCo( pNtk );
pObjNew->fInvert = Aig_ObjFaninC0(pObj);
Nwk_ObjAddFanin( pObjNew, Aig_ObjFanin0(pObj)->pData );
//printf( "%d ", pObjNew->Id );
}
else if ( Aig_ObjIsConst1(pObj) )
{
@ -331,6 +332,7 @@ Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p, Vec_Ptr_t * vAigToI
assert( 0 );
pObj->pData = pObjNew;
}
//printf( "\n" );
Vec_PtrFree( vIfToAig );
pNtk->pManTime = Tim_ManDup( pIfMan->pManTim, 0 );
Nwk_ManMinimumBase( pNtk, 0 );

44
src/aig/nwk/nwkUtil.c
View File

@ -502,6 +502,49 @@ int Nwk_ManMinimumBaseNode( Nwk_Obj_t * pObj, Vec_Int_t * vTruth, int fVerbose )
return 1;
}
/**Function*************************************************************
Synopsis [Minimizes the support of all nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Nwk_ManMinimumBaseInt( Nwk_Man_t * pNtk, int fVerbose )
{
Vec_Int_t * vTruth;
Nwk_Obj_t * pObj;
int i, Counter = 0;
vTruth = Vec_IntAlloc( 1 << 16 );
Nwk_ManForEachNode( pNtk, pObj, i )
Counter += Nwk_ManMinimumBaseNode( pObj, vTruth, fVerbose );
if ( fVerbose && Counter )
printf( "Support minimization reduced support of %d nodes.\n", Counter );
Vec_IntFree( vTruth );
return Counter;
}
/**Function*************************************************************
Synopsis [Minimizes the support of all nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Nwk_ManMinimumBaseRec( Nwk_Man_t * pNtk, int fVerbose )
{
int i, clk = clock();
for ( i = 0; Nwk_ManMinimumBaseInt( pNtk, fVerbose ); i++ );
ABC_PRT( "Minbase", clock() - clk );
}
/**Function*************************************************************
Synopsis [Minimizes the support of all nodes.]
@ -585,6 +628,7 @@ void Nwk_ManRemoveDupFanins( Nwk_Man_t * pNtk, int fVerbose )
}
}
Vec_IntFree( vTruth );
// Nwk_ManMinimumBase( pNtk, fVerbose );
}
////////////////////////////////////////////////////////////////////////

11
src/aig/saig/saigAbs.c
View File

@ -24,6 +24,7 @@
#include "satSolver.h"
#include "satStore.h"
#include "ssw.h"
#include "ioa.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@ -681,7 +682,7 @@ Ssw_Cex_t * Saig_ManCexShrink( Aig_Man_t * p, Aig_Man_t * pAbs, Ssw_Cex_t * pCex
}
return pCex;
}
/**Function*************************************************************
Synopsis [Performs proof-based abstraction using BMC of the given depth.]
@ -859,6 +860,7 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
printf( "Refining abstraction...\n" );
for ( Iter = 0; ; Iter++ )
{
char FileName[100];
pTemp = Saig_ManProofRefine( p, pResult, vFlops, nFramesBmc, nConfMaxBmc, fVerbose );
if ( pTemp == NULL )
break;
@ -869,9 +871,16 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
Aig_ManPrintStats( pResult );
else
printf( " -----------------------------------------------------\n" );
// output the intermediate result of abstraction
sprintf( FileName, "gabs%02d.aig", Iter );
Ioa_WriteAiger( pResult, FileName, 0, 0 );
printf( "Intermediate abstracted model was written into file \"%s\".\n", FileName );
// check if the ratio is reached
if ( 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pTemp))/Aig_ManRegNum(p) < 1.0*nRatio )
{
printf( "Refinements is stopped because flop reduction is less than %d%%\n", nRatio );
Aig_ManStop( pResult );
pResult = NULL;
break;
}
}

4
src/aig/saig/saigBmc.c
View File

@ -87,7 +87,7 @@ Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nFramesMax, int nNodesMax,
Saig_Bmc_t * p;
Aig_Obj_t * pObj;
int i, Lit;
assert( Aig_ManRegNum(pAig) > 0 );
// assert( Aig_ManRegNum(pAig) > 0 );
p = (Saig_Bmc_t *)ABC_ALLOC( char, sizeof(Saig_Bmc_t) );
memset( p, 0, sizeof(Saig_Bmc_t) );
// set parameters
@ -589,7 +589,7 @@ void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConf
Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
printf( "Params: FramesMax = %d. NodesDelta = %d. ConfMaxOne = %d. ConfMaxAll = %d.\n",
nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll );
}
}
for ( Iter = 0; ; Iter++ )
{
clk2 = clock();

6
src/aig/saig/saigBmc2.c
View File

@ -162,6 +162,8 @@ Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax
return pFrames;
}
#include "utilMem.h"
/**Function*************************************************************
Synopsis [Performs BMC for the given AIG.]
@ -228,6 +230,8 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
// create the SAT solver
clk = clock();
pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) );
//if ( s_fInterrupt )
//return -1;
pSat = sat_solver_new();
sat_solver_setnvars( pSat, pCnf->nVars );
for ( i = 0; i < pCnf->nClauses; i++ )
@ -255,6 +259,8 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
int clkPart = clock();
Aig_ManForEachPo( pFrames, pObj, i )
{
//if ( s_fInterrupt )
//return -1;
Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
if ( fVerbose )
{

2
src/aig/saig/saigSimExt.c
View File

@ -251,7 +251,7 @@ Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstPi, Ssw_Cex_t
{
Vec_Int_t * vRes, * vResInv, * vUndo, * vVis, * vVis2;
int i, f, Value;
assert( Aig_ManRegNum(p) > 0 );
// assert( Aig_ManRegNum(p) > 0 );
assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Aig_BitWordNum(2*(pCex->iFrame+1)) );
// start simulation data
Value = Saig_ManSimDataInit( p, pCex, vSimInfo, NULL );

4
src/aig/ssw/sswSim.c
View File

@ -1280,11 +1280,11 @@ void Ssw_SmlFreeCounterExample( Ssw_Cex_t * pCex )
***********************************************************************/
int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p )
{
{
Ssw_Sml_t * pSml;
Aig_Obj_t * pObj;
int RetValue, i, k, iBit;
assert( Aig_ManRegNum(pAig) > 0 );
// assert( Aig_ManRegNum(pAig) > 0 );
assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) );
// start a new sequential simulator
pSml = Ssw_SmlStart( pAig, 0, p->iFrame+1, 1 );

2
src/base/abc/abcNtk.c
View File

@ -1334,7 +1334,7 @@ Abc_Ntk_t * Abc_NtkTrim( Abc_Ntk_t * pNtk )
// filter POs
k = m = 0;
Abc_NtkForEachCo( pNtk, pObj, i )
{
{
if ( Abc_ObjIsPo(pObj) )
{
// remove constant nodes and PI pointers

333
src/base/abci/abc.c
View File

@ -153,6 +153,7 @@ static int Abc_CommandIFraig ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandDFraig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCSweep ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDProve2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbSec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSimSec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMatch ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -311,6 +312,7 @@ static int Abc_CommandAbc9Force ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandAbc9Embed ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9If ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Era ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Dch ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbcTestNew ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -543,6 +545,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Verification", "sec", Abc_CommandSec, 0 );
Cmd_CommandAdd( pAbc, "Verification", "dsec", Abc_CommandDSec, 0 );
Cmd_CommandAdd( pAbc, "Verification", "dprove", Abc_CommandDProve, 0 );
Cmd_CommandAdd( pAbc, "Verification", "dprove2", Abc_CommandDProve2, 0 );
Cmd_CommandAdd( pAbc, "Verification", "absec", Abc_CommandAbSec, 0 );
Cmd_CommandAdd( pAbc, "Verification", "simsec", Abc_CommandSimSec, 0 );
Cmd_CommandAdd( pAbc, "Verification", "match", Abc_CommandMatch, 0 );
@ -631,6 +634,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "AIG", "&embed", Abc_CommandAbc9Embed, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&if", Abc_CommandAbc9If, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&era", Abc_CommandAbc9Era, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&dch", Abc_CommandAbc9Dch, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&test", Abc_CommandAbc9Test, 0 );
Cmd_CommandAdd( pAbc, "Various", "testnew", Abc_CommandAbcTestNew, 0 );
@ -672,6 +676,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
void For_ManFileExperiment();
// For_ManFileExperiment();
}
{
}
}
@ -5437,7 +5443,7 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pNtkRes == NULL )
{
fprintf( pErr, "Miter computation has failed.\n" );
return 1;
return 0;
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
@ -6539,23 +6545,24 @@ int Abc_CommandReach( Abc_Frame_t * pAbc, int argc, char ** argv )
int nIterMax;
int fPartition;
int fReorder;
int fReorderImage;
int fVerbose;
int c;
extern void Abc_NtkVerifyUsingBdds( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
extern void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
extern void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
nBddMax = 50000;
nIterMax = 1000;
fPartition = 1;
fReorder = 1;
fVerbose = 0;
nBddMax = 50000;
nIterMax = 1000;
fPartition = 1;
fReorder = 1;
fReorderImage = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "BFprvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "BFprovh" ) ) != EOF )
{
switch ( c )
{
@ -6587,6 +6594,9 @@ int Abc_CommandReach( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'r':
fReorder ^= 1;
break;
case 'o':
fReorderImage ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -6626,16 +6636,17 @@ int Abc_CommandReach( Abc_Frame_t * pAbc, int argc, char ** argv )
}
*/
// Abc_NtkVerifyUsingBdds( pNtk, nBddMax, nIterMax, fPartition, fReorder, fVerbose );
Abc_NtkDarReach( pNtk, nBddMax, nIterMax, fPartition, fReorder, fVerbose );
Abc_NtkDarReach( pNtk, nBddMax, nIterMax, fPartition, fReorder, fReorderImage, fVerbose );
return 0;
usage:
fprintf( pErr, "usage: reach [-BF num] [-prvh]\n" );
fprintf( pErr, "usage: reach [-BF num] [-provh]\n" );
fprintf( pErr, "\t verifies sequential miter using BDD-based reachability\n" );
fprintf( pErr, "\t-B num : max number of nodes in the intermediate BDDs [default = %d]\n", nBddMax );
fprintf( pErr, "\t-F num : max number of reachability iterations [default = %d]\n", nIterMax );
fprintf( pErr, "\t-p : enable partitioned image computation [default = %s]\n", fPartition? "yes": "no" );
fprintf( pErr, "\t-r : enable dynamic BDD variable reordering [default = %s]\n", fReorder? "yes": "no" );
fprintf( pErr, "\t-o : toggles BDD variable reordering during image computation [default = %s]\n", fReorderImage? "yes": "no" );
fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
@ -9554,7 +9565,6 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
int c;
extern Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars );
pNtk = Abc_FrameReadNtk(pAbc);
@ -9564,7 +9574,7 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
Dch_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptgcvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptgcfvh" ) ) != EOF )
{
switch ( c )
{
@ -9616,6 +9626,9 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'c':
pPars->fUseCSat ^= 1;
break;
case 'f':
pPars->fLightSynth ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
@ -9646,7 +9659,7 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: dch [-WCS num] [-sptgcvh]\n" );
fprintf( pErr, "usage: dch [-WCS num] [-sptgcfvh]\n" );
fprintf( pErr, "\t computes structural choices using a new approach\n" );
fprintf( pErr, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords );
fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
@ -9656,6 +9669,7 @@ usage:
fprintf( pErr, "\t-t : toggle simulation of the TFO classes [default = %s]\n", pPars->fSimulateTfo? "yes": "no" );
fprintf( pErr, "\t-g : toggle using GIA to prove equivalences [default = %s]\n", pPars->fUseGia? "yes": "no" );
fprintf( pErr, "\t-c : toggle using circuit-based SAT vs. MiniSat [default = %s]\n", pPars->fUseCSat? "yes": "no" );
fprintf( pErr, "\t-f : toggle using faster logic synthesis [default = %s]\n", pPars->fLightSynth? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
@ -16581,7 +16595,7 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Fra_SecSetDefaultParams( pSecPar );
// pSecPar->TimeLimit = 300;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "cbFCGDVBRarmfijwvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "cbFCGDVBRarmfijkouwvh" ) ) != EOF )
{
switch ( c )
{
@ -16686,6 +16700,15 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'j':
pSecPar->fInterpolation ^= 1;
break;
case 'k':
pSecPar->fInterSeparate ^= 1;
break;
case 'o':
pSecPar->fReorderImage ^= 1;
break;
case 'u':
pSecPar->fReadUnsolved ^= 1;
break;
case 'w':
pSecPar->fVeryVerbose ^= 1;
break;
@ -16712,12 +16735,21 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_NtkDarProve( pNtk, pSecPar );
pAbc->pCex = pNtk->pSeqModel; // temporary ???
// Fra_SmlWriteCounterExample( stdout, Aig_Man_t * pAig, Fra_Cex_t * p )
// read back the resulting unsolved reduced sequential miter
if ( pSecPar->fReadUnsolved && pSecPar->nSMnumber >= 0 )
{
char FileName[100];
sprintf( FileName, "sm%02d.aig", pSecPar->nSMnumber );
pNtk = Io_Read( FileName, Io_ReadFileType(FileName), 1 );
if ( pNtk == NULL )
printf( "Cannot read back unsolved reduced sequential miter \"%s\",\n", FileName );
else
Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
}
return 0;
usage:
fprintf( pErr, "usage: dprove [-FCGDVBR num] [-cbarmfijwvh]\n" );
fprintf( pErr, "usage: dprove [-FCGDVBR num] [-cbarmfijouwvh]\n" );
fprintf( pErr, "\t performs SEC on the sequential miter\n" );
fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", pSecPar->nFramesMax );
fprintf( pErr, "\t-C num : the conflict limit at a node during induction [default = %d]\n", pSecPar->nBTLimit );
@ -16734,11 +16766,105 @@ usage:
fprintf( pErr, "\t-f : toggles the internal use of fraiging [default = %s]\n", pSecPar->fFraiging? "yes": "no" );
fprintf( pErr, "\t-i : toggles the use of induction [default = %s]\n", pSecPar->fInduction? "yes": "no" );
fprintf( pErr, "\t-j : toggles the use of interpolation [default = %s]\n", pSecPar->fInterpolation? "yes": "no" );
// fprintf( pErr, "\t-n : toggles the use of different induction prover [default = %s]\n", pSecPar->fUseNewProver? "yes": "no" );
fprintf( pErr, "\t-k : toggles applying interpolation to each output [default = %s]\n", pSecPar->fInterSeparate? "yes": "no" );
fprintf( pErr, "\t-o : toggles using BDD variable reordering during image computation [default = %s]\n", pSecPar->fReorderImage? "yes": "no" );
fprintf( pErr, "\t-u : toggles reading back unsolved reduced sequential miter [default = %s]\n", pSecPar->fReadUnsolved? "yes": "no" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", pSecPar->fVerbose? "yes": "no" );
fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", pSecPar->fVeryVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandDProve2( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
int nConfLast;
int fSeparate;
int fVeryVerbose;
int fVerbose;
int c;
extern int Abc_NtkDProve2( Abc_Ntk_t * pNtk, int nConfLast, int fSeparate, int fVeryVerbose, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
nConfLast = 75000;
fSeparate = 0;
fVeryVerbose = 0;
fVerbose = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Ckwvh" ) ) != EOF )
{
switch ( c )
{
case 'C':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
nConfLast = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nConfLast < 0 )
goto usage;
break;
case 'k':
fSeparate ^= 1;
break;
case 'w':
fVeryVerbose ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
printf( "This command works only for structrally hashed networks. Run \"st\".\n" );
return 0;
}
if ( Abc_NtkLatchNum(pNtk) == 0 )
{
printf( "This command works only for sequential networks.\n" );
return 0;
}
// perform verification
Abc_NtkDProve2( pNtk, nConfLast, fSeparate, fVeryVerbose, fVerbose );
return 0;
usage:
fprintf( pErr, "usage: dprove2 [-C num] [-kwvh]\n" );
fprintf( pErr, "\t improved integrated solver of sequential miters\n" );
fprintf( pErr, "\t-C num : the conflict limit during final BMC [default = %d]\n", nConfLast );
fprintf( pErr, "\t-k : toggles solving each output separately [default = %s]\n", fSeparate? "yes": "no" );
fprintf( pErr, "\t-w : toggles very verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
@ -18098,7 +18224,7 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
Inter_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "CNFrtpomcgbvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "CNFrtpomcgbkvh" ) ) != EOF )
{
switch ( c )
{
@ -18159,6 +18285,9 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'b':
pPars->fUseBackward ^= 1;
break;
case 'k':
pPars->fUseSeparate ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
@ -18174,7 +18303,7 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
{
fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
return 0;
}
@ -18185,10 +18314,29 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( Abc_NtkPoNum(pNtk) != 1 )
{
fprintf( stdout, "Currently only works for single-output miters (run \"orpos\").\n" );
return 0;
if ( pPars->fUseSeparate )
{
printf( "Each of %d outputs will be solved separately.\n", Abc_NtkPoNum(pNtk) );
Abc_NtkDarBmcInter( pNtk, pPars );
}
else
{
Abc_Ntk_t * pNtkNew = Abc_NtkDup( pNtk );
printf( "All %d outputs will be ORed together.\n", Abc_NtkPoNum(pNtk) );
if ( !Abc_NtkCombinePos( pNtkNew, 0 ) )
{
Abc_NtkDelete( pNtkNew );
printf( "ORing outputs has failed.\n" );
return 0;
}
Abc_NtkDarBmcInter( pNtkNew, pPars );
Abc_NtkDelete( pNtkNew );
}
}
else
{
Abc_NtkDarBmcInter( pNtk, pPars );
}
Abc_NtkDarBmcInter( pNtk, pPars );
return 0;
usage:
@ -18205,6 +18353,7 @@ usage:
fprintf( pErr, "\t-c : toggle using inductive containment check [default = %s]\n", pPars->fCheckKstep? "yes": "no" );
fprintf( pErr, "\t-g : toggle using bias for global variables using SAT [default = %s]\n", pPars->fUseBias? "yes": "no" );
fprintf( pErr, "\t-b : toggle using backward interpolation [default = %s]\n", pPars->fUseBackward? "yes": "no" );
fprintf( pErr, "\t-k : toggle solving each output separately [default = %s]\n", pPars->fUseSeparate? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
@ -18585,7 +18734,7 @@ int Abc_CommandInduction( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: ind [-FC num] [-vh]\n" );
fprintf( pErr, "\t runs K-step induction for the property output\n" );
fprintf( pErr, "\t runs the inductive case of the K-step induction\n" );
fprintf( pErr, "\t-F num : the max number of timeframes [default = %d]\n", nFramesMax );
fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver [default = %d]\n", nConfMax );
fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
@ -19959,7 +20108,7 @@ int Abc_CommandAbc8Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
Dch_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptfvh" ) ) != EOF )
{
switch ( c )
{
@ -20005,6 +20154,9 @@ int Abc_CommandAbc8Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
case 't':
pPars->fSimulateTfo ^= 1;
break;
case 'f':
pPars->fLightSynth ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
@ -20027,12 +20179,12 @@ int Abc_CommandAbc8Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "Abc_CommandAbc8Dch(): Tranformation of the AIG has failed.\n" );
return 1;
}
Aig_ManStop( pAbc->pAbc8Aig );
// Aig_ManStop( pAbc->pAbc8Aig );
pAbc->pAbc8Aig = pAigNew;
return 0;
usage:
fprintf( stdout, "usage: *dch [-WCS num] [-sptvh]\n" );
fprintf( stdout, "usage: *dch [-WCS num] [-sptfvh]\n" );
fprintf( stdout, "\t computes structural choices using a new approach\n" );
fprintf( stdout, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords );
fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
@ -20040,6 +20192,7 @@ usage:
fprintf( stdout, "\t-s : toggle synthesizing three snapshots [default = %s]\n", pPars->fSynthesis? "yes": "no" );
fprintf( stdout, "\t-p : toggle power-aware rewriting [default = %s]\n", pPars->fPower? "yes": "no" );
fprintf( stdout, "\t-t : toggle simulation of the TFO classes [default = %s]\n", pPars->fSimulateTfo? "yes": "no" );
fprintf( stdout, "\t-f : toggle using lighter logic synthesis [default = %s]\n", pPars->fLightSynth? "yes": "no" );
fprintf( stdout, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
return 1;
@ -20973,7 +21126,7 @@ int Abc_CommandAbc8Scl( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) )
{
fprintf( stdout, "Abc_CommandAbc8Scl(): The network is combinational (run \"*fraig\").\n" );
fprintf( stdout, "Abc_CommandAbc8Scl(): The network is combinational.\n" );
return 0;
}
@ -21092,7 +21245,7 @@ int Abc_CommandAbc8Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) )
{
fprintf( stdout, "Abc_CommandAbc8Lcorr(): The network is combinational (run \"*fraig\").\n" );
fprintf( stdout, "Abc_CommandAbc8Lcorr(): The network is combinational.\n" );
return 0;
}
@ -21285,7 +21438,7 @@ int Abc_CommandAbc8Ssw( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) )
{
fprintf( stdout, "The network is combinational (run \"*fraig\").\n" );
fprintf( stdout, "The network is combinational.\n" );
return 0;
}
@ -21518,7 +21671,7 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) )
{
fprintf( stdout, "The network is combinational (run \"*fraig\").\n" );
fprintf( stdout, "The network is combinational.\n" );
return 0;
}
@ -23890,7 +24043,7 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
int fCSat = 0;
Cec_ManSatSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "CSNnmfcvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "CSNnmftcvh" ) ) != EOF )
{
switch ( c )
{
@ -23936,6 +24089,9 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'f':
pPars->fFirstStop ^= 1;
break;
case 't':
pPars->fLearnCls ^= 1;
break;
case 'c':
fCSat ^= 1;
break;
@ -23955,7 +24111,9 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Vec_Int_t * vCounters;
Vec_Str_t * vStatus;
if ( pPars->fNonChrono )
if ( pPars->fLearnCls )
vCounters = Tas_ManSolveMiterNc( pAbc->pAig, pPars->nBTLimit, &vStatus, pPars->fVerbose );
else if ( pPars->fNonChrono )
vCounters = Cbs_ManSolveMiterNc( pAbc->pAig, pPars->nBTLimit, &vStatus, pPars->fVerbose );
else
vCounters = Cbs_ManSolveMiter( pAbc->pAig, pPars->nBTLimit, &vStatus, pPars->fVerbose );
@ -23970,7 +24128,7 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( stdout, "usage: &sat [-CSN <num>] [-nmfcvh]\n" );
fprintf( stdout, "usage: &sat [-CSN <num>] [-nmfctvh]\n" );
fprintf( stdout, "\t performs SAT solving for the combinational outputs\n" );
fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
fprintf( stdout, "\t-S num : the min number of variables to recycle the solver [default = %d]\n", pPars->nSatVarMax );
@ -23979,6 +24137,7 @@ usage:
fprintf( stdout, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "yes": "no" );
fprintf( stdout, "\t-f : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" );
fprintf( stdout, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", fCSat? "yes": "no" );
fprintf( stdout, "\t-t : toggle using learning in curcuit-based solver [default = %s]\n", pPars->fLearnCls? "yes": "no" );
fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
return 1;
@ -24139,18 +24298,23 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
{
char * pFileName = "gsrm.aig";
Gia_Man_t * pTemp;
char * pFileName = "gsrm.aig";
char * pFileName2 = "gsyn.aig";
Gia_Man_t * pTemp, * pAux;
int c, fVerbose = 0;
int fSynthesis = 0;
int fDualOut = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "dvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "dsvh" ) ) != EOF )
{
switch ( c )
{
case 'd':
fDualOut ^= 1;
break;
case 's':
fSynthesis ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -24165,22 +24329,38 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "Abc_CommandAbc9Srm(): There is no AIG.\n" );
return 1;
}
// pAbc->pAig = Gia_ManSpecReduce( pTemp = pAbc->pAig, fDualOut );
// Gia_ManStop( pTemp );
pTemp = Gia_ManSpecReduce( pAbc->pAig, fDualOut, fVerbose );
if ( pTemp )
{
pTemp = Gia_ManSeqStructSweep( pAux = pTemp, 1, 1, 0 );
Gia_ManStop( pAux );
Gia_WriteAiger( pTemp, pFileName, 0, 0 );
printf( "Speculatively reduced model was written into file \"%s\".\n", pFileName );
Gia_ManPrintStatsShort( pTemp );
Gia_ManStop( pTemp );
}
if ( fSynthesis )
{
pTemp = Gia_ManEquivReduce( pAbc->pAig, 1, fDualOut, fVerbose );
if ( pTemp )
{
pTemp = Gia_ManSeqStructSweep( pAux = pTemp, 1, 1, 0 );
Gia_ManStop( pAux );
Gia_WriteAiger( pTemp, pFileName2, 0, 0 );
printf( "Reduced original network was written into file \"%s\".\n", pFileName2 );
Gia_ManPrintStatsShort( pTemp );
Gia_ManStop( pTemp );
}
}
return 0;
usage:
fprintf( stdout, "usage: &srm [-dvh]\n" );
fprintf( stdout, "usage: &srm [-dsvh]\n" );
fprintf( stdout, "\t writes speculatively reduced model into file \"%s\"\n", pFileName );
fprintf( stdout, "\t-d : toggle creating dual output miter [default = %s]\n", fDualOut? "yes": "no" );
fprintf( stdout, "\t-s : toggle writing reduced network for synthesis [default = %s]\n", fSynthesis? "yes": "no" );
fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
return 1;
@ -24765,7 +24945,7 @@ int Abc_CommandAbc9Era( Abc_Frame_t * pAbc, int argc, char ** argv )
Gia_Man_t * pTemp = NULL;
int c, fVerbose = 0;
int fMiter = 0;
int nStatesMax = 1000000;
int nStatesMax = 10000000;
extern void Gia_ManCollectReachable( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbose );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Smvh" ) ) != EOF )
@ -24823,6 +25003,75 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
{
// extern void Hcd_ComputeChoicesTest( Gia_Man_t * pAig, int nBTLimit, int fSynthesis, int fUseMiniSat, int fVerbose );
Gia_Man_t * pTemp = NULL;
int nBTLimit = 100;
int fSynthesis = 1;
int fUseMiniSat = 0;
int c, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Csmvh" ) ) != EOF )
{
switch ( c )
{
case 'C':
if ( globalUtilOptind >= argc )
{
fprintf( stdout, "Command line switch \"-C\" should be followed by a positive integer.\n" );
goto usage;
}
nBTLimit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nBTLimit < 0 )
goto usage;
break;
case 's':
fSynthesis ^= 1;
break;
case 'm':
fUseMiniSat ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pAig == NULL )
{
printf( "Abc_CommandAbc9Test(): There is no AIG.\n" );
return 1;
}
// Hcd_ComputeChoicesTest( pAbc->pAig, nBTLimit, fSynthesis, fUseMiniSat, fVerbose );
return 0;
usage:
fprintf( stdout, "usage: &dch [-C num] [-smvh]\n" );
fprintf( stdout, "\t computing choices using the latest algorithm\n" );
fprintf( stdout, "\t-C num : the max number of states to traverse (num > 0) [default = %d]\n", nBTLimit );
fprintf( stdout, "\t-s : toggle printing verbose information [default = %s]\n", fSynthesis? "yes": "no" );
fprintf( stdout, "\t-m : toggle using MiniSat as a SAT solver [default = %s]\n", fUseMiniSat? "yes": "no" );
fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []

185
src/base/abci/abcDar.c
View File

@ -895,45 +895,37 @@ Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, in
***********************************************************************/
Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars )
{
extern Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose );
extern Aig_Man_t * Cec_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars );
extern Gia_Man_t * Dar_NewChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose );
extern Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars );
Vec_Ptr_t * vAigs;
Aig_Man_t * pMan, * pTemp;
Abc_Ntk_t * pNtkAig;
int i, clk;
Gia_Man_t * pGia;
int clk;
assert( Abc_NtkIsStrash(pNtk) );
pMan = Abc_NtkToDar( pNtk, 0, 0 );
if ( pMan == NULL )
return NULL;
clk = clock();
if ( pPars->fSynthesis )
{
// vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, pPars->fPower, pPars->fVerbose );
vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, pPars->fPower, 0 );
Aig_ManStop( pMan );
// swap around the first and the last
pTemp = Vec_PtrPop( vAigs );
Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
Vec_PtrWriteEntry( vAigs, 0, pTemp );
}
pGia = Dar_NewChoiceSynthesis( pMan, 1, 1, pPars->fPower, 0 );
else
{
vAigs = Vec_PtrAlloc( 1 );
Vec_PtrPush( vAigs, pMan );
pGia = Gia_ManFromAig( pMan );
Aig_ManStop( pMan );
}
pPars->timeSynth = clock() - clk;
if ( pPars->fUseGia )
pMan = Cec_ComputeChoices( vAigs, pPars );
pMan = Cec_ComputeChoices( pGia, pPars );
else
pMan = Dch_ComputeChoices( vAigs, pPars );
pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
// pNtkAig = Abc_NtkFromDar( pNtk, pMan );
Aig_ManStop( pMan );
// cleanup
Vec_PtrForEachEntry( vAigs, pTemp, i )
{
pMan = Gia_ManToAigSkip( pGia, 3 );
Gia_ManStop( pGia );
pMan = Dch_ComputeChoices( pTemp = pMan, pPars );
Aig_ManStop( pTemp );
Vec_PtrFree( vAigs );
}
pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
Aig_ManStop( pMan );
return pNtkAig;
}
@ -1535,6 +1527,18 @@ Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, in
return pNtkAig;
}
/*
#include <signal.h>
#include "utilMem.h"
static void sigfunc( int signo )
{
if (signo == SIGINT) {
printf("SIGINT received!\n");
s_fInterrupt = 1;
}
}
*/
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
@ -1550,6 +1554,19 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta,
{
Aig_Man_t * pMan;
int status, RetValue = -1, clk = clock();
/*
s_fInterrupt = 0;
if ( signal(SIGINT,sigfunc) == SIG_ERR )
{
printf("Could not setup signal handler for SIGINT!\n");
return RetValue;
}
printf("Waiting for SIGINT. Press Ctrl+C to exit.\n");
// while ( !s_fInterrupt );
// return RetValue;
*/
// derive the AIG manager
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
@ -1572,8 +1589,12 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta,
printf( "No output was asserted in %d frames. Reached conflict limit (%d). ", iFrame, nBTLimit );
else // if ( RetValue == 0 )
{
extern void Aig_ManCounterExampleValueTest( Aig_Man_t * pAig, Fra_Cex_t * pCex );
Fra_Cex_t * pCex = pNtk->pSeqModel;
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
Aig_ManCounterExampleValueTest( pMan, pCex );
}
}
else
@ -1628,6 +1649,92 @@ ABC_PRT( "Time", clock() - clk );
return RetValue;
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars )
{
int RetValue, iFrame, clk = clock();
assert( pMan->nRegs > 0 );
if ( pPars->fUseSeparate )
{
Aig_Man_t * pTemp, * pAux;
Aig_Obj_t * pObjPo;
int i, Counter = 0;
Saig_ManForEachPo( pMan, pObjPo, i )
{
if ( Aig_ObjFanin0(pObjPo) == Aig_ManConst1(pMan) )
continue;
pTemp = Aig_ManDupOneOutput( pMan, i, 1 );
pTemp = Aig_ManScl( pAux = pTemp, 1, 1, 0 );
Aig_ManStop( pAux );
if ( Aig_ObjFanin0(pObjPo) == Aig_ManConst1(pMan) )
{
Aig_ManStop( pTemp );
continue;
}
RetValue = Inter_ManPerformInterpolation( pTemp, pPars, &iFrame );
if ( pTemp->pSeqModel )
{
Ssw_Cex_t * pCex;
pCex = pMan->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
pCex->iPo = i;
Aig_ManStop( pTemp );
break;
}
// if solved, remove the output
if ( RetValue == 1 )
{
Aig_ObjPatchFanin0( pMan, pObjPo, Aig_ManConst0(pMan) );
// printf( "Output %3d : Solved ", i );
}
else
{
Counter++;
// printf( "Output %3d : Undec ", i );
}
// Aig_ManPrintStats( pTemp );
Aig_ManStop( pTemp );
printf( "Solving output %3d (out of %3d) using interpolation.\r", i, Saig_ManPoNum(pMan) );
}
Aig_ManCleanup( pMan );
if ( pMan->pSeqModel == NULL )
{
printf( "Interpolation left %d (out of %d) outputs unsolved \n", Counter, Saig_ManPoNum(pMan) );
if ( Counter )
RetValue = -1;
}
/*
pMan = Aig_ManDupUnsolvedOutputs( pTemp = pMan, 1 );
Aig_ManStop( pTemp );
pMan = Aig_ManScl( pTemp = pMan, 1, 1, 0 );
Aig_ManStop( pTemp );
*/
}
else
{
RetValue = Inter_ManPerformInterpolation( pMan, pPars, &iFrame );
}
if ( RetValue == 1 )
printf( "Property proved. " );
else if ( RetValue == 0 )
printf( "Property DISPROVED in frame %d (use \"write_counter\" to dump a witness). ", iFrame );
else if ( RetValue == -1 )
printf( "Property UNDECIDED. " );
else
assert( 0 );
ABC_PRT( "Time", clock() - clk );
return RetValue;
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
@ -1642,30 +1749,16 @@ ABC_PRT( "Time", clock() - clk );
int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars )
{
Aig_Man_t * pMan;
int RetValue, iFrame, clk = clock();
// derive the AIG manager
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
{
printf( "Converting miter into AIG has failed.\n" );
return -1;
}
assert( pMan->nRegs > 0 );
RetValue = Inter_ManPerformInterpolation( pMan, pPars, &iFrame );
if ( RetValue == 1 )
printf( "Property proved. " );
else if ( RetValue == 0 )
{
printf( "Property DISPROVED in frame %d (use \"write_counter\" to dump a witness). ", iFrame );
ABC_FREE( pNtk->pModel );
ABC_FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
}
else if ( RetValue == -1 )
printf( "Property UNDECIDED. " );
else
assert( 0 );
ABC_PRT( "Time", clock() - clk );
Abc_NtkDarBmcInter_int( pMan, pPars );
ABC_FREE( pNtk->pModel );
ABC_FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
Aig_ManStop( pMan );
return 1;
}
@ -2411,7 +2504,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
else
{
RetValue = 0;
printf( "Simulation of %d frames with %d words did not assert the outputs. ",
printf( "Simulation of %d frames with %d words did not assert the outputs. ",
nFrames, nWords );
}
Gia_ManStop( pGia );
@ -2439,7 +2532,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
else
{
RetValue = 0;
printf( "Simulation of %d frames with %d words did not assert the outputs. ",
printf( "Simulation of %d frames with %d words did not assert the outputs. ",
nFrames, nWords );
}
Fra_SmlStop( pSml );
@ -3187,14 +3280,14 @@ Abc_Ntk_t * Abc_NtkDarCleanupAig( Abc_Ntk_t * pNtk, int fCleanupPis, int fCleanu
SeeAlso []
***********************************************************************/
void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose )
void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose )
{
extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent );
extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent );
Aig_Man_t * pMan;
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
return;
Aig_ManVerifyUsingBdds( pMan, nBddMax, nIterMax, fPartition, fReorder, fVerbose, 0 );
Aig_ManVerifyUsingBdds( pMan, nBddMax, nIterMax, fPartition, fReorder, fReorderImage, fVerbose, 0 );
ABC_FREE( pNtk->pModel );
ABC_FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;

6
src/base/abci/abcTiming.c
View File

@ -157,7 +157,7 @@ void Abc_NtkTimeSetDefaultRequired( Abc_Ntk_t * pNtk, float Rise, float Fall )
if ( pNtk->pManTime == NULL )
pNtk->pManTime = Abc_ManTimeStart();
pNtk->pManTime->tReqDef.Rise = Rise;
pNtk->pManTime->tReqDef.Rise = Fall;
pNtk->pManTime->tReqDef.Fall = Fall;
pNtk->pManTime->tReqDef.Worst = ABC_MAX( Rise, Fall );
}
@ -185,7 +185,7 @@ void Abc_NtkTimeSetArrival( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall
vTimes = pNtk->pManTime->vArrs;
pTime = vTimes->pArray[ObjId];
pTime->Rise = Rise;
pTime->Fall = Rise;
pTime->Fall = Fall;
pTime->Worst = ABC_MAX( Rise, Fall );
}
@ -213,7 +213,7 @@ void Abc_NtkTimeSetRequired( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall
vTimes = pNtk->pManTime->vReqs;
pTime = vTimes->pArray[ObjId];
pTime->Rise = Rise;
pTime->Fall = Rise;
pTime->Fall = Fall;
pTime->Worst = ABC_MAX( Rise, Fall );
}

1
src/base/abci/module.make
View File

@ -12,6 +12,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcDar.c \
src/base/abci/abcDebug.c \
src/base/abci/abcDelay.c \
src/base/abci/abcDprove2.c \
src/base/abci/abcDress.c \
src/base/abci/abcDsd.c \
src/base/abci/abcExtract.c \

3
src/base/io/ioWriteBlif.c
View File

@ -579,7 +579,8 @@ void Io_WriteTimingInfo( FILE * pFile, Abc_Ntk_t * pNtk )
pTime = Abc_NodeReadArrival(pNode);
if ( pTime->Rise == pTimeDef->Rise && pTime->Fall == pTimeDef->Fall )
continue;
fprintf( pFile, ".input_arrival %s %g %g\n", Abc_ObjName(pNode), pTime->Rise, pTime->Fall );
// fprintf( pFile, ".input_arrival %s %g %g\n", Abc_ObjName(pNode), pTime->Rise, pTime->Fall );
fprintf( pFile, ".input_arrival %s %g %g\n", Abc_ObjName(Abc_ObjFanout0(pNode)), pTime->Rise, pTime->Fall );
}
}

131
src/base/main/main.c
View File

@ -23,10 +23,12 @@
// this line should be included in the library project
//#define ABC_LIB
//#define ABC_USE_BINARY 1
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static int TypeCheck( Abc_Frame_t * pAbc, char * s);
////////////////////////////////////////////////////////////////////////
@ -46,7 +48,11 @@ static int TypeCheck( Abc_Frame_t * pAbc, char * s);
SeeAlso []
***********************************************************************/
#if defined(ABC_USE_BINARY)
int main_( int argc, char * argv[] )
#else
int main( int argc, char * argv[] )
#endif
{
Abc_Frame_t * pAbc;
char sCommandUsr[500], sCommandTmp[100], sReadCmd[20], sWriteCmd[20], c;
@ -67,7 +73,7 @@ int main( int argc, char * argv[] )
pAbc = Abc_FrameGetGlobalFrame();
// default options
fBatch = 0;
fBatch = 0;
fInitSource = 1;
fInitRead = 0;
fFinalWrite = 0;
@ -313,127 +319,6 @@ static int TypeCheck( Abc_Frame_t * pAbc, char * s )
/**Function*************************************************************
Synopsis [Find the file name.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Abc_MainFileName( char * pFileName )
{
static char Buffer[200];
char * pExtension;
assert( strlen(pFileName) < 190 );
pExtension = Extra_FileNameExtension( pFileName );
if ( pExtension == NULL )
sprintf( Buffer, "%s.opt", pFileName );
else
{
strncpy( Buffer, pFileName, pExtension-pFileName-1 );
sprintf( Buffer+(pExtension-pFileName-1), ".opt.%s", pExtension );
}
return Buffer;
}
/**Function*************************************************************
Synopsis [The main() procedure.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int main_( int argc, char * argv[] )
{
extern void Nwk_ManPrintStatsUpdate( void * p, void * pAig, void * pNtk,
int nRegInit, int nLutInit, int nLevInit, int Time );
char * pComs[20] =
{
/*00*/ "*r -am ",
/*01*/ "*w -abc 1.aig",
/*02*/ "*lcorr -nc",//; *ps",
/*03*/ "*scorr -nc",//; *ps",
/*04*/ "*dch; *if -K 4 -C 16 -F 3 -A 2; *sw -m",//; *ps",
/*05*/ "*dch; *if -K 4 -C 16 -F 3 -A 2; *sw -m",//; *ps",
/*06*/ "*w ",
/*07*/ "*w -abc 2.aig",
/*08*/ "miter -mc 1.aig 2.aig; sim -F 4 -W 4 -mv"
};
char Command[1000];
int i, nComs;
Abc_Frame_t * pAbc;
FILE * pFile;
int nRegInit, nLutInit, nLevInit;
int clkStart = clock();
// added to detect memory leaks:
#if defined(_DEBUG) && defined(_MSC_VER)
_CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF );
#endif
// check that the file is present
if ( argc != 2 )
{
printf( "Expecting one command argument (file name).\n" );
return 0;
}
pFile = fopen( argv[1], "r" );
if ( pFile == NULL )
{
printf( "Cannot open file \"%s\".\n", argv[1] );
return 0;
}
fclose( pFile );
// count the number of commands
for ( nComs = 0; nComs < 20; nComs++ )
if ( pComs[nComs] == NULL )
break;
// perform the commands
printf( "Reading design \"%s\"...\n", argv[1] );
pAbc = Abc_FrameGetGlobalFrame();
for ( i = 0; i < nComs; i++ )
{
if ( i == 0 )
sprintf( Command, "%s%s", pComs[i], argv[1] );
else if ( i == 6 )
sprintf( Command, "%s%s", pComs[i], Abc_MainFileName(argv[1]) );
else
sprintf( Command, "%s", pComs[i] );
if ( Cmd_CommandExecute( pAbc, Command ) )
{
printf( "Internal command %d failed.\n", i );
return 0;
}
if ( i == 0 )
{
extern int Nwk_ManStatsRegs( void * p );
extern int Nwk_ManStatsLuts( void * pNtk );
extern int Nwk_ManStatsLevs( void * pNtk );
nRegInit = Nwk_ManStatsRegs( pAbc->pAbc8Ntl );
nLutInit = Nwk_ManStatsLuts( pAbc->pAbc8Nwk );
nLevInit = Nwk_ManStatsLevs( pAbc->pAbc8Nwk );
}
if ( i >= 1 && i <= 5 )
Nwk_ManPrintStatsUpdate( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, pAbc->pAbc8Nwk,
nRegInit, nLutInit, nLevInit, clkStart );
}
Abc_Stop();
printf( "Writing optimized design \"%s\"...\n", Abc_MainFileName(argv[1]) );
ABC_PRT( "Total time", clock() - clkStart );
printf( "\n" );
return 0;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

60
src/base/main/mainFrame.c
View File

@ -28,6 +28,9 @@
static Abc_Frame_t * s_GlobalFrame = NULL;
extern void * Aig_ManDupSimple( void * p );
extern void Aig_ManStop( void * pAig );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@ -148,11 +151,16 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
if ( p->pManDec ) Dec_ManStop( p->pManDec );
if ( p->dd ) Extra_StopManager( p->dd );
if ( p->vStore ) Vec_PtrFree( p->vStore );
if ( p->pSave1 ) Aig_ManStop( p->pSave1 );
if ( p->pSave2 ) Aig_ManStop( p->pSave2 );
if ( p->pSave3 ) Aig_ManStop( p->pSave3 );
if ( p->pSave4 ) Aig_ManStop( p->pSave4 );
Abc_FrameDeleteAllNetworks( p );
ABC_FREE( p );
s_GlobalFrame = NULL;
}
/**Function*************************************************************
Synopsis []
@ -513,6 +521,58 @@ Abc_Frame_t * Abc_FrameReadGlobalFrame()
return s_GlobalFrame;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_FrameSetSave1( void * pAig )
{
Abc_Frame_t * pFrame = Abc_FrameGetGlobalFrame();
if ( pFrame->pSave1 )
Aig_ManStop( pFrame->pSave1 );
pFrame->pSave1 = pAig;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_FrameSetSave2( void * pAig )
{
Abc_Frame_t * pFrame = Abc_FrameGetGlobalFrame();
if ( pFrame->pSave2 )
Aig_ManStop( pFrame->pSave2 );
pFrame->pSave2 = pAig;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void * Abc_FrameReadSave1() { void * pAig = Abc_FrameGetGlobalFrame()->pSave1; Abc_FrameGetGlobalFrame()->pSave1 = NULL; return pAig; }
void * Abc_FrameReadSave2() { void * pAig = Abc_FrameGetGlobalFrame()->pSave2; Abc_FrameGetGlobalFrame()->pSave2 = NULL; return pAig; }
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

5
src/base/main/mainInt.h
View File

@ -82,6 +82,11 @@ struct Abc_Frame_t_
void * pAig;
void * pCex;
void * pSave1;
void * pSave2;
void * pSave3;
void * pSave4;
// the addition to keep the best Ntl that can be used to restore
void * pAbc8NtlBestDelay; // the best delay, Ntl
void * pAbc8NtlBestArea; // the best area

2
src/map/amap/amapRule.c
View File

@ -296,7 +296,7 @@ Kit_DsdPrint( stdout, pNtk );
{
assert( iNod > 1 );
pNod = Amap_LibNod( pLib, Amap_Lit2Var(iNod) );
assert( pNod->Type == AMAP_OBJ_MUX || pNod->nSuppSize == pGate->nPins );
// assert( pNod->Type == AMAP_OBJ_MUX || pNod->nSuppSize == pGate->nPins );
pSet = (Amap_Set_t *)Aig_MmFlexEntryFetch( pLib->pMemSet, sizeof(Amap_Set_t) );
memset( pSet, 0, sizeof(Amap_Set_t) );
pSet->iGate = pGate->Id;

4
src/map/if/ifMap.c
View File

@ -207,7 +207,9 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode, int fP
for ( pTemp = pObj->pEquiv; pTemp; pTemp = pTemp->pEquiv )
{
assert( pTemp->nRefs == 0 );
assert( p->pPars->fSeqMap || pTemp->pCutSet->nCuts > 0 );
// assert( p->pPars->fSeqMap || pTemp->pCutSet->nCuts > 0 ); // June 9, 2009
if ( pTemp->pCutSet->nCuts == 0 )
continue;
// go through the cuts of this node
If_ObjForEachCut( pTemp, pCutTemp, i )
{

25
src/map/mapper/mapperLib.c
View File

@ -174,15 +174,20 @@ int Map_SuperLibDeriveFromGenlib( Mio_Library_t * pLib )
{
Abc_Frame_t * pAbc = Abc_FrameGetGlobalFrame();
char * pNameGeneric;
char FileNameGenlib[100];
char FileNameSuper[100];
char CommandSuper[500];
char CommandRead[500];
char * FileNameGenlib;
char * FileNameSuper;
char * CommandSuper;
char * CommandRead;
FILE * pFile;
if ( pLib == NULL )
return 0;
FileNameGenlib = ABC_ALLOC( char, 10000 );
FileNameSuper = ABC_ALLOC( char, 10000 );
CommandSuper = ABC_ALLOC( char, 10000 );
CommandRead = ABC_ALLOC( char, 10000 );
// write the current library into the file
sprintf( FileNameGenlib, "%s_temp", Mio_LibraryReadName(pLib) );
pFile = fopen( FileNameGenlib, "w" );
@ -197,6 +202,10 @@ int Map_SuperLibDeriveFromGenlib( Mio_Library_t * pLib )
sprintf( CommandSuper, "super -l 1 -i 5 -d 10000000 -a 10000000 -t 100 %s", FileNameGenlib );
if ( Cmd_CommandExecute( pAbc, CommandSuper ) )
{
ABC_FREE( FileNameGenlib );
ABC_FREE( FileNameSuper );
ABC_FREE( CommandSuper );
ABC_FREE( CommandRead );
fprintf( stdout, "Cannot execute command \"%s\".\n", CommandSuper );
return 0;
}
@ -215,6 +224,10 @@ int Map_SuperLibDeriveFromGenlib( Mio_Library_t * pLib )
unlink( FileNameSuper );
#endif
fprintf( stdout, "Cannot execute command \"%s\".\n", CommandRead );
ABC_FREE( FileNameGenlib );
ABC_FREE( FileNameSuper );
ABC_FREE( CommandSuper );
ABC_FREE( CommandRead );
return 0;
}
@ -225,6 +238,10 @@ int Map_SuperLibDeriveFromGenlib( Mio_Library_t * pLib )
unlink( FileNameSuper );
#endif
*/
ABC_FREE( FileNameGenlib );
ABC_FREE( FileNameSuper );
ABC_FREE( CommandSuper );
ABC_FREE( CommandRead );
return 1;
}

16
src/map/super/superGate.c
View File

@ -67,8 +67,8 @@ struct Super_ManStruct_t_
int Time; // the runtime of the generation procedure
int TimeLimit; // the runtime limit (in seconds)
int TimeSec; // the time passed (in seconds)
int TimeStop; // the time to stop computation (in miliseconds)
int TimePrint; // the time to print message
double TimeStop; // the time to stop computation (in miliseconds)
double TimePrint; // the time to print message
};
struct Super_GateStruct_t_
@ -1107,10 +1107,12 @@ void Super_WriteLibrary( Super_Man_t * pMan )
{
Super_Gate_t * pGate, * pGateNext;
FILE * pFile;
char FileName[100];
char * FileName;
char * pNameGeneric;
int i, Counter;
FileName = ABC_ALLOC( char, 10000 );
// get the file name
pNameGeneric = Extra_FileNameGeneric( pMan->pName );
sprintf( FileName, "%s.super_old", pNameGeneric );
@ -1152,6 +1154,8 @@ if ( pMan->fVerbose )
printf( "The supergates are written using old format \"%s\" ", FileName );
printf( "(%0.3f Mb).\n", ((double)Extra_FileSize(FileName))/(1<<20) );
}
ABC_FREE( FileName );
}
/**Function*************************************************************
@ -1251,11 +1255,13 @@ void Super_WriteLibraryTree( Super_Man_t * pMan )
{
Super_Gate_t * pSuper;
FILE * pFile;
char FileName[100];
char * FileName;
char * pNameGeneric;
int i, Counter;
int posStart;
FileName = ABC_ALLOC( char, 10000 );
// get the file name
pNameGeneric = Extra_FileNameGeneric( pMan->pName );
sprintf( FileName, "%s.super", pNameGeneric );
@ -1286,6 +1292,8 @@ if ( pMan->fVerbose )
printf( "The supergates are written using new format \"%s\" ", FileName );
printf( "(%0.3f Mb).\n", ((double)Extra_FileSize(FileName))/(1<<20) );
}
ABC_FREE( FileName );
}
/**Function*************************************************************

24
src/misc/util/abc_global.h
View File

@ -153,6 +153,15 @@ typedef unsigned __int64 ABC_UINT64_T;
#define ABC_MIN(a,b) ((a) < (b) ? (a) : (b))
#define ABC_INFINITY (100000000)
#define ABC_PRT(a,t) (printf("%s = ", (a)), printf("%7.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC)))
#define ABC_PRTn(a,t) (printf("%s = ", (a)), printf("%6.2f sec ", (float)(t)/(float)(CLOCKS_PER_SEC)))
#define ABC_PRTP(a,t,T) (printf("%s = ", (a)), printf("%7.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), (T)? 100.0*(t)/(T) : 0.0))
#define ABC_PRM(a,f) (printf("%s = ", (a)), printf("%7.2f Mb ", 1.0*(f)/(1<<20)))
//#define ABC_USE_MEM_REC 1
#ifndef ABC_USE_MEM_REC
#define ABC_ALLOC(type, num) ((type *) malloc(sizeof(type) * (num)))
#define ABC_CALLOC(type, num) ((type *) calloc((num), sizeof(type)))
#define ABC_FALLOC(type, num) ((type *) memset(malloc(sizeof(type) * (num)), 0xff, sizeof(type) * (num)))
@ -160,11 +169,16 @@ typedef unsigned __int64 ABC_UINT64_T;
#define ABC_REALLOC(type, obj, num) \
((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
((type *) malloc(sizeof(type) * (num))))
#define ABC_PRT(a,t) (printf("%s = ", (a)), printf("%7.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC)))
#define ABC_PRTn(a,t) (printf("%s = ", (a)), printf("%6.2f sec ", (float)(t)/(float)(CLOCKS_PER_SEC)))
#define ABC_PRTP(a,t,T) (printf("%s = ", (a)), printf("%7.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), (T)? 100.0*(t)/(T) : 0.0))
#define ABC_PRM(a,f) (printf("%s = ", (a)), printf("%7.2f Mb ", 1.0*(f)/(1<<20)))
#else
#include "utilMem.h"
#define ABC_ALLOC(type, num) ((type *) Util_MemRecAlloc(malloc(sizeof(type) * (num))))
#define ABC_CALLOC(type, num) ((type *) Util_MemRecAlloc(calloc((num), sizeof(type))))
#define ABC_FALLOC(type, num) ((type *) memset(Util_MemRecAlloc(malloc(sizeof(type) * (num))), 0xff, sizeof(type) * (num)))
#define ABC_FREE(obj) ((obj) ? (free((char *) Util_MemRecFree(obj)), (obj) = 0) : 0)
#define ABC_REALLOC(type, obj, num) \
((obj) ? ((type *) Util_MemRecAlloc(realloc((char *)(Util_MemRecFree(obj)), sizeof(type) * (num)))) : \
((type *) Util_MemRecAlloc(malloc(sizeof(type) * (num)))))
#endif
#ifdef __cplusplus
}

2
src/misc/util/util_hack.h
View File

@ -58,7 +58,7 @@ extern "C" {
# define ARGS(args) args
# else
# define ARGS(args) ()
# endif
# endif
#endif
extern long Extra_CpuTime();

1
src/misc/vec/vec.h
View File

@ -37,7 +37,6 @@
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////

22
src/misc/vec/vecStr.h
View File

@ -570,6 +570,28 @@ static inline char Vec_StrPop( Vec_Str_t * p )
return p->pArray[--p->nSize];
}
/**Function*************************************************************
Synopsis [Reverses the order of entries.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_StrReverseOrder( Vec_Str_t * p )
{
int i, Temp;
for ( i = 0; i < p->nSize/2; i++ )
{
Temp = p->pArray[i];
p->pArray[i] = p->pArray[p->nSize-1-i];
p->pArray[p->nSize-1-i] = Temp;
}
}
/**Function*************************************************************
Synopsis [Comparison procedure for two clauses.]

2
src/opt/mfs/mfsResub.c
View File

@ -207,7 +207,7 @@ p->timeInt += clock() - clk;
printf( "\n" );
}
iVar = -1;
while ( 1 )
while ( 1 )
{
if ( fVeryVerbose )
{