summaryrefslogtreecommitdiffstats
path: root/src/aig/ntl/ntlFraig.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/ntl/ntlFraig.c')
-rw-r--r--src/aig/ntl/ntlFraig.c114
1 files changed, 96 insertions, 18 deletions
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index 86d92b3c..767ea6e4 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -181,6 +181,35 @@ void Ntl_ManReduce( Ntl_Man_t * p, Aig_Man_t * pAig )
/**Function*************************************************************
+ Synopsis [Resets complemented attributes of the collapsed AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ntl_ManResetComplemented( Ntl_Man_t * p, Aig_Man_t * pAigCol )
+{
+ Ntl_Mod_t * pRoot;
+ Ntl_Obj_t * pObj;
+ Aig_Obj_t * pObjCol;
+ int i;
+ pRoot = Ntl_ManRootModel(p);
+ Ntl_ModelForEachLatch( pRoot, pObj, i )
+ {
+ if ( (pObj->LatchId & 3) == 1 )
+ {
+ pObjCol = Ntl_ObjFanout0(pObj)->pCopy;
+ assert( pObjCol->fPhase == 0 );
+ pObjCol->fPhase = 1;
+ }
+ }
+}
+
+/**Function*************************************************************
+
Synopsis [Finalizes the transformation.]
Description []
@@ -242,14 +271,14 @@ Ntl_Man_t * Ntl_ManFraig( Ntl_Man_t * p, int nPartSize, int nConfLimit, int nLev
// collapse the AIG
pAig = Ntl_ManExtract( p );
pNew = Ntl_ManInsertAig( p, pAig );
- pAigCol = Ntl_ManCollapse( pNew );
+ pAigCol = Ntl_ManCollapse( pNew, 0 );
// perform fraiging for the given design
nPartSize = nPartSize? nPartSize : Aig_ManPoNum(pAigCol);
pTemp = Aig_ManFraigPartitioned( pAigCol, nPartSize, nConfLimit, nLevelMax, fVerbose );
Aig_ManStop( pTemp );
- // finalize the transformatoin
+ // finalize the transformation
pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose );
Ntl_ManFree( pAux );
Aig_ManStop( pAig );
@@ -273,20 +302,17 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe
Ntl_Man_t * pNew, * pAux;
Aig_Man_t * pAig, * pAigCol, * pTemp;
- // transform the design
- Ntl_ManTransformInitValues( p );
-
// collapse the AIG
pAig = Ntl_ManExtract( p );
pNew = Ntl_ManInsertAig( p, pAig );
- pAigCol = Ntl_ManCollapse( pNew );
+ pAigCol = Ntl_ManCollapse( pNew, 1 );
// perform SCL for the given design
pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, fVerbose );
Aig_ManStop( pTemp );
- // finalize the transformatoin
+ // finalize the transformation
pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose );
Ntl_ManFree( pAux );
Aig_ManStop( pAig );
@@ -310,20 +336,17 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose )
Ntl_Man_t * pNew, * pAux;
Aig_Man_t * pAig, * pAigCol, * pTemp;
- // transform the design
- Ntl_ManTransformInitValues( p );
-
// collapse the AIG
pAig = Ntl_ManExtract( p );
pNew = Ntl_ManInsertAig( p, pAig );
- pAigCol = Ntl_ManCollapse( pNew );
+ pAigCol = Ntl_ManCollapse( pNew, 1 );
// perform SCL for the given design
pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL );
Aig_ManStop( pTemp );
- // finalize the transformatoin
+ // finalize the transformation
pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose );
Ntl_ManFree( pAux );
Aig_ManStop( pAig );
@@ -347,20 +370,17 @@ Ntl_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Fra_Ssw_t * pPars )
Ntl_Man_t * pNew, * pAux;
Aig_Man_t * pAig, * pAigCol, * pTemp;
- // transform the design
- Ntl_ManTransformInitValues( p );
-
// collapse the AIG
pAig = Ntl_ManExtract( p );
pNew = Ntl_ManInsertAig( p, pAig );
- pAigCol = Ntl_ManCollapse( pNew );
+ pAigCol = Ntl_ManCollapse( pNew, 1 );
// perform SCL for the given design
pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
pTemp = Fra_FraigInduction( pAigCol, pPars );
Aig_ManStop( pTemp );
- // finalize the transformatoin
+ // finalize the transformation
pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, pPars->fVerbose );
Ntl_ManFree( pAux );
Aig_ManStop( pAig );
@@ -459,6 +479,63 @@ void Ntl_ManAttachWhiteBoxes( Ntl_Man_t * p, Aig_Man_t * pAigCol, Aig_Man_t * pA
/**Function*************************************************************
+ Synopsis [Flip complemented edges.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ntl_ManFlipEdges( Ntl_Man_t * p, Aig_Man_t * pAigCol )
+{
+ Ntl_Mod_t * pRoot;
+ Ntl_Obj_t * pObj;
+ Aig_Obj_t * pObjCol, * pFanin;
+ int i, iLatch;
+ pRoot = Ntl_ManRootModel(p);
+ iLatch = 0;
+ Ntl_ModelForEachLatch( pRoot, pObj, i )
+ {
+ if ( (pObj->LatchId & 3) == 1 )
+ {
+ pObjCol = Aig_ManPi( pAigCol, Ntl_ModelPiNum(pRoot) + iLatch );
+ assert( pObjCol->fMarkA == 0 );
+ pObjCol->fMarkA = 1;
+ }
+ iLatch++;
+ }
+ // flip pointers to the complemented edges
+ Aig_ManForEachObj( pAigCol, pObjCol, i )
+ {
+ pFanin = Aig_ObjFanin0(pObjCol);
+ if ( pFanin && pFanin->fMarkA )
+ pObjCol->pFanin0 = Aig_Not(pObjCol->pFanin0);
+ pFanin = Aig_ObjFanin1(pObjCol);
+ if ( pFanin && pFanin->fMarkA )
+ pObjCol->pFanin1 = Aig_Not(pObjCol->pFanin1);
+ }
+ // flip complemented latch derivers and undo the marks
+ iLatch = 0;
+ Ntl_ModelForEachLatch( pRoot, pObj, i )
+ {
+ if ( (pObj->LatchId & 3) == 1 )
+ {
+ // flip the latch input
+ pObjCol = Aig_ManPo( pAigCol, Ntl_ModelPoNum(pRoot) + iLatch );
+ pObjCol->pFanin0 = Aig_Not(pObjCol->pFanin0);
+ // unmark the latch output
+ pObjCol = Aig_ManPi( pAigCol, Ntl_ModelPiNum(pRoot) + iLatch );
+ assert( pObjCol->fMarkA == 1 );
+ pObjCol->fMarkA = 0;
+ }
+ iLatch++;
+ }
+}
+
+/**Function*************************************************************
+
Synopsis [Returns AIG with WB after sequential SAT sweeping.]
Description []
@@ -473,13 +550,14 @@ Ntl_Man_t * Ntl_ManSsw2( Ntl_Man_t * p, Fra_Ssw_t * pPars )
Ntl_Man_t * pNew;
Aig_Man_t * pAigRed, * pAigCol;
// collapse the AIG
- pAigCol = Ntl_ManCollapse( p );
+ pAigCol = Ntl_ManCollapse( p, 1 );
pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
// transform the collapsed AIG
pAigRed = Fra_FraigInduction( pAigCol, pPars );
Aig_ManStop( pAigRed );
pAigRed = Aig_ManDupReprBasic( pAigCol );
// insert the result back
+ Ntl_ManFlipEdges( p, pAigRed );
Ntl_ManTransferCopy( p );
pNew = Ntl_ManInsertAig( p, pAigRed );
// attach the white-boxes
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-07 18:52:30 +0000