Skip to content

A
abc
Commit daadd43b by Bruno Schmitt
Options

Merged alanmi/abc into default

parents dcd37b6a 9895f30d
Showing with 72 additions and 17 deletions
abcexe.dsp
......@@ -90,6 +90,10 @@ LINK32=link.exe
SOURCE=.\src\base\main\main.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\ssw\sswSat.c
# End Source File
# End Group
# Begin Group "Header Files"
......
src/base/abci/abc.c
......@@ -14828,12 +14828,12 @@ usage:
***********************************************************************/
int Abc_CommandDumpEquiv( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Abc_NtkDumpEquiv( Abc_Ntk_t * pNtks[2], char * pFileName, int nConfs, int fVerbose );
extern void Abc_NtkDumpEquiv( Abc_Ntk_t * pNtks[2], char * pFileName, int nConfs, int fByName, int fVerbose );
Abc_Ntk_t * pNtks[2] = {NULL};
char * pFileName[2], * pFileNameOut;
int c, nConfs = 1000, fVerbose = 0;
int c, nConfs = 1000, fByName = 1, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Cvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Cnvh" ) ) != EOF )
{
switch ( c )
{
......@@ -14848,6 +14848,9 @@ int Abc_CommandDumpEquiv( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nConfs < 0 )
goto usage;
break;
case 'n':
fByName ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
......@@ -14872,20 +14875,25 @@ int Abc_CommandDumpEquiv( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
Abc_NtkToAig( pNtks[c] );
}
if ( Abc_NtkCiNum(pNtks[0]) != Abc_NtkCiNum(pNtks[1]) )
Abc_Print( -1, "The number of primary inputs of networks \"%s\" and \"%s\" does not match.\n", Abc_NtkName(pNtks[0]), Abc_NtkName(pNtks[1]) );
// if ( Abc_NtkCiNum(pNtks[0]) != Abc_NtkCiNum(pNtks[1]) )
// Abc_Print( -1, "The number of primary inputs of networks \"%s\" and \"%s\" does not match.\n", Abc_NtkName(pNtks[0]), Abc_NtkName(pNtks[1]) );
// else if ( Abc_NtkCoNum(pNtks[0]) != Abc_NtkCoNum(pNtks[1]) )
// Abc_Print( -1, "The number of primary outputs of networks \"%s\" and \"%s\" does not match.\n", Abc_NtkName(pNtks[0]), Abc_NtkName(pNtks[1]) );
else
Abc_NtkDumpEquiv( pNtks, pFileNameOut, nConfs, fVerbose );
// else
Abc_NtkDumpEquiv( pNtks, pFileNameOut, nConfs, fByName, fVerbose );
Abc_NtkDelete( pNtks[0] );
Abc_NtkDelete( pNtks[1] );
return 0;
usage:
Abc_Print( -2, "usage: dump_equiv [-C num] [-vh] <file1.blif> <file2.blif> <file_dump_equiv.txt>\n" );
Abc_Print( -2, "usage: dump_equiv [-C num] [-nvh] <file1.blif> <file2.blif> <file_dump_equiv.txt>\n" );
Abc_Print( -2, "\t computes equivalence classes of nodes in <file1> and <file2>\n" );
Abc_Print( -2, "\t By default this procedure performs matching of primary inputs by name.\n" );
Abc_Print( -2, "\t Those inputs that cannot be matched are treated as free variables.\n" );
Abc_Print( -2, "\t There is no effort to match primary outputs. Indeed, if two outputs\n" );
Abc_Print( -2, "\t are equivalent, they will belong to the same equivalence class in the end.\n" );
Abc_Print( -2, "\t-C num : the maximum number of conflicts at each node [default = %d]\n", nConfs );
Abc_Print( -2, "\t-n : enable matching of primary inputs by name [default = %s]\n", fByName? "yes": "no" );
Abc_Print( -2, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\t<file1> : first network whose nodes are considered\n" );
src/base/abci/abcDress3.c
......@@ -112,7 +112,7 @@ int Abc_ConvertHopToGia( Gia_Man_t * p, Hop_Obj_t * pRoot )
SeeAlso []
***********************************************************************/
void Abc_NtkAigToGiaOne( Gia_Man_t * p, Abc_Ntk_t * pNtk )
void Abc_NtkAigToGiaOne( Gia_Man_t * p, Abc_Ntk_t * pNtk, Vec_Int_t * vMap )
{
Hop_Man_t * pHopMan;
Hop_Obj_t * pHopObj;
......@@ -125,7 +125,7 @@ void Abc_NtkAigToGiaOne( Gia_Man_t * p, Abc_Ntk_t * pNtk )
// image primary inputs
Abc_NtkCleanCopy( pNtk );
Abc_NtkForEachCi( pNtk, pNode, i )
pNode->iTemp = Gia_ManCiLit(p, i);
pNode->iTemp = Gia_ManCiLit(p, Vec_IntEntry(vMap, i));
// iterate through nodes used in the mapping
vNodes = Abc_NtkDfs( pNtk, 1 );
Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
......@@ -143,25 +143,68 @@ void Abc_NtkAigToGiaOne( Gia_Man_t * p, Abc_Ntk_t * pNtk )
Abc_NtkForEachCo( pNtk, pNode, i )
Gia_ManAppendCo( p, Abc_ObjFanin0(pNode)->iTemp );
}
Gia_Man_t * Abc_NtkAigToGiaTwo( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
Gia_Man_t * Abc_NtkAigToGiaTwo( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fByName )
{
Gia_Man_t * p;
Gia_Obj_t * pObj;
Abc_Obj_t * pNode;
int i;
Vec_Int_t * vMap1, * vMap2;
int i, Index = 0;
assert( Abc_NtkIsAigLogic(pNtk1) );
assert( Abc_NtkIsAigLogic(pNtk2) );
// find common variables
if ( fByName )
{
int nCommon = 0;
vMap1 = Vec_IntStartNatural( Abc_NtkCiNum(pNtk1) );
vMap2 = Vec_IntAlloc( Abc_NtkCiNum(pNtk2) );
Abc_NtkForEachCi( pNtk1, pNode, i )
pNode->iTemp = Index++;
assert( Index == Abc_NtkCiNum(pNtk1) );
Abc_NtkForEachCi( pNtk2, pNode, i )
{
int Num = Nm_ManFindIdByName( pNtk1->pManName, Abc_ObjName(pNode), ABC_OBJ_PI );
if ( Num < 0 )
Num = Nm_ManFindIdByName( pNtk1->pManName, Abc_ObjName(pNode), ABC_OBJ_BO );
assert( Num < 0 || Abc_ObjIsCi(Abc_NtkObj(pNtk1, Num)) );
if ( Num >= 0 )
Vec_IntPush( vMap2, Abc_NtkObj(pNtk1, Num)->iTemp ), nCommon++;
else
Vec_IntPush( vMap2, Index++ );
}
// report
printf( "Matched %d vars by name.", nCommon );
if ( nCommon != Abc_NtkCiNum(pNtk1) )
printf( " Netlist1 has %d unmatched vars.", Abc_NtkCiNum(pNtk1) - nCommon );
if ( nCommon != Abc_NtkCiNum(pNtk2) )
printf( " Netlist2 has %d unmatched vars.", Abc_NtkCiNum(pNtk2) - nCommon );
printf( "\n" );
}
else
{
vMap1 = Vec_IntStartNatural( Abc_NtkCiNum(pNtk1) );
vMap2 = Vec_IntStartNatural( Abc_NtkCiNum(pNtk2) );
// report
printf( "Matched %d vars by order.", Abc_MinInt(Abc_NtkCiNum(pNtk1), Abc_NtkCiNum(pNtk2)) );
if ( Abc_NtkCiNum(pNtk1) < Abc_NtkCiNum(pNtk2) )
printf( " The last %d vars of Netlist2 are unmatched vars.", Abc_NtkCiNum(pNtk2) - Abc_NtkCiNum(pNtk1) );
if ( Abc_NtkCiNum(pNtk1) > Abc_NtkCiNum(pNtk2) )
printf( " The last %d vars of Netlist1 are unmatched vars.", Abc_NtkCiNum(pNtk1) - Abc_NtkCiNum(pNtk2) );
printf( "\n" );
}
// create new manager
p = Gia_ManStart( 10000 );
p->pName = Abc_UtilStrsav( Abc_NtkName(pNtk1) );
p->pSpec = Abc_UtilStrsav( Abc_NtkSpec(pNtk1) );
Abc_NtkForEachCi( pNtk1, pNode, i )
for ( i = 0; i < Index; i++ )
Gia_ManAppendCi(p);
// add logic
Gia_ManHashAlloc( p );
Abc_NtkAigToGiaOne( p, pNtk1 );
Abc_NtkAigToGiaOne( p, pNtk2 );
Abc_NtkAigToGiaOne( p, pNtk1, vMap1 );
Abc_NtkAigToGiaOne( p, pNtk2, vMap2 );
Gia_ManHashStop( p );
Vec_IntFree( vMap1 );
Vec_IntFree( vMap2 );
// add extra POs to dangling nodes
Gia_ManCreateValueRefs( p );
Gia_ManForEachAnd( p, pObj, i )
......@@ -268,12 +311,12 @@ void Abc_NtkDumpEquivFile( char * pFileName, Vec_Int_t * vClasses, Abc_Ntk_t * p
SeeAlso []
***********************************************************************/
void Abc_NtkDumpEquiv( Abc_Ntk_t * pNtks[2], char * pFileName, int nConfs, int fVerbose )
void Abc_NtkDumpEquiv( Abc_Ntk_t * pNtks[2], char * pFileName, int nConfs, int fByName, int fVerbose )
{
//abctime clk = Abc_Clock();
Vec_Int_t * vClasses;
// derive shared AIG for the two networks
Gia_Man_t * pGia = Abc_NtkAigToGiaTwo( pNtks[0], pNtks[1] );
Gia_Man_t * pGia = Abc_NtkAigToGiaTwo( pNtks[0], pNtks[1], fByName );
if ( fVerbose )
printf( "Computing equivalences for networks \"%s\" and \"%s\" with conflict limit %d.\n", Abc_NtkName(pNtks[0]), Abc_NtkName(pNtks[1]), nConfs );
// compute equivalences in this AIG
......
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