summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/aig/aig.h21
-rw-r--r--src/aig/aig/aigCheck.c3
-rw-r--r--src/aig/aig/aigDfs.c12
-rw-r--r--src/aig/aig/aigMan.c5
-rw-r--r--src/aig/aig/aigPart.c4
-rw-r--r--src/aig/aig/aigRepr.c2
-rw-r--r--src/aig/aig/aigScl.c17
-rw-r--r--src/aig/aig/aigUtil.c140
-rw-r--r--src/aig/aig/module.make1
-rw-r--r--src/aig/dar/darBalance.c2
-rw-r--r--src/aig/dar/darRefact.c8
-rw-r--r--src/aig/fra/fraInd.c9
-rw-r--r--src/aig/fra/fraSec.c6
-rw-r--r--src/aig/fra/fraSim.c5
-rw-r--r--src/aig/hop/hop.h10
-rw-r--r--src/aig/ioa/ioaWriteAig.c3
-rw-r--r--src/aig/ivy/ivyFraig.c8
-rw-r--r--src/aig/kit/kitAig.c121
-rw-r--r--src/aig/kit/kitDsd.c2
-rw-r--r--src/aig/kit/kitIsop.c60
-rw-r--r--src/aig/kit/kitTruth.c29
-rw-r--r--src/aig/kit/module.make3
22 files changed, 386 insertions, 85 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index fe237142..63456b5d 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -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 );
diff --git a/src/aig/aig/aigCheck.c b/src/aig/aig/aigCheck.c
index f4a6bf6b..8c53e635 100644
--- a/src/aig/aig/aigCheck.c
+++ b/src/aig/aig/aigCheck.c
@@ -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",
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index 9cfaf69c..e9821bdc 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -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;
}
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 1e0ee278..d2714380 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -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 );
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
index 4c879ee8..65e35fc4 100644
--- a/src/aig/aig/aigPart.c
+++ b/src/aig/aig/aigPart.c
@@ -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)
diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c
index 787ede49..6356afd3 100644
--- a/src/aig/aig/aigRepr.c
+++ b/src/aig/aig/aigRepr.c
@@ -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);
diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c
index 2f00a7eb..abd424c1 100644
--- a/src/aig/aig/aigScl.c
+++ b/src/aig/aig/aigScl.c
@@ -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
diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
index 86cd02ce..2fba3cb1 100644
--- a/src/aig/aig/aigUtil.c
+++ b/src/aig/aig/aigUtil.c
@@ -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 ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make
index d1b1cd3b..c35e7121 100644
--- a/src/aig/aig/module.make
+++ b/src/aig/aig/module.make
@@ -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 \
diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c
index d4266103..989535f2 100644
--- a/src/aig/dar/darBalance.c
+++ b/src/aig/dar/darBalance.c
@@ -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);
diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c
index a5435862..142c7721 100644
--- a/src/aig/dar/darRefact.c
+++ b/src/aig/dar/darRefact.c
@@ -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
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 98025280..f45e8af0 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -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();
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 0919e035..f9bbfe44 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -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 );
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index d379cf53..b77c775a 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -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 );
}
}
}
diff --git a/src/aig/hop/hop.h b/src/aig/hop/hop.h
index c5815a2c..e8e916cc 100644
--- a/src/aig/hop/hop.h
+++ b/src/aig/hop/hop.h
@@ -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
};
diff --git a/src/aig/ioa/ioaWriteAig.c b/src/aig/ioa/ioaWriteAig.c
index 74462bbd..a6c23fd4 100644
--- a/src/aig/ioa/ioaWriteAig.c
+++ b/src/aig/ioa/ioaWriteAig.c
@@ -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 );
diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c
index 81ed895e..1ab91dd2 100644
--- a/src/aig/ivy/ivyFraig.c
+++ b/src/aig/ivy/ivyFraig.c
@@ -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
diff --git a/src/aig/kit/kitAig.c b/src/aig/kit/kitAig.c
new file mode 100644
index 00000000..0d5c1686
--- /dev/null
+++ b/src/aig/kit/kitAig.c
@@ -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 ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/kit/kitDsd.c b/src/aig/kit/kitDsd.c
index abd07e68..e24a9964 100644
--- a/src/aig/kit/kitDsd.c
+++ b/src/aig/kit/kitDsd.c
@@ -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 );
diff --git a/src/aig/kit/kitIsop.c b/src/aig/kit/kitIsop.c
index cc61a6bd..42fae2ea 100644
--- a/src/aig/kit/kitIsop.c
+++ b/src/aig/kit/kitIsop.c
@@ -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 )
diff --git a/src/aig/kit/kitTruth.c b/src/aig/kit/kitTruth.c
index 65389ef9..5360ad7f 100644
--- a/src/aig/kit/kitTruth.c
+++ b/src/aig/kit/kitTruth.c
@@ -1634,6 +1634,33 @@ int Kit_TruthCountMinterms( unsigned * pTruth, int nVars, int * pRes, int * pByt
/**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.]
Description [Returns 0 if the function is a constant.]
@@ -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( ", " );
}
}
diff --git a/src/aig/kit/module.make b/src/aig/kit/module.make
index 25c8e767..ea62381b 100644
--- a/src/aig/kit/module.make
+++ b/src/aig/kit/module.make
@@ -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 \
generated by cgit v1.2.3 (git 2.25.1) at 2025-03-31 20:32:26 +0000