summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2014-06-04 23:33:58 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2014-06-04 23:33:58 -0700
commitfa48d46b82e58cff1b5c965658349be3b6f53d58 (patch)
treee11fb6163f91676cdfee3789ddb6cca1c6cb1056
parent102782a5a1cd9e9a59b87810e04d78b838976ae1 (diff)
parentf18b0254c82da1ecdccb910f7b38aadfa93e7a05 (diff)
downloadabc-fa48d46b82e58cff1b5c965658349be3b6f53d58.tar.gz
abc-fa48d46b82e58cff1b5c965658349be3b6f53d58.tar.bz2
abc-fa48d46b82e58cff1b5c965658349be3b6f53d58.zip
Merged in lj/abc-lj/unfold2-dev (pull request #6)
pull request for unfold2
-rw-r--r--Makefile2
-rw-r--r--src/aig/aig/aig.h4
-rw-r--r--src/aig/aig/aigMan.c8
-rw-r--r--src/aig/saig/saig.h5
-rw-r--r--src/aig/saig/saigConstr2.c2
-rw-r--r--src/aig/saig/saigUnfold2.c495
-rw-r--r--src/base/abci/abc.c6
-rw-r--r--src/base/abci/abcDar.c2
-rw-r--r--src/base/abci/abcDarUnfold2.c69
-rw-r--r--src/base/abci/abciUnfold2.c186
10 files changed, 775 insertions, 4 deletions
diff --git a/Makefile b/Makefile
index 72b35134..50357b3e 100644
--- a/Makefile
+++ b/Makefile
@@ -131,7 +131,7 @@ tags:
$(PROG): $(OBJ)
@echo "$(MSG_PREFIX)\`\` Building binary:" $(notdir $@)
- @$(LD) -o $@ $^ $(LIBS)
+ $(LD) -o $@ $^ $(LIBS)
lib$(PROG).a: $(OBJ)
@echo "$(MSG_PREFIX)\`\` Linking:" $(notdir $@)
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index db7d380d..e92e512c 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -165,6 +165,10 @@ struct Aig_Man_t_
// timing statistics
abctime time1;
abctime time2;
+ //-- jlong -- begin
+ Vec_Ptr_t * unfold2_type_I;
+ Vec_Ptr_t * unfold2_type_II;
+ //-- jlong -- end
};
// cut computation
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 230a2b18..246e0501 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -60,6 +60,10 @@ Aig_Man_t * Aig_ManStart( int nNodesMax )
p->vCos = Vec_PtrAlloc( 100 );
p->vObjs = Vec_PtrAlloc( 1000 );
p->vBufs = Vec_PtrAlloc( 100 );
+ //--jlong -- begin
+ p->unfold2_type_I = Vec_PtrAlloc( 4);
+ p->unfold2_type_II = Vec_PtrAlloc( 4);
+ //--jlong -- end
// prepare the internal memory manager
p->pMemObjs = Aig_MmFixedStart( sizeof(Aig_Obj_t), nNodesMax );
// create the constant node
@@ -200,6 +204,10 @@ void Aig_ManStop( Aig_Man_t * p )
Vec_PtrFreeP( &p->vCos );
Vec_PtrFreeP( &p->vObjs );
Vec_PtrFreeP( &p->vBufs );
+ //--jlong -- begin
+ Vec_PtrFreeP( &p->unfold2_type_I );
+ Vec_PtrFreeP( &p->unfold2_type_II );
+ //--jlong -- end
Vec_IntFreeP( &p->vLevelR );
Vec_VecFreeP( &p->vLevels );
Vec_IntFreeP( &p->vFlopNums );
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 475f476d..380af64b 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -116,6 +116,11 @@ extern void Saig_ManDetectConstrFuncTest( Aig_Man_t * p, int nFrame
/*=== saigConstr2.c ==========================================================*/
extern Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose );
extern Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose );
+// -- jlong -- begin
+extern Aig_Man_t * Saig_ManDupFoldConstrsFunc2( Aig_Man_t * pAig, int fCompl, int fVerbose, int typeII_cnt );
+extern Aig_Man_t * Saig_ManDupUnfoldConstrsFunc2( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose , int * typeII_cnt);
+// --jlong -- end
+
/*=== saigDual.c ==========================================================*/
extern Aig_Man_t * Saig_ManDupDual( Aig_Man_t * pAig, Vec_Int_t * vDcFlops, int nDualPis, int fDualFfs, int fMiterFfs, int fComplPo, int fCheckZero, int fCheckOne );
extern void Saig_ManBlockPo( Aig_Man_t * pAig, int nCycles );
diff --git a/src/aig/saig/saigConstr2.c b/src/aig/saig/saigConstr2.c
index 8ab5df51..6e560b59 100644
--- a/src/aig/saig/saigConstr2.c
+++ b/src/aig/saig/saigConstr2.c
@@ -1008,6 +1008,6 @@ Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbo
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
-
+#include "saigUnfold2.c"
ABC_NAMESPACE_IMPL_END
diff --git a/src/aig/saig/saigUnfold2.c b/src/aig/saig/saigUnfold2.c
new file mode 100644
index 00000000..e5ff9d2c
--- /dev/null
+++ b/src/aig/saig/saigUnfold2.c
@@ -0,0 +1,495 @@
+
+int Saig_ManFilterUsingIndOne2( Aig_Man_t * p, Aig_Man_t * pFrame, sat_solver * pSat, Cnf_Dat_t * pCnf, int nConfs, int nProps, int Counter
+ , int type_ /* jlong -- */
+ )
+{
+ Aig_Obj_t * pObj;
+ int Lit, status;
+ pObj = Aig_ManCo( pFrame, Counter*3+type_ ); /* which co */
+ Lit = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 );
+ status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfs, 0, 0, 0 );
+ if ( status == l_False ) /* unsat */
+ return status;
+ if ( status == l_Undef )
+ {
+ printf( "Solver returned undecided.\n" );
+ return status;
+ }
+ assert( status == l_True );
+ return status;
+}
+
+Aig_Man_t * Saig_ManCreateIndMiter2( Aig_Man_t * pAig, Vec_Vec_t * vCands )
+{
+ int nFrames = 3;
+ Vec_Ptr_t * vNodes;
+ Aig_Man_t * pFrames;
+ Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
+ Aig_Obj_t ** pObjMap;
+ int i, f, k;
+
+ // create mapping for the frames nodes
+ pObjMap = ABC_CALLOC( Aig_Obj_t *, nFrames * Aig_ManObjNumMax(pAig) );
+
+ // start the fraig package
+ pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames );
+ pFrames->pName = Abc_UtilStrsav( pAig->pName );
+ pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
+ // map constant nodes
+ for ( f = 0; f < nFrames; f++ )
+ Aig_ObjSetFrames( pObjMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) );
+ // create PI nodes for the frames
+ for ( f = 0; f < nFrames; f++ )
+ Aig_ManForEachPiSeq( pAig, pObj, i )
+ Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, Aig_ObjCreateCi(pFrames) );
+ // set initial state for the latches
+ Aig_ManForEachLoSeq( pAig, pObj, i )
+ Aig_ObjSetFrames( pObjMap, nFrames, pObj, 0, Aig_ObjCreateCi(pFrames) );
+
+ // add timeframes
+ for ( f = 0; f < nFrames; f++ )
+ {
+ // add internal nodes of this frame
+ Aig_ManForEachNode( pAig, pObj, i )
+ {
+ pObjNew = Aig_And( pFrames, Aig_ObjChild0Frames(pObjMap,nFrames,pObj,f), Aig_ObjChild1Frames(pObjMap,nFrames,pObj,f) );
+ Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
+ }
+ // set the latch inputs and copy them into the latch outputs of the next frame
+ Aig_ManForEachLiLoSeq( pAig, pObjLi, pObjLo, i )
+ {
+ pObjNew = Aig_ObjChild0Frames(pObjMap,nFrames,pObjLi,f);
+ if ( f < nFrames - 1 )
+ Aig_ObjSetFrames( pObjMap, nFrames, pObjLo, f+1, pObjNew );
+ }
+ }
+
+ // go through the candidates
+ Vec_VecForEachLevel( vCands, vNodes, i )
+ {
+ Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
+ {
+ Aig_Obj_t * pObjR = Aig_Regular(pObj);
+ Aig_Obj_t * pNode0 = pObjMap[nFrames*Aig_ObjId(pObjR)+0];
+ Aig_Obj_t * pNode1 = pObjMap[nFrames*Aig_ObjId(pObjR)+1];
+ {
+ Aig_Obj_t * pFan0 = Aig_NotCond( pNode0, Aig_IsComplement(pObj) );
+ Aig_Obj_t * pFan1 = Aig_NotCond( pNode1, !Aig_IsComplement(pObj) );
+ Aig_Obj_t * pMiter = Aig_And( pFrames, pFan0, pFan1 );
+ Aig_ObjCreateCo( pFrames, pMiter );
+
+ /* need to check p & Xp is satisfiable */
+ /* jlong -- begin */
+ Aig_Obj_t * pMiter2 = Aig_And( pFrames, pFan0, Aig_Not(pFan1));
+ Aig_ObjCreateCo( pFrames, pMiter2 ); /* jlong -- end */
+ }
+
+ { /* jlong -- begin */
+ Aig_Obj_t * pNode2 = pObjMap[nFrames*Aig_ObjId(pObjR)+2];
+ Aig_Obj_t * pFan0 = Aig_NotCond( pNode0, Aig_IsComplement(pObj) );
+ Aig_Obj_t * pFan1 = Aig_NotCond( pNode1, Aig_IsComplement(pObj) );
+ Aig_Obj_t * pFan2 = Aig_NotCond( pNode2, !Aig_IsComplement(pObj) );
+ Aig_Obj_t * pMiter = Aig_And( pFrames, Aig_And(pFrames, pFan0, pFan1 ), pFan2);
+ Aig_ObjCreateCo( pFrames, pMiter ); /* jlong -- end */
+ }
+
+ }
+ }
+ Aig_ManCleanup( pFrames );
+ ABC_FREE( pObjMap );
+
+//Aig_ManShow( pAig, 0, NULL );
+//Aig_ManShow( pFrames, 0, NULL );
+ return pFrames;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Detects constraints functionally.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_ManFilterUsingInd2( Aig_Man_t * p, Vec_Vec_t * vCands, int nConfs, int nProps, int fVerbose )
+{
+ Vec_Ptr_t * vNodes;
+ Aig_Man_t * pFrames;
+ sat_solver * pSat;
+ Cnf_Dat_t * pCnf;
+ Aig_Obj_t * pObj;
+ int i, k, k2, Counter;
+ /*
+ Vec_VecForEachLevel( vCands, vNodes, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
+ printf( "%d ", Aig_ObjId(Aig_Regular(pObj)) );
+ printf( "\n" );
+ */
+ // create timeframes
+ // pFrames = Saig_ManUnrollInd( p );
+ pFrames = Saig_ManCreateIndMiter2( p, vCands );
+ assert( Aig_ManCoNum(pFrames) == Vec_VecSizeSize(vCands)*3 );
+ // start the SAT solver
+ pCnf = Cnf_DeriveSimple( pFrames, Aig_ManCoNum(pFrames) );
+ pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+ // check candidates
+ if ( fVerbose )
+ printf( "Filtered cands: \n" );
+ Counter = 0;
+ Vec_VecForEachLevel( vCands, vNodes, i )
+ {
+ assert(i==0); /* only one item */
+ k2 = 0;
+ Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
+ {
+ if ( Saig_ManFilterUsingIndOne2( p, pFrames, pSat, pCnf, nConfs, nProps, Counter++ , 0) == l_False)
+ // if ( Saig_ManFilterUsingIndOne_old( p, pSat, pCnf, nConfs, pObj ) )
+ {
+ Vec_PtrWriteEntry( vNodes, k2++, pObj );
+ if ( fVerbose )
+ printf( "%d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
+ printf( " type I : %d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
+ Vec_PtrPush(p->unfold2_type_I, pObj);
+ }
+ /* jlong -- begin */
+ else if ( Saig_ManFilterUsingIndOne2( p, pFrames, pSat, pCnf, nConfs, nProps, Counter-1 , 1) == l_True ) /* can be self-conflicting */
+ {
+ if ( Saig_ManFilterUsingIndOne2( p, pFrames, pSat, pCnf, nConfs, nProps, Counter-1 , 2) == l_False ){
+ //Vec_PtrWriteEntry( vNodes, k2++, pObj );
+ if ( fVerbose )
+ printf( "%d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
+ printf( " type II: %d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
+ Vec_PtrWriteEntry( vNodes, k2++, pObj ); /* add type II constraints */
+ Vec_PtrPush(p->unfold2_type_II, pObj);
+ }
+ }
+ /* jlong -- end */
+ }
+ Vec_PtrShrink( vNodes, k2 );
+ }
+
+ // clean up
+ Cnf_DataFree( pCnf );
+ sat_solver_delete( pSat );
+ if ( fVerbose )
+ Aig_ManPrintStats( pFrames );
+ Aig_ManStop( pFrames );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Returns the number of variables implied by the output.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Vec_t * Ssw_ManFindDirectImplications2( Aig_Man_t * p, int nFrames, int nConfs, int nProps, int fVerbose )
+{
+ Vec_Vec_t * vCands = NULL;
+ Vec_Ptr_t * vNodes;
+ Cnf_Dat_t * pCnf;
+ sat_solver * pSat;
+ Aig_Man_t * pFrames;
+ Aig_Obj_t * pObj, * pRepr, * pReprR;
+ int i, f, k, value;
+ assert(nFrames == 1);
+ vCands = Vec_VecAlloc( nFrames );
+ assert(nFrames == 1);
+ // perform unrolling
+ pFrames = Saig_ManUnrollCOI( p, nFrames );
+ assert( Aig_ManCoNum(pFrames) == 1 );
+ // start the SAT solver
+ pCnf = Cnf_DeriveSimple( pFrames, 0 );
+ pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+ if ( pSat != NULL )
+ {
+ Aig_ManIncrementTravId( p );
+ for ( f = 0; f < nFrames; f++ )
+ {
+ Aig_ManForEachObj( p, pObj, i )
+ {
+ if ( !Aig_ObjIsCand(pObj) )
+ continue;
+ //--jlong : also use internal nodes as well
+ /* if ( !Aig_ObjIsCi(pObj) ) */
+ /* continue; */
+ if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+ continue;
+ // get the node from timeframes
+ pRepr = p->pObjCopies[nFrames*i + nFrames-1-f];
+ pReprR = Aig_Regular(pRepr);
+ if ( pCnf->pVarNums[Aig_ObjId(pReprR)] < 0 )
+ continue;
+ // value = pSat->assigns[ pCnf->pVarNums[Aig_ObjId(pReprR)] ];
+ value = sat_solver_get_var_value( pSat, pCnf->pVarNums[Aig_ObjId(pReprR)] );
+ if ( value == l_Undef )
+ continue;
+ // label this node as taken
+ Aig_ObjSetTravIdCurrent(p, pObj);
+ if ( Saig_ObjIsLo(p, pObj) )
+ Aig_ObjSetTravIdCurrent( p, Aig_ObjFanin0(Saig_ObjLoToLi(p, pObj)) );
+ // remember the node
+ Vec_VecPush( vCands, f, Aig_NotCond( pObj, (value == l_True) ^ Aig_IsComplement(pRepr) ) );
+ // printf( "%s%d ", (value == l_False)? "":"!", i );
+ }
+ }
+ // printf( "\n" );
+ sat_solver_delete( pSat );
+ }
+ Aig_ManStop( pFrames );
+ Cnf_DataFree( pCnf );
+
+ if ( fVerbose )
+ {
+ printf( "Found %3d candidates.\n", Vec_VecSizeSize(vCands) );
+ Vec_VecForEachLevel( vCands, vNodes, k )
+ {
+ printf( "Level %d. Cands =%d ", k, Vec_PtrSize(vNodes) );
+ // Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+ // printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
+ printf( "\n" );
+ }
+ }
+
+ ABC_FREE( p->pObjCopies );
+ /* -- jlong -- this does the SAT proof of the constraints */
+ Saig_ManFilterUsingInd2( p, vCands, nConfs, nProps, fVerbose );
+ if ( Vec_VecSizeSize(vCands) )
+ printf( "Found %3d constraints after filtering.\n", Vec_VecSizeSize(vCands) );
+ if ( fVerbose )
+ {
+ Vec_VecForEachLevel( vCands, vNodes, k )
+ {
+ printf( "Level %d. Constr =%d ", k, Vec_PtrSize(vNodes) );
+ // Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+ // printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
+ printf( "\n" );
+ }
+ }
+
+ return vCands;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Duplicates the AIG while unfolding constraints.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManDupUnfoldConstrsFunc2( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose , int * typeII_cnt){
+ Aig_Man_t * pNew;
+ Vec_Vec_t * vCands;
+ Vec_Ptr_t * vNewFlops;
+ Aig_Obj_t * pObj;
+ int i, k, nNewFlops;
+ const int fCompl = 0 ;
+ if ( fOldAlgo )
+ vCands = Saig_ManDetectConstrFunc( pAig, nFrames, nConfs, nProps, fVerbose );
+ else
+ vCands = Ssw_ManFindDirectImplications2( pAig, nFrames, nConfs, nProps, fVerbose );
+ if ( vCands == NULL || Vec_VecSizeSize(vCands) == 0 )
+ {
+ Vec_VecFreeP( &vCands );
+ return Aig_ManDupDfs( pAig );
+ }
+ // create new manager
+ pNew = Aig_ManDupWithoutPos( pAig ); /* good */
+ pNew->nConstrs = pAig->nConstrs + Vec_VecSizeSize(vCands);
+ pNew->nConstrs = pAig->nConstrs + Vec_PtrSize(pAig->unfold2_type_II)
+ + Vec_PtrSize(pAig->unfold2_type_I);
+ // pNew->nConstrsTypeII = Vec_PtrSize(pAig->unfold2_type_II);
+ *typeII_cnt = Vec_PtrSize(pAig->unfold2_type_II);
+
+ /* new set of registers */
+
+ // add normal POs
+ Saig_ManForEachPo( pAig, pObj, i )
+ Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
+ // create constraint outputs
+ vNewFlops = Vec_PtrAlloc( 100 );
+
+
+ Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_I, pObj, k){
+ Aig_Obj_t * x = Aig_ObjRealCopy(pObj);
+ Aig_ObjCreateCo(pNew, x);
+ }
+
+ Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_II, pObj, k){
+ Aig_Obj_t * type_II_latch
+ = Aig_ObjCreateCi(pNew); /* will get connected later; */
+ Aig_Obj_t * x = Aig_ObjRealCopy(pObj);
+
+ Aig_Obj_t * n = Aig_And(pNew,
+ Aig_NotCond(type_II_latch, fCompl),
+ Aig_NotCond(x, fCompl));
+ Aig_ObjCreateCo(pNew, n);//Aig_Not(n));
+ }
+
+ // add latch outputs
+ Saig_ManForEachLi( pAig, pObj, i )
+ Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
+
+ Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_II, pObj, k){
+ Aig_Obj_t * x = Aig_ObjRealCopy(pObj);
+ Aig_ObjCreateCo(pNew, x);
+ }
+
+ // add new latch outputs
+ nNewFlops = Vec_PtrSize(pAig->unfold2_type_II);
+ //assert( nNewFlops == Vec_PtrSize(vNewFlops) );
+ Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) + nNewFlops );
+ printf("#reg after unfold2: %d\n", Aig_ManRegNum(pAig) + nNewFlops );
+ Vec_VecFreeP( &vCands );
+ Vec_PtrFree( vNewFlops );
+ return pNew;
+
+}
+
+/**Function*************************************************************
+
+ Synopsis [Duplicates the AIG while unfolding constraints.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManDupFoldConstrsFunc2( Aig_Man_t * pAig, int fCompl, int fVerbose ,
+ int typeII_cnt)
+{
+ Aig_Man_t * pAigNew;
+ Aig_Obj_t * pMiter, * pFlopOut, * pFlopIn, * pObj;
+ int i;
+ if ( Aig_ManConstrNum(pAig) == 0 )
+ return Aig_ManDupDfs( pAig );
+ assert( Aig_ManConstrNum(pAig) < Saig_ManPoNum(pAig) );
+ // start the new manager
+ pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
+ pAigNew->pName = Abc_UtilStrsav( pAig->pName );
+ pAigNew->pSpec = Abc_UtilStrsav( pAig->pSpec );
+ // map the constant node
+ Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
+ // create variables for PIs
+ Aig_ManForEachCi( pAig, pObj, i )
+ pObj->pData = Aig_ObjCreateCi( pAigNew );
+ // add internal nodes of this frame
+ Aig_ManForEachNode( pAig, pObj, i )
+ pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+
+ // OR the constraint outputs
+ pMiter = Aig_ManConst0( pAigNew );
+ int typeII_cc = 0;//typeII_cnt;
+ typeII_cnt = 0;
+
+ int type_II = 0;
+
+ Saig_ManForEachPo( pAig, pObj, i )
+ {
+
+ if ( i < Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
+ continue;
+ if (i + typeII_cnt >= Saig_ManPoNum(pAig) ) {
+ type_II = 1;
+ }
+ /* now we got the constraint */
+ if (type_II) {
+
+ Aig_Obj_t * type_II_latch
+ = Aig_ObjCreateCi(pAigNew); /* will get connected later; */
+ pMiter = Aig_Or(pAigNew, pMiter,
+ Aig_And(pAigNew,
+ Aig_NotCond(type_II_latch, fCompl),
+ Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) )
+ );
+ printf( "modeling typeII : %d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
+ } else
+ pMiter = Aig_Or( pAigNew, pMiter, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
+ }
+
+ // create additional flop
+ if ( Saig_ManRegNum(pAig) > 0 )
+ {
+ pFlopOut = Aig_ObjCreateCi( pAigNew );
+ pFlopIn = Aig_Or( pAigNew, pMiter, pFlopOut );
+ }
+ else
+ pFlopIn = pMiter;
+
+ // create primary output
+ Saig_ManForEachPo( pAig, pObj, i )
+ {
+ if ( i >= Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
+ continue;
+ pMiter = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_Not(pFlopIn) );
+ Aig_ObjCreateCo( pAigNew, pMiter );
+ }
+
+ // transfer to register outputs
+ {
+ /* the same for type I and type II */
+ Aig_Obj_t * pObjLi, *pObjLo;
+
+ Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) {
+ if( i + typeII_cc < Aig_ManRegNum(pAig)) {
+ Aig_Obj_t *c = Aig_Mux(pAigNew, Aig_Not(pFlopIn),
+ Aig_ObjChild0Copy(pObjLi) ,
+ pObjLo->pData);
+ Aig_ObjCreateCo( pAigNew, c);
+ } else {
+ printf ( "skipping: reg%d\n", i);
+ Aig_ObjCreateCo( pAigNew,Aig_ObjChild0Copy(pObjLi));
+ }
+ }
+
+ }
+ if(0)Saig_ManForEachLi( pAig, pObj, i ) {
+ Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
+ }
+ Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
+
+ type_II = 0;
+ Saig_ManForEachPo( pAig, pObj, i )
+ {
+
+ if ( i < Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
+ continue;
+ if (i + typeII_cnt >= Saig_ManPoNum(pAig) ) {
+ type_II = 1;
+ }
+ /* now we got the constraint */
+ if (type_II) {
+ Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj));
+ Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAigNew)+1 );
+ printf( "Latch for typeII : %d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
+ }
+ }
+
+
+ // create additional flop
+
+ if ( Saig_ManRegNum(pAig) > 0 )
+ {
+ Aig_ObjCreateCo( pAigNew, pFlopIn );
+ Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAigNew)+1 );
+ }
+ printf("#reg after fold2: %d\n", Aig_ManRegNum(pAigNew));
+ // perform cleanup
+ Aig_ManCleanup( pAigNew );
+ Aig_ManSeqCleanup( pAigNew );
+ return pAigNew;
+}
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 2323ac36..05a03aca 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -295,6 +295,8 @@ static int Abc_CommandInduction ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandConstr ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandUnfold ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFold ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandUnfold2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFold2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBm ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBm2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSaucy ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -871,6 +873,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Verification", "constr", Abc_CommandConstr, 0 );
Cmd_CommandAdd( pAbc, "Verification", "unfold", Abc_CommandUnfold, 1 );
Cmd_CommandAdd( pAbc, "Verification", "fold", Abc_CommandFold, 1 );
+ Cmd_CommandAdd( pAbc, "Verification", "unfold2", Abc_CommandUnfold2, 1 ); // jlong
+ Cmd_CommandAdd( pAbc, "Verification", "fold2", Abc_CommandFold2, 1 ); // jlong
Cmd_CommandAdd( pAbc, "Verification", "bm", Abc_CommandBm, 1 );
Cmd_CommandAdd( pAbc, "Verification", "bm2", Abc_CommandBm2, 1 );
Cmd_CommandAdd( pAbc, "Verification", "saucy3", Abc_CommandSaucy, 1 );
@@ -35347,5 +35351,5 @@ usage:
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
-
+#include "abciUnfold2.c"
ABC_NAMESPACE_IMPL_END
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 1870e713..894c9d17 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -4560,6 +4560,6 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
-
+#include "abcDarUnfold2.c"
ABC_NAMESPACE_IMPL_END
diff --git a/src/base/abci/abcDarUnfold2.c b/src/base/abci/abcDarUnfold2.c
new file mode 100644
index 00000000..7ebc316c
--- /dev/null
+++ b/src/base/abci/abcDarUnfold2.c
@@ -0,0 +1,69 @@
+/**Function*************************************************************
+
+ Synopsis [Performs BDD-based reachability analysis.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarFold2( Abc_Ntk_t * pNtk, int fCompl, int fVerbose , int);
+Abc_Ntk_t * Abc_NtkDarUnfold2( 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;
+ int typeII_cnt = 0;
+ assert( Abc_NtkIsStrash(pNtk) );
+ pMan = Abc_NtkToDar( pNtk, 0, 1 );
+ if ( pMan == NULL )
+ return NULL;
+ if ( fStruct ){
+ assert(0);//pMan = Saig_ManDupUnfoldConstrs( pTemp = pMan );
+ }else
+ pMan = Saig_ManDupUnfoldConstrsFunc2( pTemp = pMan, nFrames, nConfs, nProps, fOldAlgo, fVerbose , &typeII_cnt);
+ Aig_ManStop( pTemp );
+ if ( pMan == NULL )
+ return NULL;
+ // typeII_cnt = pMan->nConstrsTypeII;
+ pNtkAig = Abc_NtkFromAigPhase( pMan );
+ pNtkAig->pName = Extra_UtilStrsav(pMan->pName);
+ pNtkAig->pSpec = Extra_UtilStrsav(pMan->pSpec);
+ Aig_ManStop( pMan );
+
+ return pNtkAig;//Abc_NtkDarFold2(pNtkAig, 0, fVerbose, typeII_cnt);
+
+ //return pNtkAig;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs BDD-based reachability analysis.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarFold2( Abc_Ntk_t * pNtk, int fCompl, int fVerbose
+ , int typeII_cnt
+ )
+{
+ 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_ManDupFoldConstrsFunc2( pTemp = pMan, fCompl, fVerbose, typeII_cnt );
+ Aig_ManStop( pTemp );
+ pNtkAig = Abc_NtkFromAigPhase( pMan );
+ pNtkAig->pName = Extra_UtilStrsav(pMan->pName);
+ pNtkAig->pSpec = Extra_UtilStrsav(pMan->pSpec);
+ Aig_ManStop( pMan );
+ return pNtkAig;
+}
+
diff --git a/src/base/abci/abciUnfold2.c b/src/base/abci/abciUnfold2.c
new file mode 100644
index 00000000..c3780c15
--- /dev/null
+++ b/src/base/abci/abciUnfold2.c
@@ -0,0 +1,186 @@
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandUnfold2( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Abc_Ntk_t * pNtk, * pNtkRes;
+ int nFrames;
+ int nConfs;
+ int nProps;
+ int fStruct = 0;
+ int fOldAlgo = 0;
+ int fVerbose;
+ int c;
+ extern Abc_Ntk_t * Abc_NtkDarUnfold2( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nProps, int fStruct, int fOldAlgo, int fVerbose );
+ pNtk = Abc_FrameReadNtk(pAbc);
+ // set defaults
+ nFrames = 1;
+ nConfs = 1000;
+ nProps = 1000;
+ fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "CPvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ /* case 'F': */
+ /* if ( globalUtilOptind >= argc ) */
+ /* { */
+ /* Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); */
+ /* goto usage; */
+ /* } */
+ /* nFrames = atoi(argv[globalUtilOptind]); */
+ /* globalUtilOptind++; */
+ /* if ( nFrames < 0 ) */
+ /* goto usage; */
+ /* break; */
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nConfs = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nConfs < 0 )
+ goto usage;
+ break;
+ case 'P':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nProps = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nProps < 0 )
+ goto usage;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ Abc_Print( -1, "Empty network.\n" );
+ return 1;
+ }
+ if ( Abc_NtkIsComb(pNtk) )
+ {
+ Abc_Print( -1, "The network is combinational.\n" );
+ return 0;
+ }
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ Abc_Print( -1, "Currently only works for structurally hashed circuits.\n" );
+ return 0;
+ }
+ if ( Abc_NtkConstrNum(pNtk) > 0 )
+ {
+ Abc_Print( -1, "Constraints are already extracted.\n" );
+ return 0;
+ }
+ if ( Abc_NtkPoNum(pNtk) > 1 && !fStruct )
+ {
+ Abc_Print( -1, "Functional constraint extraction works for single-output miters (use \"orpos\").\n" );
+ return 0;
+ }
+ // modify the current network
+ pNtkRes = Abc_NtkDarUnfold2( pNtk, nFrames, nConfs, nProps, fStruct, fOldAlgo, fVerbose );
+ if ( pNtkRes == NULL )
+ {
+ Abc_Print( 1,"Transformation has failed.\n" );
+ return 0;
+ }
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ return 0;
+usage:
+ Abc_Print( -2, "usage: unfold2 [-FCP num] [-savh]\n" );
+ Abc_Print( -2, "\t unfold hidden constraints as separate outputs\n" );
+ Abc_Print( -2, "\t-C num : the max number of conflicts in SAT solving [default = %d]\n", nConfs );
+ Abc_Print( -2, "\t-P num : the max number of constraint propagations [default = %d]\n", nProps );
+ Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+
+
+int Abc_CommandFold2( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Abc_Ntk_t * pNtk, * pNtkRes;
+ int fCompl;
+ int fVerbose;
+ int c;
+ extern Abc_Ntk_t * Abc_NtkDarFold2( Abc_Ntk_t * pNtk, int fCompl, int fVerbose , int);
+ pNtk = Abc_FrameReadNtk(pAbc);
+ // set defaults
+ fCompl = 0;
+ fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "cvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ /* case 'c': */
+ /* fCompl ^= 1; */
+ /* break; */
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ Abc_Print( -1, "Empty network.\n" );
+ return 1;
+ }
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ Abc_Print( -1, "Currently only works for structurally hashed circuits.\n" );
+ return 0;
+ }
+ if ( Abc_NtkConstrNum(pNtk) == 0 )
+ {
+ Abc_Print( 0, "The network has no constraints.\n" );
+ return 0;
+ }
+ if ( Abc_NtkIsComb(pNtk) )
+ Abc_Print( 0, "The network is combinational.\n" );
+ // modify the current network
+ pNtkRes = Abc_NtkDarFold2( pNtk, fCompl, fVerbose ,0);
+ if ( pNtkRes == NULL )
+ {
+ Abc_Print( 1,"Transformation has failed.\n" );
+ return 0;
+ }
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ return 0;
+usage:
+ Abc_Print( -2, "usage: fold [-cvh]\n" );
+ Abc_Print( -2, "\t folds constraints represented as separate outputs\n" );
+ // Abc_Print( -2, "\t-c : toggle complementing constraints while folding [default = %s]\n", fCompl? "yes": "no" );
+ Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}