summaryrefslogtreecommitdiffstats
path: root/src/base/abci/abcDar.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/abci/abcDar.c')
-rw-r--r--src/base/abci/abcDar.c588
1 files changed, 465 insertions, 123 deletions
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index dbe98631..31ef986c 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -19,6 +19,7 @@
***********************************************************************/
#include "abc.h"
+#include "main.h"
#include "giaAig.h"
#include "saig.h"
#include "dar.h"
@@ -29,11 +30,14 @@
#include "dch.h"
#include "ssw.h"
#include "cgt.h"
-//#include "fsim.h"
+#include "bbr.h"
#include "gia.h"
#include "cec.h"
+#include "csw.h"
#include "giaAbs.h"
+ABC_NAMESPACE_IMPL_START
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -100,6 +104,7 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters )
// create the manager
pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
pMan->fCatchExor = fExors;
+ pMan->nConstrs = pNtk->nConstrs;
pMan->pName = Extra_UtilStrsav( pNtk->pName );
// transfer the pointers to the basic nodes
@@ -174,6 +179,7 @@ Aig_Man_t * Abc_NtkToDarChoices( Abc_Ntk_t * pNtk )
// create the manager
pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
pMan->pName = Extra_UtilStrsav( pNtk->pName );
+ pMan->nConstrs = pNtk->nConstrs;
if ( Abc_NtkGetChoiceNum(pNtk) )
{
pMan->pEquivs = ABC_ALLOC( Aig_Obj_t *, Abc_NtkObjNum(pNtk) );
@@ -184,13 +190,13 @@ Aig_Man_t * Abc_NtkToDarChoices( Abc_Ntk_t * pNtk )
Abc_NtkForEachCi( pNtk, pObj, i )
pObj->pCopy = (Abc_Obj_t *)Aig_ObjCreatePi(pMan);
// perform the conversion of the internal nodes (assumes DFS ordering)
- Vec_PtrForEachEntry( vNodes, pObj, i )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
{
pObj->pCopy = (Abc_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj), (Aig_Obj_t *)Abc_ObjChild1Copy(pObj) );
// printf( "%d->%d ", pObj->Id, ((Aig_Obj_t *)pObj->pCopy)->Id );
if ( Abc_AigNodeIsChoice( pObj ) )
{
- for ( pPrev = pObj, pFanin = pObj->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
+ for ( pPrev = pObj, pFanin = (Abc_Obj_t *)pObj->pData; pFanin; pPrev = pFanin, pFanin = (Abc_Obj_t *)pFanin->pData )
Aig_ObjSetEquiv( pMan, (Aig_Obj_t *)pPrev->pCopy, (Aig_Obj_t *)pFanin->pCopy );
// Aig_ManCreateChoice( pIfMan, (Aig_Obj_t *)pNode->pCopy );
}
@@ -232,17 +238,18 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
// assert( Aig_ManRegNum(pMan) == Abc_NtkLatchNum(pNtkOld) );
// perform strashing
pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
+ pNtkNew->nConstrs = pMan->nConstrs;
// transfer the pointers to the basic nodes
Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
Aig_ManForEachPi( pMan, pObj, i )
pObj->pData = Abc_NtkCi(pNtkNew, i);
// rebuild the AIG
vNodes = Aig_ManDfs( pMan, 1 );
- Vec_PtrForEachEntry( vNodes, pObj, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
if ( Aig_ObjIsBuf(pObj) )
pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
else
- pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
+ pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
Vec_PtrFree( vNodes );
// connect the PO nodes
Aig_ManForEachPo( pMan, pObj, i )
@@ -287,6 +294,7 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
// assert( Aig_ManRegNum(pMan) != Abc_NtkLatchNum(pNtkOld) );
// perform strashing
pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
+ pNtkNew->nConstrs = pMan->nConstrs;
// consider the case of target enlargement
if ( Abc_NtkCiNum(pNtkNew) < Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan) )
{
@@ -309,17 +317,17 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
pObjNew = Abc_NtkCreateLatch( pNtkNew );
pObjLi->pData = Abc_NtkCreateBi( pNtkNew );
pObjLo->pData = Abc_NtkCreateBo( pNtkNew );
- Abc_ObjAddFanin( pObjNew, pObjLi->pData );
- Abc_ObjAddFanin( pObjLo->pData, pObjNew );
+ Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)pObjLi->pData );
+ Abc_ObjAddFanin( (Abc_Obj_t *)pObjLo->pData, pObjNew );
Abc_LatchSetInit0( pObjNew );
}
// rebuild the AIG
vNodes = Aig_ManDfs( pMan, 1 );
- Vec_PtrForEachEntry( vNodes, pObj, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
if ( Aig_ObjIsBuf(pObj) )
pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
else
- pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
+ pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
Vec_PtrFree( vNodes );
// connect the PO nodes
Aig_ManForEachPo( pMan, pObj, i )
@@ -412,6 +420,7 @@ Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan )
assert( pMan->nAsserts == 0 );
// perform strashing
pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
+ pNtkNew->nConstrs = pMan->nConstrs;
// duplicate the name and the spec
// pNtkNew->pName = Extra_UtilStrsav(pMan->pName);
// pNtkNew->pSpec = Extra_UtilStrsav(pMan->pSpec);
@@ -438,19 +447,19 @@ Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan )
pObjNew = Abc_NtkCreateLatch( pNtkNew );
pObjLi->pData = Abc_NtkCreateBi( pNtkNew );
pObjLo->pData = Abc_NtkCreateBo( pNtkNew );
- Abc_ObjAddFanin( pObjNew, pObjLi->pData );
- Abc_ObjAddFanin( pObjLo->pData, pObjNew );
+ Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)pObjLi->pData );
+ Abc_ObjAddFanin( (Abc_Obj_t *)pObjLo->pData, pObjNew );
Abc_LatchSetInit0( pObjNew );
- Abc_ObjAssignName( pObjLi->pData, Abc_ObjName(pObjLi->pData), NULL );
- Abc_ObjAssignName( pObjLo->pData, Abc_ObjName(pObjLo->pData), NULL );
+ Abc_ObjAssignName( (Abc_Obj_t *)pObjLi->pData, Abc_ObjName((Abc_Obj_t *)pObjLi->pData), NULL );
+ Abc_ObjAssignName( (Abc_Obj_t *)pObjLo->pData, Abc_ObjName((Abc_Obj_t *)pObjLo->pData), NULL );
}
// rebuild the AIG
vNodes = Aig_ManDfs( pMan, 1 );
- Vec_PtrForEachEntry( vNodes, pObj, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
if ( Aig_ObjIsBuf(pObj) )
pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
else
- pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
+ pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
Vec_PtrFree( vNodes );
// connect the PO nodes
Aig_ManForEachPo( pMan, pObj, i )
@@ -490,6 +499,7 @@ Abc_Ntk_t * Abc_NtkAfterTrim( Aig_Man_t * pMan, Abc_Ntk_t * pNtkOld )
assert( pMan->vCiNumsOrig != NULL );
// perform strashing
pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
+ pNtkNew->nConstrs = pMan->nConstrs;
// duplicate the name and the spec
// pNtkNew->pName = Extra_UtilStrsav(pMan->pName);
// pNtkNew->pSpec = Extra_UtilStrsav(pMan->pSpec);
@@ -520,23 +530,23 @@ Abc_Ntk_t * Abc_NtkAfterTrim( Aig_Man_t * pMan, Abc_Ntk_t * pNtkOld )
pObjNew = Abc_NtkCreateLatch( pNtkNew );
pObjLi->pData = Abc_NtkCreateBi( pNtkNew );
pObjLo->pData = Abc_NtkCreateBo( pNtkNew );
- Abc_ObjAddFanin( pObjNew, pObjLi->pData );
- Abc_ObjAddFanin( pObjLo->pData, pObjNew );
+ Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)pObjLi->pData );
+ Abc_ObjAddFanin( (Abc_Obj_t *)pObjLo->pData, pObjNew );
Abc_LatchSetInit0( pObjNew );
// find the name
pObjOld = Abc_NtkCi( pNtkOld, Vec_IntEntry(pMan->vCiNumsOrig, Saig_ManPiNum(pMan)+i) );
- Abc_ObjAssignName( pObjLo->pData, Abc_ObjName(pObjOld), NULL );
+ Abc_ObjAssignName( (Abc_Obj_t *)pObjLo->pData, Abc_ObjName(pObjOld), NULL );
// find the name
pObjOld = Abc_NtkCo( pNtkOld, Saig_ManPoNum(pMan)+i );
- Abc_ObjAssignName( pObjLi->pData, Abc_ObjName(pObjOld), NULL );
+ Abc_ObjAssignName( (Abc_Obj_t *)pObjLi->pData, Abc_ObjName(pObjOld), NULL );
}
// rebuild the AIG
vNodes = Aig_ManDfs( pMan, 1 );
- Vec_PtrForEachEntry( vNodes, pObj, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
if ( Aig_ObjIsBuf(pObj) )
pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
else
- pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
+ pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
Vec_PtrFree( vNodes );
// connect the PO nodes
Aig_ManForEachPo( pMan, pObj, i )
@@ -546,7 +556,7 @@ Abc_Ntk_t * Abc_NtkAfterTrim( Aig_Man_t * pMan, Abc_Ntk_t * pNtkOld )
}
// check the resulting AIG
if ( !Abc_NtkCheck( pNtkNew ) )
- fprintf( stdout, "Abc_NtkFromAigPhase(): Network check has failed.\n" );
+ fprintf( stdout, "Abc_NtkAfterTrim(): Network check has failed.\n" );
return pNtkNew;
}
@@ -571,6 +581,7 @@ Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
assert( Aig_ManBufNum(pMan) == 0 );
// perform strashing
pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
+ pNtkNew->nConstrs = pMan->nConstrs;
// transfer the pointers to the basic nodes
Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
Aig_ManForEachPi( pMan, pObj, i )
@@ -578,15 +589,15 @@ Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
// rebuild the AIG
vNodes = Aig_ManDfsChoices( pMan );
- Vec_PtrForEachEntry( vNodes, pObj, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
{
- pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
+ pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
if ( (pTemp = Aig_ObjEquiv(pMan, pObj)) )
{
Abc_Obj_t * pAbcRepr, * pAbcObj;
assert( pTemp->pData != NULL );
- pAbcRepr = pObj->pData;
- pAbcObj = pTemp->pData;
+ pAbcRepr = (Abc_Obj_t *)pObj->pData;
+ pAbcObj = (Abc_Obj_t *)pTemp->pData;
pAbcObj->pData = pAbcRepr->pData;
pAbcRepr->pData = pAbcObj;
}
@@ -622,6 +633,7 @@ Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
// assert( Aig_ManLatchNum(pMan) > 0 );
// perform strashing
pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
+ pNtkNew->nConstrs = pMan->nConstrs;
// transfer the pointers to the basic nodes
Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
Aig_ManForEachPi( pMan, pObj, i )
@@ -640,7 +652,7 @@ Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
Abc_NtkAddDummyBoxNames( pNtkNew );
// rebuild the AIG
vNodes = Aig_ManDfs( pMan, 1 );
- Vec_PtrForEachEntry( vNodes, pObj, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
{
// add the first fanin
pObj->pData = pFaninNew0 = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
@@ -650,9 +662,9 @@ Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
pFaninNew1 = (Abc_Obj_t *)Aig_ObjChild1Copy(pObj);
// create the new node
if ( Aig_ObjIsExor(pObj) )
- pObj->pData = pObjNew = Abc_AigXor( pNtkNew->pManFunc, pFaninNew0, pFaninNew1 );
+ pObj->pData = pObjNew = Abc_AigXor( (Abc_Aig_t *)pNtkNew->pManFunc, pFaninNew0, pFaninNew1 );
else
- pObj->pData = pObjNew = Abc_AigAnd( pNtkNew->pManFunc, pFaninNew0, pFaninNew1 );
+ pObj->pData = pObjNew = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, pFaninNew0, pFaninNew1 );
}
Vec_PtrFree( vNodes );
// connect the PO nodes
@@ -665,7 +677,7 @@ Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
Aig_ManForEachObj( pMan, pObj, i )
{
pFaninNew = (Abc_Obj_t *)Aig_ObjChild0Copy( pObj );
- Abc_ObjAddFanin( Abc_ObjFanin0(Abc_ObjFanin0(pObj->pData)), pFaninNew );
+ Abc_ObjAddFanin( Abc_ObjFanin0(Abc_ObjFanin0((Abc_Obj_t *)pObj->pData)), pFaninNew );
}
if ( !Abc_NtkCheck( pNtkNew ) )
fprintf( stdout, "Abc_NtkFromIvySeq(): Network check has failed.\n" );
@@ -860,7 +872,7 @@ Abc_Ntk_t * Abc_NtkDarFraigPart( Abc_Ntk_t * pNtk, int nPartSize, int nConfLimit
***********************************************************************/
Abc_Ntk_t * Abc_NtkCSweep( Abc_Ntk_t * pNtk, int nCutsMax, int nLeafMax, int fVerbose )
{
- extern Aig_Man_t * Csw_Sweep( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose );
+// extern Aig_Man_t * Csw_Sweep( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose );
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
pMan = Abc_NtkToDar( pNtk, 0, 0 );
@@ -1026,7 +1038,7 @@ 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 Gia_Man_t * Dar_NewChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose );
+ extern Gia_Man_t * Dar_NewChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fLightSynth, int fVerbose );
extern Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars );
Aig_Man_t * pMan, * pTemp;
@@ -1039,7 +1051,7 @@ Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars )
return NULL;
clk = clock();
if ( pPars->fSynthesis )
- pGia = Dar_NewChoiceSynthesis( pMan, 1, 1, pPars->fPower, 0 );
+ pGia = Dar_NewChoiceSynthesis( pMan, 1, 1, pPars->fPower, pPars->fLightSynth, pPars->fVerbose );
else
{
pGia = Gia_ManFromAig( pMan );
@@ -1121,23 +1133,23 @@ Abc_Ntk_t * Abc_NtkConstructFromCnf( Abc_Ntk_t * pNtk, Cnf_Man_t * p, Vec_Ptr_t
Aig_ManPi(p->pManAig, i)->pData = pNode->pCopy;
// process the nodes in topological order
vCover = Vec_IntAlloc( 1 << 16 );
- Vec_PtrForEachEntry( vMapped, pObj, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
{
// create new node
pNodeNew = Abc_NtkCreateNode( pNtkNew );
// add fanins according to the cut
- pCut = pObj->pData;
+ pCut = (Cnf_Cut_t *)pObj->pData;
Cnf_CutForEachLeaf( p->pManAig, pCut, pLeaf, k )
- Abc_ObjAddFanin( pNodeNew, pLeaf->pData );
+ Abc_ObjAddFanin( pNodeNew, (Abc_Obj_t *)pLeaf->pData );
// add logic function
if ( pCut->nFanins < 5 )
{
uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vCover );
- pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCut->nFanins, vCover );
+ pNodeNew->pData = Abc_SopCreateFromIsop( (Extra_MmFlex_t *)pNtkNew->pManFunc, pCut->nFanins, vCover );
}
else
- pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCut->nFanins, pCut->vIsop[1] );
+ pNodeNew->pData = Abc_SopCreateFromIsop( (Extra_MmFlex_t *)pNtkNew->pManFunc, pCut->nFanins, pCut->vIsop[1] );
// save the node
pObj->pData = pNodeNew;
}
@@ -1146,7 +1158,7 @@ Abc_Ntk_t * Abc_NtkConstructFromCnf( Abc_Ntk_t * pNtk, Cnf_Man_t * p, Vec_Ptr_t
Abc_NtkForEachCo( pNtk, pNode, i )
{
pObj = Aig_ManPo(p->pManAig, i);
- pNodeNew = Abc_ObjNotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
+ pNodeNew = Abc_ObjNotCond( (Abc_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
}
@@ -1240,7 +1252,7 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit
assert( Abc_NtkPoNum(pNtk) == 1 );
pMan = Abc_NtkToDar( pNtk, 0, 0 );
RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, fAlignPol, fAndOuts, fVerbose );
- pNtk->pModel = pMan->pData, pMan->pData = NULL;
+ pNtk->pModel = (int *)pMan->pData, pMan->pData = NULL;
Aig_ManStop( pMan );
return RetValue;
}
@@ -1265,7 +1277,7 @@ int Abc_NtkPartitionedSat( Abc_Ntk_t * pNtk, int nAlgo, int nPartSize, int nConf
assert( Abc_NtkLatchNum(pNtk) == 0 );
pMan = Abc_NtkToDar( pNtk, 0, 0 );
RetValue = Aig_ManPartitionedSat( pMan, nAlgo, nPartSize, nConfPart, nConfTotal, fAlignPol, fSynthesize, fVerbose );
- pNtk->pModel = pMan->pData, pMan->pData = NULL;
+ pNtk->pModel = (int *)pMan->pData, pMan->pData = NULL;
Aig_ManStop( pMan );
return RetValue;
}
@@ -1362,7 +1374,7 @@ int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int fPa
RetValue = Fra_FraigCec( &pMan, 100000, fVerbose );
// transfer model if given
if ( pNtk2 == NULL )
- pNtk1->pModel = pMan->pData, pMan->pData = NULL;
+ pNtk1->pModel = (int *)pMan->pData, pMan->pData = NULL;
Aig_ManStop( pMan );
finish:
@@ -1458,10 +1470,10 @@ ABC_PRT( "Initial fraiging time", clock() - clk );
***********************************************************************/
void Abc_NtkPrintLatchEquivClasses( Abc_Ntk_t * pNtk, Aig_Man_t * pAig )
{
- bool header_dumped = false;
+ int header_dumped = 0;
int num_orig_latches = Abc_NtkLatchNum(pNtk);
char **pNames = ABC_ALLOC( char *, num_orig_latches );
- bool *p_irrelevant = ABC_ALLOC( bool, num_orig_latches );
+ int *p_irrelevant = ABC_ALLOC( int, num_orig_latches );
char * pFlopName, * pReprName;
Aig_Obj_t * pFlop, * pRepr;
Abc_Obj_t * pNtkFlop;
@@ -1560,7 +1572,7 @@ Abc_Ntk_t * Abc_NtkDarSeqSweep2( Abc_Ntk_t * pNtk, Ssw_Pars_t * pPars )
if ( pPars->fFlopVerbose )
Abc_NtkPrintLatchEquivClasses(pNtk, pTemp);
- Aig_ManStop( pTemp );
+ Aig_ManStop( pTemp );
if ( pMan == NULL )
return NULL;
@@ -1681,7 +1693,7 @@ static void sigfunc( int signo )
SeeAlso []
***********************************************************************/
-int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int nNodeDelta, int nTimeOut, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int nCofFanLit, int fVerbose )
+int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int nNodeDelta, int nTimeOut, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int nCofFanLit, int fVerbose, int * piFrames )
{
Aig_Man_t * pMan;
int status, RetValue = -1, clk = clock();
@@ -1711,25 +1723,31 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int
{
int iFrame;
RetValue = Saig_ManBmcSimple( pMan, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &iFrame, nCofFanLit );
+ if ( piFrames )
+ *piFrames = iFrame;
ABC_FREE( pNtk->pModel );
ABC_FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
if ( RetValue == 1 )
- printf( "No output was asserted in %d frames. ", iFrame );
+ {
+// printf( "No output was asserted in %d frames. ", iFrame );
+ printf( "Incorrect return value. " );
+ }
else if ( RetValue == -1 )
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 );
+// extern void Aig_ManCounterExampleValueTest( Aig_Man_t * pAig, Abc_Cex_t * pCex );
- Fra_Cex_t * pCex = pNtk->pSeqModel;
+ Abc_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 );
}
+ABC_PRT( "Time", clock() - clk );
}
else
- {
+ {
/*
Fra_BmcPerformSimple( pMan, nFrames, nBTLimit, fRewrite, fVerbose );
ABC_FREE( pNtk->pModel );
@@ -1737,7 +1755,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
if ( pNtk->pSeqModel )
{
- Fra_Cex_t * pCex = pNtk->pSeqModel;
+ Abc_Cex_t * pCex = pNtk->pSeqModel;
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
RetValue = 0;
}
@@ -1759,16 +1777,15 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int
printf( "No output was asserted in %d frames. Reached conflict limit (%d). ", iFrame, nBTLimit );
else // if ( RetValue == 0 )
{
- Fra_Cex_t * pCex = pNtk->pSeqModel;
+ Abc_Cex_t * pCex = pNtk->pSeqModel;
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
}
*/
- Saig_BmcPerform( pMan, nStart, nFrames, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fVerbose, 0 );
+ RetValue = Saig_BmcPerform( pMan, nStart, nFrames, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fVerbose, 0, piFrames );
ABC_FREE( pNtk->pModel );
ABC_FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
}
-ABC_PRT( "Time", clock() - clk );
// verify counter-example
if ( pNtk->pSeqModel )
{
@@ -1782,6 +1799,73 @@ ABC_PRT( "Time", clock() - clk );
/**Function*************************************************************
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
+{
+ Aig_Man_t * pMan;
+ int status, RetValue = -1, clk = clock();
+ pMan = Abc_NtkToDar( pNtk, 0, 1 );
+ if ( pMan == NULL )
+ {
+ printf( "Converting miter into AIG has failed.\n" );
+ return RetValue;
+ }
+ assert( pMan->nRegs > 0 );
+ RetValue = Saig_ManBmcScalable( pMan, pPars );
+ ABC_FREE( pNtk->pModel );
+ ABC_FREE( pNtk->pSeqModel );
+ pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
+ if ( RetValue == 1 )
+ {
+// printf( "No output was asserted in %d frames. ", pPars->iFrame );
+ printf( "Incorrect return value. " );
+ }
+ else if ( RetValue == -1 )
+ {
+ if ( pPars->nFailOuts == 0 )
+ printf( "No output was asserted in %d frames. Reached conflict limit (%d). ", pPars->iFrame, pPars->nConfLimit );
+ else
+ {
+ printf( "The total of %d outputs was asserted in %d frames. Reached conflict limit (%d). ", pPars->nFailOuts, pPars->iFrame, pPars->nConfLimit );
+ if ( pNtk->pSeqModelVec )
+ Vec_PtrFreeFree( pNtk->pSeqModelVec );
+ pNtk->pSeqModelVec = pMan->pSeqModelVec; pMan->pSeqModelVec = NULL;
+ }
+ }
+ else // if ( RetValue == 0 )
+ {
+ if ( !pPars->fSolveAll )
+ {
+ Abc_Cex_t * pCex = pNtk->pSeqModel;
+ printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
+ }
+ else
+ {
+ printf( "Incorrect return value. " );
+// printf( "At least one output was asserted (out=%d, frame=%d). ", pCex->iPo, pCex->iFrame );
+ }
+ }
+ ABC_PRT( "Time", clock() - clk );
+ if ( pNtk->pSeqModel )
+ {
+ status = Ssw_SmlRunCounterExample( pMan, pNtk->pSeqModel );
+ if ( status == 0 )
+ printf( "Abc_NtkDarBmc3(): Counter-example verification has FAILED.\n" );
+ }
+ Aig_ManStop( pMan );
+ return RetValue;
+}
+
+/**Function*************************************************************
+
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
@@ -1791,10 +1875,13 @@ ABC_PRT( "Time", clock() - clk );
SeeAlso []
***********************************************************************/
-int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars )
+int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars, Aig_Man_t ** ppNtkRes )
{
int RetValue, iFrame, clk = clock();
+ int nTotalProvedSat = 0;
assert( pMan->nRegs > 0 );
+ if ( ppNtkRes )
+ *ppNtkRes = NULL;
if ( pPars->fUseSeparate )
{
Aig_Man_t * pTemp, * pAux;
@@ -1804,17 +1891,39 @@ int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars )
{
if ( Aig_ObjFanin0(pObjPo) == Aig_ManConst1(pMan) )
continue;
+ if ( pPars->fVerbose )
+ printf( "Solving output %2d (out of %2d):\n", i, Saig_ManPoNum(pMan) );
pTemp = Aig_ManDupOneOutput( pMan, i, 1 );
pTemp = Aig_ManScl( pAux = pTemp, 1, 1, 0 );
Aig_ManStop( pAux );
- RetValue = Inter_ManPerformInterpolation( pTemp, pPars, &iFrame );
+ if ( Aig_ManRegNum(pTemp) == 0 )
+ {
+ pTemp->pSeqModel = NULL;
+ RetValue = Fra_FraigSat( pTemp, pPars->nBTLimit, 0, 0, 0, 0 );
+ if ( pTemp->pData )
+ pTemp->pSeqModel = Gia_ManCreateFromComb( Aig_ManRegNum(pMan), Saig_ManPiNum(pMan), i, (int *)pTemp->pData );
+// pNtk->pModel = pTemp->pData, pTemp->pData = NULL;
+ }
+ else
+ 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 ( pPars->fDropSatOuts )
+ {
+ printf( "Output %d proved SAT in frame %d (replacing by const 0 and continuing...)\n", i, pTemp->pSeqModel->iFrame );
+ Aig_ObjPatchFanin0( pMan, pObjPo, Aig_ManConst0(pMan) );
+ Aig_ManStop( pTemp );
+ nTotalProvedSat++;
+ continue;
+ }
+ else
+ {
+ Abc_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 )
@@ -1838,17 +1947,19 @@ int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars )
if ( Counter )
RetValue = -1;
}
-/*
- pMan = Aig_ManDupUnsolvedOutputs( pTemp = pMan, 1 );
- Aig_ManStop( pTemp );
- pMan = Aig_ManScl( pTemp = pMan, 1, 1, 0 );
- Aig_ManStop( pTemp );
-*/
+ if ( ppNtkRes )
+ {
+ pTemp = Aig_ManDupUnsolvedOutputs( pMan, 1 );
+ *ppNtkRes = Aig_ManScl( pTemp, 1, 1, 0 );
+ Aig_ManStop( pTemp );
+ }
}
else
{
RetValue = Inter_ManPerformInterpolation( pMan, pPars, &iFrame );
}
+ if ( nTotalProvedSat )
+ printf( "The total of %d outputs proved SAT and replaced by const 0 in this run.\n", nTotalProvedSat );
if ( RetValue == 1 )
printf( "Property proved. " );
else if ( RetValue == 0 )
@@ -1872,21 +1983,34 @@ ABC_PRT( "Time", clock() - clk );
SeeAlso []
***********************************************************************/
-int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars )
+int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars, Abc_Ntk_t ** ppNtkRes )
{
Aig_Man_t * pMan;
+ int RetValue;
+ if ( ppNtkRes )
+ *ppNtkRes = NULL;
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
{
printf( "Converting miter into AIG has failed.\n" );
return -1;
}
- Abc_NtkDarBmcInter_int( pMan, pPars );
+ if ( pPars->fUseSeparate && ppNtkRes )
+ {
+ Aig_Man_t * pManNew;
+ RetValue = Abc_NtkDarBmcInter_int( pMan, pPars, &pManNew );
+ *ppNtkRes = Abc_NtkFromAigPhase( pManNew );
+ Aig_ManStop( pManNew );
+ }
+ else
+ {
+ RetValue = Abc_NtkDarBmcInter_int( pMan, pPars, NULL );
+ }
ABC_FREE( pNtk->pModel );
ABC_FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
Aig_ManStop( pMan );
- return 1;
+ return RetValue;
}
/**Function*************************************************************
@@ -1945,7 +2069,7 @@ int Abc_NtkDarDemiter( Abc_Ntk_t * pNtk )
int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
{
Aig_Man_t * pMan;
- int RetValue, clkTotal = clock();
+ int RetValue = -1, clkTotal = clock();
if ( pSecPar->fTryComb || Abc_NtkLatchNum(pNtk) == 0 )
{
Prove_Params_t Params, * pParams = &Params;
@@ -1990,7 +2114,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
}
if ( pSecPar->fTryBmc )
{
- RetValue = Abc_NtkDarBmc( pNtk, 0, 20, 100000, -1, 0, 2000, -1, 0, 1, 0, 0 );
+ RetValue = Abc_NtkDarBmc( pNtk, 0, 20, 100000, -1, 0, 2000, -1, 0, 1, 0, 0, NULL );
if ( RetValue == 0 )
{
printf( "Networks are not equivalent.\n" );
@@ -2023,7 +2147,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
if ( pNtk->pSeqModel )
{
- Fra_Cex_t * pCex = pNtk->pSeqModel;
+ Abc_Cex_t * pCex = pNtk->pSeqModel;
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness).\n", pCex->iPo, pCex->iFrame );
if ( !Ssw_SmlRunCounterExample( pMan, pNtk->pSeqModel ) )
printf( "Abc_NtkDarProve(): Counter-example verification has FAILED.\n" );
@@ -2065,7 +2189,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Fra_Sec_t * pSecPar )
printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
// report the error
pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, pSecPar->nFramesMax );
- Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, pSecPar->nFramesMax );
+// Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, pSecPar->nFramesMax );
ABC_FREE( pMiter->pModel );
Abc_NtkDelete( pMiter );
return 0;
@@ -2272,7 +2396,7 @@ Abc_Ntk_t * Abc_NtkDarMatch( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nDist, in
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchEqual, int fVerbose )
+Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchEqual, int fSaveNames, int fVerbose )
{
extern void Aig_ManPrintControlFanouts( Aig_Man_t * p );
Abc_Ntk_t * pNtkAig;
@@ -2280,17 +2404,23 @@ Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchE
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
return NULL;
-// Aig_ManSeqCleanup( pMan );
-// if ( fLatchConst && pMan->nRegs )
-// pMan = Aig_ManConstReduce( pMan, fVerbose );
-// if ( fLatchEqual && pMan->nRegs )
-// pMan = Aig_ManReduceLaches( pMan, fVerbose );
- if ( pMan->vFlopNums )
- Vec_IntFree( pMan->vFlopNums );
- pMan->vFlopNums = NULL;
+ if ( fSaveNames )
+ {
+ Aig_ManSeqCleanup( pMan );
+ if ( fLatchConst && pMan->nRegs )
+ pMan = Aig_ManConstReduce( pMan, fVerbose );
+ if ( fLatchEqual && pMan->nRegs )
+ pMan = Aig_ManReduceLaches( pMan, fVerbose );
+ }
+ else
+ {
+ if ( pMan->vFlopNums )
+ Vec_IntFree( pMan->vFlopNums );
+ pMan->vFlopNums = NULL;
+ pMan = Aig_ManScl( pTemp = pMan, fLatchConst, fLatchEqual, fVerbose );
+ Aig_ManStop( pTemp );
+ }
- pMan = Aig_ManScl( pTemp = pMan, fLatchConst, fLatchEqual, fVerbose );
- Aig_ManStop( pTemp );
pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
//Aig_ManPrintControlFanouts( pMan );
Aig_ManStop( pMan );
@@ -2512,12 +2642,12 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
extern int Cec_ManSimulate( Aig_Man_t * pAig, int nWords, int nIters, int TimeLimit, int fMiter, int fVerbose );
extern int Raig_ManSimulate( Aig_Man_t * pAig, int nWords, int nIters, int TimeLimit, int fMiter, int fVerbose );
Aig_Man_t * pMan;
- Fra_Cex_t * pCex;
- int status, RetValue, clk = clock();
+ Abc_Cex_t * pCex;
+ int status, RetValue = -1, clk = clock();
if ( Abc_NtkGetChoiceNum(pNtk) )
{
printf( "Removing %d choices from the AIG.\n", Abc_NtkGetChoiceNum(pNtk) );
- Abc_AigCleanup(pNtk->pManFunc);
+ Abc_AigCleanup((Abc_Aig_t *)pNtk->pManFunc);
}
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( fComb || Abc_NtkLatchNum(pNtk) == 0 )
@@ -2530,7 +2660,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
{
printf( "Simulation iterated %d times with %d words asserted output %d in frame %d. ",
nFrames, nWords, pCex->iPo, pCex->iFrame );
- status = Ssw_SmlRunCounterExample( pMan, (Ssw_Cex_t *)pCex );
+ status = Ssw_SmlRunCounterExample( pMan, pCex );
if ( status == 0 )
printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
}
@@ -2557,7 +2687,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
{
printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
nFrames, nWords, pCex->iPo, pCex->iFrame );
- status = Ssw_SmlRunCounterExample( pMan, (Ssw_Cex_t *)pCex );
+ status = Ssw_SmlRunCounterExample( pMan, pCex );
if ( status == 0 )
printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
}
@@ -2587,7 +2717,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
{
printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
nFrames, nWords, pCex->iPo, pCex->iFrame );
- status = Ssw_SmlRunCounterExample( pMan, (Ssw_Cex_t *)pCex );
+ status = Ssw_SmlRunCounterExample( pMan, pCex );
if ( status == 0 )
printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
}
@@ -2614,22 +2744,21 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
pGia = Gia_ManFromAig( pMan );
if ( Gia_ManSimSimulate( pGia, pPars ) )
{
- if ( (pCex = (Fra_Cex_t *)pGia->pCexSeq) )
+ if ( pGia->pCexSeq )
{
printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
- nFrames, nWords, pCex->iPo, pCex->iFrame );
- status = Ssw_SmlRunCounterExample( pMan, (Ssw_Cex_t *)pCex );
+ nFrames, nWords, pGia->pCexSeq->iPo, pGia->pCexSeq->iFrame );
+ status = Ssw_SmlRunCounterExample( pMan, pGia->pCexSeq );
if ( status == 0 )
printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
}
ABC_FREE( pNtk->pModel );
ABC_FREE( pNtk->pSeqModel );
- pNtk->pSeqModel = pCex; pMan->pSeqModel = NULL;
- RetValue = 1;
+ pNtk->pSeqModel = pGia->pCexSeq; pGia->pCexSeq = NULL;
+ RetValue = 0;
}
else
{
- RetValue = 0;
printf( "Simulation of %d frames with %d words did not assert the outputs. ",
nFrames, nWords );
}
@@ -2646,18 +2775,17 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
{
printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
nFrames, nWords, pCex->iPo, pCex->iFrame );
- status = Ssw_SmlRunCounterExample( pMan, (Ssw_Cex_t *)pCex );
+ status = Ssw_SmlRunCounterExample( pMan, pCex );
if ( status == 0 )
printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
}
ABC_FREE( pNtk->pModel );
ABC_FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pCex;
- RetValue = 1;
+ RetValue = 0;
}
else
{
- RetValue = 0;
printf( "Simulation of %d frames with %d words did not assert the outputs. ",
nFrames, nWords );
}
@@ -2669,7 +2797,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
{
printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
nFrames, nWords, pCex->iPo, pCex->iFrame );
- status = Ssw_SmlRunCounterExample( pMan, (Ssw_Cex_t *)pCex );
+ status = Ssw_SmlRunCounterExample( pMan, pCex );
if ( status == 0 )
printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
}
@@ -2762,15 +2890,15 @@ Abc_Ntk_t * Abc_NtkDarEnlarge( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
SeeAlso []
***********************************************************************/
-void Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fVerbose )
-{
+int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fVerbose, int fVeryVerbose )
+{
Aig_Man_t * pMan, * pTemp;
int clkTotal = clock();
int RetValue;
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
- return;
- RetValue = Saig_ManInduction( pTemp = pMan, nFramesMax, nConfMax, fVerbose );
+ return -1;
+ RetValue = Saig_ManInduction( pTemp = pMan, nFramesMax, nConfMax, fUnique, fUniqueAll, fVerbose, fVeryVerbose );
Aig_ManStop( pTemp );
if ( RetValue == 1 )
{
@@ -2787,6 +2915,7 @@ ABC_PRT( "Time", clock() - clkTotal );
printf( "Networks are UNDECIDED. " );
ABC_PRT( "Time", clock() - clkTotal );
}
+ return RetValue;
}
@@ -2801,7 +2930,7 @@ ABC_PRT( "Time", clock() - clkTotal );
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, Gia_ParAbs_t * pPars )
+Abc_Ntk_t * Abc_NtkDarCegar( Abc_Ntk_t * pNtk, Gia_ParAbs_t * pPars )
{
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
@@ -2810,8 +2939,29 @@ Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, Gia_ParAbs_t * pPars )
if ( pMan == NULL )
return NULL;
- Aig_ManSetRegNum( pMan, pMan->nRegs );
- pMan = Saig_ManProofAbstraction( pTemp = pMan, pPars );
+ if ( pPars->fConstr )
+ {
+ printf( "This option is currently not implemented.\n" );
+ Aig_ManStop( pMan );
+ return NULL;
+ }
+ if ( pPars->fConstr )
+ {
+ if ( Saig_ManDetectConstrTest(pMan) )
+ {
+ printf( "Performing abstraction while dynamically adding constraints...\n" );
+ pMan = Saig_ManDupUnfoldConstrs( pTemp = pMan );
+ Aig_ManStop( pTemp );
+ pMan = Saig_ManConCexAbstraction( pTemp = pMan, pPars );
+ }
+ else
+ {
+ printf( "Constraints are not available. Performing abstraction w/o constraints.\n" );
+ pMan = Saig_ManCexAbstraction( pTemp = pMan, pPars );
+ }
+ }
+ else
+ pMan = Saig_ManCexAbstraction( pTemp = pMan, pPars );
if ( pTemp->pSeqModel )
{
ABC_FREE( pNtk->pModel );
@@ -3024,16 +3174,17 @@ void Abc_NtkPrintSccs( Abc_Ntk_t * pNtk, int fVerbose )
SeeAlso []
***********************************************************************/
-void Abc_NtkDarPrintCone( Abc_Ntk_t * pNtk )
+int Abc_NtkDarPrintCone( Abc_Ntk_t * pNtk )
{
extern void Saig_ManPrintCones( Aig_Man_t * pAig );
Aig_Man_t * pMan;
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
- return;
+ return 0;
assert( Aig_ManRegNum(pMan) > 0 );
Saig_ManPrintCones( pMan );
Aig_ManStop( pMan );
+ return 1;
}
/**Function*************************************************************
@@ -3114,6 +3265,33 @@ Abc_Ntk_t * Abc_NtkPhaseAbstract( Abc_Ntk_t * pNtk, int nFrames, int nPref, int
SeeAlso []
***********************************************************************/
+int Abc_NtkPhaseFrameNum( Abc_Ntk_t * pNtk )
+{
+ extern int Saig_ManPhaseFrameNum( Aig_Man_t * p, Vec_Int_t * vInits );
+ Vec_Int_t * vInits;
+ Aig_Man_t * pMan;
+ int nFrames;
+ pMan = Abc_NtkToDar( pNtk, 0, 1 );
+ if ( pMan == NULL )
+ return 1;
+ vInits = Abc_NtkGetLatchValues(pNtk);
+ nFrames = Saig_ManPhaseFrameNum( pMan, vInits );
+ Vec_IntFree( vInits );
+ Aig_ManStop( pMan );
+ return nFrames;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs phase abstraction.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
Abc_Ntk_t * Abc_NtkDarSynchOne( Abc_Ntk_t * pNtk, int nWords, int fVerbose )
{
extern Aig_Man_t * Saig_SynchSequenceApply( Aig_Man_t * pAig, int nWords, int fVerbose );
@@ -3406,23 +3584,29 @@ 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 fReorderImage, int fVerbose )
+int Abc_NtkDarReach( Abc_Ntk_t * pNtk, Saig_ParBbr_t * pPars )
{
- 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;
+ int RetValue;
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
- return;
- Aig_ManVerifyUsingBdds( pMan, nBddMax, nIterMax, fPartition, fReorder, fReorderImage, fVerbose, 0 );
+ return -1;
+ RetValue = Aig_ManVerifyUsingBdds( pMan, pPars );
ABC_FREE( pNtk->pModel );
ABC_FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
Aig_ManStop( pMan );
+ return RetValue;
}
+ABC_NAMESPACE_IMPL_END
+
#include "amap.h"
#include "mio.h"
+ABC_NAMESPACE_IMPL_START
+
+
/**Function*************************************************************
Synopsis []
@@ -3436,15 +3620,15 @@ void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartitio
***********************************************************************/
Abc_Ntk_t * Amap_ManProduceNetwork( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMapping )
{
- extern void * Abc_FrameReadLibGen();
- Mio_Library_t * pLib = Abc_FrameReadLibGen();
+// extern void * Abc_FrameReadLibGen();
+ Mio_Library_t * pLib = (Mio_Library_t *)Abc_FrameReadLibGen();
Amap_Out_t * pRes;
Vec_Ptr_t * vNodesNew;
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pNodeNew, * pFaninNew;
int i, k, iPis, iPos, nDupGates;
// make sure gates exist in the current library
- Vec_PtrForEachEntry( vMapping, pRes, i )
+ Vec_PtrForEachEntry( Amap_Out_t *, vMapping, pRes, i )
if ( pRes->pName && Mio_LibraryReadGateByName( pLib, pRes->pName ) == NULL )
{
printf( "Current library does not contain gate \"%s\".\n", pRes->pName );
@@ -3455,7 +3639,7 @@ Abc_Ntk_t * Amap_ManProduceNetwork( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMapping )
pNtkNew->pManFunc = pLib;
iPis = iPos = 0;
vNodesNew = Vec_PtrAlloc( Vec_PtrSize(vMapping) );
- Vec_PtrForEachEntry( vMapping, pRes, i )
+ Vec_PtrForEachEntry( Amap_Out_t *, vMapping, pRes, i )
{
if ( pRes->Type == -1 )
pNodeNew = Abc_NtkCi( pNtkNew, iPis++ );
@@ -3468,7 +3652,7 @@ Abc_Ntk_t * Amap_ManProduceNetwork( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMapping )
}
for ( k = 0; k < pRes->nFans; k++ )
{
- pFaninNew = Vec_PtrEntry( vNodesNew, pRes->pFans[k] );
+ pFaninNew = (Abc_Obj_t *)Vec_PtrEntry( vNodesNew, pRes->pFans[k] );
Abc_ObjAddFanin( pNodeNew, pFaninNew );
}
Vec_PtrPush( vNodesNew, pNodeNew );
@@ -3477,7 +3661,7 @@ Abc_Ntk_t * Amap_ManProduceNetwork( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMapping )
assert( iPis == Abc_NtkCiNum(pNtkNew) );
assert( iPos == Abc_NtkCoNum(pNtkNew) );
// decouple the PO driver nodes to reduce the number of levels
- nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
+ nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
// if ( nDupGates && Map_ManReadVerbose(pMan) )
// printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
return pNtkNew;
@@ -3513,7 +3697,7 @@ Abc_Ntk_t * Abc_NtkDarAmap( Abc_Ntk_t * pNtk, Amap_Par_t * pPars )
Aig_ManStop( pMan );
if ( vMapping == NULL )
return NULL;
- pMem = Vec_PtrPop( vMapping );
+ pMem = (Aig_MmFlex_t *)Vec_PtrPop( vMapping );
pNtkAig = Amap_ManProduceNetwork( pNtk, vMapping );
Aig_MmFlexStop( pMem, 0 );
Vec_PtrFree( vMapping );
@@ -3539,8 +3723,149 @@ Abc_Ntk_t * Abc_NtkDarAmap( Abc_Ntk_t * pNtk, Amap_Par_t * pPars )
SeeAlso []
***********************************************************************/
+void Abc_NtkDarConstr( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nProps, int fStruct, int fOldAlgo, int fVerbose )
+{
+ Aig_Man_t * pMan;//, * pMan2;//, * pTemp;
+ assert( Abc_NtkIsStrash(pNtk) );
+ pMan = Abc_NtkToDar( pNtk, 0, 1 );
+ if ( pMan == NULL )
+ return;
+ if ( fStruct )
+ Saig_ManDetectConstrTest( pMan );
+ else
+ Saig_ManDetectConstrFuncTest( pMan, nFrames, nConfs, nProps, fOldAlgo, fVerbose );
+ Aig_ManStop( pMan );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs BDD-based reachability analysis.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarUnfold( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nProps, int fStruct, int fOldAlgo, int fVerbose )
+{
+ Abc_Ntk_t * pNtkAig;
+ Aig_Man_t * pMan, * pTemp;
+ assert( Abc_NtkIsStrash(pNtk) );
+ pMan = Abc_NtkToDar( pNtk, 0, 1 );
+ if ( pMan == NULL )
+ return NULL;
+ if ( fStruct )
+ pMan = Saig_ManDupUnfoldConstrs( pTemp = pMan );
+ else
+ pMan = Saig_ManDupUnfoldConstrsFunc( pTemp = pMan, nFrames, nConfs, nProps, fOldAlgo, fVerbose );
+ Aig_ManStop( pTemp );
+ if ( pMan == NULL )
+ return NULL;
+ pNtkAig = Abc_NtkFromAigPhase( pMan );
+ pNtkAig->pName = Extra_UtilStrsav(pMan->pName);
+ pNtkAig->pSpec = Extra_UtilStrsav(pMan->pSpec);
+ Aig_ManStop( pMan );
+ return pNtkAig;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs BDD-based reachability analysis.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarFold( Abc_Ntk_t * pNtk, int fCompl, int fVerbose )
+{
+ Abc_Ntk_t * pNtkAig;
+ Aig_Man_t * pMan, * pTemp;
+ assert( Abc_NtkIsStrash(pNtk) );
+ pMan = Abc_NtkToDar( pNtk, 0, 1 );
+ if ( pMan == NULL )
+ return NULL;
+ pMan = Saig_ManDupFoldConstrsFunc( pTemp = pMan, fCompl, fVerbose );
+ Aig_ManStop( pTemp );
+ pNtkAig = Abc_NtkFromAigPhase( pMan );
+ pNtkAig->pName = Extra_UtilStrsav(pMan->pName);
+ pNtkAig->pSpec = Extra_UtilStrsav(pMan->pSpec);
+ Aig_ManStop( pMan );
+ return pNtkAig;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs BDD-based reachability analysis.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkDarConstrProfile( Abc_Ntk_t * pNtk, int fVerbose )
+{
+ extern int Ssw_ManProfileConstraints( Aig_Man_t * p, int nWords, int nFrames, int fVerbose );
+ extern Vec_Int_t * Saig_ManComputeSwitchProbs( Aig_Man_t * p, int nFrames, int nPref, int fProbOne );
+ Aig_Man_t * pMan;
+// Vec_Int_t * vProbOne;
+// Aig_Obj_t * pObj;
+// int i, Entry;
+ assert( Abc_NtkIsStrash(pNtk) );
+ assert( Abc_NtkConstrNum(pNtk) );
+ pMan = Abc_NtkToDar( pNtk, 0, 1 );
+ if ( pMan == NULL )
+ return;
+ // value in the init state
+// Abc_AigSetNodePhases( pNtk );
+/*
+ // derive probabilities
+ vProbOne = Saig_ManComputeSwitchProbs( pMan, 48, 16, 1 );
+ // iterate over the constraint outputs
+ Saig_ManForEachPo( pMan, pObj, i )
+ {
+ Entry = Vec_IntEntry( vProbOne, Aig_ObjId(pObj) );
+ if ( i < Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan) )
+ printf( "Primary output : ", i );
+ else
+ printf( "Constraint %3d : ", i-(Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan)) );
+ printf( "ProbOne = %f ", Aig_Int2Float(Entry) );
+ printf( "AllZeroValue = %d ", Aig_ObjPhase(pObj) );
+ printf( "\n" );
+ }
+*/
+ // double-check
+ Ssw_ManProfileConstraints( pMan, 16, 64, 1 );
+ printf( "TwoFrameSatValue = %d.\n", Ssw_ManSetConstrPhases(pMan, 2, NULL) );
+ // clean up
+// Vec_IntFree( vProbOne );
+ Aig_ManStop( pMan );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs BDD-based reachability analysis.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
void Abc_NtkDarTest( Abc_Ntk_t * pNtk )
{
+// extern void Saig_ManDetectConstr( Aig_Man_t * p );
+// extern void Saig_ManDetectConstrFuncTest( Aig_Man_t * p );
+ extern void Saig_ManFoldConstrTest( Aig_Man_t * pAig );
+
+
// extern void Fsim_ManTest( Aig_Man_t * pAig );
extern Vec_Int_t * Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose, Aig_Man_t ** ppMiter );
// Vec_Int_t * vPairs;
@@ -3571,8 +3896,24 @@ Aig_ManPrintStats( pMan );
Aig_ManStop( pMan );
Aig_ManStop( pMan2 );
*/
+// Ioa_WriteAigerBufferTest( pMan, "test.aig", 0, 0 );
+// Saig_ManFoldConstrTest( pMan );
+ {
+ extern void Saig_ManBmcSectionsTest( Aig_Man_t * p );
+ extern void Saig_ManBmcTerSimTest( Aig_Man_t * p );
+ extern void Saig_ManBmcSupergateTest( Aig_Man_t * p );
+ extern void Saig_ManBmcMappingTest( Aig_Man_t * p );
+// Saig_ManBmcSectionsTest( pMan );
+// Saig_ManBmcTerSimTest( pMan );
+// Saig_ManBmcSupergateTest( pMan );
+// Saig_ManBmcMappingTest( pMan );
+ }
+
+
// Saig_MvManSimulate( pMan, 1 );
+// Saig_ManDetectConstr( pMan );
+// Saig_ManDetectConstrFuncTest( pMan );
// Fsim_ManTest( pMan );
Aig_ManStop( pMan );
@@ -3624,7 +3965,7 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
return NULL;
/*
Aig_ManSetRegNum( pMan, pMan->nRegs );
- pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 0, 0, 0, -1, -1, 99, fUseBdds, fUseDprove, 0, 1 );
+ pMan = Saig_ManCexAbstraction( pTemp = pMan, 5, 10000, 0, 0, 0, -1, -1, 99, fUseBdds, fUseDprove, 0, 1 );
Aig_ManStop( pTemp );
if ( pMan == NULL )
return NULL;
@@ -3642,7 +3983,6 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
Aig_ManStop( pMan );
*/
-
pNtkAig = Abc_NtkFromDar( pNtk, pMan );
Aig_ManStop( pMan );
@@ -3655,3 +3995,5 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+