The-OpenROAD-Project/abc
1
0
Fork 0
mirror of https://github.com/The-OpenROAD-Project/abc.git synced 2026-03-12 11:26:17 +08:00
Code Issues Actions Packages Projects Releases Wiki Activity

Version abc70926

Browse Source
This commit is contained in:
Alan Mishchenko
2007-09-26 08:01:00 -07:00
parent d62ee0a90d
commit 7d7e60f2dc
41 changed files with 846 additions and 297 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
abc.dsp
View File

@@ -2798,6 +2798,10 @@ SOURCE=.\src\aig\kit\kit.h
# End Source File
# Begin Source File
SOURCE=.\src\aig\kit\kitAig.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\kit\kitBdd.c
# End Source File
# Begin Source File

21
src/aig/aig/aig.h
View File

@@ -68,19 +68,23 @@ typedef enum {
// the AIG node
struct Aig_Obj_t_ // 8 words
{
void * pData; // misc (cuts, copy, etc)
Aig_Obj_t * pNext; // strashing table
Aig_Obj_t * pFanin0; // fanin
Aig_Obj_t * pFanin1; // fanin
unsigned long Type : 3; // object type
unsigned long fPhase : 1; // value under 000...0 pattern
unsigned long fMarkA : 1; // multipurpose mask
unsigned long fMarkB : 1; // multipurpose mask
unsigned long nRefs : 26; // reference count
unsigned int Type : 3; // object type
unsigned int fPhase : 1; // value under 000...0 pattern
unsigned int fMarkA : 1; // multipurpose mask
unsigned int fMarkB : 1; // multipurpose mask
unsigned int nRefs : 26; // reference count
unsigned Level : 24; // the level of this node
unsigned nCuts : 8; // the number of cuts
int TravId; // unique ID of last traversal involving the node
int Id; // unique ID of the node
union { // temporary store for user's data
void * pData;
int iData;
float dData;
};
};
// the AIG manager
@@ -133,6 +137,10 @@ struct Aig_Man_t_
void (*pImpFunc) (void*, void*); // implication checking precedure
void * pImpData; // implication checking data
Aig_TMan_t * pManTime; // the timing manager
Vec_Int_t * vPiIds;
Vec_Int_t * vPoIds;
Vec_Ptr_t * vMapped;
Vec_Int_t * vFlopNums;
// timing statistics
int time1;
int time2;
@@ -497,6 +505,7 @@ extern void Aig_ObjPrintVerbose( Aig_Obj_t * pObj, int fHaig );
extern void Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig );
extern void Aig_ManDump( Aig_Man_t * p );
extern void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
extern void Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName );
/*=== aigWin.c =========================================================*/
extern void Aig_ManFindCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited, int nSizeLimit, int nFanoutLimit );

3
src/aig/aig/aigCheck.c
View File

@@ -89,7 +89,8 @@ int Aig_ManCheck( Aig_Man_t * p )
}
}
// count the total number of nodes
if ( Aig_ManObjNum(p) != 1 + Aig_ManPiNum(p) + Aig_ManPoNum(p) + Aig_ManBufNum(p) + Aig_ManAndNum(p) + Aig_ManExorNum(p) + Aig_ManLatchNum(p) )
if ( Aig_ManObjNum(p) != 1 + Aig_ManPiNum(p) + Aig_ManPoNum(p) +
Aig_ManBufNum(p) + Aig_ManAndNum(p) + Aig_ManExorNum(p) + Aig_ManLatchNum(p) )
{
printf( "Aig_ManCheck: The number of created nodes is wrong.\n" );
printf( "C1 = %d. Pi = %d. Po = %d. Buf = %d. And = %d. Xor = %d. Lat = %d. Total = %d.\n",

12
src/aig/aig/aigDfs.c
View File

@@ -270,22 +270,22 @@ int Aig_ManCountLevels( Aig_Man_t * p )
Aig_Obj_t * pObj;
int i, LevelsMax, Level0, Level1;
// initialize the levels
Aig_ManConst1(p)->pData = NULL;
Aig_ManConst1(p)->iData = 0;
Aig_ManForEachPi( p, pObj, i )
pObj->pData = NULL;
pObj->iData = 0;
// compute levels in a DFS order
vNodes = Aig_ManDfs( p );
Vec_PtrForEachEntry( vNodes, pObj, i )
{
Level0 = (int)Aig_ObjFanin0(pObj)->pData;
Level1 = (int)Aig_ObjFanin1(pObj)->pData;
pObj->pData = (void *)(1 + Aig_ObjIsExor(pObj) + AIG_MAX(Level0, Level1));
Level0 = Aig_ObjFanin0(pObj)->iData;
Level1 = Aig_ObjFanin1(pObj)->iData;
pObj->iData = 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Level0, Level1);
}
Vec_PtrFree( vNodes );
// get levels of the POs
LevelsMax = 0;
Aig_ManForEachPo( p, pObj, i )
LevelsMax = AIG_MAX( LevelsMax, (int)Aig_ObjFanin0(pObj)->pData );
LevelsMax = AIG_MAX( LevelsMax, Aig_ObjFanin0(pObj)->iData );
return LevelsMax;
}

5
src/aig/aig/aigMan.c
View File

@@ -139,6 +139,8 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->nRegs = p->nRegs;
pNew->nAsserts = p->nAsserts;
if ( p->vFlopNums )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
@@ -226,6 +228,8 @@ void Aig_ManStop( Aig_Man_t * p )
{
Aig_Obj_t * pObj;
int i;
if ( p->vMapped )
Vec_PtrFree( p->vMapped );
// print time
if ( p->time1 ) { PRT( "time1", p->time1 ); }
if ( p->time2 ) { PRT( "time2", p->time2 ); }
@@ -246,6 +250,7 @@ void Aig_ManStop( Aig_Man_t * p )
if ( p->vBufs ) Vec_PtrFree( p->vBufs );
if ( p->vLevelR ) Vec_IntFree( p->vLevelR );
if ( p->vLevels ) Vec_VecFree( p->vLevels );
if ( p->vFlopNums) Vec_IntFree( p->vFlopNums );
FREE( p->pName );
FREE( p->pObjCopies );
FREE( p->pReprs );

4
src/aig/aig/aigPart.c
View File

@@ -890,7 +890,7 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize )
// start the total fraiged AIG
pAigTotal = Aig_ManStartFrom( pAig );
Aig_ManReprStart( pAigTotal, Vec_PtrSize(vAigs) * Aig_ManObjNumMax(pAig) );
Aig_ManReprStart( pAigTotal, Vec_PtrSize(vAigs) * Aig_ManObjNumMax(pAig) + 10000 );
vOutsTotal = Vec_PtrStart( Aig_ManPoNum(pAig) );
// set the PI numbers
@@ -932,7 +932,7 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize )
Aig_ManForEachObj( pAigPart, pObj, k )
ppData[k] = pObj->pData;
// report the process
printf( "Fraiging part %4d (out of %4d) PI = %5d. PO = %5d. And = %6d. Lev = %4d.\r",
printf( "Part %4d (out of %4d) PI = %5d. PO = %5d. And = %6d. Lev = %4d.\r",
i+1, Vec_PtrSize(vParts), Aig_ManPiNum(pAigPart), Aig_ManPoNum(pAigPart),
Aig_ManNodeNum(pAigPart), Aig_ManLevelNum(pAigPart) );
// compute equivalence classes (to be stored in pNew->pReprs)

2
src/aig/aig/aigRepr.c
View File

@@ -270,6 +270,8 @@ Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p, int fOrdered )
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->nRegs = p->nRegs;
if ( p->vFlopNums )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
// map the const and primary inputs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);

17
src/aig/aig/aigScl.c
View File

@@ -50,6 +50,8 @@ Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap )
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->nRegs = p->nRegs;
pNew->nAsserts = p->nAsserts;
if ( p->vFlopNums )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
@@ -152,6 +154,20 @@ int Aig_ManSeqCleanup( Aig_Man_t * p )
// if some latches are removed, update PIs/POs
if ( Vec_PtrSize(vNodes) < Aig_ManPoNum(p) )
{
if ( p->vFlopNums )
{
int nTruePos = Aig_ManPoNum(p)-Aig_ManRegNum(p);
// remember numbers of flops in the flops
Aig_ManForEachLiSeq( p, pObj, i )
pObj->pNext = (void *)Vec_IntEntry( p->vFlopNums, i - nTruePos );
// reset the flop numbers
Vec_PtrForEachEntryStart( vNodes, pObj, i, nTruePos )
Vec_IntWriteEntry( p->vFlopNums, i - nTruePos, (int)pObj->pNext );
Vec_IntShrink( p->vFlopNums, Vec_PtrSize(vNodes) - nTruePos );
// clean the next pointer
Aig_ManForEachLiSeq( p, pObj, i )
pObj->pNext = NULL;
}
// collect new CIs/COs
vCis = Vec_PtrAlloc( Aig_ManPiNum(p) );
Aig_ManForEachPi( p, pObj, i )
@@ -184,6 +200,7 @@ int Aig_ManSeqCleanup( Aig_Man_t * p )
Vec_PtrFree( p->vPos ); p->vPos = vCos;
p->nObjs[AIG_OBJ_PI] = Vec_PtrSize( p->vPis );
p->nObjs[AIG_OBJ_PO] = Vec_PtrSize( p->vPos );
}
Vec_PtrFree( vNodes );
// remove dangling nodes

140
src/aig/aig/aigUtil.c
View File

@@ -672,13 +672,13 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
// collect nodes in the DFS order
vNodes = Aig_ManDfs( p );
// assign IDs to objects
Aig_ManConst1(p)->pData = (void *)Counter++;
Aig_ManConst1(p)->iData = Counter++;
Aig_ManForEachPi( p, pObj, i )
pObj->pData = (void *)Counter++;
pObj->iData = Counter++;
Aig_ManForEachPo( p, pObj, i )
pObj->pData = (void *)Counter++;
pObj->iData = Counter++;
Vec_PtrForEachEntry( vNodes, pObj, i )
pObj->pData = (void *)Counter++;
pObj->iData = Counter++;
nDigits = Aig_Base10Log( Counter );
// write the file
pFile = fopen( pFileName, "w" );
@@ -688,51 +688,157 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
// write PIs
fprintf( pFile, ".inputs" );
Aig_ManForEachPiSeq( p, pObj, i )
fprintf( pFile, " n%0*d", nDigits, (int)pObj->pData );
fprintf( pFile, " n%0*d", nDigits, pObj->iData );
fprintf( pFile, "\n" );
// write POs
fprintf( pFile, ".outputs" );
Aig_ManForEachPoSeq( p, pObj, i )
fprintf( pFile, " n%0*d", nDigits, (int)pObj->pData );
fprintf( pFile, " n%0*d", nDigits, pObj->iData );
fprintf( pFile, "\n" );
// write latches
if ( Aig_ManRegNum(p) )
{
fprintf( pFile, "\n" );
Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
fprintf( pFile, ".latch n%0*d n%0*d 0\n", nDigits, (int)pObjLi->pData, nDigits, (int)pObjLo->pData );
fprintf( pFile, ".latch n%0*d n%0*d 0\n", nDigits, pObjLi->iData, nDigits, pObjLo->iData );
fprintf( pFile, "\n" );
}
// write nodes
Vec_PtrForEachEntry( vNodes, pObj, i )
{
fprintf( pFile, ".names n%0*d n%0*d n%0*d\n",
nDigits, (int)Aig_ObjFanin0(pObj)->pData,
nDigits, (int)Aig_ObjFanin1(pObj)->pData,
nDigits, (int)pObj->pData );
nDigits, Aig_ObjFanin0(pObj)->iData,
nDigits, Aig_ObjFanin1(pObj)->iData,
nDigits, pObj->iData );
fprintf( pFile, "%d%d 1\n", !Aig_ObjFaninC0(pObj), !Aig_ObjFaninC1(pObj) );
}
// write POs
Aig_ManForEachPo( p, pObj, i )
{
if ( (int)pObj->pData == 1359 )
{
int x = 0;
}
fprintf( pFile, ".names n%0*d n%0*d\n",
nDigits, (int)Aig_ObjFanin0(pObj)->pData,
nDigits, (int)pObj->pData );
nDigits, Aig_ObjFanin0(pObj)->iData,
nDigits, pObj->iData );
fprintf( pFile, "%d 1\n", !Aig_ObjFaninC0(pObj) );
if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
pConst1 = Aig_ManConst1(p);
}
if ( pConst1 )
fprintf( pFile, ".names n%0*d\n 1\n", nDigits, (int)pConst1->pData );
fprintf( pFile, ".names n%0*d\n 1\n", nDigits, pConst1->iData );
fprintf( pFile, ".end\n\n" );
fclose( pFile );
Vec_PtrFree( vNodes );
}
/**Function*************************************************************
Synopsis [Writes the AIG into the BLIF file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName )
{
FILE * pFile;
Vec_Ptr_t * vNodes;
Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pConst1 = NULL;
int i, nDigits, Counter = 0;
if ( Aig_ManPoNum(p) == 0 )
{
printf( "Aig_ManDumpBlif(): AIG manager does not have POs.\n" );
return;
}
// collect nodes in the DFS order
vNodes = Aig_ManDfs( p );
// assign IDs to objects
Aig_ManConst1(p)->iData = Counter++;
Aig_ManForEachPi( p, pObj, i )
pObj->iData = Counter++;
Aig_ManForEachPo( p, pObj, i )
pObj->iData = Counter++;
Vec_PtrForEachEntry( vNodes, pObj, i )
pObj->iData = Counter++;
nDigits = Aig_Base10Log( Counter );
// write the file
pFile = fopen( pFileName, "w" );
fprintf( pFile, "// Verilog file written by procedure Aig_ManDumpVerilog() in ABC\n" );
fprintf( pFile, "// http://www.eecs.berkeley.edu/~alanmi/abc/\n" );
fprintf( pFile, "module %s ( clock", p->pName? p->pName: "test" );
Aig_ManForEachPiSeq( p, pObj, i )
fprintf( pFile, ", n%0*d", nDigits, pObj->iData );
Aig_ManForEachPoSeq( p, pObj, i )
fprintf( pFile, ", n%0*d", nDigits, pObj->iData );
fprintf( pFile, " );\n" );
// write PIs
Aig_ManForEachPiSeq( p, pObj, i )
fprintf( pFile, "input n%0*d;\n", nDigits, pObj->iData );
// write POs
Aig_ManForEachPoSeq( p, pObj, i )
fprintf( pFile, "output n%0*d;\n", nDigits, pObj->iData );
// write latches
if ( Aig_ManRegNum(p) )
{
Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
fprintf( pFile, "reg n%0*d;\n", nDigits, pObjLo->iData );
Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
fprintf( pFile, "wire n%0*d;\n", nDigits, pObjLi->iData );
}
// write nodes
Vec_PtrForEachEntry( vNodes, pObj, i )
fprintf( pFile, "wire n%0*d;\n", nDigits, pObj->iData );
// write nodes
Vec_PtrForEachEntry( vNodes, pObj, i )
{
fprintf( pFile, "assign n%0*d = %sn%0*d & %sn%0*d;\n",
nDigits, pObj->iData,
!Aig_ObjFaninC0(pObj) ? " " : "~", nDigits, Aig_ObjFanin0(pObj)->iData,
!Aig_ObjFaninC1(pObj) ? " " : "~", nDigits, Aig_ObjFanin1(pObj)->iData
);
}
// write POs
Aig_ManForEachPoSeq( p, pObj, i )
{
fprintf( pFile, "assign n%0*d = %sn%0*d;\n",
nDigits, pObj->iData,
!Aig_ObjFaninC0(pObj) ? " " : "~", nDigits, Aig_ObjFanin0(pObj)->iData );
if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
pConst1 = Aig_ManConst1(p);
}
if ( Aig_ManRegNum(p) )
{
Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
{
fprintf( pFile, "assign n%0*d = %sn%0*d;\n",
nDigits, pObjLi->iData,
!Aig_ObjFaninC0(pObjLi) ? " " : "~", nDigits, Aig_ObjFanin0(pObjLi)->iData );
if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObjLi)) )
pConst1 = Aig_ManConst1(p);
}
}
if ( pConst1 )
fprintf( pFile, "assign n%0*d = 1\'b1;\n", nDigits, pConst1->iData );
// write initial state
if ( Aig_ManRegNum(p) )
{
Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
fprintf( pFile, "always @ (posedge clock) begin n%0*d <= n%0*d; end\n",
nDigits, pObjLo->iData,
nDigits, pObjLi->iData );
Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
fprintf( pFile, "initial begin n%0*d <= 1\'b0; end\n",
nDigits, pObjLo->iData );
}
fprintf( pFile, "endmodule\n\n" );
fclose( pFile );
Vec_PtrFree( vNodes );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

1
src/aig/aig/module.make
View File

@@ -13,6 +13,7 @@ SRC += src/aig/aig/aigCheck.c \
src/aig/aig/aigScl.c \
src/aig/aig/aigSeq.c \
src/aig/aig/aigTable.c \
src/aig/aig/aigTime.c \
src/aig/aig/aigTiming.c \
src/aig/aig/aigTruth.c \
src/aig/aig/aigTsim.c \

2
src/aig/dar/darBalance.c
View File

@@ -57,6 +57,8 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->nRegs = p->nRegs;
pNew->nAsserts = p->nAsserts;
if ( p->vFlopNums )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
// map the PI nodes
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);

8
src/aig/dar/darRefact.c
View File

@@ -463,7 +463,7 @@ int Dar_ObjCutLevelAchieved( Vec_Ptr_t * vCut, int nLevelMin )
***********************************************************************/
int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
{
ProgressBar * pProgress;
Bar_Progress_t * pProgress;
Ref_Man_t * p;
Vec_Ptr_t * vCut, * vCut2;
Aig_Obj_t * pObj, * pObjNew;
@@ -485,10 +485,10 @@ int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
vCut2 = Vec_VecEntry( p->vCuts, 1 );
p->nNodesInit = Aig_ManNodeNum(pAig);
nNodesOld = Vec_PtrSize( pAig->vObjs );
pProgress = Extra_ProgressBarStart( stdout, nNodesOld );
pProgress = Bar_ProgressStart( stdout, nNodesOld );
Aig_ManForEachObj( pAig, pObj, i )
{
Extra_ProgressBarUpdate( pProgress, i, NULL );
Bar_ProgressUpdate( pProgress, i, NULL );
if ( !Aig_ObjIsNode(pObj) )
continue;
if ( i > nNodesOld )
@@ -564,7 +564,7 @@ p->timeEval += clock() - clk;
p->timeTotal = clock() - clkStart;
p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
Extra_ProgressBarStop( pProgress );
Bar_ProgressStop( pProgress );
// put the nodes into the DFS order and reassign their IDs
// Aig_NtkReassignIds( p );
// fix the levels

9
src/aig/fra/fraInd.c
View File

@@ -147,6 +147,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
Fra_ObjSetFraig( pObj, 0, Aig_ObjCreatePi(pManFraig) );
// add timeframes
// pManFraig->fAddStrash = 1;
for ( f = 0; f < p->nFramesAll - 1; f++ )
{
// set the constraints on the latch outputs
@@ -163,6 +164,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
Aig_ManForEachLiLoSeq( p->pManAig, pObjLi, pObjLo, k )
Fra_ObjSetFraig( pObjLo, f+1, Fra_ObjChild0Fra(pObjLi,f) );
}
// pManFraig->fAddStrash = 0;
// mark the asserts
pManFraig->nAsserts = Aig_ManPoNum(pManFraig);
// add the POs for the latch outputs of the last frame
@@ -348,7 +350,9 @@ PRT( "Time", clock() - clk );
// mark the classes as non-refined
p->pCla->fRefinement = 0;
// derive non-init K-timeframes while implementing e-classes
clk2 = clock();
p->pManFraig = Fra_FramesWithClasses( p );
p->timeTrav += clock() - clk2;
//Aig_ManDumpBlif( p->pManFraig, "testaig.blif" );
// perform AIG rewriting
@@ -406,6 +410,9 @@ PRT( "Time", clock() - clk );
p->nSatCallsRecent = 0;
p->nSatCallsSkipped = 0;
Fra_FraigSweep( p );
// Sat_SolverPrintStats( stdout, p->pSat );
// remove FRAIG and SAT solver
Aig_ManStop( p->pManFraig ); p->pManFraig = NULL;
sat_solver_delete( p->pSat ); p->pSat = NULL;
@@ -425,7 +432,7 @@ PRT( "Time", clock() - clk );
}
}
/*
// check implications using simulation
// verify implications using simulation
if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
{
int Temp, clk = clock();

6
src/aig/fra/fraSec.c
View File

@@ -169,7 +169,7 @@ PRT( "Time", clock() - clk );
// perform fraiging
clk = clock();
pNew = Fra_FraigEquivence( pTemp = pNew, 1000 );
pNew = Fra_FraigEquivence( pTemp = pNew, 100 );
Aig_ManStop( pTemp );
if ( fVerbose )
{
@@ -199,13 +199,14 @@ PRT( "Time", clock() - clk );
clk = clock();
pNew = Aig_ManDup( pTemp = pNew, 1 );
Aig_ManStop( pTemp );
pNew = Dar_ManRewriteDefault( pTemp = pNew );
pNew = Dar_ManRewriteDefault( pNew );
if ( fVerbose )
{
printf( "Rewriting: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
PRT( "Time", clock() - clk );
}
// perform retiming
clk = clock();
pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
@@ -218,6 +219,7 @@ clk = clock();
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
PRT( "Time", clock() - clk );
}
if ( pNew->nRegs )
pNew = Aig_ManConstReduce( pNew, 0 );

5
src/aig/fra/fraSim.c
View File

@@ -432,12 +432,11 @@ void Fra_SmlAssignDist1( Fra_Sml_t * p, unsigned * pPat )
// assert( p->pManFraig == NULL || nTruePis * p->nFrames + k == Aig_ManPiNum(p->pManFraig) );
// flip one bit of the last frame
if ( fUseDist1 && p->nFrames == 2 )
if ( fUseDist1 ) //&& p->nFrames == 2 )
{
Limit = AIG_MIN( nTruePis, p->nWordsFrame * 32 - 1 );
for ( i = 0; i < Limit; i++ )
Aig_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ), i+1 );
// Aig_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig, nTruePis*(p->nFrames-2) + i)->Id ), i+1 );
Aig_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ) + p->nWordsFrame*(p->nFrames-1), i+1 );
}
}
}

10
src/aig/hop/hop.h
View File

@@ -67,11 +67,11 @@ struct Hop_Obj_t_ // 6 words
Hop_Obj_t * pNext; // strashing table
Hop_Obj_t * pFanin0; // fanin
Hop_Obj_t * pFanin1; // fanin
unsigned long Type : 3; // object type
unsigned long fPhase : 1; // value under 000...0 pattern
unsigned long fMarkA : 1; // multipurpose mask
unsigned long fMarkB : 1; // multipurpose mask
unsigned long nRefs : 26; // reference count (level)
unsigned int Type : 3; // object type
unsigned int fPhase : 1; // value under 000...0 pattern
unsigned int fMarkA : 1; // multipurpose mask
unsigned int fMarkB : 1; // multipurpose mask
unsigned int nRefs : 26; // reference count (level)
int Id; // unique ID of the node
};

3
src/aig/ioa/ioaWriteAig.c
View File

@@ -249,7 +249,8 @@ void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols )
*/
// write the comment
fprintf( pFile, "c\n" );
fprintf( pFile, "%s\n", pMan->pName );
if ( pMan->pName )
fprintf( pFile, ".model %s\n", pMan->pName );
fprintf( pFile, "This file was produced by the AIG package in ABC on %s\n", Ioa_TimeStamp() );
fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
fclose( pFile );

8
src/aig/ivy/ivyFraig.c
View File

@@ -2101,8 +2101,8 @@ int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pN
p->nSatVars = 1;
sat_solver_setnvars( p->pSat, 1000 );
// var 0 is reserved for const1 node - add the clause
pLits[0] = toLit( 0 );
sat_solver_addclause( p->pSat, pLits, pLits + 1 );
// pLits[0] = toLit( 0 );
// sat_solver_addclause( p->pSat, pLits, pLits + 1 );
}
// if the nodes do not have SAT variables, allocate them
@@ -2235,8 +2235,8 @@ int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew )
p->nSatVars = 1;
sat_solver_setnvars( p->pSat, 1000 );
// var 0 is reserved for const1 node - add the clause
pLits[0] = toLit( 0 );
sat_solver_addclause( p->pSat, pLits, pLits + 1 );
// pLits[0] = toLit( 0 );
// sat_solver_addclause( p->pSat, pLits, pLits + 1 );
}
// if the nodes do not have SAT variables, allocate them

121
src/aig/kit/kitAig.c Normal file
View File

@@ -0,0 +1,121 @@
/**CFile****************************************************************
FileName [kitAig.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Computation kit.]
Synopsis [Procedures involving AIGs.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - Dec 6, 2006.]
Revision [$Id: kitAig.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
***********************************************************************/
#include "kit.h"
#include "aig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Transforms the decomposition graph into the AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Kit_GraphToAigInternal( Aig_Man_t * pMan, Kit_Graph_t * pGraph )
{
Kit_Node_t * pNode;
Aig_Obj_t * pAnd0, * pAnd1;
int i;
// check for constant function
if ( Kit_GraphIsConst(pGraph) )
return Aig_NotCond( Aig_ManConst1(pMan), Kit_GraphIsComplement(pGraph) );
// check for a literal
if ( Kit_GraphIsVar(pGraph) )
return Aig_NotCond( Kit_GraphVar(pGraph)->pFunc, Kit_GraphIsComplement(pGraph) );
// build the AIG nodes corresponding to the AND gates of the graph
Kit_GraphForEachNode( pGraph, pNode, i )
{
pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );
pAnd1 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );
pNode->pFunc = Aig_And( pMan, pAnd0, pAnd1 );
}
// complement the result if necessary
return Aig_NotCond( pNode->pFunc, Kit_GraphIsComplement(pGraph) );
}
/**Function*************************************************************
Synopsis [Strashes one logic node using its SOP.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Kit_GraphToAig( Aig_Man_t * pMan, Aig_Obj_t ** pFanins, Kit_Graph_t * pGraph )
{
Kit_Node_t * pNode;
int i;
// collect the fanins
Kit_GraphForEachLeaf( pGraph, pNode, i )
pNode->pFunc = pFanins[i];
// perform strashing
return Kit_GraphToAigInternal( pMan, pGraph );
}
/**Function*************************************************************
Synopsis [Strashed onen logic nodes using its truth table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Kit_TruthToAig( Aig_Man_t * pMan, Aig_Obj_t ** pFanins, unsigned * pTruth, int nVars, Vec_Int_t * vMemory )
{
Aig_Obj_t * pObj;
Kit_Graph_t * pGraph;
// transform truth table into the decomposition tree
if ( vMemory == NULL )
{
vMemory = Vec_IntAlloc( 0 );
pGraph = Kit_TruthToGraph( pTruth, nVars, vMemory );
Vec_IntFree( vMemory );
}
else
pGraph = Kit_TruthToGraph( pTruth, nVars, vMemory );
// derive the AIG for the decomposition tree
pObj = Kit_GraphToAig( pMan, pFanins, pGraph );
Kit_GraphFree( pGraph );
return pObj;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

2
src/aig/kit/kitDsd.c
View File

@@ -2058,7 +2058,7 @@ int Kit_DsdEval( unsigned * pTruth, int nVars, int nLutSize )
// recompute the truth table
p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk) );
pTruthC = Kit_DsdTruthCompute( p, pNtk );
if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
if ( !Kit_TruthIsEqual( pTruth, pTruthC, nVars ) )
printf( "Verification failed.\n" );
Kit_DsdManFree( p );

60
src/aig/kit/kitIsop.c
View File

@@ -58,7 +58,7 @@ int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryB
assert( nVars >= 0 && nVars < 16 );
// if nVars < 5, make sure it does not depend on those vars
// for ( i = nVars; i < 5; i++ )
// assert( !Extra_TruthVarInSupport(puTruth, 5, i) );
// assert( !Kit_TruthVarInSupport(puTruth, 5, i) );
// prepare memory manager
Vec_IntClear( vMemory );
Vec_IntGrow( vMemory, KIT_ISOP_MEM_LIMIT );
@@ -69,7 +69,7 @@ int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryB
vMemory->nSize = -1;
return -1;
}
assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) );
assert( Kit_TruthIsEqual( puTruth, pResult, nVars ) );
if ( pcRes->nCubes == 0 || (pcRes->nCubes == 1 && pcRes->pCubes[0] == 0) )
{
vMemory->pArray[0] = 0;
@@ -79,18 +79,18 @@ int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryB
if ( fTryBoth )
{
// compute ISOP for the complemented polarity
Extra_TruthNot( puTruth, puTruth, nVars );
Kit_TruthNot( puTruth, puTruth, nVars );
pResult = Kit_TruthIsop_rec( puTruth, puTruth, nVars, pcRes2, vMemory );
if ( pcRes2->nCubes >= 0 )
{
assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) );
assert( Kit_TruthIsEqual( puTruth, pResult, nVars ) );
if ( pcRes->nCubes > pcRes2->nCubes )
{
RetValue = 1;
pcRes = pcRes2;
}
}
Extra_TruthNot( puTruth, puTruth, nVars );
Kit_TruthNot( puTruth, puTruth, nVars );
}
// printf( "%d ", vMemory->nSize );
// move the cover representation to the beginning of the memory buffer
@@ -117,9 +117,9 @@ unsigned * Kit_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Kit
unsigned * puRes0, * puRes1, * puRes2;
unsigned * puOn0, * puOn1, * puOnDc0, * puOnDc1, * pTemp, * pTemp0, * pTemp1;
int i, k, Var, nWords, nWordsAll;
// assert( Extra_TruthIsImply( puOn, puOnDc, nVars ) );
// assert( Kit_TruthIsImply( puOn, puOnDc, nVars ) );
// allocate room for the resulting truth table
nWordsAll = Extra_TruthWordNum( nVars );
nWordsAll = Kit_TruthWordNum( nVars );
pTemp = Vec_IntFetch( vStore, nWordsAll );
if ( pTemp == NULL )
{
@@ -127,14 +127,14 @@ unsigned * Kit_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Kit
return NULL;
}
// check for constants
if ( Extra_TruthIsConst0( puOn, nVars ) )
if ( Kit_TruthIsConst0( puOn, nVars ) )
{
pcRes->nCubes = 0;
pcRes->pCubes = NULL;
Extra_TruthClear( pTemp, nVars );
Kit_TruthClear( pTemp, nVars );
return pTemp;
}
if ( Extra_TruthIsConst1( puOnDc, nVars ) )
if ( Kit_TruthIsConst1( puOnDc, nVars ) )
{
pcRes->nCubes = 1;
pcRes->pCubes = Vec_IntFetch( vStore, 1 );
@@ -144,14 +144,14 @@ unsigned * Kit_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Kit
return NULL;
}
pcRes->pCubes[0] = 0;
Extra_TruthFill( pTemp, nVars );
Kit_TruthFill( pTemp, nVars );
return pTemp;
}
assert( nVars > 0 );
// find the topmost var
for ( Var = nVars-1; Var >= 0; Var-- )
if ( Extra_TruthVarInSupport( puOn, nVars, Var ) ||
Extra_TruthVarInSupport( puOnDc, nVars, Var ) )
if ( Kit_TruthVarInSupport( puOn, nVars, Var ) ||
Kit_TruthVarInSupport( puOnDc, nVars, Var ) )
break;
assert( Var >= 0 );
// consider a simple case when one-word computation can be used
@@ -163,30 +163,30 @@ unsigned * Kit_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Kit
return pTemp;
}
assert( Var >= 5 );
nWords = Extra_TruthWordNum( Var );
nWords = Kit_TruthWordNum( Var );
// cofactor
puOn0 = puOn; puOn1 = puOn + nWords;
puOnDc0 = puOnDc; puOnDc1 = puOnDc + nWords;
pTemp0 = pTemp; pTemp1 = pTemp + nWords;
// solve for cofactors
Extra_TruthSharp( pTemp0, puOn0, puOnDc1, Var );
Kit_TruthSharp( pTemp0, puOn0, puOnDc1, Var );
puRes0 = Kit_TruthIsop_rec( pTemp0, puOnDc0, Var, pcRes0, vStore );
if ( pcRes0->nCubes == -1 )
{
pcRes->nCubes = -1;
return NULL;
}
Extra_TruthSharp( pTemp1, puOn1, puOnDc0, Var );
Kit_TruthSharp( pTemp1, puOn1, puOnDc0, Var );
puRes1 = Kit_TruthIsop_rec( pTemp1, puOnDc1, Var, pcRes1, vStore );
if ( pcRes1->nCubes == -1 )
{
pcRes->nCubes = -1;
return NULL;
}
Extra_TruthSharp( pTemp0, puOn0, puRes0, Var );
Extra_TruthSharp( pTemp1, puOn1, puRes1, Var );
Extra_TruthOr( pTemp0, pTemp0, pTemp1, Var );
Extra_TruthAnd( pTemp1, puOnDc0, puOnDc1, Var );
Kit_TruthSharp( pTemp0, puOn0, puRes0, Var );
Kit_TruthSharp( pTemp1, puOn1, puRes1, Var );
Kit_TruthOr( pTemp0, pTemp0, pTemp1, Var );
Kit_TruthAnd( pTemp1, puOnDc0, puOnDc1, Var );
puRes2 = Kit_TruthIsop_rec( pTemp0, pTemp1, Var, pcRes2, vStore );
if ( pcRes2->nCubes == -1 )
{
@@ -210,16 +210,16 @@ unsigned * Kit_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Kit
pcRes->pCubes[k++] = pcRes2->pCubes[i];
assert( k == pcRes->nCubes );
// create the resulting truth table
Extra_TruthOr( pTemp0, puRes0, puRes2, Var );
Extra_TruthOr( pTemp1, puRes1, puRes2, Var );
Kit_TruthOr( pTemp0, puRes0, puRes2, Var );
Kit_TruthOr( pTemp1, puRes1, puRes2, Var );
// copy the table if needed
nWords <<= 1;
for ( i = 1; i < nWordsAll/nWords; i++ )
for ( k = 0; k < nWords; k++ )
pTemp[i*nWords + k] = pTemp[k];
// verify in the end
// assert( Extra_TruthIsImply( puOn, pTemp, nVars ) );
// assert( Extra_TruthIsImply( pTemp, puOnDc, nVars ) );
// assert( Kit_TruthIsImply( puOn, pTemp, nVars ) );
// assert( Kit_TruthIsImply( pTemp, puOnDc, nVars ) );
return pTemp;
}
@@ -264,17 +264,17 @@ unsigned Kit_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Kit_Sop_t
assert( nVars > 0 );
// find the topmost var
for ( Var = nVars-1; Var >= 0; Var-- )
if ( Extra_TruthVarInSupport( &uOn, 5, Var ) ||
Extra_TruthVarInSupport( &uOnDc, 5, Var ) )
if ( Kit_TruthVarInSupport( &uOn, 5, Var ) ||
Kit_TruthVarInSupport( &uOnDc, 5, Var ) )
break;
assert( Var >= 0 );
// cofactor
uOn0 = uOn1 = uOn;
uOnDc0 = uOnDc1 = uOnDc;
Extra_TruthCofactor0( &uOn0, Var + 1, Var );
Extra_TruthCofactor1( &uOn1, Var + 1, Var );
Extra_TruthCofactor0( &uOnDc0, Var + 1, Var );
Extra_TruthCofactor1( &uOnDc1, Var + 1, Var );
Kit_TruthCofactor0( &uOn0, Var + 1, Var );
Kit_TruthCofactor1( &uOn1, Var + 1, Var );
Kit_TruthCofactor0( &uOnDc0, Var + 1, Var );
Kit_TruthCofactor1( &uOnDc1, Var + 1, Var );
// solve for cofactors
uRes0 = Kit_TruthIsop5_rec( uOn0 & ~uOnDc1, uOnDc0, Var, pcRes0, vStore );
if ( pcRes0->nCubes == -1 )

29
src/aig/kit/kitTruth.c
View File

@@ -1632,6 +1632,33 @@ int Kit_TruthCountMinterms( unsigned * pTruth, int nVars, int * pRes, int * pByt
return nTotal;
}
/**Function*************************************************************
Synopsis [Prints the hex unsigned into a file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_PrintHexadecimal( FILE * pFile, unsigned Sign[], int nVars )
{
int nDigits, Digit, k;
// write the number into the file
nDigits = (1 << nVars) / 4;
for ( k = nDigits - 1; k >= 0; k-- )
{
Digit = ((Sign[k/8] >> ((k%8) * 4)) & 15);
if ( Digit < 10 )
fprintf( pFile, "%d", Digit );
else
fprintf( pFile, "%c", 'a' + Digit-10 );
}
// fprintf( pFile, "\n" );
}
/**Function*************************************************************
Synopsis [Fast counting minterms for the functions.]
@@ -1665,7 +1692,7 @@ void Kit_TruthCountMintermsPrecomp()
uWord |= (bit_count[i & 0x33] << 16);
uWord |= (bit_count[i & 0x0f] << 24);
printf( "0x" );
Extra_PrintHexadecimal( stdout, &uWord, 5 );
Kit_PrintHexadecimal( stdout, &uWord, 5 );
printf( ", " );
}
}

3
src/aig/kit/module.make
View File

@@ -1,4 +1,5 @@
SRC += src/aig/kit/kitBdd.c \
SRC += src/aig/kit/kitAig.c \
src/aig/kit/kitBdd.c \
src/aig/kit/kitCloud.c src/aig/kit/cloud.c \
src/aig/kit/kitDsd.c \
src/aig/kit/kitFactor.c \

60
src/base/abc/abc.h
View File

@@ -638,6 +638,8 @@ extern int Abc_NtkCountSelfFeedLatches( Abc_Ntk_t * pNtk );
extern int Abc_NtkRemoveSelfFeedLatches( Abc_Ntk_t * pNtk );
extern Vec_Int_t * Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk );
extern void Abc_NtkInsertLatchValues( Abc_Ntk_t * pNtk, Vec_Int_t * vValues );
extern Abc_Obj_t * Abc_NtkAddLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pDriver, Abc_InitType_t Init );
extern void Abc_NtkConvertDcLatches( Abc_Ntk_t * pNtk );
/*=== abcLib.c ==========================================================*/
extern Abc_Lib_t * Abc_LibCreate( char * pName );
extern void Abc_LibFree( Abc_Lib_t * pLib, Abc_Ntk_t * pNtk );
@@ -662,35 +664,6 @@ extern Abc_Ntk_t * Abc_NtkMiterQuantifyPis( Abc_Ntk_t * pNtk );
extern int Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter );
extern void Abc_NtkMiterReport( Abc_Ntk_t * pMiter );
extern Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial );
/*=== abcObj.c ==========================================================*/
extern Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
extern void Abc_ObjRecycle( Abc_Obj_t * pObj );
extern Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
extern void Abc_NtkDeleteObj( Abc_Obj_t * pObj );
extern void Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj, int fOnlyNodes );
extern void Abc_NtkDeleteAll_rec( Abc_Obj_t * pObj );
extern Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCopyName );
extern Abc_Obj_t * Abc_NtkDupBox( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pBox, int fCopyName );
extern Abc_Obj_t * Abc_NtkCloneObj( Abc_Obj_t * pNode );
extern Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName );
extern Abc_Obj_t * Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName );
extern Abc_Obj_t * Abc_NtkFindCi( Abc_Ntk_t * pNtk, char * pName );
extern Abc_Obj_t * Abc_NtkFindCo( Abc_Ntk_t * pNtk, char * pName );
extern Abc_Obj_t * Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName );
extern Abc_Obj_t * Abc_NtkCreateNodeConst0( Abc_Ntk_t * pNtk );
extern Abc_Obj_t * Abc_NtkCreateNodeConst1( Abc_Ntk_t * pNtk );
extern Abc_Obj_t * Abc_NtkCreateNodeInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin );
extern Abc_Obj_t * Abc_NtkCreateNodeBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin );
extern Abc_Obj_t * Abc_NtkCreateNodeAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
extern Abc_Obj_t * Abc_NtkCreateNodeOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
extern Abc_Obj_t * Abc_NtkCreateNodeExor( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
extern Abc_Obj_t * Abc_NtkCreateNodeMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t * pNode1, Abc_Obj_t * pNode0 );
extern bool Abc_NodeIsConst( Abc_Obj_t * pNode );
extern bool Abc_NodeIsConst0( Abc_Obj_t * pNode );
extern bool Abc_NodeIsConst1( Abc_Obj_t * pNode );
extern bool Abc_NodeIsBuf( Abc_Obj_t * pNode );
extern bool Abc_NodeIsInv( Abc_Obj_t * pNode );
extern void Abc_NodeComplement( Abc_Obj_t * pNode );
/*=== abcNames.c ====================================================*/
extern char * Abc_ObjName( Abc_Obj_t * pNode );
extern char * Abc_ObjAssignName( Abc_Obj_t * pObj, char * pName, char * pSuffix );
@@ -737,6 +710,35 @@ extern Abc_Ntk_t * Abc_NtkCreateWithNode( char * pSop );
extern void Abc_NtkDelete( Abc_Ntk_t * pNtk );
extern void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk );
extern void Abc_NtkMakeComb( Abc_Ntk_t * pNtk );
/*=== abcObj.c ==========================================================*/
extern Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
extern void Abc_ObjRecycle( Abc_Obj_t * pObj );
extern Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
extern void Abc_NtkDeleteObj( Abc_Obj_t * pObj );
extern void Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj, int fOnlyNodes );
extern void Abc_NtkDeleteAll_rec( Abc_Obj_t * pObj );
extern Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCopyName );
extern Abc_Obj_t * Abc_NtkDupBox( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pBox, int fCopyName );
extern Abc_Obj_t * Abc_NtkCloneObj( Abc_Obj_t * pNode );
extern Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName );
extern Abc_Obj_t * Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName );
extern Abc_Obj_t * Abc_NtkFindCi( Abc_Ntk_t * pNtk, char * pName );
extern Abc_Obj_t * Abc_NtkFindCo( Abc_Ntk_t * pNtk, char * pName );
extern Abc_Obj_t * Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName );
extern Abc_Obj_t * Abc_NtkCreateNodeConst0( Abc_Ntk_t * pNtk );
extern Abc_Obj_t * Abc_NtkCreateNodeConst1( Abc_Ntk_t * pNtk );
extern Abc_Obj_t * Abc_NtkCreateNodeInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin );
extern Abc_Obj_t * Abc_NtkCreateNodeBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin );
extern Abc_Obj_t * Abc_NtkCreateNodeAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
extern Abc_Obj_t * Abc_NtkCreateNodeOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
extern Abc_Obj_t * Abc_NtkCreateNodeExor( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
extern Abc_Obj_t * Abc_NtkCreateNodeMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t * pNode1, Abc_Obj_t * pNode0 );
extern bool Abc_NodeIsConst( Abc_Obj_t * pNode );
extern bool Abc_NodeIsConst0( Abc_Obj_t * pNode );
extern bool Abc_NodeIsConst1( Abc_Obj_t * pNode );
extern bool Abc_NodeIsBuf( Abc_Obj_t * pNode );
extern bool Abc_NodeIsInv( Abc_Obj_t * pNode );
extern void Abc_NodeComplement( Abc_Obj_t * pNode );
/*=== abcPrint.c ==========================================================*/
extern void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored );
extern void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk );

107
src/base/abc/abcLatch.c
View File

@@ -211,6 +211,113 @@ void Abc_NtkInsertLatchValues( Abc_Ntk_t * pNtk, Vec_Int_t * vValues )
pLatch->pData = (void *)(vValues? (Vec_IntEntry(vValues,i)? ABC_INIT_ONE : ABC_INIT_ZERO) : ABC_INIT_DC);
}
/**Function*************************************************************
Synopsis [Creates latch with the given initial value.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Obj_t * Abc_NtkAddLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pDriver, Abc_InitType_t Init )
{
Abc_Obj_t * pLatchOut, * pLatch, * pLatchIn;
pLatchOut = Abc_NtkCreateBo(pNtk);
pLatch = Abc_NtkCreateLatch(pNtk);
pLatchIn = Abc_NtkCreateBi(pNtk);
Abc_ObjAssignName( pLatchOut, Abc_ObjName(pLatch), "_lo" );
Abc_ObjAssignName( pLatchIn, Abc_ObjName(pLatch), "_li" );
Abc_ObjAddFanin( pLatchOut, pLatch );
Abc_ObjAddFanin( pLatch, pLatchIn );
Abc_ObjAddFanin( pLatchIn, pDriver );
pLatch->pData = (void *)Init;
return pLatchOut;
}
/**Function*************************************************************
Synopsis [Creates MUX.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkNodeConvertToMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t * pNode1, Abc_Obj_t * pNode0, Abc_Obj_t * pMux )
{
assert( Abc_NtkIsLogic(pNtk) );
Abc_ObjAddFanin( pMux, pNodeC );
Abc_ObjAddFanin( pMux, pNode1 );
Abc_ObjAddFanin( pMux, pNode0 );
if ( Abc_NtkHasSop(pNtk) )
pMux->pData = Abc_SopRegister( pNtk->pManFunc, "11- 1\n0-1 1\n" );
else if ( Abc_NtkHasBdd(pNtk) )
pMux->pData = Cudd_bddIte(pNtk->pManFunc,Cudd_bddIthVar(pNtk->pManFunc,0),Cudd_bddIthVar(pNtk->pManFunc,1),Cudd_bddIthVar(pNtk->pManFunc,2)), Cudd_Ref( pMux->pData );
else if ( Abc_NtkHasAig(pNtk) )
pMux->pData = Hop_Mux(pNtk->pManFunc,Hop_IthVar(pNtk->pManFunc,0),Hop_IthVar(pNtk->pManFunc,1),Hop_IthVar(pNtk->pManFunc,2));
else
assert( 0 );
}
/**Function*************************************************************
Synopsis [Converts registers with DC values into additional PIs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkConvertDcLatches( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pCtrl, * pLatch, * pMux, * pPi;
Abc_InitType_t Init = ABC_INIT_ZERO;
int i, fFound = 0, Counter;
// check if there are latches with DC values
Abc_NtkForEachLatch( pNtk, pLatch, i )
if ( Abc_LatchIsInitDc(pLatch) )
{
fFound = 1;
break;
}
if ( !fFound )
return;
// add control latch
pCtrl = Abc_NtkAddLatch( pNtk, Abc_NtkCreateNodeConst1(pNtk), Init );
// add fanouts for each latch with DC values
Counter = 0;
Abc_NtkForEachLatch( pNtk, pLatch, i )
{
if ( !Abc_LatchIsInitDc(pLatch) )
continue;
// change latch value
pLatch->pData = (void *)Init;
// if the latch output has the same name as a PO, rename it
if ( Abc_NodeFindCoFanout( Abc_ObjFanout0(pLatch) ) )
{
Nm_ManDeleteIdName( pLatch->pNtk->pManName, Abc_ObjFanout0(pLatch)->Id );
Abc_ObjAssignName( Abc_ObjFanout0(pLatch), Abc_ObjName(pLatch), "_lo" );
}
// create new PIs
pPi = Abc_NtkCreatePi( pNtk );
Abc_ObjAssignName( pPi, Abc_ObjName(pLatch), "_pi" );
// create a new node and transfer fanout from latch output to the new node
pMux = Abc_NtkCreateNode( pNtk );
Abc_ObjTransferFanout( Abc_ObjFanout0(pLatch), pMux );
// convert the node into a mux
Abc_NtkNodeConvertToMux( pNtk, pCtrl, Abc_ObjFanout0(pLatch), pPi, pMux );
Counter++;
}
printf( "The number of converted latches with DC values = %d.\n", Counter );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

73
src/base/abci/abc.c
View File

@@ -161,6 +161,7 @@ static int Abc_CommandIf ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandScut ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandInit ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandZero ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandUndc ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPipe ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSeq ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandUnseq ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -329,6 +330,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
// Cmd_CommandAdd( pAbc, "Sequential", "scut", Abc_CommandScut, 0 );
Cmd_CommandAdd( pAbc, "Sequential", "init", Abc_CommandInit, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "zero", Abc_CommandZero, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "undc", Abc_CommandUndc, 1 );
// Cmd_CommandAdd( pAbc, "Sequential", "pipe", Abc_CommandPipe, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "retime", Abc_CommandRetime, 1 );
// Cmd_CommandAdd( pAbc, "Sequential", "sfpga", Abc_CommandSeqFpga, 1 );
@@ -6318,12 +6320,18 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
*/
/*
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
return 0;
}
*/
if ( Abc_NtkIsStrash(pNtk) )
{
fprintf( stdout, "Currently only works for logic circuits.\n" );
return 0;
}
// pNtkRes = Abc_NtkDar( pNtk );
// pNtkRes = Abc_NtkDarRetime( pNtk, nLevels, 1 );
@@ -10448,6 +10456,69 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandUndc( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
int c;
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( Abc_NtkIsComb(pNtk) )
{
fprintf( pErr, "The current network is combinational.\n" );
return 0;
}
if ( !Abc_NtkIsLogic(pNtk) )
{
fprintf( pErr, "This command works only for logic networks.\n" );
return 0;
}
// get the new network
Abc_NtkConvertDcLatches( pNtk );
return 0;
usage:
fprintf( pErr, "usage: undc [-h]\n" );
fprintf( pErr, "\t converts latches with DC init values into free PIs\n" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []

26
src/base/abci/abcDar.c
View File

@@ -85,7 +85,10 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
pMan->pName = Extra_UtilStrsav( pNtk->pName );
// save the number of registers
if ( fRegisters )
{
pMan->nRegs = Abc_NtkLatchNum(pNtk);
pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs );
}
// transfer the pointers to the basic nodes
Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
Abc_NtkForEachCi( pNtk, pObj, i )
@@ -114,6 +117,7 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
// remove dangling nodes
if ( nNodes = Aig_ManCleanup( pMan ) )
printf( "Abc_NtkToDar(): Unexpected %d dangling nodes when converting to AIG!\n", nNodes );
Aig_ManDumpVerilog( pMan, "test.v" );
if ( !Aig_ManCheck( pMan ) )
{
printf( "Abc_NtkToDar: AIG check has failed.\n" );
@@ -141,7 +145,7 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
Abc_Obj_t * pObjNew;
Aig_Obj_t * pObj;
int i;
assert( Aig_ManRegNum(pMan) == Abc_NtkLatchNum(pNtkOld) );
// assert( Aig_ManRegNum(pMan) == Abc_NtkLatchNum(pNtkOld) );
// perform strashing
pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
// transfer the pointers to the basic nodes
@@ -192,7 +196,7 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
{
Vec_Ptr_t * vNodes;
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pObjNew;
Abc_Obj_t * pObjNew, * pLatch;
Aig_Obj_t * pObj, * pObjLo, * pObjLi;
int i;
// assert( Aig_ManRegNum(pMan) != Abc_NtkLatchNum(pNtkOld) );
@@ -212,7 +216,19 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
Abc_ObjAddFanin( pObjLo->pData, pObjNew );
Abc_LatchSetInit0( pObjNew );
}
Abc_NtkAddDummyBoxNames( pNtkNew );
if ( pMan->vFlopNums == NULL )
Abc_NtkAddDummyBoxNames( pNtkNew );
else
{
assert( Abc_NtkBoxNum(pNtkOld) == Abc_NtkLatchNum(pNtkOld) );
Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
{
pLatch = Abc_NtkBox( pNtkOld, Vec_IntEntry( pMan->vFlopNums, i ) );
Abc_ObjAssignName( pObjNew, Abc_ObjName(pLatch), NULL );
Abc_ObjAssignName( Abc_ObjFanin0(pObjNew), Abc_ObjName(Abc_ObjFanin0(pLatch)), NULL );
Abc_ObjAssignName( Abc_ObjFanout0(pObjNew), Abc_ObjName(Abc_ObjFanout0(pLatch)), NULL );
}
}
// rebuild the AIG
vNodes = Aig_ManDfs( pMan );
Vec_PtrForEachEntry( vNodes, pObj, i )
@@ -959,8 +975,8 @@ Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, in
// so fraiging does not reduce the number of functions represented by nodes
Fraig_ParamsSetDefault( &Params );
Params.nBTLimit = 100000;
pNtkFraig = Abc_NtkFraig( pNtk, &Params, 0, 0 );
// pNtkFraig = Abc_NtkDup( pNtk );
// pNtkFraig = Abc_NtkFraig( pNtk, &Params, 0, 0 );
pNtkFraig = Abc_NtkDup( pNtk );
if ( fVerbose )
{
PRT( "Initial fraiging time", clock() - clk );

2
src/base/abci/abcPrint.c
View File

@@ -314,7 +314,7 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk )
}
else
{
if ( Abc_LatchIsInit1(pLatch) == Abc_NodeIsConst1(pLatch) )
if ( Abc_LatchIsInit1(pLatch) == Abc_NodeIsConst1(Abc_ObjFanin0(Abc_ObjFanin0(pLatch))) )
Counter2++;
}
}

155
src/base/abci/xaaaa.c
View File

@@ -1,155 +0,0 @@
/**CFile****************************************************************
FileName [abc_.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Network and node package.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: abc_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "abc.h"
#include "kit.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkPrintMeasures( unsigned * pTruth, int nVars )
{
unsigned uCofs[10][32];
int i, k, nOnes;
// total pairs
nOnes = Kit_TruthCountOnes( uCofs[0], nVars );
printf( "Total = %d.\n", nOnes * ((1 << nVars) - nOnes) );
// print measures for individual variables
for ( i = 0; i < nVars; i++ )
{
Kit_TruthUniqueNew( uCofs[0], pTruth, nVars, i );
nOnes = Kit_TruthCountOnes( uCofs[0], nVars );
printf( "%7d ", nOnes );
}
printf( "\n" );
// consider pairs
for ( i = 0; i < nVars; i++ )
for ( k = 0; k < nVars; k++ )
{
if ( i == k )
{
printf( " " );
continue;
}
Kit_TruthCofactor0New( uCofs[0], pTruth, nVars, i );
Kit_TruthCofactor1New( uCofs[1], pTruth, nVars, i );
Kit_TruthCofactor0New( uCofs[2], uCofs[0], nVars, k ); // 00
Kit_TruthCofactor1New( uCofs[3], uCofs[0], nVars, k ); // 01
Kit_TruthCofactor0New( uCofs[4], uCofs[1], nVars, k ); // 10
Kit_TruthCofactor1New( uCofs[5], uCofs[1], nVars, k ); // 11
Kit_TruthAndPhase( uCofs[6], uCofs[2], uCofs[5], nVars, 0, 1 ); // 00 & 11'
Kit_TruthAndPhase( uCofs[7], uCofs[2], uCofs[5], nVars, 1, 0 ); // 00' & 11
Kit_TruthAndPhase( uCofs[8], uCofs[3], uCofs[4], nVars, 0, 1 ); // 01 & 10'
Kit_TruthAndPhase( uCofs[9], uCofs[3], uCofs[4], nVars, 1, 0 ); // 01' & 10
nOnes = Kit_TruthCountOnes( uCofs[6], nVars ) +
Kit_TruthCountOnes( uCofs[7], nVars ) +
Kit_TruthCountOnes( uCofs[8], nVars ) +
Kit_TruthCountOnes( uCofs[9], nVars );
printf( "%7d ", nOnes );
if ( k == nVars - 1 )
printf( "\n" );
}
printf( "\n" );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_Ntk4VarTable( Abc_Ntk_t * pNtk )
{
static u4VarTts[222] = {
0x0000, 0x0001, 0x0003, 0x0006, 0x0007, 0x000f, 0x0016, 0x0017, 0x0018, 0x0019,
0x001b, 0x001e, 0x001f, 0x003c, 0x003d, 0x003f, 0x0069, 0x006b, 0x006f, 0x007e,
0x007f, 0x00ff, 0x0116, 0x0117, 0x0118, 0x0119, 0x011a, 0x011b, 0x011e, 0x011f,
0x012c, 0x012d, 0x012f, 0x013c, 0x013d, 0x013e, 0x013f, 0x0168, 0x0169, 0x016a,
0x016b, 0x016e, 0x016f, 0x017e, 0x017f, 0x0180, 0x0181, 0x0182, 0x0183, 0x0186,
0x0187, 0x0189, 0x018b, 0x018f, 0x0196, 0x0197, 0x0198, 0x0199, 0x019a, 0x019b,
0x019e, 0x019f, 0x01a8, 0x01a9, 0x01aa, 0x01ab, 0x01ac, 0x01ad, 0x01ae, 0x01af,
0x01bc, 0x01bd, 0x01be, 0x01bf, 0x01e8, 0x01e9, 0x01ea, 0x01eb, 0x01ee, 0x01ef,
0x01fe, 0x033c, 0x033d, 0x033f, 0x0356, 0x0357, 0x0358, 0x0359, 0x035a, 0x035b,
0x035e, 0x035f, 0x0368, 0x0369, 0x036a, 0x036b, 0x036c, 0x036d, 0x036e, 0x036f,
0x037c, 0x037d, 0x037e, 0x03c0, 0x03c1, 0x03c3, 0x03c5, 0x03c6, 0x03c7, 0x03cf,
0x03d4, 0x03d5, 0x03d6, 0x03d7, 0x03d8, 0x03d9, 0x03db, 0x03dc, 0x03dd, 0x03de,
0x03fc, 0x0660, 0x0661, 0x0662, 0x0663, 0x0666, 0x0667, 0x0669, 0x066b, 0x066f,
0x0672, 0x0673, 0x0676, 0x0678, 0x0679, 0x067a, 0x067b, 0x067e, 0x0690, 0x0691,
0x0693, 0x0696, 0x0697, 0x069f, 0x06b0, 0x06b1, 0x06b2, 0x06b3, 0x06b4, 0x06b5,
0x06b6, 0x06b7, 0x06b9, 0x06bd, 0x06f0, 0x06f1, 0x06f2, 0x06f6, 0x06f9, 0x0776,
0x0778, 0x0779, 0x077a, 0x077e, 0x07b0, 0x07b1, 0x07b4, 0x07b5, 0x07b6, 0x07bc,
0x07e0, 0x07e1, 0x07e2, 0x07e3, 0x07e6, 0x07e9, 0x07f0, 0x07f1, 0x07f2, 0x07f8,
0x0ff0, 0x1668, 0x1669, 0x166a, 0x166b, 0x166e, 0x167e, 0x1681, 0x1683, 0x1686,
0x1687, 0x1689, 0x168b, 0x168e, 0x1696, 0x1697, 0x1698, 0x1699, 0x169a, 0x169b,
0x169e, 0x16a9, 0x16ac, 0x16ad, 0x16bc, 0x16e9, 0x177e, 0x178e, 0x1796, 0x1798,
0x179a, 0x17ac, 0x17e8, 0x18e7, 0x19e1, 0x19e3, 0x19e6, 0x1bd8, 0x1be4, 0x1ee1,
0x3cc3, 0x6996
};
int Counters[222];
Vec_Ptr_t * vNodes;
Abc_Obj_t * pObj;
int i;
// set elementary truth tables
Abc_NtkForEachPi( pNtk, pObj, i )
pObj
Abc_NtkForEachPo( pNtk, pObj, i )
{
vNodes = Abc_NtkDfsNodes( pNtk, &pObj, i );
Vec_PtrFree( vNodes );
}
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

61
src/base/io/io.c
View File

@@ -34,6 +34,7 @@ static int IoCommandReadBench ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadDsd ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadEdif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadEqn ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadInit ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadPla ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadTruth ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadVerilog ( Abc_Frame_t * pAbc, int argc, char **argv );
@@ -86,6 +87,7 @@ void Io_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "I/O", "read_dsd", IoCommandReadDsd, 1 );
// Cmd_CommandAdd( pAbc, "I/O", "read_edif", IoCommandReadEdif, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_eqn", IoCommandReadEqn, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_init", IoCommandReadInit, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_pla", IoCommandReadPla, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_truth", IoCommandReadTruth, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_verilog", IoCommandReadVerilog, 1 );
@@ -643,6 +645,65 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int IoCommandReadInit( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
char * pFileName;
int c;
extern void Io_ReadBenchInit( Abc_Ntk_t * pNtk, char * pFileName );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
case 'h':
goto usage;
default:
goto usage;
}
}
if ( argc != globalUtilOptind + 1 )
goto usage;
if ( pNtk == NULL )
{
fprintf( pErr, "Empty network.\n" );
return 1;
}
// get the input file name
pFileName = argv[globalUtilOptind];
// read the file using the corresponding file reader
pNtk = Abc_NtkDup( pNtk );
Io_ReadBenchInit( pNtk, pFileName );
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
return 0;
usage:
fprintf( pAbc->Err, "usage: read_init [-h] <file>\n" );
fprintf( pAbc->Err, "\t reads initial state of the network in BENCH format\n" );
fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
return 1;
}
/**Function*************************************************************
Synopsis []

15
src/base/io/ioReadAiger.c
View File

@@ -245,6 +245,21 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
// printf( "Io_ReadAiger(): I/O/register names are not given. Generating short names.\n" );
Abc_NtkShortNames( pNtkNew );
}
// read the name of the model if given
if ( *pCur == 'c' )
{
if ( !strncmp( pCur + 2, ".model", 6 ) )
{
char * pTemp;
for ( pTemp = pCur + 9; *pTemp && *pTemp != '\n'; pTemp++ );
*pTemp = 0;
free( pNtkNew->pName );
pNtkNew->pName = Extra_UtilStrsav( pCur + 9 );
}
}
// skipping the comments
free( pContents );
Vec_PtrFree( vNodes );

95
src/base/io/ioReadBench.c
View File

@@ -66,6 +66,7 @@ Abc_Ntk_t * Io_ReadBench( char * pFileName, int fCheck )
}
return pNtk;
}
/**Function*************************************************************
Synopsis []
@@ -82,7 +83,7 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
ProgressBar * pProgress;
Vec_Ptr_t * vTokens;
Abc_Ntk_t * pNtk;
Abc_Obj_t * pNode;
Abc_Obj_t * pNode, * pNet;
Vec_Str_t * vString;
unsigned uTruth[8];
char * pType, ** ppNames, * pString;
@@ -241,11 +242,34 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
Extra_ProgressBarStop( pProgress );
Vec_StrFree( vString );
// check if constant have been added
// if ( pNet = Abc_NtkFindNet( pNtk, "vdd" ) )
// Io_ReadCreateConst( pNtk, "vdd", 1 );
// if ( pNet = Abc_NtkFindNet( pNtk, "gnd" ) )
// Io_ReadCreateConst( pNtk, "gnd", 0 );
// check if constant 0 is present
if ( (pNet = Abc_NtkFindNet( pNtk, "gnd" )) )
{
if ( Abc_ObjFaninNum(pNet) == 0 )
Io_ReadCreateConst( pNtk, "gnd", 0 );
}
if ( (pNet = Abc_NtkFindNet( pNtk, "1" )) )
{
if ( Abc_ObjFaninNum(pNet) == 0 )
{
printf( "Io_ReadBenchNetwork(): Adding constant 0 fanin to non-driven net \"1\".\n" );
Io_ReadCreateConst( pNtk, "1", 0 );
}
}
// check if constant 1 is present
if ( (pNet = Abc_NtkFindNet( pNtk, "vdd" )) )
{
if ( Abc_ObjFaninNum(pNet) == 0 )
Io_ReadCreateConst( pNtk, "vdd", 1 );
}
if ( (pNet = Abc_NtkFindNet( pNtk, "2" )) )
{
if ( Abc_ObjFaninNum(pNet) == 0 )
{
printf( "Io_ReadBenchNetwork(): Adding constant 1 fanin to non-driven net \"2\".\n" );
Io_ReadCreateConst( pNtk, "2", 1 );
}
}
Abc_NtkFinalizeRead( pNtk );
@@ -269,6 +293,65 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
}
/**Function*************************************************************
Synopsis [Reads initial state in BENCH format.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Io_ReadBenchInit( Abc_Ntk_t * pNtk, char * pFileName )
{
char pBuffer[1000];
FILE * pFile;
char * pToken;
Abc_Obj_t * pObj;
int Num;
pFile = fopen( pFileName, "r" );
if ( pFile == NULL )
{
printf( "Io_ReadBenchInit(): Failed to open file \"%s\".\n", pFileName );
return;
}
while ( fgets( pBuffer, 999, pFile ) )
{
pToken = strtok( pBuffer, " \n\t\r" );
// find the latch output
Num = Nm_ManFindIdByName( pNtk->pManName, pToken, ABC_OBJ_BO );
if ( Num < 0 )
{
printf( "Io_ReadBenchInit(): Cannot find register with output %s.\n", pToken );
continue;
}
pObj = Abc_ObjFanin0( Abc_NtkObj( pNtk, Num ) );
if ( !Abc_ObjIsLatch(pObj) )
{
printf( "Io_ReadBenchInit(): The signal is not a register output %s.\n", pToken );
continue;
}
// assign the new init state
pToken = strtok( NULL, " \n\t\r" );
if ( pToken[0] == '0' )
Abc_LatchSetInit0( pObj );
else if ( pToken[0] == '1' )
Abc_LatchSetInit1( pObj );
else if ( pToken[0] == '2' )
Abc_LatchSetInitDc( pObj );
else
{
printf( "Io_ReadBenchInit(): The signal %s has unknown initial value (%s).\n",
Abc_ObjName(Abc_ObjFanout0(pObj)), pToken );
continue;
}
}
fclose( pFile );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

3
src/base/io/ioWriteAiger.c
View File

@@ -248,7 +248,8 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols )
// write the comment
fprintf( pFile, "c\n" );
fprintf( pFile, "%s\n", pNtk->pName );
if ( pNtk->pName && strlen(pNtk->pName) > 0 )
fprintf( pFile, ".model %s\n", pNtk->pName );
fprintf( pFile, "This file was produced by ABC on %s\n", Extra_TimeStamp() );
fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
fclose( pFile );

3
src/misc/st/st.c
View File

@@ -31,7 +31,8 @@
#define ST_NUMCMP(x,y) ((x) != (y))
#define ST_NUMHASH(x,size) (ABS((long)x)%(size))
#define ST_PTRHASH(x,size) ((int)((unsigned long)(x)>>2)%size)
//#define ST_PTRHASH(x,size) ((int)((unsigned long)(x)>>2)%size) // 64-bit bug fix 9/17/2007
#define ST_PTRHASH(x,size) ((int)(((unsigned long)(x)>>2)%size))
#define EQUAL(func, x, y) \
((((func) == st_numcmp) || ((func) == st_ptrcmp)) ?\
(ST_NUMCMP((x),(y)) == 0) : ((*func)((x), (y)) == 0))

3
src/misc/st/stmm.c
View File

@@ -17,7 +17,8 @@
#define STMM_NUMCMP(x,y) ((x) != (y))
#define STMM_NUMHASH(x,size) (ABS((long)x)%(size))
#define STMM_PTRHASH(x,size) ((int)((unsigned long)(x)>>2)%size)
//#define STMM_PTRHASH(x,size) ((int)((unsigned long)(x)>>2)%size) // 64-bit bug fix 9/17/2007
#define STMM_PTRHASH(x,size) ((int)(((unsigned long)(x)>>2)%size))
#define EQUAL(func, x, y) \
((((func) == stmm_numcmp) || ((func) == stmm_ptrcmp)) ?\
(STMM_NUMCMP((x),(y)) == 0) : ((*func)((x), (y)) == 0))

8
src/misc/vec/vec.h
View File

@@ -27,6 +27,10 @@ extern "C" {
#ifdef _WIN32
#define inline __inline // compatible with MS VS 6.0
#pragma warning(disable : 4152) // warning C4152: nonstandard extension, function/data pointer conversion in expression
#pragma warning(disable : 4244) // warning C4244: '+=' : conversion from 'int ' to 'unsigned short ', possible loss of data
#pragma warning(disable : 4514) // warning C4514: 'Vec_StrPop' : unreferenced inline function has been removed
#pragma warning(disable : 4710) // warning C4710: function 'Vec_PtrGrow' not inlined
#endif
////////////////////////////////////////////////////////////////////////
@@ -71,6 +75,10 @@ extern "C" {
#define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
#endif
#ifndef PRTP
#define PRTP(a,t,T) printf("%s = ", (a)); printf("%6.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), (T)? 100.0*(t)/(T) : 0.0)
#endif
#include "vecInt.h"
#include "vecFlt.h"
#include "vecStr.h"

22
src/misc/vec/vecInt.h
View File

@@ -103,6 +103,28 @@ static inline Vec_Int_t * Vec_IntStart( int nSize )
return p;
}
/**Function*************************************************************
Synopsis [Allocates a vector with the given size and cleans it.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Int_t * Vec_IntStartNatural( int nSize )
{
Vec_Int_t * p;
int i;
p = Vec_IntAlloc( nSize );
p->nSize = nSize;
for ( i = 0; i < nSize; i++ )
p->pArray[i] = i;
return p;
}
/**Function*************************************************************
Synopsis [Creates the vector from an integer array of the given size.]

3
src/opt/lpk/lpkCore.c
View File

@@ -507,6 +507,9 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
int i, Iter, nNodes, nNodesPrev, clk = clock();
assert( Abc_NtkIsLogic(pNtk) );
// sweep dangling nodes as a preprocessing step
Abc_NtkSweep( pNtk, 0 );
// get the number of inputs
pPars->nLutSize = Abc_NtkGetFaninMax( pNtk );
// adjust the number of crossbars based on LUT size

18
src/sat/bsat/satSolver.c
View File

@@ -90,9 +90,9 @@ static inline void clause_setactivity(clause* c, float a) { *((float*)&c->lits[
//=================================================================================================
// Encode literals in clause pointers:
static clause* clause_from_lit (lit l) { return (clause*)((unsigned long)l + (unsigned long)l + 1); }
static bool clause_is_lit (clause* c) { return ((unsigned long)c & 1); }
static lit clause_read_lit (clause* c) { return (lit)((unsigned long)c >> 1); }
static inline clause* clause_from_lit (lit l) { return (clause*)((unsigned long)l + (unsigned long)l + 1); }
static inline bool clause_is_lit (clause* c) { return ((unsigned long)c & 1); }
static inline lit clause_read_lit (clause* c) { return (lit)((unsigned long)c >> 1); }
//=================================================================================================
// Simple helpers:
@@ -148,7 +148,7 @@ static inline void order_unassigned(sat_solver* s, int v) // undoorder
}
}
static int order_select(sat_solver* s, float random_var_freq) // selectvar
static inline int order_select(sat_solver* s, float random_var_freq) // selectvar
{
int* heap;
double* activity;
@@ -442,7 +442,7 @@ static inline void assume(sat_solver* s, lit l){
}
static inline void sat_solver_canceluntil(sat_solver* s, int level) {
static void sat_solver_canceluntil(sat_solver* s, int level) {
lit* trail;
lbool* values;
clause** reasons;
@@ -723,13 +723,14 @@ clause* sat_solver_propagate(sat_solver* s)
//printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p));
for (i = j = begin; i < end; ){
if (clause_is_lit(*i)){
// s->stats.inspects2++;
*j++ = *i;
if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p))){
confl = s->binary;
(clause_begin(confl))[1] = lit_neg(p);
(clause_begin(confl))[0] = clause_read_lit(*i++);
// Copy the remaining watches:
// s->stats.inspects2 += end - i;
while (i < end)
*j++ = *i++;
}
@@ -770,6 +771,7 @@ clause* sat_solver_propagate(sat_solver* s)
if (!enqueue(s,lits[0], *i)){
confl = *i++;
// Copy the remaining watches:
// s->stats.inspects2 += end - i;
while (i < end)
*j++ = *i++;
}
@@ -1154,6 +1156,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sin
lit* i;
// set the external limits
s->nCalls++;
s->nRestarts = 0;
s->nConfLimit = 0;
s->nInsLimit = 0;
@@ -1175,12 +1178,13 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sin
assume(s, *i);
if (sat_solver_propagate(s) == NULL)
break;
// falltrough
// fallthrough
case -1: /* l_False */
sat_solver_canceluntil(s, 0);
return l_False;
}
}
s->nCalls2++;
s->root_level = sat_solver_dlevel(s);

2
src/sat/bsat/satSolver.h
View File

@@ -172,6 +172,8 @@ struct sat_solver_t
veci act_vars; // variables whose activity has changed
double* factors; // the activity factors
int nRestarts; // the number of local restarts
int nCalls; // the number of local restarts
int nCalls2; // the number of local restarts
Sat_MmStep_t * pMem;

12
src/sat/bsat/satUtil.c
View File

@@ -146,11 +146,13 @@ void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement )
***********************************************************************/
void Sat_SolverPrintStats( FILE * pFile, sat_solver * p )
{
printf( "starts : %d\n", (int)p->stats.starts );
printf( "conflicts : %d\n", (int)p->stats.conflicts );
printf( "decisions : %d\n", (int)p->stats.decisions );
printf( "propagations : %d\n", (int)p->stats.propagations );
printf( "inspects : %d\n", (int)p->stats.inspects );
// printf( "calls : %8d (%d)\n", (int)p->nCalls, (int)p->nCalls2 );
printf( "starts : %8d\n", (int)p->stats.starts );
printf( "conflicts : %8d\n", (int)p->stats.conflicts );
printf( "decisions : %8d\n", (int)p->stats.decisions );
printf( "propagations : %8d\n", (int)p->stats.propagations );
printf( "inspects : %8d\n", (int)p->stats.inspects );
// printf( "inspects2 : %8d\n", (int)p->stats.inspects2 );
}
/**Function*************************************************************