summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--abc.dsp40
-rw-r--r--src/aig/aig/aig.h1
-rw-r--r--src/aig/aig/aigDup.c24
-rw-r--r--src/aig/aig/aigFrames.c1
-rw-r--r--src/aig/aig/aigObj.c5
-rw-r--r--src/aig/aig/aigRepr.c2
-rw-r--r--src/aig/aig/aigRet.c2
-rw-r--r--src/aig/aig/aigScl.c2
-rw-r--r--src/aig/dar/darBalance.c7
-rw-r--r--src/aig/fra/fraSec.c2
-rw-r--r--src/aig/ioa/ioaReadAig.c51
-rw-r--r--src/aig/ntl/ntlExtract.c2
-rw-r--r--src/aig/ntl/ntlFraig.c8
-rw-r--r--src/aig/saig/saig.h4
-rw-r--r--src/aig/saig/saigHaig.c662
-rw-r--r--src/aig/saig/saigRetStep.c18
-rw-r--r--src/base/abci/abc.c92
-rw-r--r--src/base/abci/abcDar.c15
-rw-r--r--src/map/pcm/module.make0
-rw-r--r--src/map/ply/module.make0
20 files changed, 657 insertions, 281 deletions
diff --git a/abc.dsp b/abc.dsp
index ac1ef5f9..2831bf81 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -3245,6 +3245,26 @@ SOURCE=.\src\aig\mfx\mfxStrash.c
SOURCE=.\src\aig\mfx\mfxWin.c
# End Source File
# End Group
+# Begin Group "bbr"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\aig\bbr\bbr.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\bbr\bbrImage.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\bbr\bbrNtbdd.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\bbr\bbrReach.c
+# End Source File
+# End Group
# Begin Group "saig"
# PROP Default_Filter ""
@@ -3297,26 +3317,6 @@ SOURCE=.\src\aig\saig\saigScl.c
SOURCE=.\src\aig\saig\saigTrans.c
# End Source File
# End Group
-# Begin Group "bbr"
-
-# PROP Default_Filter ""
-# Begin Source File
-
-SOURCE=.\src\aig\bbr\bbr.h
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\bbr\bbrImage.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\bbr\bbrNtbdd.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\bbr\bbrReach.c
-# End Source File
-# End Group
# End Group
# End Group
# Begin Group "Header Files"
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 5861bc36..745de35d 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -152,6 +152,7 @@ struct Aig_Man_t_
Vec_Ptr_t * vOnehots;
Aig_Man_t * pManHaig;
int fCreatePios;
+ Vec_Int_t * vEquPairs;
// timing statistics
int time1;
int time2;
diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
index 1ec92968..db9e7288 100644
--- a/src/aig/aig/aigDup.c
+++ b/src/aig/aig/aigDup.c
@@ -51,9 +51,6 @@ Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p )
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
- pNew->nRegs = p->nRegs;
- pNew->nTruePis = p->nTruePis;
- pNew->nTruePos = p->nTruePos;
pNew->nAsserts = p->nAsserts;
if ( p->vFlopNums )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
@@ -90,6 +87,7 @@ Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p )
pObj->pData = pObjNew;
}
assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
+ Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
// pass the HAIG manager
if ( p->pManHaig != NULL )
{
@@ -152,9 +150,6 @@ Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p )
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
- pNew->nRegs = p->nRegs;
- pNew->nTruePis = p->nTruePis;
- pNew->nTruePos = p->nTruePos;
pNew->nAsserts = p->nAsserts;
if ( p->vFlopNums )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
@@ -184,6 +179,7 @@ Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p )
pObj->pData = pObjNew;
}
assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
+ Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
// pass the HAIG manager
if ( p->pManHaig != NULL )
{
@@ -216,9 +212,6 @@ Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p )
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
- pNew->nRegs = p->nRegs;
- pNew->nTruePis = p->nTruePis;
- pNew->nTruePos = p->nTruePos;
pNew->nAsserts = p->nAsserts;
if ( p->vFlopNums )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
@@ -256,6 +249,7 @@ Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p )
assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
if ( (nNodes = Aig_ManCleanup( pNew )) )
printf( "Aig_ManDupOrdered(): Cleanup after AIG duplication removed %d nodes.\n", nNodes );
+ Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
// duplicate the timing manager
if ( p->pManTime )
pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
@@ -292,7 +286,6 @@ Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p )
pNew->fCatchExor = 1;
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
- pNew->nRegs = p->nRegs;
pNew->nAsserts = p->nAsserts;
if ( p->vFlopNums )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
@@ -328,6 +321,7 @@ Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p )
pObj->pData = pObjNew;
}
Aig_ManCleanup( pNew );
+ Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
// duplicate the timing manager
if ( p->pManTime )
pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
@@ -394,7 +388,6 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p )
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
- pNew->nRegs = p->nRegs;
pNew->nAsserts = p->nAsserts;
if ( p->vFlopNums )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
@@ -435,6 +428,7 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p )
assert( p->pEquivs != NULL || 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 );
+ Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
// duplicate the timing manager
if ( p->pManTime )
pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
@@ -541,7 +535,6 @@ Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Aig_Man_t * pGuide )
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
- pNew->nRegs = p->nRegs;
pNew->nAsserts = p->nAsserts;
if ( p->vFlopNums )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
@@ -584,6 +577,7 @@ Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Aig_Man_t * pGuide )
// 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 );
+ Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
// duplicate the timing manager
if ( p->pManTime )
pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
@@ -614,7 +608,6 @@ Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p )
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
- pNew->nRegs = p->nRegs;
pNew->nAsserts = p->nAsserts;
if ( p->vFlopNums )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
@@ -658,6 +651,7 @@ Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p )
assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
// if ( (nNodes = Aig_ManCleanup( pNew )) )
// printf( "Aig_ManDupLevelized(): Cleanup after AIG duplication removed %d nodes.\n", nNodes );
+ Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
// duplicate the timing manager
if ( p->pManTime )
pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
@@ -745,7 +739,6 @@ Aig_Man_t * Aig_ManDupRepres( Aig_Man_t * p )
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
- pNew->nRegs = p->nRegs;
if ( p->vFlopNums )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
// map the const and primary inputs
@@ -766,6 +759,7 @@ Aig_Man_t * Aig_ManDupRepres( Aig_Man_t * p )
else
assert( 0 );
}
+ Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
// check the new manager
if ( !Aig_ManCheck(pNew) )
printf( "Aig_ManDupRepres: Check has failed.\n" );
@@ -818,7 +812,6 @@ Aig_Man_t * Aig_ManDupRepresDfs( Aig_Man_t * p )
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
- pNew->nRegs = p->nRegs;
if ( p->vFlopNums )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
// map the const and primary inputs
@@ -839,6 +832,7 @@ Aig_Man_t * Aig_ManDupRepresDfs( Aig_Man_t * p )
else
assert( 0 );
}
+ Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
// check the new manager
if ( !Aig_ManCheck(pNew) )
printf( "Aig_ManDupRepresDfs: Check has failed.\n" );
diff --git a/src/aig/aig/aigFrames.c b/src/aig/aig/aigFrames.c
index f8bc4bda..4cd23290 100644
--- a/src/aig/aig/aigFrames.c
+++ b/src/aig/aig/aigFrames.c
@@ -117,6 +117,7 @@ Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int
pObjNew = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Frames(pObjMap,nFs,pObj,fEnlarge?0:nFs-1) );
Aig_ObjSetFrames( pObjMap, nFs, pObj, nFs-1, pObjNew );
}
+ Aig_ManSetRegNum( pFrames, Aig_ManRegNum(pAig) );
}
Aig_ManCleanup( pFrames );
// return the new manager
diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c
index b5a404ab..86117f10 100644
--- a/src/aig/aig/aigObj.c
+++ b/src/aig/aig/aigObj.c
@@ -473,9 +473,10 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
// printf( "Setting HAIG node %d equivalent to HAIG node %d (over = %d).\n",
// pObjNewR->pHaig->Id, pObjOld->pHaig->Id, pObjNewR->pHaig->pHaig != NULL );
assert( pObjNewR->pHaig != NULL );
-// assert( pObjNewR->pHaig->pHaig == NULL );
assert( !Aig_IsComplement(pObjNewR->pHaig) );
- pObjNewR->pHaig->pHaig = pObjOld->pHaig;
+ assert( p->pManHaig->vEquPairs != NULL );
+ Vec_IntPush( p->pManHaig->vEquPairs, pObjNewR->pHaig->Id );
+ Vec_IntPush( p->pManHaig->vEquPairs, pObjOld->pHaig->Id );
}
else
pObjOld->pHaig = pObjNewR->pHaig? pObjNewR->pHaig : pObjOld->pHaig;
diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c
index 54ab0a33..b0605c1e 100644
--- a/src/aig/aig/aigRepr.c
+++ b/src/aig/aig/aigRepr.c
@@ -270,7 +270,6 @@ Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p, int fOrdered )
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
- pNew->nRegs = p->nRegs;
if ( p->vFlopNums )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
// map the const and primary inputs
@@ -294,6 +293,7 @@ Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p, int fOrdered )
// transfer the POs
Aig_ManForEachPo( p, pObj, i )
Aig_ObjCreatePo( pNew, Aig_ObjChild0Repr(p, pObj) );
+ Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
// check the new manager
if ( !Aig_ManCheck(pNew) )
printf( "Aig_ManDupRepr: Check has failed.\n" );
diff --git a/src/aig/aig/aigRet.c b/src/aig/aig/aigRet.c
index e20b1d4f..4641318a 100644
--- a/src/aig/aig/aigRet.c
+++ b/src/aig/aig/aigRet.c
@@ -809,7 +809,7 @@ Aig_Man_t * Rtm_ManToAig( Rtm_Man_t * pRtm )
// assert( Aig_Regular(pObjNew)->nRefs > 0 );
}
free( pLatches );
- pNew->nRegs = nLatches;
+ Aig_ManSetRegNum( pNew, nLatches );
// remove useless nodes
Aig_ManCleanup( pNew );
if ( !Aig_ManCheck( pNew ) )
diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c
index 1474fcd5..2adcabfb 100644
--- a/src/aig/aig/aigScl.c
+++ b/src/aig/aig/aigScl.c
@@ -49,7 +49,6 @@ Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap )
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
- pNew->nRegs = p->nRegs;
pNew->nAsserts = p->nAsserts;
assert( p->vFlopNums == NULL || Vec_IntSize(p->vFlopNums) == p->nRegs );
if ( p->vFlopNums )
@@ -101,6 +100,7 @@ Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap )
Aig_ManForEachPo( p, pObj, i )
Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
assert( Aig_ManNodeNum(p) >= Aig_ManNodeNum(pNew) );
+ Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
// check the resulting network
if ( !Aig_ManCheck(pNew) )
printf( "Aig_ManRemap(): The check has failed.\n" );
diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c
index 49ca963b..35da7fe2 100644
--- a/src/aig/dar/darBalance.c
+++ b/src/aig/dar/darBalance.c
@@ -359,9 +359,10 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t *
// printf( "Balancing HAIG node %d equivalent to HAIG node %d (over = %d).\n",
// pObjNewR->pHaig->Id, pObjOld->pHaig->Id, pObjNewR->pHaig->pHaig != NULL );
assert( pObjNewR->pHaig != NULL );
-// assert( pObjNewR->pHaig->pHaig == NULL );
assert( !Aig_IsComplement(pObjNewR->pHaig) );
- pObjNewR->pHaig->pHaig = pObjOld->pHaig;
+ assert( pNew->pManHaig->vEquPairs != NULL );
+ Vec_IntPush( pNew->pManHaig->vEquPairs, pObjNewR->pHaig->Id );
+ Vec_IntPush( pNew->pManHaig->vEquPairs, pObjOld->pHaig->Id );
}
else
Aig_Regular(pObjNew)->pHaig = pObjOld->pHaig;
@@ -390,7 +391,6 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
- pNew->nRegs = p->nRegs;
pNew->nAsserts = p->nAsserts;
if ( p->vFlopNums )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
@@ -463,6 +463,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
Vec_VecFree( vStore );
// remove dangling nodes
Aig_ManCleanup( pNew );
+ Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
// check the resulting AIG
if ( !Aig_ManCheck(pNew) )
printf( "Dar_ManBalance(): The check has failed.\n" );
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index ec6b7795..c01c7a84 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -57,7 +57,7 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p )
p->fVeryVerbose = 0; // enables very verbose reporting
p->TimeLimit = 0; // enables the timeout
// internal parameters
- p->fReportSolution = 1; // enables specialized format for reporting solution
+ p->fReportSolution = 0; // enables specialized format for reporting solution
}
/**Function*************************************************************
diff --git a/src/aig/ioa/ioaReadAig.c b/src/aig/ioa/ioaReadAig.c
index 498cdd30..342bd9fa 100644
--- a/src/aig/ioa/ioaReadAig.c
+++ b/src/aig/ioa/ioaReadAig.c
@@ -104,7 +104,7 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
Vec_Int_t * vLits = NULL;
Vec_Ptr_t * vNodes, * vDrivers;//, * vTerms;
Aig_Obj_t * pObj, * pNode0, * pNode1;
- Aig_Man_t * pManNew;
+ Aig_Man_t * pNew;
int nTotal, nInputs, nOutputs, nLatches, nAnds, nFileSize, i;//, iTerm, nDigits;
char * pContents, * pDrivers, * pSymbols, * pCur, * pName;//, * pType;
unsigned uLit0, uLit1, uLit;
@@ -143,39 +143,39 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
}
// allocate the empty AIG
- pManNew = Aig_ManStart( nAnds );
+ pNew = Aig_ManStart( nAnds );
pName = Ioa_FileNameGeneric( pFileName );
- pManNew->pName = Aig_UtilStrsav( pName );
-// pManNew->pSpec = Ioa_UtilStrsav( pFileName );
+ pNew->pName = Aig_UtilStrsav( pName );
+// pNew->pSpec = Ioa_UtilStrsav( pFileName );
free( pName );
// prepare the array of nodes
vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds );
- Vec_PtrPush( vNodes, Aig_ManConst0(pManNew) );
+ Vec_PtrPush( vNodes, Aig_ManConst0(pNew) );
// create the PIs
for ( i = 0; i < nInputs + nLatches; i++ )
{
- pObj = Aig_ObjCreatePi(pManNew);
+ pObj = Aig_ObjCreatePi(pNew);
Vec_PtrPush( vNodes, pObj );
}
/*
// create the POs
for ( i = 0; i < nOutputs + nLatches; i++ )
{
- pObj = Aig_ObjCreatePo(pManNew);
+ pObj = Aig_ObjCreatePo(pNew);
}
*/
// create the latches
- pManNew->nRegs = nLatches;
+ pNew->nRegs = nLatches;
/*
nDigits = Ioa_Base10Log( nLatches );
for ( i = 0; i < nLatches; i++ )
{
- pObj = Aig_ObjCreateLatch(pManNew);
+ pObj = Aig_ObjCreateLatch(pNew);
Aig_LatchSetInit0( pObj );
- pNode0 = Aig_ObjCreateBi(pManNew);
- pNode1 = Aig_ObjCreateBo(pManNew);
+ pNode0 = Aig_ObjCreateBi(pNew);
+ pNode1 = Aig_ObjCreateBo(pNew);
Aig_ObjAddFanin( pObj, pNode0 );
Aig_ObjAddFanin( pNode1, pObj );
Vec_PtrPush( vNodes, pNode1 );
@@ -211,7 +211,7 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
pNode1 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
assert( Vec_PtrSize(vNodes) == i + 1 + nInputs + nLatches );
- Vec_PtrPush( vNodes, Aig_And(pManNew, pNode0, pNode1) );
+ Vec_PtrPush( vNodes, Aig_And(pNew, pNode0, pNode1) );
}
// Bar_ProgressStop( pProgress );
@@ -259,9 +259,9 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
// create the POs
for ( i = 0; i < nOutputs; i++ )
- Aig_ObjCreatePo( pManNew, Vec_PtrEntry(vDrivers, nLatches + i) );
+ Aig_ObjCreatePo( pNew, Vec_PtrEntry(vDrivers, nLatches + i) );
for ( i = 0; i < nLatches; i++ )
- Aig_ObjCreatePo( pManNew, Vec_PtrEntry(vDrivers, i) );
+ Aig_ObjCreatePo( pNew, Vec_PtrEntry(vDrivers, i) );
Vec_PtrFree( vDrivers );
/*
@@ -275,11 +275,11 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
// get the terminal type
pType = pCur;
if ( *pCur == 'i' )
- vTerms = pManNew->vPis;
+ vTerms = pNew->vPis;
else if ( *pCur == 'l' )
- vTerms = pManNew->vBoxes;
+ vTerms = pNew->vBoxes;
else if ( *pCur == 'o' )
- vTerms = pManNew->vPos;
+ vTerms = pNew->vPos;
else
{
fprintf( stdout, "Wrong terminal type.\n" );
@@ -311,13 +311,13 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
}
// assign the remaining names
- Aig_ManForEachPi( pManNew, pObj, i )
+ Aig_ManForEachPi( pNew, pObj, i )
{
if ( pObj->pCopy ) continue;
Aig_ObjAssignName( pObj, Aig_ObjName(pObj), NULL );
Counter++;
}
- Aig_ManForEachLatchOutput( pManNew, pObj, i )
+ Aig_ManForEachLatchOutput( pNew, pObj, i )
{
if ( pObj->pCopy ) continue;
Aig_ObjAssignName( pObj, Aig_ObjName(pObj), NULL );
@@ -325,7 +325,7 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
Aig_ObjAssignName( Aig_ObjFanin0(Aig_ObjFanin0(pObj)), Aig_ObjName(pObj), "_in" );
Counter++;
}
- Aig_ManForEachPo( pManNew, pObj, i )
+ Aig_ManForEachPo( pNew, pObj, i )
{
if ( pObj->pCopy ) continue;
Aig_ObjAssignName( pObj, Aig_ObjName(pObj), NULL );
@@ -337,7 +337,7 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
else
{
// printf( "Ioa_ReadAiger(): I/O/register names are not given. Generating short names.\n" );
- Aig_ManShortNames( pManNew );
+ Aig_ManShortNames( pNew );
}
*/
@@ -346,16 +346,17 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
Vec_PtrFree( vNodes );
// remove the extra nodes
- Aig_ManCleanup( pManNew );
+ Aig_ManCleanup( pNew );
+ Aig_ManSetRegNum( pNew, Aig_ManRegNum(pNew) );
// check the result
- if ( fCheck && !Aig_ManCheck( pManNew ) )
+ if ( fCheck && !Aig_ManCheck( pNew ) )
{
printf( "Ioa_ReadAiger: The network check has failed.\n" );
- Aig_ManStop( pManNew );
+ Aig_ManStop( pNew );
return NULL;
}
- return pManNew;
+ return pNew;
}
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index a6fb58ae..be6626df 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -715,7 +715,7 @@ Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 )
pMiter = Aig_Miter(pAig, vPairs);
Vec_PtrFree( vPairs );
Aig_ObjPatchFanin0( pAig, Aig_ManPo(pAig,0), pMiter );
- pAig->nRegs = Ntl_ModelLatchNum( pRoot1 ) + Ntl_ModelLatchNum( pRoot2 );
+ Aig_ManSetRegNum( pAig, Ntl_ModelLatchNum( pRoot1 ) + Ntl_ModelLatchNum( pRoot2 ) );
Aig_ManCleanup( pAig );
return pAig;
}
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index 1b135212..6de41679 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -312,7 +312,7 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe
pAigCol = Ntl_ManCollapse( pNew, 1 );
// perform SCL for the given design
- pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
+ Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) );
pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, fVerbose );
Aig_ManStop( pTemp );
@@ -346,7 +346,7 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose )
pAigCol = Ntl_ManCollapse( pNew, 1 );
// perform SCL for the given design
- pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
+ Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) );
pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL, 0 );
Aig_ManStop( pTemp );
@@ -380,7 +380,7 @@ Ntl_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Fra_Ssw_t * pPars )
pAigCol = Ntl_ManCollapse( pNew, 1 );
// perform SCL for the given design
- pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
+ Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) );
pTemp = Fra_FraigInduction( pAigCol, pPars );
Aig_ManStop( pTemp );
@@ -555,7 +555,7 @@ Ntl_Man_t * Ntl_ManSsw2( Ntl_Man_t * p, Fra_Ssw_t * pPars )
Aig_Man_t * pAigRed, * pAigCol;
// collapse the AIG
pAigCol = Ntl_ManCollapse( p, 1 );
- pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
+ Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) );
// transform the collapsed AIG
pAigRed = Fra_FraigInduction( pAigCol, pPars );
Aig_ManStop( pAigRed );
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 8ec680b8..49d3f5ef 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -80,7 +80,7 @@ extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int n
/*=== saigCone.c ==========================================================*/
extern void Saig_ManPrintCones( Aig_Man_t * p );
/*=== saigHaig.c ==========================================================*/
-extern void Saig_ManHaigRecord( Aig_Man_t * p );
+extern Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose );
/*=== saigIoa.c ==========================================================*/
extern void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
extern Aig_Man_t * Saig_ManReadBlif( char * pFileName );
@@ -94,7 +94,7 @@ extern Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, in
extern Aig_Man_t * Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut );
extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
/*=== saigRetStep.c ==========================================================*/
-extern void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward );
+extern int Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward, int fAddBugs );
/*=== saigScl.c ==========================================================*/
extern void Saig_ManReportUselessRegisters( Aig_Man_t * pAig );
/*=== saigTrans.c ==========================================================*/
diff --git a/src/aig/saig/saigHaig.c b/src/aig/saig/saigHaig.c
index 64f4e943..8974ecb9 100644
--- a/src/aig/saig/saigHaig.c
+++ b/src/aig/saig/saigHaig.c
@@ -43,17 +43,19 @@
***********************************************************************/
void Aig_ManHaigSpeculate( Aig_Man_t * pFrames, Aig_Obj_t * pObj )
{
- Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew, * pMiter;
+ Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew;//, * pMiter;
+ Aig_Obj_t * pPo;
// skip nodes without representative
pObjRepr = pObj->pHaig;
if ( pObjRepr == NULL )
return;
- assert( pObjRepr->Id < pObj->Id );
+// assert( pObjRepr->Id < pObj->Id );
// get the new node
pObjNew = pObj->pData;
// get the new node of the representative
pObjReprNew = pObjRepr->pData;
// if this is the same node, no need to add constraints
+ assert( pObjNew != NULL && pObjReprNew != NULL );
if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
return;
// these are different nodes - perform speculative reduction
@@ -61,10 +63,19 @@ void Aig_ManHaigSpeculate( Aig_Man_t * pFrames, Aig_Obj_t * pObj )
// set the new node
pObj->pData = pObjNew2;
// add the constraint
- pMiter = Aig_Exor( pFrames, pObjNew, pObjReprNew );
- pMiter = Aig_NotCond( pMiter, !Aig_ObjPhaseReal(pMiter) );
- assert( Aig_ObjPhaseReal(pMiter) == 1 );
- Aig_ObjCreatePo( pFrames, pMiter );
+ if ( pObj->fMarkA )
+ return;
+// pMiter = Aig_Exor( pFrames, pObjNew, pObjReprNew );
+// pMiter = Aig_NotCond( pMiter, !Aig_ObjPhaseReal(pMiter) );
+// assert( Aig_ObjPhaseReal(pMiter) == 1 );
+// Aig_ObjCreatePo( pFrames, pMiter );
+ if ( Aig_ObjPhaseReal(pObjNew) != Aig_ObjPhaseReal(pObjReprNew) )
+ pObjReprNew = Aig_Not(pObjReprNew);
+ pPo = Aig_ObjCreatePo( pFrames, pObjNew );
+ Aig_ObjCreatePo( pFrames, pObjReprNew );
+
+ // remember the node corresponding to this PO
+ pPo->pData = pObj;
}
/**Function*************************************************************
@@ -98,27 +109,14 @@ Aig_Man_t * Aig_ManHaigFrames( Aig_Man_t * pHaig, int nFrames )
Aig_ManSetPioNumbers( pHaig );
for ( f = 0; f < nFrames; f++ )
{
- Aig_ManForEachObj( pHaig, pObj, i )
- {
- if ( Aig_ObjIsConst1(pObj) || Aig_ObjIsPo(pObj) )
- continue;
- if ( Saig_ObjIsPi(pHaig, pObj) )
- {
- pObj->pData = Aig_ObjCreatePi( pFrames );
- continue;
- }
- if ( Saig_ObjIsLo(pHaig, pObj) )
- {
- Aig_ManHaigSpeculate( pFrames, pObj );
- continue;
- }
- if ( Aig_ObjIsNode(pObj) )
- {
- pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
- Aig_ManHaigSpeculate( pFrames, pObj );
- continue;
- }
- assert( 0 );
+ // create primary inputs
+ Saig_ManForEachPi( pHaig, pObj, i )
+ pObj->pData = Aig_ObjCreatePi( pFrames );
+ // create internal nodes
+ Aig_ManForEachNode( pHaig, pObj, i )
+ {
+ pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+ Aig_ManHaigSpeculate( pFrames, pObj );
}
if ( f == nFrames - 2 )
nAssumptions = Aig_ManPoNum(pFrames);
@@ -148,76 +146,325 @@ Aig_Man_t * Aig_ManHaigFrames( Aig_Man_t * pHaig, int nFrames )
SeeAlso []
***********************************************************************/
-int Aig_ManHaigVerify2( Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
+int Aig_ManMapHaigNodes( Aig_Man_t * pHaig )
+{
+ Aig_Obj_t * pObj1, * pObj2;
+ int Id1, Id2, i, Counter = 0;
+ Aig_ManForEachObj( pHaig, pObj1, i )
+ pObj1->pHaig = NULL;
+ Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i )
+ {
+ Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i );
+ pObj1 = Aig_ManObj( pHaig, Id1 );
+ pObj2 = Aig_ManObj( pHaig, Id2 );
+ assert( pObj1 != pObj2 );
+ assert( !Aig_ObjIsPi(pObj1) || !Aig_ObjIsPi(pObj2) );
+ if ( Aig_ObjIsPi(pObj1) )
+ {
+ Counter += (int)(pObj2->pHaig != NULL);
+ pObj2->pHaig = pObj1;
+ }
+ else if ( Aig_ObjIsPi(pObj2) )
+ {
+ Counter += (int)(pObj1->pHaig != NULL);
+ pObj1->pHaig = pObj2;
+ }
+ else if ( pObj1->Id < pObj2->Id )
+ {
+ Counter += (int)(pObj2->pHaig != NULL);
+ pObj2->pHaig = pObj1;
+ }
+ else
+ {
+ Counter += (int)(pObj1->pHaig != NULL);
+ pObj1->pHaig = pObj2;
+ }
+ }
+// printf( "Overwrites %d out of %d.\n", Counter, Vec_IntSize(pHaig->vEquPairs)/2 );
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_ManHaigVerifyComb( Aig_Man_t * pHaig )
{
int nBTLimit = 0;
+ Vec_Ptr_t * vResult;
Aig_Man_t * pFrames;
Cnf_Dat_t * pCnf;
sat_solver * pSat;
- Aig_Obj_t * pObj;
- int i, Lit, RetValue, Counter;
+ Aig_Obj_t * pObj1, * pObj2;
+ int i, RetValue, RetValue1, RetValue2, Counter, Lits[2];
int clk = clock();
+ printf( "Filtering combinational cases:\n" );
+// return;
+
// create time frames with speculative reduction and convert them into CNF
clk = clock();
- pFrames = Aig_ManHaigFrames( pHaig, nFrames );
-Aig_ManShow( pFrames, 0, NULL );
+ pFrames = Aig_ManHaigFrames( pHaig, 1 );
- printf( "AIG: " );
- Aig_ManPrintStats( pAig );
- printf( "HAIG: " );
- Aig_ManPrintStats( pHaig );
- printf( "Frames: " );
+ // collect the HAIG nodes that were used to create spec miters
+ vResult = Vec_PtrAlloc( Aig_ManPoNum(pFrames)/2 );
+ Aig_ManForEachPo( pFrames, pObj1, i )
+ {
+ pObj2 = Aig_ManPo( pFrames, ++i );
+ Vec_PtrPush( vResult, pObj1->pData );
+ }
+
+ printf( "Frames: " );
Aig_ManPrintStats( pFrames );
- printf( "Additional frames stats: Assumptions = %d. Asserts = %d.\n",
- Aig_ManPoNum(pFrames) - pFrames->nAsserts, pFrames->nAsserts );
- pCnf = Cnf_DeriveSimple( pFrames, pFrames->nAsserts );
-PRT( "Preparation", clock() - clk );
+
+// pFrames = Dar_ManRwsat( pTemp = pFrames, 1, 0 );
+// Aig_ManStop( pTemp );
+
+ printf( "Frames: " );
+ Aig_ManPrintStats( pFrames );
+
+ printf( "Additional frames stats: Assumptions = %d. Asserts = %d. Pairs = %d.\n",
+ Aig_ManPoNum(pFrames)/2 - pFrames->nAsserts/2, pFrames->nAsserts/2, Vec_IntSize(pHaig->vEquPairs)/2 );
+// pCnf = Cnf_DeriveSimple( pFrames, Aig_ManPoNum(pFrames) );
+ pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) );
// pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts );
//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
- Saig_ManDumpBlif( pHaig, "haig_temp.blif" );
- Saig_ManDumpBlif( pFrames, "haig_temp_frames.blif" );
+// Saig_ManDumpBlif( pHaig, "haig_temp.blif" );
+// Saig_ManDumpBlif( pFrames, "haig_temp_frames.blif" );
// create the SAT solver to be used for this problem
pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
if ( pSat == NULL )
{
printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" );
- return -1;
+ return;
}
-
- // solve each output
+PRT( "Preparation", clock() - clk );
+
+
+ // check in the second timeframe
clk = clock();
- if ( pFrames->nAsserts == 0 )
+ Counter = 0;
+ printf( "Started solving ...\r" );
+ Aig_ManForEachPo( pFrames, pObj1, i )
{
- RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
- if ( RetValue != l_False )
- printf( "SAT solver is wrong\n" );
+ pObj2 = Aig_ManPo( pFrames, ++i );
+ assert( pObj1->fPhase == pObj2->fPhase );
+
+ Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
+ Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 1 );
+
+ RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)10, (sint64)0, (sint64)0, (sint64)0 );
+ if ( RetValue1 == l_False )
+ {
+ Lits[0] = lit_neg( Lits[0] );
+ Lits[1] = lit_neg( Lits[1] );
+ RetValue = sat_solver_addclause( pSat, Lits, Lits + 2 );
+ assert( RetValue );
+ }
+
+ Lits[0]++;
+ Lits[1]--;
+
+ RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)10, (sint64)0, (sint64)0, (sint64)0 );
+ if ( RetValue2 == l_False )
+ {
+ Lits[0] = lit_neg( Lits[0] );
+ Lits[1] = lit_neg( Lits[1] );
+ RetValue = sat_solver_addclause( pSat, Lits, Lits + 2 );
+ assert( RetValue );
+ }
+
+ if ( RetValue1 != l_False || RetValue2 != l_False )
+ {
+ Counter++;
+ }
+ else
+ {
+ pObj1 = Vec_PtrEntry( vResult, i/2 );
+ assert( pObj1->pHaig != NULL );
+ pObj1->fMarkA = 1;
+ }
+
+ if ( i % 50 == 1 )
+ printf( "Solving assertion %6d out of %6d.\r",
+ (i - (Aig_ManPoNum(pFrames) - pFrames->nAsserts))/2,
+ pFrames->nAsserts/2 );
+// if ( nClasses == 1000 )
+// break;
}
+ printf( " \r" );
+PRT( "Solving ", clock() - clk );
+ if ( Counter )
+ printf( "Verification failed for %d out of %d assertions.\n", Counter, pFrames->nAsserts/2 );
else
+ printf( "Verification is successful for all %d assertions.\n", pFrames->nAsserts/2 );
+
+ // clean up
+ Aig_ManStop( pFrames );
+ Cnf_DataFree( pCnf );
+ sat_solver_delete( pSat );
+ Vec_PtrFree( vResult );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_ManHaigVerify( Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
+{
+ int nBTLimit = 0;
+ Aig_Man_t * pFrames, * pTemp;
+ Cnf_Dat_t * pCnf;
+ sat_solver * pSat;
+ Aig_Obj_t * pObj1, * pObj2;
+ int i, RetValue1, RetValue2, Counter, Lits[2], nOvers;
+ int clk = clock();
+
+ nOvers = Aig_ManMapHaigNodes( pHaig );
+
+// if ( nFrames == 2 )
+// Aig_ManHaigVerifyComb( pHaig );
+
+ // create time frames with speculative reduction and convert them into CNF
+clk = clock();
+ pFrames = Aig_ManHaigFrames( pHaig, nFrames );
+ Aig_ManCleanMarkA( pHaig );
+
+ printf( "Frames: " );
+ Aig_ManPrintStats( pFrames );
+
+ pFrames = Dar_ManRwsat( pTemp = pFrames, 1, 0 );
+ Aig_ManStop( pTemp );
+
+ printf( "Frames synt:" );
+ Aig_ManPrintStats( pFrames );
+
+ printf( "Additional frames stats: Assumptions = %d. Assertions = %d. Pairs = %d. Over = %d.\n",
+ Aig_ManPoNum(pFrames)/2 - pFrames->nAsserts/2, pFrames->nAsserts/2, Vec_IntSize(pHaig->vEquPairs)/2, nOvers );
+// pCnf = Cnf_DeriveSimple( pFrames, Aig_ManPoNum(pFrames) );
+ pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) );
+
+// pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts );
+//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
+// Saig_ManDumpBlif( pHaig, "haig_temp.blif" );
+// Saig_ManDumpBlif( pFrames, "haig_temp_frames.blif" );
+ // create the SAT solver to be used for this problem
+ pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+ if ( pSat == NULL )
{
- Counter = 0;
- Aig_ManForEachPo( pFrames, pObj, i )
+ printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" );
+ return 0;
+ }
+
+ if ( nFrames == 2 )
+ {
+ // add clauses for the first frame
+ Aig_ManForEachPo( pFrames, pObj1, i )
{
- if ( i < Aig_ManPoNum(pFrames) - pFrames->nAsserts )
- continue;
- Lit = toLitCond( pCnf->pVarNums[pObj->Id], 1 );
- RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
- if ( RetValue != l_False )
- Counter++;
+ if ( i >= Aig_ManPoNum(pFrames) - pFrames->nAsserts )
+ break;
+
+ pObj2 = Aig_ManPo( pFrames, ++i );
+ assert( pObj1->fPhase == pObj2->fPhase );
+
+ Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
+ Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 1 );
+ if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
+ {
+ sat_solver_delete( pSat );
+ return 0;
+ }
+ Lits[0]++;
+ Lits[1]--;
+ if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
+ {
+ sat_solver_delete( pSat );
+ return 0;
+ }
}
-PRT( "Solving ", clock() - clk );
- if ( Counter )
- printf( "Verification failed for %d classes.\n", Counter );
- else
- printf( "Verification is successful.\n" );
+
+ if ( !sat_solver_simplify(pSat) )
+ {
+ sat_solver_delete( pSat );
+ return 0;
+ }
+ }
+PRT( "Preparation", clock() - clk );
+
+
+ // check in the second timeframe
+clk = clock();
+ Counter = 0;
+ printf( "Started solving ...\r" );
+ Aig_ManForEachPo( pFrames, pObj1, i )
+ {
+ if ( i < Aig_ManPoNum(pFrames) - pFrames->nAsserts )
+ continue;
+
+ pObj2 = Aig_ManPo( pFrames, ++i );
+ assert( pObj1->fPhase == pObj2->fPhase );
+
+ Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
+ Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 1 );
+
+ RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+ if ( RetValue1 == l_False )
+ {
+ Lits[0] = lit_neg( Lits[0] );
+ Lits[1] = lit_neg( Lits[1] );
+// RetValue = sat_solver_addclause( pSat, Lits, Lits + 2 );
+// assert( RetValue );
+ }
+
+ Lits[0]++;
+ Lits[1]--;
+
+ RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+ if ( RetValue2 == l_False )
+ {
+ Lits[0] = lit_neg( Lits[0] );
+ Lits[1] = lit_neg( Lits[1] );
+// RetValue = sat_solver_addclause( pSat, Lits, Lits + 2 );
+// assert( RetValue );
+ }
+
+ if ( RetValue1 != l_False || RetValue2 != l_False )
+ Counter++;
+
+ if ( i % 50 == 1 )
+ printf( "Solving assertion %6d out of %6d.\r",
+ (i - (Aig_ManPoNum(pFrames) - pFrames->nAsserts))/2,
+ pFrames->nAsserts/2 );
+// if ( nClasses == 1000 )
+// break;
}
+ printf( " \r" );
+PRT( "Solving ", clock() - clk );
+ if ( Counter )
+ printf( "Verification failed for %d out of %d assertions.\n", Counter, pFrames->nAsserts/2 );
+ else
+ printf( "Verification is successful for all %d assertions.\n", pFrames->nAsserts/2 );
// clean up
Aig_ManStop( pFrames );
Cnf_DataFree( pCnf );
sat_solver_delete( pSat );
- return Counter;
+ return 1;
}
/**Function*************************************************************
@@ -231,22 +478,28 @@ PRT( "Solving ", clock() - clk );
SeeAlso []
***********************************************************************/
-int Aig_ManHaigVerify( Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
+int Aig_ManHaigVerify2( Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
{
int nBTLimit = 0;
Cnf_Dat_t * pCnf;
sat_solver * pSat;
- Aig_Obj_t * pObj, * pRepr;
- int i, RetValue, Counter, Lits[2];
- int nClasses = 0;
+ Aig_Obj_t * pObj1, * pObj2;
+ int i, RetValue1, RetValue2, Counter, Lits[2];
int clk = clock();
+ int Delta;
+ int Id1, Id2;
assert( nFrames == 1 || nFrames == 2 );
clk = clock();
pCnf = Cnf_DeriveSimple( pHaig, Aig_ManPoNum(pHaig) );
+// Aig_ManForEachObj( pHaig, pObj, i )
+// printf( "%d=%d ", pObj->Id, pCnf->pVarNums[pObj->Id] );
+// printf( "\n" );
+
// create the SAT solver to be used for this problem
pSat = Cnf_DataWriteIntoSolver( pCnf, nFrames, 0 );
+//Sat_SolverWriteDimacs( pSat, "1.cnf", NULL, NULL, 0 );
if ( pSat == NULL )
{
printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" );
@@ -255,16 +508,15 @@ clk = clock();
if ( nFrames == 2 )
{
- // add clauses for the first frame
- Aig_ManForEachObj( pHaig, pObj, i )
+ Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i )
{
- pRepr = pObj->pHaig;
- if ( pRepr == NULL )
- continue;
- if ( pRepr->fPhase ^ pObj->fPhase )
+ Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i );
+ pObj1 = Aig_ManObj( pHaig, Id1 );
+ pObj2 = Aig_ManObj( pHaig, Id2 );
+ if ( pObj1->fPhase ^ pObj2->fPhase )
{
- Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
- Lits[1] = toLitCond( pCnf->pVarNums[pRepr->Id], 0 );
+ Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
+ Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 0 );
if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
{
sat_solver_delete( pSat );
@@ -280,8 +532,8 @@ clk = clock();
}
else
{
- Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
- Lits[1] = toLitCond( pCnf->pVarNums[pRepr->Id], 1 );
+ Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
+ Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 1 );
if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
{
sat_solver_delete( pSat );
@@ -297,12 +549,10 @@ clk = clock();
}
}
- // add clauses for the next timeframe
- {
- int nLitsAll = 2 * pCnf->nVars;
- int * pLits = pCnf->pClauses[0];
- for ( i = 0; i < pCnf->nLiterals; i++ )
- pLits[i] += nLitsAll;
+ if ( !sat_solver_simplify(pSat) )
+ {
+ sat_solver_delete( pSat );
+ return 0;
}
}
PRT( "Preparation", clock() - clk );
@@ -311,51 +561,53 @@ PRT( "Preparation", clock() - clk );
// check in the second timeframe
clk = clock();
Counter = 0;
- nClasses = 0;
- Aig_ManForEachObj( pHaig, pObj, i )
+ Delta = (nFrames == 2)? pCnf->nVars : 0;
+ Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i )
{
- pRepr = pObj->pHaig;
- if ( pRepr == NULL )
- continue;
- nClasses++;
- if ( pRepr->fPhase ^ pObj->fPhase )
+ Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i );
+ pObj1 = Aig_ManObj( pHaig, Id1 );
+ pObj2 = Aig_ManObj( pHaig, Id2 );
+ if ( pObj1->fPhase ^ pObj2->fPhase )
{
- Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
- Lits[1] = toLitCond( pCnf->pVarNums[pRepr->Id], 0 );
+ Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id]+Delta, 0 );
+ Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id]+Delta, 0 );
- RetValue = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
- if ( RetValue != l_False )
- Counter++;
+ RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
Lits[0]++;
Lits[1]++;
- RetValue = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
- if ( RetValue != l_False )
+ RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+
+ if ( RetValue1 != l_False || RetValue2 != l_False )
Counter++;
}
else
{
- Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
- Lits[1] = toLitCond( pCnf->pVarNums[pRepr->Id], 1 );
+ Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id]+Delta, 0 );
+ Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id]+Delta, 1 );
- RetValue = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
- if ( RetValue != l_False )
- Counter++;
+ RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
Lits[0]++;
Lits[1]--;
- RetValue = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
- if ( RetValue != l_False )
+ RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+
+ if ( RetValue1 != l_False || RetValue2 != l_False )
Counter++;
}
+ if ( i % 50 == 1 )
+ printf( "Solving assertion %6d out of %6d.\r", i/2, Vec_IntSize(pHaig->vEquPairs)/2 );
+
+// if ( i / 2 > 1000 )
+// break;
}
PRT( "Solving ", clock() - clk );
if ( Counter )
- printf( "Verification failed for %d out of %d classes.\n", Counter, nClasses );
+ printf( "Verification failed for %d out of %d classes.\n", Counter, Vec_IntSize(pHaig->vEquPairs)/2 );
else
- printf( "Verification is successful for all %d classes.\n", nClasses );
+ printf( "Verification is successful for all %d classes.\n", Vec_IntSize(pHaig->vEquPairs)/2 );
Cnf_DataFree( pCnf );
sat_solver_delete( pSat );
@@ -373,96 +625,174 @@ PRT( "Solving ", clock() - clk );
SeeAlso []
***********************************************************************/
-void Saig_ManHaigRecord( Aig_Man_t * p )
+Aig_Man_t * Saig_ManHaigDump( Aig_Man_t * pHaig )
+{
+ Vec_Ptr_t * vTemp;
+ Aig_Obj_t * pObj, * pObj1, * pObj2, * pMiter;
+ int Id1, Id2, i;
+ // remove regular POs
+ Aig_ManSetPioNumbers( pHaig );
+ vTemp = Vec_PtrAlloc( Saig_ManRegNum(pHaig) );
+ Aig_ManForEachPo( pHaig, pObj, i )
+ {
+ if ( Saig_ObjIsPo(pHaig, pObj) )
+ {
+ Aig_ObjDisconnect( pHaig, pObj );
+ Vec_PtrWriteEntry( pHaig->vObjs, pObj->Id, NULL );
+ }
+ else
+ {
+ Vec_PtrPush( vTemp, pObj );
+ }
+ }
+ Vec_PtrShrink( pHaig->vPos, 0 );
+ pHaig->nObjs[AIG_OBJ_PO] = Vec_PtrSize( vTemp );
+ // add new POs
+ Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i )
+ {
+ Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i );
+ pObj1 = Aig_ManObj( pHaig, Id1 );
+ pObj2 = Aig_ManObj( pHaig, Id2 );
+ assert( pObj1 != pObj2 );
+ assert( !Aig_ObjIsPi(pObj1) || !Aig_ObjIsPi(pObj2) );
+ pMiter = Aig_Exor( pHaig, pObj1, pObj2 );
+ pMiter = Aig_NotCond( pMiter, Aig_ObjPhaseReal(pMiter) );
+ assert( Aig_ObjPhaseReal(pMiter) == 0 );
+ Aig_ObjCreatePo( pHaig, pMiter );
+ }
+ printf( "Added %d property outputs.\n", Vec_IntSize(pHaig->vEquPairs)/2 );
+ // add the registers
+ Vec_PtrForEachEntry( vTemp, pObj, i )
+ Vec_PtrPush( pHaig->vPos, pObj );
+ Vec_PtrFree( vTemp );
+ assert( pHaig->nObjs[AIG_OBJ_PO] == Vec_PtrSize(pHaig->vPos) );
+ Aig_ManCleanup( pHaig );
+ Aig_ManSetRegNum( pHaig, pHaig->nRegs );
+// return pHaig;
+
+ printf( "HAIG: " );
+ Aig_ManPrintStats( pHaig );
+ printf( "HAIG is written into file \"haig.blif\".\n" );
+ Saig_ManDumpBlif( pHaig, "haig.blif" );
+
+ Vec_IntFree( pHaig->vEquPairs );
+ Aig_ManStop( pHaig );
+ return NULL;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose )
{
- extern void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward );
- int fUseRetiming = (int)( Aig_ManRegNum(p) > 0 );
+ int fSeqHaig = (int)( Aig_ManRegNum(p) > 0 );
Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
Aig_Man_t * pNew, * pTemp;
Aig_Obj_t * pObj;
- int i;
+ int i, k, nStepsReal, clk = clock();
Dar_ManDefaultRwrParams( pParsRwr );
+
+clk = clock();
// duplicate this manager
pNew = Aig_ManDupSimple( p );
-
// create its history AIG
pNew->pManHaig = Aig_ManDupSimple( pNew );
Aig_ManForEachObj( pNew, pObj, i )
pObj->pHaig = pObj->pData;
// remove structural hashing table
Aig_TableClear( pNew->pManHaig );
+ pNew->pManHaig->vEquPairs = Vec_IntAlloc( 10000 );
+PRT( "HAIG setup time", clock() - clk );
- // perform retiming
- if ( fUseRetiming )
+clk = clock();
+ if ( fSeqHaig )
{
-/*
- // perform balancing
- pNew = Dar_ManBalance( pTemp = pNew, 0 );
- assert( pNew->pManHaig != NULL );
- assert( pTemp->pManHaig == NULL );
- Aig_ManStop( pTemp );
-
- // perform rewriting
- Dar_ManRewrite( pNew, pParsRwr );
- pNew = Aig_ManDupDfs( pTemp = pNew );
- assert( pNew->pManHaig != NULL );
- assert( pTemp->pManHaig == NULL );
- Aig_ManStop( pTemp );
-*/
- // perform retiming
- Saig_ManRetimeSteps( pNew, 1000, 1 );
- pNew = Aig_ManDupSimpleDfs( pTemp = pNew );
- assert( pNew->pManHaig != NULL );
- assert( pTemp->pManHaig == NULL );
- Aig_ManStop( pTemp );
-
- // perform balancing
- pNew = Dar_ManBalance( pTemp = pNew, 0 );
- assert( pNew->pManHaig != NULL );
- assert( pTemp->pManHaig == NULL );
- Aig_ManStop( pTemp );
-
- // perform rewriting
- Dar_ManRewrite( pNew, pParsRwr );
- pNew = Aig_ManDupDfs( pTemp = pNew );
- assert( pNew->pManHaig != NULL );
- assert( pTemp->pManHaig == NULL );
- Aig_ManStop( pTemp );
+ if ( fRetimingOnly )
+ {
+ // perform retiming
+ nStepsReal = Saig_ManRetimeSteps( pNew, nSteps, 1, fAddBugs );
+ pNew = Aig_ManDupSimpleDfs( pTemp = pNew );
+ Aig_ManStop( pTemp );
+ printf( "Performed %d retiming moves.\n", nStepsReal );
+ }
+ else
+ {
+ for ( k = 0; k < nIters; k++ )
+ {
+ // perform balancing
+ pNew = Dar_ManBalance( pTemp = pNew, 0 );
+ Aig_ManStop( pTemp );
+
+ // perform rewriting
+ Dar_ManRewrite( pNew, pParsRwr );
+ pNew = Aig_ManDupDfs( pTemp = pNew );
+ Aig_ManStop( pTemp );
+
+ // perform retiming
+ nStepsReal = Saig_ManRetimeSteps( pNew, nSteps, 1, fAddBugs );
+ pNew = Aig_ManDupSimpleDfs( pTemp = pNew );
+ Aig_ManStop( pTemp );
+ printf( "Performed %d retiming moves.\n", nStepsReal );
+ }
+ }
}
else
{
- // perform balancing
- pNew = Dar_ManBalance( pTemp = pNew, 0 );
- assert( pNew->pManHaig != NULL );
- assert( pTemp->pManHaig == NULL );
- Aig_ManStop( pTemp );
-/*
- // perform rewriting
- Dar_ManRewrite( pNew, pParsRwr );
- pNew = Aig_ManDupDfs( pTemp = pNew );
- assert( pNew->pManHaig != NULL );
- assert( pTemp->pManHaig == NULL );
- Aig_ManStop( pTemp );
-*/
+ for ( k = 0; k < nIters; k++ )
+ {
+ // perform balancing
+ pNew = Dar_ManBalance( pTemp = pNew, 0 );
+ Aig_ManStop( pTemp );
+
+ // perform rewriting
+ Dar_ManRewrite( pNew, pParsRwr );
+ pNew = Aig_ManDupDfs( pTemp = pNew );
+ Aig_ManStop( pTemp );
+ }
}
+PRT( "Synthesis time ", clock() - clk );
// use the haig for verification
- Aig_ManAntiCleanup( pNew->pManHaig );
+// Aig_ManAntiCleanup( pNew->pManHaig );
Aig_ManSetRegNum( pNew->pManHaig, pNew->pManHaig->nRegs );
//Aig_ManShow( pNew->pManHaig, 0, NULL );
- printf( "AIG: " );
+ printf( "AIG before: " );
+ Aig_ManPrintStats( p );
+ printf( "AIG after: " );
Aig_ManPrintStats( pNew );
- printf( "HAIG: " );
+ printf( "HAIG: " );
Aig_ManPrintStats( pNew->pManHaig );
- if ( !Aig_ManHaigVerify( pNew, pNew->pManHaig, 1+fUseRetiming ) )
- printf( "Constructing SAT solver has failed.\n" );
+ if ( fUseCnf )
+ {
+ if ( !Aig_ManHaigVerify2( pNew, pNew->pManHaig, 1+fSeqHaig ) )
+ printf( "Constructing SAT solver has failed.\n" );
+ }
+ else
+ {
+ if ( !Aig_ManHaigVerify( pNew, pNew->pManHaig, 1+fSeqHaig ) )
+ printf( "Constructing SAT solver has failed.\n" );
+ }
+ Saig_ManHaigDump( pNew->pManHaig );
+ pNew->pManHaig = NULL;
+ return pNew;
+/*
// cleanup
+ Vec_IntFree( pNew->pManHaig->vEquPairs );
Aig_ManStop( pNew->pManHaig );
pNew->pManHaig = NULL;
- Aig_ManStop( pNew );
+ return pNew;
+*/
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/saig/saigRetStep.c b/src/aig/saig/saigRetStep.c
index f7c27a93..fe726702 100644
--- a/src/aig/saig/saigRetStep.c
+++ b/src/aig/saig/saigRetStep.c
@@ -39,7 +39,7 @@
SeeAlso []
***********************************************************************/
-Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj )
+Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj, int fMakeBug )
{
Aig_Obj_t * pFanin0, * pFanin1;
Aig_Obj_t * pInput0, * pInput1;
@@ -72,6 +72,12 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj )
// get the condition when the register should be complemetned
fCompl = Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj);
+ if ( fMakeBug )
+ {
+ printf( "Introducing bug during retiming.\n" );
+ pInput1 = Aig_Not( pInput1 );
+ }
+
// create new node
pObjNew = Aig_And( p, pInput0, pInput1 );
@@ -162,7 +168,7 @@ Aig_Obj_t * Saig_ManRetimeNodeBwd( Aig_Man_t * p, Aig_Obj_t * pObjLo )
SeeAlso []
***********************************************************************/
-void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward )
+int Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward, int fAddBugs )
{
Aig_Obj_t * pObj, * pObjNew;
int RetValue, s, i;
@@ -175,12 +181,15 @@ void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward )
{
Aig_ManForEachNode( p, pObj, i )
{
- pObjNew = Saig_ManRetimeNodeFwd( p, pObj );
+ pObjNew = Saig_ManRetimeNodeFwd( p, pObj, fAddBugs && (s == 10) );
+// pObjNew = Saig_ManRetimeNodeFwd( p, pObj, 0 );
if ( pObjNew == NULL )
continue;
Aig_ObjReplace( p, pObj, pObjNew, 0 );
break;
}
+ if ( i == Vec_PtrSize(p->vObjs) )
+ break;
}
}
else
@@ -195,6 +204,8 @@ void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward )
Aig_ObjReplace( p, pObj, pObjNew, 0 );
break;
}
+ if ( i == Vec_PtrSize(p->vObjs) )
+ break;
}
}
p->fCreatePios = 0;
@@ -202,6 +213,7 @@ void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward )
RetValue = Aig_ManCleanup( p );
assert( RetValue == 0 );
Aig_ManSetRegNum( p, p->nRegs );
+ return s;
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 8d27c0d2..fc4056a4 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -149,9 +149,9 @@ static int Abc_CommandFraigClean ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandFraigSweep ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFraigDress ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandHaigStart ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandHaigStop ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandHaigUse ( Abc_Frame_t * pAbc, int argc, char ** argv );
+//static int Abc_CommandHaigStart ( Abc_Frame_t * pAbc, int argc, char ** argv );
+//static int Abc_CommandHaigStop ( Abc_Frame_t * pAbc, int argc, char ** argv );
+//static int Abc_CommandHaigUse ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRecStart ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRecStop ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -404,9 +404,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Fraiging", "fraig_sweep", Abc_CommandFraigSweep, 1 );
Cmd_CommandAdd( pAbc, "Fraiging", "dress", Abc_CommandFraigDress, 1 );
- Cmd_CommandAdd( pAbc, "Choicing", "haig_start", Abc_CommandHaigStart, 0 );
- Cmd_CommandAdd( pAbc, "Choicing", "haig_stop", Abc_CommandHaigStop, 0 );
- Cmd_CommandAdd( pAbc, "Choicing", "haig_use", Abc_CommandHaigUse, 1 );
+// Cmd_CommandAdd( pAbc, "Choicing", "haig_start", Abc_CommandHaigStart, 0 );
+// Cmd_CommandAdd( pAbc, "Choicing", "haig_stop", Abc_CommandHaigStop, 0 );
+// Cmd_CommandAdd( pAbc, "Choicing", "haig_use", Abc_CommandHaigUse, 1 );
Cmd_CommandAdd( pAbc, "Choicing", "rec_start", Abc_CommandRecStart, 0 );
Cmd_CommandAdd( pAbc, "Choicing", "rec_stop", Abc_CommandRecStop, 0 );
@@ -7505,7 +7505,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk );
// extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
// extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
- extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
+ extern Abc_Ntk_t * Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose );
// extern void Abc_NtkDarTestBlif( char * pFileName );
// extern Abc_Ntk_t * Abc_NtkDarPartition( Abc_Ntk_t * pNtk );
// extern Abc_Ntk_t * Abc_NtkTestExor( Abc_Ntk_t * pNtk, int fVerbose );
@@ -7519,13 +7519,13 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
-// printf( "This command is temporarily disabled.\n" );
-// return 0;
+ printf( "This command is temporarily disabled.\n" );
+ return 0;
// set defaults
fVeryVerbose = 0;
fVerbose = 1;
- fBmc = 1;
+ fBmc = 0;
nFrames = 1;
nLevels = 200;
Extra_UtilGetoptReset();
@@ -7685,7 +7685,6 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
*/
-// Abc_NtkDarHaigRecord( pNtk );
// Abc_NtkDarClau( pNtk, nFrames, nLevels, fBmc, fVerbose, fVeryVerbose );
/*
if ( globalUtilOptind != 1 )
@@ -7699,11 +7698,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// Abc_NtkDarPartition( pNtk );
//Abc_NtkDarTest( pNtk );
-
-Abc_NtkDarHaigRecord( pNtk );
-return 0;
-
- pNtkRes = Abc_NtkDarRetimeStep( pNtk, 0 );
+// pNtkRes = Abc_NtkDarRetimeStep( pNtk, 0 );
+ pNtkRes = Abc_NtkDarHaigRecord( pNtk, 3, 3000, 0, 0, 0, 0 );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
@@ -7713,7 +7709,7 @@ return 0;
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
- fprintf( pErr, "usage: test [-vwh]\n" );
+ fprintf( pErr, "usage: test [-bvwh]\n" );
fprintf( pErr, "\t testbench for new procedures\n" );
fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-w : toggle printing very verbose information [default = %s]\n", fVeryVerbose? "yes": "no" );
@@ -9398,19 +9394,29 @@ int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
- int c, fUseZeroCost, fVerbose, nIters;
- extern Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int nIters, int fUseZeroCost, int fVerbose );
+ int c;
+ int nIters;
+ int nSteps;
+ int fRetimingOnly;
+ int fAddBugs;
+ int fUseCnf;
+ int fVerbose;
+
+ extern Abc_Ntk_t * Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- nIters = 2;
- fUseZeroCost = 0;
- fVerbose = 1;
+ nIters = 3;
+ nSteps = 3000;
+ fRetimingOnly = 0;
+ fAddBugs = 0;
+ fUseCnf = 0;
+ fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Izvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "ISrbcvh" ) ) != EOF )
{
switch ( c )
{
@@ -9425,11 +9431,28 @@ int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nIters < 0 )
goto usage;
break;
- case 'z':
- fUseZeroCost ^= 1;
+ case 'S':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-S\" should be followed by a positive integer.\n" );
+ goto usage;
+ }
+ nSteps = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nSteps < 0 )
+ goto usage;
+ break;
+ case 'r':
+ fRetimingOnly ^= 1;
+ break;
+ case 'b':
+ fAddBugs ^= 1;
+ break;
+ case 'c':
+ fUseCnf ^= 1;
break;
case 'v':
- fVerbose ^= 1;
+ fUseCnf ^= 1;
break;
case 'h':
goto usage;
@@ -9448,7 +9471,7 @@ int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- pNtkRes = Abc_NtkIvyHaig( pNtk, nIters, fUseZeroCost, fVerbose );
+ pNtkRes = Abc_NtkDarHaigRecord( pNtk, nIters, nSteps, fRetimingOnly, fAddBugs, fUseCnf, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
@@ -9459,10 +9482,17 @@ int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: haig [-Izvh]\n" );
- fprintf( pErr, "\t prints HAIG stats after sequential rewriting\n" );
- fprintf( pErr, "\t-I num : the number of rewriting iterations [default = %d]\n", nIters );
- fprintf( pErr, "\t-z : toggle zero-cost replacements [default = %s]\n", fUseZeroCost? "yes": "no" );
+ fprintf( pErr, "usage: haig [-IS num] [-rbcvh]\n" );
+ fprintf( pErr, "\t run a few rounds of comb+seq synthesis to test HAIG recording\n" );
+ fprintf( pErr, "\t the current network is set to be the result of synthesis performed\n" );
+ fprintf( pErr, "\t (this network can be verified using command \"dsec\")\n" );
+ fprintf( pErr, "\t HAIG is written out into the file \"haig.blif\"\n" );
+ fprintf( pErr, "\t (this HAIG can be proved using \"r haig.blif; st; dprove -abc -F 16\")\n" );
+ fprintf( pErr, "\t-I num : the number of rounds of comb+seq synthesis [default = %d]\n", nIters );
+ fprintf( pErr, "\t-S num : the number of forward retiming moves performed [default = %d]\n", nSteps );
+ fprintf( pErr, "\t-r : toggle the use of retiming only [default = %s]\n", fRetimingOnly? "yes": "no" );
+ fprintf( pErr, "\t-b : toggle bug insertion [default = %s]\n", fAddBugs? "yes": "no" );
+ fprintf( pErr, "\t-c : enable CNF-based proof (no speculative reduction) [default = %s]\n", fUseCnf? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index f369918e..d746e315 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1655,7 +1655,7 @@ Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose )
pMan->vFlopNums = NULL;
Aig_ManPrintStats(pMan);
- Saig_ManRetimeSteps( pMan, 1000, 1 );
+ Saig_ManRetimeSteps( pMan, 1000, 1, 0 );
Aig_ManPrintStats(pMan);
pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
@@ -1674,18 +1674,23 @@ Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose )
SeeAlso []
***********************************************************************/
-void Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk )
+Abc_Ntk_t * Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose )
{
- Aig_Man_t * pMan;
+ Abc_Ntk_t * pNtkAig;
+ Aig_Man_t * pMan, * pTemp;
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
- return;
+ return NULL;
if ( pMan->vFlopNums )
Vec_IntFree( pMan->vFlopNums );
pMan->vFlopNums = NULL;
- Saig_ManHaigRecord( pMan );
+ pMan = Saig_ManHaigRecord( pTemp = pMan, nIters, nSteps, fRetimingOnly, fAddBugs, fUseCnf, fVerbose );
+ Aig_ManStop( pTemp );
+
+ pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
Aig_ManStop( pMan );
+ return pNtkAig;
}
/**Function*************************************************************
diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/src/map/pcm/module.make
diff --git a/src/map/ply/module.make b/src/map/ply/module.make
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/src/map/ply/module.make
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-20 18:24:12 +0000