summaryrefslogtreecommitdiffstats
path: root/src/aig/kit
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/kit')
-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
5 files changed, 182 insertions, 33 deletions
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 2024-10-30 09:53:50 +0000