summaryrefslogtreecommitdiffstats
path: root/src/aig/ntl
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/ntl')
-rw-r--r--src/aig/ntl/ntl.h6
-rw-r--r--src/aig/ntl/ntlEc.c2
-rw-r--r--src/aig/ntl/ntlExtract.c9
-rw-r--r--src/aig/ntl/ntlFraig.c114
-rw-r--r--src/aig/ntl/ntlMan.c29
-rw-r--r--src/aig/ntl/ntlReadBlif.c2
-rw-r--r--src/aig/ntl/ntlWriteBlif.c21
7 files changed, 153 insertions, 30 deletions
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index fc9d21bc..0ba62bea 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -235,7 +235,7 @@ extern void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2,
extern Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 );
/*=== ntlExtract.c ==========================================================*/
extern Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p );
-extern Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p );
+extern Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq );
extern Aig_Man_t * Ntl_ManCollapseForCec( Ntl_Man_t * p );
extern Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 );
/*=== ntlInsert.c ==========================================================*/
@@ -247,12 +247,13 @@ extern int Ntl_ManCheck( Ntl_Man_t * pMan );
extern int Ntl_ModelCheck( Ntl_Mod_t * pModel );
extern void Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel );
/*=== ntlMan.c ============================================================*/
-extern Ntl_Man_t * Ntl_ManAlloc( char * pFileName );
+extern Ntl_Man_t * Ntl_ManAlloc();
extern void Ntl_ManCleanup( Ntl_Man_t * p );
extern Ntl_Man_t * Ntl_ManStartFrom( Ntl_Man_t * p );
extern Ntl_Man_t * Ntl_ManDup( Ntl_Man_t * p );
extern void Ntl_ManFree( Ntl_Man_t * p );
extern int Ntl_ManIsComb( Ntl_Man_t * p );
+extern int Ntl_ManLatchNum( Ntl_Man_t * p );
extern Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName );
extern void Ntl_ManPrintStats( Ntl_Man_t * p );
extern Tim_Man_t * Ntl_ManReadTimeMan( Ntl_Man_t * p );
@@ -292,6 +293,7 @@ extern Tim_Man_t * Ntl_ManCreateTiming( Ntl_Man_t * p );
extern Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck );
/*=== ntlWriteBlif.c ==========================================================*/
extern void Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName );
+extern void Ioa_WriteBlifLogic( Nwk_Man_t * pNtk, Ntl_Man_t * p, char * pFileName );
/*=== ntlUtil.c ==========================================================*/
extern int Ntl_ModelCountLut1( Ntl_Mod_t * pRoot );
extern int Ntl_ManCountSimpleCoDrivers( Ntl_Man_t * p );
diff --git a/src/aig/ntl/ntlEc.c b/src/aig/ntl/ntlEc.c
index 7cb6d6f5..0cd75cbc 100644
--- a/src/aig/ntl/ntlEc.c
+++ b/src/aig/ntl/ntlEc.c
@@ -238,7 +238,7 @@ void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan
// derive AIGs
*ppMan1 = Ntl_ManCollapseForCec( pMan1 );
*ppMan2 = Ntl_ManCollapseForCec( pMan2 );
- // cleanup
+ // cleanup
Ntl_ManFree( pMan1 );
Ntl_ManFree( pMan2 );
}
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index 5a681a7e..f278cba8 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -404,7 +404,7 @@ int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
SeeAlso []
***********************************************************************/
-Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p )
+Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq )
{
Aig_Man_t * pAig;
Ntl_Mod_t * pRoot;
@@ -443,6 +443,8 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p )
assert( Ntl_ObjFanoutNum(pObj) == 1 );
pNet = Ntl_ObjFanout0(pObj);
pNet->pCopy = Aig_ObjCreatePi( p->pAig );
+ if ( fSeq && (pObj->LatchId & 3) == 1 )
+ pNet->pCopy = Aig_Not(pNet->pCopy);
if ( pNet->nVisits )
{
printf( "Ntl_ManCollapse(): Latch output is duplicated or defined as a primary input.\n" );
@@ -470,7 +472,10 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p )
printf( "Ntl_ManCollapse(): Error: Combinational loop is detected.\n" );
return 0;
}
- Aig_ObjCreatePo( p->pAig, pNet->pCopy );
+ if ( fSeq && (pObj->LatchId & 3) == 1 )
+ Aig_ObjCreatePo( p->pAig, Aig_Not(pNet->pCopy) );
+ else
+ Aig_ObjCreatePo( p->pAig, pNet->pCopy );
}
// cleanup the AIG
Aig_ManCleanup( p->pAig );
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
diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c
index b4b63905..e80e02c6 100644
--- a/src/aig/ntl/ntlMan.c
+++ b/src/aig/ntl/ntlMan.c
@@ -39,7 +39,7 @@
SeeAlso []
***********************************************************************/
-Ntl_Man_t * Ntl_ManAlloc( char * pFileName )
+Ntl_Man_t * Ntl_ManAlloc()
{
Ntl_Man_t * p;
// start the manager
@@ -53,9 +53,6 @@ Ntl_Man_t * Ntl_ManAlloc( char * pFileName )
// start the manager
p->pMemObjs = Aig_MmFlexStart();
p->pMemSops = Aig_MmFlexStart();
- // same the names
- p->pName = Ntl_ManStoreFileName( p, pFileName );
- p->pSpec = Ntl_ManStoreName( p, pFileName );
return p;
}
@@ -106,7 +103,9 @@ Ntl_Man_t * Ntl_ManStartFrom( Ntl_Man_t * pOld )
Ntl_Obj_t * pBox;
Ntl_Net_t * pNet;
int i, k;
- pNew = Ntl_ManAlloc( pOld->pSpec );
+ pNew = Ntl_ManAlloc();
+ pNew->pName = Ntl_ManStoreFileName( pNew, pOld->pName );
+ pNew->pSpec = Ntl_ManStoreName( pNew, pOld->pName );
Vec_PtrForEachEntry( pOld->vModels, pModel, i )
if ( i == 0 )
{
@@ -146,7 +145,9 @@ Ntl_Man_t * Ntl_ManDup( Ntl_Man_t * pOld )
Ntl_Obj_t * pBox;
Ntl_Net_t * pNet;
int i, k;
- pNew = Ntl_ManAlloc( pOld->pSpec );
+ pNew = Ntl_ManAlloc();
+ pNew->pName = Ntl_ManStoreFileName( pNew, pOld->pName );
+ pNew->pSpec = Ntl_ManStoreName( pNew, pOld->pName );
Vec_PtrForEachEntry( pOld->vModels, pModel, i )
pModel->pCopy = Ntl_ModelDup( pNew, pModel );
Vec_PtrForEachEntry( pOld->vModels, pModel, i )
@@ -213,6 +214,22 @@ int Ntl_ManIsComb( Ntl_Man_t * p )
/**Function*************************************************************
+ Synopsis [Returns the number of registers.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ntl_ManLatchNum( Ntl_Man_t * p )
+{
+ return Ntl_ModelLatchNum(Ntl_ManRootModel(p));
+}
+
+/**Function*************************************************************
+
Synopsis [Find the model with the given name.]
Description []
diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c
index 23bb6d76..13050047 100644
--- a/src/aig/ntl/ntlReadBlif.c
+++ b/src/aig/ntl/ntlReadBlif.c
@@ -131,6 +131,8 @@ Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck )
}
// set the design name
p->pDesign = Ntl_ManAlloc( pFileName );
+ p->pDesign->pName = Ntl_ManStoreFileName( p->pDesign, pFileName );
+ p->pDesign->pSpec = Ntl_ManStoreName( p->pDesign, pFileName );
// prepare the file for parsing
Ioa_ReadReadPreparse( p );
// parse interfaces of each network
diff --git a/src/aig/ntl/ntlWriteBlif.c b/src/aig/ntl/ntlWriteBlif.c
index 24fa1370..ed45fcaf 100644
--- a/src/aig/ntl/ntlWriteBlif.c
+++ b/src/aig/ntl/ntlWriteBlif.c
@@ -141,7 +141,7 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
/**Function*************************************************************
- Synopsis [Writes the network into the BLIF file.]
+ Synopsis [Writes the netlist into the BLIF file.]
Description []
@@ -170,6 +170,25 @@ void Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName )
fclose( pFile );
}
+/**Function*************************************************************
+
+ Synopsis [Writes the logic network into the BLIF file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ioa_WriteBlifLogic( Nwk_Man_t * pNtk, Ntl_Man_t * p, char * pFileName )
+{
+ Ntl_Man_t * pNew;
+ pNew = Ntl_ManInsertNtk( p, pNtk );
+ Ioa_WriteBlif( pNew, pFileName );
+ Ntl_ManFree( pNew );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-05 19:39:15 +0000