Skip to content

A
abc
Commit dd5531ca by Alan Mishchenko
Options

Version abc70317

parent 2696cf05
Showing with 716 additions and 54 deletions
abc.dsp
...@@ -466,6 +466,10 @@ SOURCE=.\src\base\io\ioReadBlifMv.c ...@@ -466,6 +466,10 @@ SOURCE=.\src\base\io\ioReadBlifMv.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\base\io\ioReadDsd.c
# End Source File
# Begin Source File
SOURCE=.\src\base\io\ioReadEdif.c SOURCE=.\src\base\io\ioReadEdif.c
# End Source File # End Source File
# Begin Source File # Begin Source File
...@@ -1674,6 +1678,10 @@ SOURCE=.\src\opt\kit\kitBdd.c ...@@ -1674,6 +1678,10 @@ SOURCE=.\src\opt\kit\kitBdd.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\opt\kit\kitDsd.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\kit\kitFactor.c SOURCE=.\src\opt\kit\kitFactor.c
# End Source File # End Source File
# Begin Source File # Begin Source File
......
abc.rc
...@@ -124,9 +124,6 @@ alias fflitmin "compress2rs; ren; sop; ps -f" ...@@ -124,9 +124,6 @@ alias fflitmin "compress2rs; ren; sop; ps -f"
#alias ttb "wh a/quip_opt/nut_001_opt.blif 1.blif" #alias ttb "wh a/quip_opt/nut_001_opt.blif 1.blif"
#alias ttv "wh a/quip_opt/nut_001_opt.blif 1.v" #alias ttv "wh a/quip_opt/nut_001_opt.blif 1.v"
alias t "r c.blif; st; haig_start; resyn; haig_use"
alias tt "r i10.blif; st; haig_start; resyn2; haig_use"
alias reach "st; ps; compress2; ps; qrel; ps; compress2; ps; qreach -v; ps" alias reach "st; ps; compress2; ps; qrel; ps; compress2; ps; qreach -v; ps"
alias qs1 "qvar -I 96 -u; ps; qbf -P 96" alias qs1 "qvar -I 96 -u; ps; qbf -P 96"
...@@ -139,3 +136,18 @@ alias qs7 "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar ...@@ -139,3 +136,18 @@ alias qs7 "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar
alias qs8 "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar -I 100 -u; qvar -I 101 -u; qvar -I 102 -u; qvar -I 103 -u; ps; qbf -P 96" alias qs8 "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar -I 100 -u; qvar -I 101 -u; qvar -I 102 -u; qvar -I 103 -u; ps; qbf -P 96"
alias qs9 "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar -I 100 -u; qvar -I 101 -u; qvar -I 102 -u; qvar -I 103 -u; qvar -I 104 -u; ps; qbf -P 96" alias qs9 "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar -I 100 -u; qvar -I 101 -u; qvar -I 102 -u; qvar -I 103 -u; qvar -I 104 -u; ps; qbf -P 96"
alias qsA "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar -I 100 -u; qvar -I 101 -u; qvar -I 102 -u; qvar -I 103 -u; qvar -I 104 -u; qvar -I 105 -u; ps; qbf -P 96" alias qsA "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar -I 100 -u; qvar -I 101 -u; qvar -I 102 -u; qvar -I 103 -u; qvar -I 104 -u; qvar -I 105 -u; ps; qbf -P 96"
alias chnew "st; haig_start; resyn2; haig_use"
alias chnewrs "st; haig_start; resyn2rs; haig_use"
alias bug "r a/quip_opt/nut_001_opt.blif; chnew; st; cec"
alias bug2 "r a/quip_opt/nut_001_opt.blif; chnew; if -K 6; ps; cec"
alias t "read_dsd a*(b+(c*d)+e); clp -r; print_dsd"
alias t1 "read_dsd a*(b+(c*d)); clp -r; print_dsd"
alias t2 "read_dsd 56BA(a,b,c,d); clp -r; print_dsd"
alias t3 "read_dsd 56BA(a,b*c,e,d); clp -r; print_dsd"
alias t4 "read_dsd 56BA(a,b*c,e+d,f); clp -r; print_dsd"
alias t5 "read_dsd 56BA(a,CA(b,c,d),e,f); clp -r; print_dsd"
alias t6 "read_dsd f*CA(b,c,d)*CA(e,a,g); clp -r; print_dsd"
src/aig/hop/hop.h
...@@ -81,7 +81,7 @@ struct Hop_Man_t_ ...@@ -81,7 +81,7 @@ struct Hop_Man_t_
// AIG nodes // AIG nodes
Vec_Ptr_t * vPis; // the array of PIs Vec_Ptr_t * vPis; // the array of PIs
Vec_Ptr_t * vPos; // the array of POs Vec_Ptr_t * vPos; // the array of POs
Vec_Ptr_t * vNodes; // the array of all nodes (optional) Vec_Ptr_t * vObjs; // the array of all nodes (optional)
Hop_Obj_t * pConst1; // the constant 1 node Hop_Obj_t * pConst1; // the constant 1 node
Hop_Obj_t Ghost; // the ghost node Hop_Obj_t Ghost; // the ghost node
// AIG node counters // AIG node counters
...@@ -131,6 +131,8 @@ static inline Hop_Obj_t * Hop_ManConst0( Hop_Man_t * p ) { return Hop_N ...@@ -131,6 +131,8 @@ static inline Hop_Obj_t * Hop_ManConst0( Hop_Man_t * p ) { return Hop_N
static inline Hop_Obj_t * Hop_ManConst1( Hop_Man_t * p ) { return p->pConst1; } static inline Hop_Obj_t * Hop_ManConst1( Hop_Man_t * p ) { return p->pConst1; }
static inline Hop_Obj_t * Hop_ManGhost( Hop_Man_t * p ) { return &p->Ghost; } static inline Hop_Obj_t * Hop_ManGhost( Hop_Man_t * p ) { return &p->Ghost; }
static inline Hop_Obj_t * Hop_ManPi( Hop_Man_t * p, int i ) { return (Hop_Obj_t *)Vec_PtrEntry(p->vPis, i); } static inline Hop_Obj_t * Hop_ManPi( Hop_Man_t * p, int i ) { return (Hop_Obj_t *)Vec_PtrEntry(p->vPis, i); }
static inline Hop_Obj_t * Hop_ManPo( Hop_Man_t * p, int i ) { return (Hop_Obj_t *)Vec_PtrEntry(p->vPos, i); }
static inline Hop_Obj_t * Hop_ManObj( Hop_Man_t * p, int i ) { return p->vObjs ? (Hop_Obj_t *)Vec_PtrEntry(p->vObjs, i) : NULL; }
static inline Hop_Edge_t Hop_EdgeCreate( int Id, int fCompl ) { return (Id << 1) | fCompl; } static inline Hop_Edge_t Hop_EdgeCreate( int Id, int fCompl ) { return (Id << 1) | fCompl; }
static inline int Hop_EdgeId( Hop_Edge_t Edge ) { return Edge >> 1; } static inline int Hop_EdgeId( Hop_Edge_t Edge ) { return Edge >> 1; }
...@@ -223,10 +225,10 @@ static inline Hop_Obj_t * Hop_ManFetchMemory( Hop_Man_t * p ) ...@@ -223,10 +225,10 @@ static inline Hop_Obj_t * Hop_ManFetchMemory( Hop_Man_t * p )
pTemp = p->pListFree; pTemp = p->pListFree;
p->pListFree = *((Hop_Obj_t **)pTemp); p->pListFree = *((Hop_Obj_t **)pTemp);
memset( pTemp, 0, sizeof(Hop_Obj_t) ); memset( pTemp, 0, sizeof(Hop_Obj_t) );
if ( p->vNodes ) if ( p->vObjs )
{ {
assert( p->nCreated == Vec_PtrSize(p->vNodes) ); assert( p->nCreated == Vec_PtrSize(p->vObjs) );
Vec_PtrPush( p->vNodes, pTemp ); Vec_PtrPush( p->vObjs, pTemp );
} }
pTemp->Id = p->nCreated++; pTemp->Id = p->nCreated++;
return pTemp; return pTemp;
......
src/aig/hop/hopMan.c
...@@ -94,10 +94,10 @@ void Hop_ManStop( Hop_Man_t * p ) ...@@ -94,10 +94,10 @@ void Hop_ManStop( Hop_Man_t * p )
if ( p->time1 ) { PRT( "time1", p->time1 ); } if ( p->time1 ) { PRT( "time1", p->time1 ); }
if ( p->time2 ) { PRT( "time2", p->time2 ); } if ( p->time2 ) { PRT( "time2", p->time2 ); }
// Hop_TableProfile( p ); // Hop_TableProfile( p );
if ( p->vChunks ) Hop_ManStopMemory( p ); if ( p->vChunks ) Hop_ManStopMemory( p );
if ( p->vPis ) Vec_PtrFree( p->vPis ); if ( p->vPis ) Vec_PtrFree( p->vPis );
if ( p->vPos ) Vec_PtrFree( p->vPos ); if ( p->vPos ) Vec_PtrFree( p->vPos );
if ( p->vNodes ) Vec_PtrFree( p->vNodes ); if ( p->vObjs ) Vec_PtrFree( p->vObjs );
free( p->pTable ); free( p->pTable );
free( p ); free( p );
} }
...@@ -115,20 +115,20 @@ void Hop_ManStop( Hop_Man_t * p ) ...@@ -115,20 +115,20 @@ void Hop_ManStop( Hop_Man_t * p )
***********************************************************************/ ***********************************************************************/
int Hop_ManCleanup( Hop_Man_t * p ) int Hop_ManCleanup( Hop_Man_t * p )
{ {
Vec_Ptr_t * vNodes; Vec_Ptr_t * vObjs;
Hop_Obj_t * pNode; Hop_Obj_t * pNode;
int i, nNodesOld; int i, nNodesOld;
assert( p->fRefCount ); assert( p->fRefCount );
nNodesOld = Hop_ManNodeNum(p); nNodesOld = Hop_ManNodeNum(p);
// collect roots of dangling nodes // collect roots of dangling nodes
vNodes = Vec_PtrAlloc( 100 ); vObjs = Vec_PtrAlloc( 100 );
Hop_ManForEachNode( p, pNode, i ) Hop_ManForEachNode( p, pNode, i )
if ( Hop_ObjRefs(pNode) == 0 ) if ( Hop_ObjRefs(pNode) == 0 )
Vec_PtrPush( vNodes, pNode ); Vec_PtrPush( vObjs, pNode );
// recursively remove dangling nodes // recursively remove dangling nodes
Vec_PtrForEachEntry( vNodes, pNode, i ) Vec_PtrForEachEntry( vObjs, pNode, i )
Hop_ObjDelete_rec( p, pNode ); Hop_ObjDelete_rec( p, pNode );
Vec_PtrFree( vNodes ); Vec_PtrFree( vObjs );
return nNodesOld - Hop_ManNodeNum(p); return nNodesOld - Hop_ManNodeNum(p);
} }
......
src/aig/hop/hopObj.c
...@@ -73,7 +73,7 @@ Hop_Obj_t * Hop_ObjCreatePo( Hop_Man_t * p, Hop_Obj_t * pDriver ) ...@@ -73,7 +73,7 @@ Hop_Obj_t * Hop_ObjCreatePo( Hop_Man_t * p, Hop_Obj_t * pDriver )
else else
pObj->nRefs = Hop_ObjLevel( Hop_Regular(pDriver) ); pObj->nRefs = Hop_ObjLevel( Hop_Regular(pDriver) );
// set the phase // set the phase
// pObj->fPhase = Hop_ObjFaninPhase(pDriver); pObj->fPhase = Hop_ObjFaninPhase(pDriver);
// update node counters of the manager // update node counters of the manager
p->nObjs[AIG_PO]++; p->nObjs[AIG_PO]++;
return pObj; return pObj;
...@@ -136,7 +136,7 @@ void Hop_ObjConnect( Hop_Man_t * p, Hop_Obj_t * pObj, Hop_Obj_t * pFan0, Hop_Obj ...@@ -136,7 +136,7 @@ void Hop_ObjConnect( Hop_Man_t * p, Hop_Obj_t * pObj, Hop_Obj_t * pFan0, Hop_Obj
else else
pObj->nRefs = Hop_ObjLevelNew( pObj ); pObj->nRefs = Hop_ObjLevelNew( pObj );
// set the phase // set the phase
// pObj->fPhase = Hop_ObjFaninPhase(pFan0) & Hop_ObjFaninPhase(pFan1); pObj->fPhase = Hop_ObjFaninPhase(pFan0) & Hop_ObjFaninPhase(pFan1);
// add the node to the structural hash table // add the node to the structural hash table
Hop_TableInsert( p, pObj ); Hop_TableInsert( p, pObj );
} }
...@@ -236,9 +236,10 @@ void Hop_ObjDelete_rec( Hop_Man_t * p, Hop_Obj_t * pObj ) ...@@ -236,9 +236,10 @@ void Hop_ObjDelete_rec( Hop_Man_t * p, Hop_Obj_t * pObj )
***********************************************************************/ ***********************************************************************/
Hop_Obj_t * Hop_ObjRepr( Hop_Obj_t * pObj ) Hop_Obj_t * Hop_ObjRepr( Hop_Obj_t * pObj )
{ {
if ( Hop_Regular(pObj)->pData == NULL ) assert( !Hop_IsComplement(pObj) );
return Hop_Regular(pObj); if ( pObj->pData == NULL || pObj->pData == pObj )
return Hop_ObjRepr( Hop_Regular(pObj)->pData ); return pObj;
return Hop_ObjRepr( pObj->pData );
} }
/**Function************************************************************* /**Function*************************************************************
......
src/base/abc/abc.h
...@@ -616,7 +616,7 @@ extern int Abc_CountZddCubes( DdManager * dd, DdNode * zCover ); ...@@ -616,7 +616,7 @@ extern int Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
extern void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk ); extern void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk );
extern int Abc_NtkSopToAig( Abc_Ntk_t * pNtk ); extern int Abc_NtkSopToAig( Abc_Ntk_t * pNtk );
extern int Abc_NtkAigToBdd( Abc_Ntk_t * pNtk ); extern int Abc_NtkAigToBdd( Abc_Ntk_t * pNtk );
extern unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth ); extern unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, int fMsbFirst );
extern int Abc_NtkMapToSop( Abc_Ntk_t * pNtk ); extern int Abc_NtkMapToSop( Abc_Ntk_t * pNtk );
extern int Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect ); extern int Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect );
extern int Abc_NtkToBdd( Abc_Ntk_t * pNtk ); extern int Abc_NtkToBdd( Abc_Ntk_t * pNtk );
......
src/base/abc/abcFunc.c
...@@ -866,7 +866,7 @@ unsigned * Abc_ConvertAigToTruth_rec2( Hop_Obj_t * pObj, Vec_Int_t * vTruth, int ...@@ -866,7 +866,7 @@ unsigned * Abc_ConvertAigToTruth_rec2( Hop_Obj_t * pObj, Vec_Int_t * vTruth, int
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth ) unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, int fMsbFirst )
{ {
static unsigned uTruths[8][8] = { // elementary truth tables static unsigned uTruths[8][8] = { // elementary truth tables
{ 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA }, { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA },
...@@ -899,9 +899,18 @@ unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, V ...@@ -899,9 +899,18 @@ unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, V
return pTruth; return pTruth;
} }
// set elementary truth tables at the leaves // set elementary truth tables at the leaves
assert( nVars <= Hop_ManPiNum(p) );
assert( Hop_ManPiNum(p) <= 8 ); assert( Hop_ManPiNum(p) <= 8 );
Hop_ManForEachPi( p, pObj, i ) if ( fMsbFirst )
pObj->pData = (void *)uTruths[i]; {
Hop_ManForEachPi( p, pObj, i )
pObj->pData = (void *)uTruths[nVars-1-i];
}
else
{
Hop_ManForEachPi( p, pObj, i )
pObj->pData = (void *)uTruths[i];
}
// clear the marks and compute the truth table // clear the marks and compute the truth table
pTruth2 = Abc_ConvertAigToTruth_rec2( pRoot, vTruth, nWords ); pTruth2 = Abc_ConvertAigToTruth_rec2( pRoot, vTruth, nWords );
// copy the result // copy the result
......
src/base/abc/abcSop.c
...@@ -855,7 +855,8 @@ char * Abc_SopFromTruthBin( char * pTruth ) ...@@ -855,7 +855,8 @@ char * Abc_SopFromTruthBin( char * pTruth )
{ {
pCube = pSopCover + i * (nVars + 3); pCube = pSopCover + i * (nVars + 3);
for ( b = 0; b < nVars; b++ ) for ( b = 0; b < nVars; b++ )
if ( Mint & (1 << b) ) if ( Mint & (1 << (nVars-1-b)) )
// if ( Mint & (1 << b) )
pCube[b] = '1'; pCube[b] = '1';
else else
pCube[b] = '0'; pCube[b] = '0';
...@@ -921,7 +922,8 @@ char * Abc_SopFromTruthHex( char * pTruth ) ...@@ -921,7 +922,8 @@ char * Abc_SopFromTruthHex( char * pTruth )
{ {
pCube = pSopCover + i * (nVars + 3); pCube = pSopCover + i * (nVars + 3);
for ( b = 0; b < nVars; b++ ) for ( b = 0; b < nVars; b++ )
if ( Mint & (1 << b) ) if ( Mint & (1 << (nVars-1-b)) )
// if ( Mint & (1 << b) )
pCube[b] = '1'; pCube[b] = '1';
else else
pCube[b] = '0'; pCube[b] = '0';
......
src/base/abci/abc.c
...@@ -47,6 +47,7 @@ static int Abc_CommandPrintKMap ( Abc_Frame_t * pAbc, int argc, char ** arg ...@@ -47,6 +47,7 @@ static int Abc_CommandPrintKMap ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandPrintGates ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPrintGates ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintSharing ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPrintSharing ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintXCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPrintXCut ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintDsd ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandShow ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandShow ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandShowBdd ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandShowBdd ( Abc_Frame_t * pAbc, int argc, char ** argv );
...@@ -61,7 +62,7 @@ static int Abc_CommandCleanup ( Abc_Frame_t * pAbc, int argc, char ** arg ...@@ -61,7 +62,7 @@ static int Abc_CommandCleanup ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandSweep ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSweep ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFastExtract ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFastExtract ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDisjoint ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDisjoint ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandImfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv );
...@@ -194,6 +195,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) ...@@ -194,6 +195,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Printing", "print_gates", Abc_CommandPrintGates, 0 ); Cmd_CommandAdd( pAbc, "Printing", "print_gates", Abc_CommandPrintGates, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_sharing", Abc_CommandPrintSharing, 0 ); Cmd_CommandAdd( pAbc, "Printing", "print_sharing", Abc_CommandPrintSharing, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_xcut", Abc_CommandPrintXCut, 0 ); Cmd_CommandAdd( pAbc, "Printing", "print_xcut", Abc_CommandPrintXCut, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_dsd", Abc_CommandPrintDsd, 0 );
Cmd_CommandAdd( pAbc, "Printing", "show", Abc_CommandShow, 0 ); Cmd_CommandAdd( pAbc, "Printing", "show", Abc_CommandShow, 0 );
Cmd_CommandAdd( pAbc, "Printing", "show_bdd", Abc_CommandShowBdd, 0 ); Cmd_CommandAdd( pAbc, "Printing", "show_bdd", Abc_CommandShowBdd, 0 );
...@@ -208,7 +210,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) ...@@ -208,7 +210,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Synthesis", "sweep", Abc_CommandSweep, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "sweep", Abc_CommandSweep, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "fx", Abc_CommandFastExtract, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "fx", Abc_CommandFastExtract, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "dsd", Abc_CommandDisjoint, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "dsd", Abc_CommandDisjoint, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "ifs", Abc_CommandIfs, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "imfs", Abc_CommandImfs, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "rewrite", Abc_CommandRewrite, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "rewrite", Abc_CommandRewrite, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "refactor", Abc_CommandRefactor, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "refactor", Abc_CommandRefactor, 1 );
...@@ -1463,6 +1465,92 @@ usage: ...@@ -1463,6 +1465,92 @@ usage:
return 1; return 1;
} }
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
int c;
int fUseLibrary;
extern void Kit_DsdTest( unsigned * pTruth, int nVars );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
fUseLibrary = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "lh" ) ) != EOF )
{
switch ( c )
{
case 'l':
fUseLibrary ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
fprintf( pErr, "Empty network.\n" );
return 1;
}
// get the truth table of the first output
if ( !Abc_NtkIsLogic(pNtk) )
{
fprintf( pErr, "Currently works only for logic networks.\n" );
return 1;
}
Abc_NtkToAig( pNtk );
// convert it to truth table
{
Abc_Obj_t * pObj = Abc_ObjFanin0( Abc_NtkPo(pNtk, 0) );
Vec_Int_t * vMemory = Vec_IntAlloc( 100 );
unsigned * pTruth;
if ( !Abc_ObjIsNode(pObj) )
{
fprintf( pErr, "The fanin of the first PO node does not have a logic function.\n" );
return 1;
}
if ( Abc_ObjFaninNum(pObj) > 8 )
{
fprintf( pErr, "Currently works only for up to 8 inputs.\n" );
return 1;
}
pTruth = Abc_ConvertAigToTruth( pNtk->pManFunc, Hop_Regular(pObj->pData), Abc_ObjFaninNum(pObj), vMemory, 1 );
if ( Hop_IsComplement(pObj->pData) )
Extra_TruthNot( pTruth, pTruth, Abc_ObjFaninNum(pObj) );
Extra_PrintBinary( stdout, pTruth, 1 << Abc_ObjFaninNum(pObj) );
printf( "\n" );
Kit_DsdTest( pTruth, Abc_ObjFaninNum(pObj) );
Vec_IntFree( vMemory );
}
return 0;
usage:
fprintf( pErr, "usage: print_dsd [-h]\n" );
fprintf( pErr, "\t print DSD formula for a single-output function with less than 16 variables\n" );
// fprintf( pErr, "\t-l : used library gate names (if mapped) [default = %s]\n", fUseLibrary? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
/**Function************************************************************* /**Function*************************************************************
...@@ -2649,7 +2737,7 @@ usage: ...@@ -2649,7 +2737,7 @@ usage:
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Abc_CommandIfs( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandImfs( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
FILE * pOut, * pErr; FILE * pOut, * pErr;
Abc_Ntk_t * pNtk; Abc_Ntk_t * pNtk;
...@@ -2756,7 +2844,7 @@ int Abc_CommandIfs( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -2756,7 +2844,7 @@ int Abc_CommandIfs( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
fprintf( pErr, "usage: ifs [-W <NM>] [-L <num>] [-C <num>] [-S <num>] [-avwh]\n" ); fprintf( pErr, "usage: imfs [-W <NM>] [-L <num>] [-C <num>] [-S <num>] [-avwh]\n" );
fprintf( pErr, "\t performs resubstitution-based resynthesis with interpolation\n" ); fprintf( pErr, "\t performs resubstitution-based resynthesis with interpolation\n" );
fprintf( pErr, "\t-W <NM> : fanin/fanout levels (NxM) of the window (00 <= NM <= 99) [default = %d%d]\n", pPars->nWindow/10, pPars->nWindow%10 ); fprintf( pErr, "\t-W <NM> : fanin/fanout levels (NxM) of the window (00 <= NM <= 99) [default = %d%d]\n", pPars->nWindow/10, pPars->nWindow%10 );
fprintf( pErr, "\t-L <num> : the largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel ); fprintf( pErr, "\t-L <num> : the largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
......
src/base/abci/abcIf.c
...@@ -150,6 +150,7 @@ If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars ) ...@@ -150,6 +150,7 @@ If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
// set up the choice node // set up the choice node
if ( Abc_AigNodeIsChoice( pNode ) ) if ( Abc_AigNodeIsChoice( pNode ) )
{ {
pIfMan->nChoices++;
for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData ) for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
If_ObjSetChoice( (If_Obj_t *)pPrev->pCopy, (If_Obj_t *)pFanin->pCopy ); If_ObjSetChoice( (If_Obj_t *)pPrev->pCopy, (If_Obj_t *)pFanin->pCopy );
If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pCopy ); If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pCopy );
......
src/base/abci/abcRenode.c
...@@ -38,6 +38,8 @@ static DdManager * s_pDd = NULL; ...@@ -38,6 +38,8 @@ static DdManager * s_pDd = NULL;
static Vec_Int_t * s_vMemory = NULL; static Vec_Int_t * s_vMemory = NULL;
static Vec_Int_t * s_vMemory2 = NULL; static Vec_Int_t * s_vMemory2 = NULL;
static int nDsdCounter = 0;
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
...@@ -62,6 +64,8 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nF ...@@ -62,6 +64,8 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nF
if ( Abc_NtkGetChoiceNum( pNtk ) ) if ( Abc_NtkGetChoiceNum( pNtk ) )
printf( "Performing renoding with choices.\n" ); printf( "Performing renoding with choices.\n" );
nDsdCounter = 0;
// set defaults // set defaults
memset( pPars, 0, sizeof(If_Par_t) ); memset( pPars, 0, sizeof(If_Par_t) );
// user-controlable paramters // user-controlable paramters
...@@ -136,6 +140,8 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nF ...@@ -136,6 +140,8 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nF
s_vMemory2 = NULL; s_vMemory2 = NULL;
} }
printf( "Decomposed %d functions.\n", nDsdCounter );
return pNtkNew; return pNtkNew;
} }
...@@ -154,6 +160,14 @@ int Abc_NtkRenodeEvalAig( If_Cut_t * pCut ) ...@@ -154,6 +160,14 @@ int Abc_NtkRenodeEvalAig( If_Cut_t * pCut )
{ {
Kit_Graph_t * pGraph; Kit_Graph_t * pGraph;
int i, nNodes; int i, nNodes;
extern void Kit_DsdTest( unsigned * pTruth, int nVars );
if ( If_CutLeaveNum(pCut) == 8 )
{
nDsdCounter++;
Kit_DsdTest( If_CutTruth(pCut), If_CutLeaveNum(pCut) );
}
pGraph = Kit_TruthToGraph( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory ); pGraph = Kit_TruthToGraph( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory );
if ( pGraph == NULL ) if ( pGraph == NULL )
{ {
......
src/base/abci/abcVerify.c
...@@ -256,13 +256,25 @@ void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, in ...@@ -256,13 +256,25 @@ void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, in
nOutputs = 0; nOutputs = 0;
Abc_NtkForEachPo( pMiter, pObj, i ) Abc_NtkForEachPo( pMiter, pObj, i )
{ {
// get the cone of this output if ( Abc_ObjFanin0(pObj) == Abc_AigConst1(pMiter) )
pMiterPart = Abc_NtkCreateCone( pMiter, Abc_ObjFanin0(pObj), Abc_ObjName(pObj), 0 ); {
if ( Abc_ObjFaninC0(pObj) ) if ( Abc_ObjFaninC0(pObj) ) // complemented -> const 0
Abc_ObjXorFaninC( Abc_NtkPo(pMiterPart,0), 0 ); RetValue = 1;
// solve the cone else
// RetValue = Abc_NtkMiterProve( &pMiterPart, pParams ); RetValue = 0;
RetValue = Abc_NtkIvyProve( &pMiterPart, pParams ); pMiterPart = NULL;
}
else
{
// get the cone of this output
pMiterPart = Abc_NtkCreateCone( pMiter, Abc_ObjFanin0(pObj), Abc_ObjName(pObj), 0 );
if ( Abc_ObjFaninC0(pObj) )
Abc_ObjXorFaninC( Abc_NtkPo(pMiterPart,0), 0 );
// solve the cone
// RetValue = Abc_NtkMiterProve( &pMiterPart, pParams );
RetValue = Abc_NtkIvyProve( &pMiterPart, pParams );
}
if ( RetValue == -1 ) if ( RetValue == -1 )
{ {
printf( "Networks are undecided (resource limits is reached).\r" ); printf( "Networks are undecided (resource limits is reached).\r" );
...@@ -286,7 +298,8 @@ void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, in ...@@ -286,7 +298,8 @@ void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, in
} }
// if ( pMiter->pModel ) // if ( pMiter->pModel )
// Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel ); // Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
Abc_NtkDelete( pMiterPart ); if ( pMiterPart )
Abc_NtkDelete( pMiterPart );
} }
Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" ); Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" );
......
src/base/io/io.c
...@@ -31,6 +31,7 @@ static int IoCommandReadBaf ( Abc_Frame_t * pAbc, int argc, char **argv ); ...@@ -31,6 +31,7 @@ static int IoCommandReadBaf ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadBlif ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadBlif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadBlifMv ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadBlifMv ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadBench ( Abc_Frame_t * pAbc, int argc, char **argv ); 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 IoCommandReadEdif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadEqn ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadEqn ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadPla ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadPla ( Abc_Frame_t * pAbc, int argc, char **argv );
...@@ -82,6 +83,7 @@ void Io_Init( Abc_Frame_t * pAbc ) ...@@ -82,6 +83,7 @@ void Io_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "I/O", "read_blif", IoCommandReadBlif, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_blif", IoCommandReadBlif, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_blif_mv", IoCommandReadBlif, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_blif_mv", IoCommandReadBlif, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_bench", IoCommandReadBench, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_bench", IoCommandReadBench, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_dsd", IoCommandReadDsd, 1 );
// Cmd_CommandAdd( pAbc, "I/O", "read_edif", IoCommandReadEdif, 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_eqn", IoCommandReadEqn, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_pla", IoCommandReadPla, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_pla", IoCommandReadPla, 1 );
...@@ -483,6 +485,67 @@ usage: ...@@ -483,6 +485,67 @@ usage:
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int IoCommandReadDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk;
char * pString;
int fCheck;
int c;
extern Abc_Ntk_t * Io_ReadDsd( char * pFormula );
fCheck = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
{
switch ( c )
{
case 'c':
fCheck ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( argc != globalUtilOptind + 1 )
goto usage;
// get the input file name
pString = argv[globalUtilOptind];
// read the file using the corresponding file reader
pNtk = Io_ReadDsd( pString );
if ( pNtk == NULL )
return 1;
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
return 0;
usage:
fprintf( pAbc->Err, "usage: read_dsd [-h] <formula>\n" );
fprintf( pAbc->Err, "\t parses a formula representing DSD of a function\n" );
fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
fprintf( pAbc->Err, "\tformula : the formula representing disjoint-support decomposition (DSD)\n" );
fprintf( pAbc->Err, "\t Example of a formula: !(a*(b+CA(c,!d,e*f))*79B3(g,h,i,k))\n" );
fprintf( pAbc->Err, "\t where \'!\' is an INV, \'*\' is an AND, \'+\' is an XOR, \n" );
fprintf( pAbc->Err, "\t CA and 79B3 are hexadecimal representations of truth tables\n" );
fprintf( pAbc->Err, "\t (in this case CA=11001010 is truth table of MUX(Ctrl,Data1,Data0))\n" );
fprintf( pAbc->Err, "\t The lower chars (a,b,c,etc) are reserved for elementary variables.\n" );
fprintf( pAbc->Err, "\t The upper chars (A,B,C,etc) are reserved for hexadecimal digits.\n" );
fprintf( pAbc->Err, "\t No spaces are allowed in the formula.\n" );
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int IoCommandReadEdif( Abc_Frame_t * pAbc, int argc, char ** argv ) int IoCommandReadEdif( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
Abc_Ntk_t * pNtk; Abc_Ntk_t * pNtk;
......
src/base/io/ioReadDsd.c 0 → 100644
/**CFile****************************************************************
FileName [ioReadDsd.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Command processing package.]
Synopsis [Procedure to read network from file.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: ioReadDsd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "io.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Finds the end of the part.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Io_ReadDsdFindEnd( char * pCur )
{
char * pEnd;
int nParts = 0;
assert( *pCur == '(' );
for ( pEnd = pCur; *pEnd; pEnd++ )
{
if ( *pEnd == '(' )
nParts++;
else if ( *pEnd == ')' )
nParts--;
if ( nParts == 0 )
return pEnd;
}
return NULL;
}
/**Function*************************************************************
Synopsis [Splits the formula into parts.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Io_ReadDsdStrSplit( char * pCur, char * pParts[], int * pTypeXor )
{
int fAnd = 0, fXor = 0, fPri = 0, nParts = 0;
assert( *pCur );
// process the parts
while ( 1 )
{
// save the current part
pParts[nParts++] = pCur;
// skip the complement
if ( *pCur == '!' )
pCur++;
// skip var
if ( *pCur >= 'a' && *pCur <= 'z' )
pCur++;
else
{
// skip hex truth table
while ( (*pCur >= '0' && *pCur <= '9') || (*pCur >= 'A' && *pCur <= 'F') )
pCur++;
// process parantheses
if ( *pCur != '(' )
{
printf( "Cannot find the opening paranthesis.\n" );
break;
}
// find the corresponding closing paranthesis
pCur = Io_ReadDsdFindEnd( pCur );
if ( pCur == NULL )
{
printf( "Cannot find the closing paranthesis.\n" );
break;
}
pCur++;
}
// check the end
if ( *pCur == 0 )
break;
// check symbol
if ( *pCur != '*' && *pCur != '+' && *pCur != ',' )
{
printf( "Wrong separating symbol.\n" );
break;
}
// remember the symbol
fAnd |= (*pCur == '*');
fXor |= (*pCur == '+');
fPri |= (*pCur == ',');
*pCur++ = 0;
}
// check separating symbols
if ( fAnd + fXor + fPri > 1 )
{
printf( "Different types of separating symbol ennPartsed.\n" );
return 0;
}
*pTypeXor = fXor;
return nParts;
}
/**Function*************************************************************
Synopsis [Recursively parses the formula.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Obj_t * Io_ReadDsd_rec( Abc_Ntk_t * pNtk, char * pCur, char * pSop )
{
Abc_Obj_t * pObj, * pFanin;
char * pEnd, * pParts[32];
int i, nParts, TypeExor;
// consider complemented formula
if ( *pCur == '!' )
{
pObj = Io_ReadDsd_rec( pNtk, pCur + 1, NULL );
return Abc_NtkCreateNodeInv( pNtk, pObj );
}
if ( *pCur == '(' )
{
assert( pCur[strlen(pCur)-1] == ')' );
pCur[strlen(pCur)-1] = 0;
nParts = Io_ReadDsdStrSplit( pCur+1, pParts, &TypeExor );
if ( nParts == 0 )
{
Abc_NtkDelete( pNtk );
return NULL;
}
pObj = Abc_NtkCreateNode( pNtk );
if ( pSop )
{
// for ( i = nParts - 1; i >= 0; i-- )
for ( i = 0; i < nParts; i++ )
{
pFanin = Io_ReadDsd_rec( pNtk, pParts[i], NULL );
if ( pFanin == NULL )
return NULL;
Abc_ObjAddFanin( pObj, pFanin );
}
}
else
{
for ( i = 0; i < nParts; i++ )
{
pFanin = Io_ReadDsd_rec( pNtk, pParts[i], NULL );
if ( pFanin == NULL )
return NULL;
Abc_ObjAddFanin( pObj, pFanin );
}
}
if ( pSop )
pObj->pData = Abc_SopRegister( pNtk->pManFunc, pSop );
else if ( TypeExor )
pObj->pData = Abc_SopCreateXorSpecial( pNtk->pManFunc, nParts );
else
pObj->pData = Abc_SopCreateAnd( pNtk->pManFunc, nParts, NULL );
return pObj;
}
if ( *pCur >= 'a' && *pCur <= 'z' )
{
assert( *(pCur+1) == 0 );
return Abc_NtkPi( pNtk, *pCur - 'a' );
}
// skip hex truth table
pEnd = pCur;
while ( (*pEnd >= '0' && *pEnd <= '9') || (*pEnd >= 'A' && *pEnd <= 'F') )
pEnd++;
if ( *pEnd != '(' )
{
printf( "Cannot find the end of hexidecimal truth table.\n" );
return NULL;
}
// parse the truth table
*pEnd = 0;
pSop = Abc_SopFromTruthHex( pCur );
*pEnd = '(';
pObj = Io_ReadDsd_rec( pNtk, pEnd, pSop );
free( pSop );
return pObj;
}
/**Function*************************************************************
Synopsis [Derives the DSD network of the formula.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Io_ReadDsd( char * pForm )
{
Abc_Ntk_t * pNtk;
Abc_Obj_t * pObj, * pTop;
Vec_Ptr_t * vNames;
char * pCur, * pFormCopy;
int i, nInputs;
// count the number of elementary variables
nInputs = 0;
for ( pCur = pForm; *pCur; pCur++ )
if ( *pCur >= 'a' && *pCur <= 'z' )
nInputs = ABC_MAX( nInputs, *pCur - 'a' );
nInputs++;
// create the network
pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
pNtk->pName = Extra_UtilStrsav( "dsd" );
// create PIs
vNames = Abc_NodeGetFakeNames( nInputs );
for ( i = 0; i < nInputs; i++ )
Abc_ObjAssignName( Abc_NtkCreatePi(pNtk), Vec_PtrEntry(vNames, i), NULL );
Abc_NodeFreeNames( vNames );
// transform the formula by inserting parantheses
// this transforms strings like PRIME(a,b,cd) into (PRIME((a),(b),(cd)))
pCur = pFormCopy = ALLOC( char, 3 * strlen(pForm) + 10 );
*pCur++ = '(';
for ( ; *pForm; pForm++ )
if ( *pForm == '(' )
{
*pCur++ = '(';
*pCur++ = '(';
}
else if ( *pForm == ')' )
{
*pCur++ = ')';
*pCur++ = ')';
}
else if ( *pForm == ',' )
{
*pCur++ = ')';
*pCur++ = ',';
*pCur++ = '(';
}
else
*pCur++ = *pForm;
*pCur++ = ')';
*pCur = 0;
// parse the formula
pObj = Io_ReadDsd_rec( pNtk, pFormCopy, NULL );
free( pFormCopy );
if ( pObj == NULL )
return NULL;
// create output
pTop = Abc_NtkCreatePo(pNtk);
Abc_ObjAssignName( pTop, "F", NULL );
Abc_ObjAddFanin( pTop, pObj );
// create the only PO
if ( !Abc_NtkCheck( pNtk ) )
{
fprintf( stdout, "Io_ReadDsd(): Network check has failed.\n" );
Abc_NtkDelete( pNtk );
return NULL;
}
return pNtk;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/base/io/ioWriteBench.c
...@@ -258,7 +258,7 @@ int Io_WriteBenchLutOneNode( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vTruth ...@@ -258,7 +258,7 @@ int Io_WriteBenchLutOneNode( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vTruth
nFanins = Abc_ObjFaninNum(pNode); nFanins = Abc_ObjFaninNum(pNode);
assert( nFanins <= 8 ); assert( nFanins <= 8 );
// compute the truth table // compute the truth table
pTruth = Abc_ConvertAigToTruth( pNode->pNtk->pManFunc, Hop_Regular(pNode->pData), nFanins, vTruth ); pTruth = Abc_ConvertAigToTruth( pNode->pNtk->pManFunc, Hop_Regular(pNode->pData), nFanins, vTruth, 0 );
if ( Hop_IsComplement(pNode->pData) ) if ( Hop_IsComplement(pNode->pData) )
Extra_TruthNot( pTruth, pTruth, nFanins ); Extra_TruthNot( pTruth, pTruth, nFanins );
// consider simple cases // consider simple cases
......
src/base/io/io_.c
...@@ -28,6 +28,18 @@ ...@@ -28,6 +28,18 @@
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/base/io/module.make
...@@ -5,6 +5,7 @@ SRC += src/base/io/io.c \ ...@@ -5,6 +5,7 @@ SRC += src/base/io/io.c \
src/base/io/ioReadBlif.c \ src/base/io/ioReadBlif.c \
src/base/io/ioReadBlifAig.c \ src/base/io/ioReadBlifAig.c \
src/base/io/ioReadBlifMv.c \ src/base/io/ioReadBlifMv.c \
src/base/io/ioReadDsd.c \
src/base/io/ioReadEdif.c \ src/base/io/ioReadEdif.c \
src/base/io/ioReadEqn.c \ src/base/io/ioReadEqn.c \
src/base/io/ioReadPla.c \ src/base/io/ioReadPla.c \
......
src/map/if/if.h
...@@ -139,6 +139,7 @@ struct If_Man_t_ ...@@ -139,6 +139,7 @@ struct If_Man_t_
unsigned * puTemp[4]; // used for the truth table computation unsigned * puTemp[4]; // used for the truth table computation
int SortMode; // one of the three sorting modes int SortMode; // one of the three sorting modes
int fNextRound; // set to 1 after the first round int fNextRound; // set to 1 after the first round
int nChoices; // the number of choice nodes
// sequential mapping // sequential mapping
Vec_Ptr_t * vLatchOrder; // topological ordering of latches Vec_Ptr_t * vLatchOrder; // topological ordering of latches
Vec_Int_t * vLags; // sequentail lags of all nodes Vec_Int_t * vLags; // sequentail lags of all nodes
......
src/map/if/ifMan.c
...@@ -480,7 +480,8 @@ void If_ManSetupSetAll( If_Man_t * p ) ...@@ -480,7 +480,8 @@ void If_ManSetupSetAll( If_Man_t * p )
if ( p->pPars->fVerbose ) if ( p->pPars->fVerbose )
{ {
printf( "Total memory = %7.2f Mb. Peak cut memory = %7.2f Mb. \n", printf( "Node = %7d. Ch = %5d. Total mem = %7.2f Mb. Peak cut mem = %7.2f Mb.\n",
If_ManAndNum(p), p->nChoices,
1.0 * (p->nObjBytes + 2*sizeof(void *)) * If_ManObjNum(p) / (1<<20), 1.0 * (p->nObjBytes + 2*sizeof(void *)) * If_ManObjNum(p) / (1<<20),
1.0 * p->nSetBytes * nCrossCut / (1<<20) ); 1.0 * p->nSetBytes * nCrossCut / (1<<20) );
} }
......
src/opt/kit/kit.h
...@@ -153,13 +153,22 @@ static inline Kit_Node_t * Kit_GraphNodeFanin1( Kit_Graph_t * pGraph, Kit_Node_t ...@@ -153,13 +153,22 @@ static inline Kit_Node_t * Kit_GraphNodeFanin1( Kit_Graph_t * pGraph, Kit_Node_t
static inline int Kit_Float2Int( float Val ) { return *((int *)&Val); } static inline int Kit_Float2Int( float Val ) { return *((int *)&Val); }
static inline float Kit_Int2Float( int Num ) { return *((float *)&Num); } static inline float Kit_Int2Float( int Num ) { return *((float *)&Num); }
static inline int Kit_BitWordNum( int nBits ) { return nBits/(8*sizeof(unsigned)) + ((nBits%(8*sizeof(unsigned))) > 0); } static inline int Kit_BitWordNum( int nBits ) { return nBits/(8*sizeof(unsigned)) + ((nBits%(8*sizeof(unsigned))) > 0); }
static inline int Kit_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); } static inline int Kit_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
static inline unsigned Kit_BitMask( int nBits ) { assert( nBits <= 32 ); return ~((~(unsigned)0) << nBits); }
static inline void Kit_TruthSetBit( unsigned * p, int Bit ) { p[Bit>>5] |= (1<<(Bit & 31)); } static inline void Kit_TruthSetBit( unsigned * p, int Bit ) { p[Bit>>5] |= (1<<(Bit & 31)); }
static inline void Kit_TruthXorBit( unsigned * p, int Bit ) { p[Bit>>5] ^= (1<<(Bit & 31)); } static inline void Kit_TruthXorBit( unsigned * p, int Bit ) { p[Bit>>5] ^= (1<<(Bit & 31)); }
static inline int Kit_TruthHasBit( unsigned * p, int Bit ) { return (p[Bit>>5] & (1<<(Bit & 31))) > 0; } static inline int Kit_TruthHasBit( unsigned * p, int Bit ) { return (p[Bit>>5] & (1<<(Bit & 31))) > 0; }
static inline int Kit_WordFindFirstBit( unsigned uWord )
{
int i;
for ( i = 0; i < 32; i++ )
if ( uWord & (1 << i) )
return i;
return -1;
}
static inline int Kit_WordCountOnes( unsigned uWord ) static inline int Kit_WordCountOnes( unsigned uWord )
{ {
uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555); uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
...@@ -183,6 +192,14 @@ static inline int Kit_TruthIsEqual( unsigned * pIn0, unsigned * pIn1, int nVars ...@@ -183,6 +192,14 @@ static inline int Kit_TruthIsEqual( unsigned * pIn0, unsigned * pIn1, int nVars
return 0; return 0;
return 1; return 1;
} }
static inline int Kit_TruthIsOpposite( unsigned * pIn0, unsigned * pIn1, int nVars )
{
int w;
for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
if ( pIn0[w] != ~pIn1[w] )
return 0;
return 1;
}
static inline int Kit_TruthIsConst0( unsigned * pIn, int nVars ) static inline int Kit_TruthIsConst0( unsigned * pIn, int nVars )
{ {
int w; int w;
...@@ -332,9 +349,11 @@ extern void Kit_TruthStretch( unsigned * pOut, unsigned * pIn, int nV ...@@ -332,9 +349,11 @@ extern void Kit_TruthStretch( unsigned * pOut, unsigned * pIn, int nV
extern void Kit_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase ); extern void Kit_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase );
extern int Kit_TruthVarInSupport( unsigned * pTruth, int nVars, int iVar ); extern int Kit_TruthVarInSupport( unsigned * pTruth, int nVars, int iVar );
extern int Kit_TruthSupportSize( unsigned * pTruth, int nVars ); extern int Kit_TruthSupportSize( unsigned * pTruth, int nVars );
extern int Kit_TruthSupport( unsigned * pTruth, int nVars ); extern unsigned Kit_TruthSupport( unsigned * pTruth, int nVars );
extern void Kit_TruthCofactor0( unsigned * pTruth, int nVars, int iVar ); extern void Kit_TruthCofactor0( unsigned * pTruth, int nVars, int iVar );
extern void Kit_TruthCofactor1( unsigned * pTruth, int nVars, int iVar ); extern void Kit_TruthCofactor1( unsigned * pTruth, int nVars, int iVar );
extern void Kit_TruthCofactor0New( unsigned * pOut, unsigned * pIn, int nVars, int iVar );
extern void Kit_TruthCofactor1New( unsigned * pOut, unsigned * pIn, int nVars, int iVar );
extern void Kit_TruthExist( unsigned * pTruth, int nVars, int iVar ); extern void Kit_TruthExist( unsigned * pTruth, int nVars, int iVar );
extern void Kit_TruthExistNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar ); extern void Kit_TruthExistNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar );
extern void Kit_TruthExistSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask ); extern void Kit_TruthExistSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask );
......
src/opt/kit/kitTruth.c
...@@ -311,7 +311,7 @@ int Kit_TruthSupportSize( unsigned * pTruth, int nVars ) ...@@ -311,7 +311,7 @@ int Kit_TruthSupportSize( unsigned * pTruth, int nVars )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Kit_TruthSupport( unsigned * pTruth, int nVars ) unsigned Kit_TruthSupport( unsigned * pTruth, int nVars )
{ {
int i, Support = 0; int i, Support = 0;
for ( i = 0; i < nVars; i++ ) for ( i = 0; i < nVars; i++ )
...@@ -324,6 +324,57 @@ int Kit_TruthSupport( unsigned * pTruth, int nVars ) ...@@ -324,6 +324,57 @@ int Kit_TruthSupport( unsigned * pTruth, int nVars )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Computes negative cofactor of the function.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_TruthCofactor0( unsigned * pTruth, int nVars, int iVar )
{
int nWords = Kit_TruthWordNum( nVars );
int i, k, Step;
assert( iVar < nVars );
switch ( iVar )
{
case 0:
for ( i = 0; i < nWords; i++ )
pTruth[i] = (pTruth[i] & 0x55555555) | ((pTruth[i] & 0x55555555) << 1);
return;
case 1:
for ( i = 0; i < nWords; i++ )
pTruth[i] = (pTruth[i] & 0x33333333) | ((pTruth[i] & 0x33333333) << 2);
return;
case 2:
for ( i = 0; i < nWords; i++ )
pTruth[i] = (pTruth[i] & 0x0F0F0F0F) | ((pTruth[i] & 0x0F0F0F0F) << 4);
return;
case 3:
for ( i = 0; i < nWords; i++ )
pTruth[i] = (pTruth[i] & 0x00FF00FF) | ((pTruth[i] & 0x00FF00FF) << 8);
return;
case 4:
for ( i = 0; i < nWords; i++ )
pTruth[i] = (pTruth[i] & 0x0000FFFF) | ((pTruth[i] & 0x0000FFFF) << 16);
return;
default:
Step = (1 << (iVar - 5));
for ( k = 0; k < nWords; k += 2*Step )
{
for ( i = 0; i < Step; i++ )
pTruth[Step+i] = pTruth[i];
pTruth += 2*Step;
}
return;
}
}
/**Function*************************************************************
Synopsis [Computes positive cofactor of the function.] Synopsis [Computes positive cofactor of the function.]
Description [] Description []
...@@ -375,7 +426,7 @@ void Kit_TruthCofactor1( unsigned * pTruth, int nVars, int iVar ) ...@@ -375,7 +426,7 @@ void Kit_TruthCofactor1( unsigned * pTruth, int nVars, int iVar )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Computes negative cofactor of the function.] Synopsis [Computes positive cofactor of the function.]
Description [] Description []
...@@ -384,7 +435,7 @@ void Kit_TruthCofactor1( unsigned * pTruth, int nVars, int iVar ) ...@@ -384,7 +435,7 @@ void Kit_TruthCofactor1( unsigned * pTruth, int nVars, int iVar )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Kit_TruthCofactor0( unsigned * pTruth, int nVars, int iVar ) void Kit_TruthCofactor0New( unsigned * pOut, unsigned * pIn, int nVars, int iVar )
{ {
int nWords = Kit_TruthWordNum( nVars ); int nWords = Kit_TruthWordNum( nVars );
int i, k, Step; int i, k, Step;
...@@ -394,31 +445,84 @@ void Kit_TruthCofactor0( unsigned * pTruth, int nVars, int iVar ) ...@@ -394,31 +445,84 @@ void Kit_TruthCofactor0( unsigned * pTruth, int nVars, int iVar )
{ {
case 0: case 0:
for ( i = 0; i < nWords; i++ ) for ( i = 0; i < nWords; i++ )
pTruth[i] = (pTruth[i] & 0x55555555) | ((pTruth[i] & 0x55555555) << 1); pOut[i] = (pIn[i] & 0x55555555) | ((pIn[i] & 0x55555555) << 1);
return; return;
case 1: case 1:
for ( i = 0; i < nWords; i++ ) for ( i = 0; i < nWords; i++ )
pTruth[i] = (pTruth[i] & 0x33333333) | ((pTruth[i] & 0x33333333) << 2); pOut[i] = (pIn[i] & 0x33333333) | ((pIn[i] & 0x33333333) << 2);
return; return;
case 2: case 2:
for ( i = 0; i < nWords; i++ ) for ( i = 0; i < nWords; i++ )
pTruth[i] = (pTruth[i] & 0x0F0F0F0F) | ((pTruth[i] & 0x0F0F0F0F) << 4); pOut[i] = (pIn[i] & 0x0F0F0F0F) | ((pIn[i] & 0x0F0F0F0F) << 4);
return; return;
case 3: case 3:
for ( i = 0; i < nWords; i++ ) for ( i = 0; i < nWords; i++ )
pTruth[i] = (pTruth[i] & 0x00FF00FF) | ((pTruth[i] & 0x00FF00FF) << 8); pOut[i] = (pIn[i] & 0x00FF00FF) | ((pIn[i] & 0x00FF00FF) << 8);
return; return;
case 4: case 4:
for ( i = 0; i < nWords; i++ ) for ( i = 0; i < nWords; i++ )
pTruth[i] = (pTruth[i] & 0x0000FFFF) | ((pTruth[i] & 0x0000FFFF) << 16); pOut[i] = (pIn[i] & 0x0000FFFF) | ((pIn[i] & 0x0000FFFF) << 16);
return; return;
default: default:
Step = (1 << (iVar - 5)); Step = (1 << (iVar - 5));
for ( k = 0; k < nWords; k += 2*Step ) for ( k = 0; k < nWords; k += 2*Step )
{ {
for ( i = 0; i < Step; i++ ) for ( i = 0; i < Step; i++ )
pTruth[Step+i] = pTruth[i]; pOut[i] = pOut[Step+i] = pIn[i];
pTruth += 2*Step; pIn += 2*Step;
pOut += 2*Step;
}
return;
}
}
/**Function*************************************************************
Synopsis [Computes positive cofactor of the function.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_TruthCofactor1New( unsigned * pOut, unsigned * pIn, int nVars, int iVar )
{
int nWords = Kit_TruthWordNum( nVars );
int i, k, Step;
assert( iVar < nVars );
switch ( iVar )
{
case 0:
for ( i = 0; i < nWords; i++ )
pOut[i] = (pIn[i] & 0xAAAAAAAA) | ((pIn[i] & 0xAAAAAAAA) >> 1);
return;
case 1:
for ( i = 0; i < nWords; i++ )
pOut[i] = (pIn[i] & 0xCCCCCCCC) | ((pIn[i] & 0xCCCCCCCC) >> 2);
return;
case 2:
for ( i = 0; i < nWords; i++ )
pOut[i] = (pIn[i] & 0xF0F0F0F0) | ((pIn[i] & 0xF0F0F0F0) >> 4);
return;
case 3:
for ( i = 0; i < nWords; i++ )
pOut[i] = (pIn[i] & 0xFF00FF00) | ((pIn[i] & 0xFF00FF00) >> 8);
return;
case 4:
for ( i = 0; i < nWords; i++ )
pOut[i] = (pIn[i] & 0xFFFF0000) | ((pIn[i] & 0xFFFF0000) >> 16);
return;
default:
Step = (1 << (iVar - 5));
for ( k = 0; k < nWords; k += 2*Step )
{
for ( i = 0; i < Step; i++ )
pOut[i] = pOut[Step+i] = pIn[Step+i];
pIn += 2*Step;
pOut += 2*Step;
} }
return; return;
} }
...@@ -733,6 +837,8 @@ void Kit_TruthMux( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVar ...@@ -733,6 +837,8 @@ void Kit_TruthMux( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVar
pOut[Step+i] = pCof1[Step+i]; pOut[Step+i] = pCof1[Step+i];
} }
pOut += 2*Step; pOut += 2*Step;
pCof0 += 2*Step;
pCof1 += 2*Step;
} }
return; return;
} }
......
src/opt/kit/module.make
SRC += src/opt/kit/kitBdd.c \ SRC += src/opt/kit/kitBdd.c \
src/opt/kit/kitDsd.c \
src/opt/kit/kitFactor.c \ src/opt/kit/kitFactor.c \
src/opt/kit/kitGraph.c \ src/opt/kit/kitGraph.c \
src/opt/kit/kitHop.c \ src/opt/kit/kitHop.c \
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment