luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Adding new command 'dump_equiv'.

This commit is contained in:
Alan Mishchenko 2016-07-21 16:40:56 -07:00
parent aa3d8a65b4
commit bfe7333f41
13 changed files with 518 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abclib.dsp
View File

@ -263,6 +263,10 @@ SOURCE=.\src\base\abci\abcDress2.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcDress3.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcDsd.c
# End Source File
# Begin Source File

6
src/aig/gia/gia.h
View File

@ -175,6 +175,8 @@ struct Gia_Man_t_
Vec_Int_t * vUserFfIds; // numbers assigned to FFs by the user
Vec_Int_t * vCiNumsOrig; // original CI names
Vec_Int_t * vCoNumsOrig; // original CO names
Vec_Int_t * vIdsOrig; // original object IDs
Vec_Int_t * vIdsEquiv; // original object IDs proved equivalent
Vec_Int_t * vCofVars; // cofactoring variables
Vec_Vec_t * vClockDoms; // clock domains
Vec_Flt_t * vTiming; // arrival/required/slack
@ -1241,6 +1243,10 @@ extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset
extern Gia_Man_t * Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, int fVerbose );
extern Gia_Man_t * Gia_ManRemoveEnables( Gia_Man_t * p );
/*=== giaEquiv.c ==========================================================*/
extern void Gia_ManOrigIdsInit( Gia_Man_t * p );
extern void Gia_ManOrigIdsStart( Gia_Man_t * p );
extern void Gia_ManOrigIdsRemap( Gia_Man_t * p, Gia_Man_t * pNew );
extern Gia_Man_t * Gia_ManOrigIdsReduce( Gia_Man_t * p, Vec_Int_t * vPairs );
extern void Gia_ManEquivFixOutputPairs( Gia_Man_t * p );
extern int Gia_ManCheckTopoOrder( Gia_Man_t * p );
extern int * Gia_ManDeriveNexts( Gia_Man_t * p );

2
src/aig/gia/giaDup.c
View File

@ -1383,7 +1383,7 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
Gia_ManForEachCo( p, pObj, i )
Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
Gia_ManForEachCo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
pNew->nConstrs = p->nConstrs;
if ( p->pCexSeq )

142
src/aig/gia/giaEquiv.c
View File

@ -32,6 +32,143 @@ ABC_NAMESPACE_IMPL_START
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Manipulating original IDs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManOrigIdsInit( Gia_Man_t * p )
{
Vec_IntFreeP( &p->vIdsOrig );
p->vIdsOrig = Vec_IntStartNatural( Gia_ManObjNum(p) );
}
void Gia_ManOrigIdsStart( Gia_Man_t * p )
{
Vec_IntFreeP( &p->vIdsOrig );
p->vIdsOrig = Vec_IntStartFull( Gia_ManObjNum(p) );
}
void Gia_ManOrigIdsRemap( Gia_Man_t * p, Gia_Man_t * pNew )
{
Gia_Obj_t * pObj; int i;
if ( p->vIdsOrig == NULL )
return;
Gia_ManOrigIdsStart( pNew );
Vec_IntWriteEntry( pNew->vIdsOrig, 0, 0 );
Gia_ManForEachObj1( p, pObj, i )
if ( ~pObj->Value && Abc_Lit2Var(pObj->Value) && Vec_IntEntry(p->vIdsOrig, i) != -1 && Vec_IntEntry(pNew->vIdsOrig, Abc_Lit2Var(pObj->Value)) == -1 )
Vec_IntWriteEntry( pNew->vIdsOrig, Abc_Lit2Var(pObj->Value), Vec_IntEntry(p->vIdsOrig, i) );
Gia_ManForEachObj( pNew, pObj, i )
assert( Vec_IntEntry(pNew->vIdsOrig, i) >= 0 );
}
// input is a set of equivalent node pairs in any order
// output is the mapping of each node into the equiv node with the smallest ID
void Gia_ManOrigIdsRemapPairsInsert( Vec_Int_t * vMap, int One, int Two )
{
int Smo = One < Two ? One : Two;
int Big = One < Two ? Two : One;
assert( Smo != Big );
if ( Vec_IntEntry(vMap, Big) == -1 )
Vec_IntWriteEntry( vMap, Big, Smo );
else
Gia_ManOrigIdsRemapPairsInsert( vMap, Smo, Vec_IntEntry(vMap, Big) );
}
int Gia_ManOrigIdsRemapPairsExtract( Vec_Int_t * vMap, int One )
{
if ( Vec_IntEntry(vMap, One) == -1 )
return One;
return Gia_ManOrigIdsRemapPairsExtract( vMap, Vec_IntEntry(vMap, One) );
}
Vec_Int_t * Gia_ManOrigIdsRemapPairs( Vec_Int_t * vEquivPairs, int nObjs )
{
Vec_Int_t * vMapResult;
Vec_Int_t * vMap2Smaller;
int i, One, Two;
// map bigger into smaller one
vMap2Smaller = Vec_IntStartFull( nObjs );
Vec_IntForEachEntryDouble( vEquivPairs, One, Two, i )
Gia_ManOrigIdsRemapPairsInsert( vMap2Smaller, One, Two );
// collect results in the topo order
vMapResult = Vec_IntStartFull( nObjs );
Vec_IntForEachEntry( vMap2Smaller, One, i )
if ( One >= 0 )
Vec_IntWriteEntry( vMapResult, i, Gia_ManOrigIdsRemapPairsExtract(vMap2Smaller, One) );
Vec_IntFree( vMap2Smaller );
return vMapResult;
}
// remap the AIG using the equivalent pairs proved
// returns the reduced AIG and the equivalence classes of the original AIG
Gia_Man_t * Gia_ManOrigIdsReduce( Gia_Man_t * p, Vec_Int_t * vPairs )
{
Gia_Man_t * pNew = NULL;
Gia_Obj_t * pObj, * pRepr; int i;
Vec_Int_t * vMap = Gia_ManOrigIdsRemapPairs( vPairs, Gia_ManObjNum(p) );
Gia_ManSetPhase( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManFillValue(p);
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
Gia_ManHashAlloc( pNew );
Gia_ManForEachAnd( p, pObj, i )
{
if ( Vec_IntEntry(vMap, i) == -1 )
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
else
{
pRepr = Gia_ManObj( p, Vec_IntEntry(vMap, i) );
pObj->Value = Abc_LitNotCond( pRepr->Value, pRepr->fPhase ^ pObj->fPhase );
}
}
Gia_ManHashStop( pNew );
Gia_ManForEachCo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Vec_IntFree( vMap );
// compute equivalences
assert( !p->pReprs && !p->pNexts );
p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
for ( i = 0; i < Gia_ManObjNum(p); i++ )
Gia_ObjSetRepr( p, i, GIA_VOID );
Gia_ManFillValue(pNew);
Gia_ManForEachAnd( p, pObj, i )
{
int iRepr = Abc_Lit2Var(pObj->Value);
if ( iRepr == 0 )
{
Gia_ObjSetRepr( p, i, 0 );
continue;
}
pRepr = Gia_ManObj( pNew, iRepr );
if ( !~pRepr->Value ) // first time
{
pRepr->Value = i;
continue;
}
// add equivalence
Gia_ObjSetRepr( p, i, pRepr->Value );
}
p->pNexts = Gia_ManDeriveNexts( p );
return pNew;
}
Gia_Man_t * Gia_ManOrigIdsReduceTest( Gia_Man_t * p, Vec_Int_t * vPairs )
{
Gia_Man_t * pTemp, * pNew = Gia_ManOrigIdsReduce( p, vPairs );
Gia_ManPrintStats( p, NULL );
Gia_ManPrintStats( pNew, NULL );
//Gia_ManStop( pNew );
// cleanup the resulting one
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;
}
/**Function*************************************************************
Synopsis [Returns 1 if AIG is not in the required topo order.]
@ -460,7 +597,7 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fS
Gia_ManForEachCo( p, pObj, i )
Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll, fDualOut );
Gia_ManForEachCo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManHashStop( pNew );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
return pNew;
@ -641,6 +778,7 @@ Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs
pNew = Gia_ManEquivReduce( p, 0, 0, 0, 0 );
if ( pNew == NULL )
return NULL;
Gia_ManOrigIdsRemap( p, pNew );
if ( fMiterPairs )
Gia_ManEquivFixOutputPairs( pNew );
if ( fSeq )
@ -649,9 +787,11 @@ Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs
Gia_ManCombMarkUsed( pNew );
Gia_ManEquivUpdatePointers( p, pNew );
pFinal = Gia_ManDupMarked( pNew );
Gia_ManOrigIdsRemap( pNew, pFinal );
Gia_ManEquivDeriveReprs( p, pNew, pFinal );
Gia_ManStop( pNew );
pFinal = Gia_ManEquivRemapDfs( pNew = pFinal );
Gia_ManOrigIdsRemap( pNew, pFinal );
Gia_ManStop( pNew );
return pFinal;
}

2
src/aig/gia/giaMan.c
View File

@ -93,6 +93,8 @@ void Gia_ManStop( Gia_Man_t * p )
Vec_FltFreeP( &p->vTiming );
Vec_VecFreeP( &p->vClockDoms );
Vec_IntFreeP( &p->vCofVars );
Vec_IntFreeP( &p->vIdsOrig );
Vec_IntFreeP( &p->vIdsEquiv );
Vec_IntFreeP( &p->vLutConfigs );
Vec_IntFreeP( &p->vEdgeDelay );
Vec_IntFreeP( &p->vEdgeDelayR );

11
src/base/abc/abcFunc.c
View File

@ -980,7 +980,7 @@ Gia_Man_t * Abc_NtkAigToGia( Abc_Ntk_t * p, int fGiaSimple )
Vec_Int_t * vMapping = NULL;
Vec_Ptr_t * vNodes;
Abc_Obj_t * pNode, * pFanin;
int i, k, nObjs;
int i, k, nObjs, iGiaObj;
assert( Abc_NtkIsAigLogic(p) );
pHopMan = (Hop_Man_t *)p->pManFunc;
// create new manager
@ -1016,15 +1016,14 @@ Gia_Man_t * Abc_NtkAigToGia( Abc_Ntk_t * p, int fGiaSimple )
{
assert( Abc_ObjFaninNum(pNode) <= Hop_ManPiNum(pHopMan) );
Abc_ConvertAigToGia( pNew, pHopObj );
if ( !Gia_ObjIsAnd(Gia_ManObj(pNew, Abc_Lit2Var(pHopObj->iData))) )
continue;
if ( vMapping && !Vec_IntEntry(vMapping, Abc_Lit2Var(pHopObj->iData)) )
iGiaObj = Abc_Lit2Var( pHopObj->iData );
if ( vMapping && Gia_ObjIsAnd(Gia_ManObj(pNew, iGiaObj)) && !Vec_IntEntry(vMapping, iGiaObj) )
{
Vec_IntWriteEntry( vMapping, Abc_Lit2Var(pHopObj->iData), Vec_IntSize(vMapping) );
Vec_IntWriteEntry( vMapping, iGiaObj, Vec_IntSize(vMapping) );
Vec_IntPush( vMapping, Abc_ObjFaninNum(pNode) );
Abc_ObjForEachFanin( pNode, pFanin, k )
Vec_IntPush( vMapping, Abc_Lit2Var(pFanin->iTemp) );
Vec_IntPush( vMapping, Abc_Lit2Var(pHopObj->iData) );
Vec_IntPush( vMapping, iGiaObj );
}
}
pNode->iTemp = Abc_LitNotCond( pHopObj->iData, Hop_IsComplement( (Hop_Obj_t *)pNode->pData ) );

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

@ -233,6 +233,7 @@ static int Abc_CommandFraigRestore ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandFraigClean ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFraigSweep ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFraigDress ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDumpEquiv ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRecStart3 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRecStop3 ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -869,6 +870,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Fraiging", "fraig_clean", Abc_CommandFraigClean, 0 );
Cmd_CommandAdd( pAbc, "Fraiging", "fraig_sweep", Abc_CommandFraigSweep, 1 );
Cmd_CommandAdd( pAbc, "Fraiging", "dress", Abc_CommandFraigDress, 1 );
Cmd_CommandAdd( pAbc, "Fraiging", "dump_equiv", Abc_CommandDumpEquiv, 0 );
Cmd_CommandAdd( pAbc, "Choicing", "rec_start3", Abc_CommandRecStart3, 0 );
Cmd_CommandAdd( pAbc, "Choicing", "rec_stop3", Abc_CommandRecStop3, 0 );
@ -14801,6 +14803,81 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
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 );
FILE * pFile = NULL;
Abc_Ntk_t * pNtks[2] = {NULL};
char * pFileName[2], * pFileNameOut;
int c, nConfs = 1000, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Cvh" ) ) != EOF )
{
switch ( c )
{
case 'C':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
nConfs = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nConfs < 0 )
goto usage;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( argc != globalUtilOptind + 3 )
{
Abc_Print( -1, "Expecting three file names on the command line.\n" );
goto usage;
}
pFileName[0] = argv[globalUtilOptind];
pFileName[1] = argv[globalUtilOptind+1];
pFileNameOut = argv[globalUtilOptind+2];
for ( c = 0; c < 2; c++ )
{
pNtks[c] = Io_Read( pFileName[c], Io_ReadFileType(pFileName[c]), 1, 0 );
if ( pNtks[c] == NULL )
goto usage;
Abc_NtkToAig( pNtks[c] );
}
Abc_NtkDumpEquiv( pNtks, pFileNameOut, nConfs, 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, "\t computes equivalence classes of nodes in <file1> and <file2>\n" );
Abc_Print( -2, "\t-C num : the maximum number of conflicts at each node [default = %d]\n", nConfs );
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" );
Abc_Print( -2, "\t<file2> : second network whose nodes are considered\n" );
Abc_Print( -2, "\t<file_dump_equiv> : text file with node equivalence classes\n" );
return 1;
}
/**Function*************************************************************
Synopsis []
@ -27022,7 +27099,7 @@ usage:
Abc_Print( -2, "\t converts the current network into GIA and moves it to the &-space\n" );
Abc_Print( -2, "\t (if the network is a sequential logic network, normalizes the flops\n" );
Abc_Print( -2, "\t to have const-0 initial values, equivalent to \"undc; st; zero\")\n" );
Abc_Print( -2, "\t-c : toggles allowing simple GIA to be improved [default = %s]\n", fGiaSimple? "yes": "no" );
Abc_Print( -2, "\t-c : toggles allowing simple GIA to be imported [default = %s]\n", fGiaSimple? "yes": "no" );
Abc_Print( -2, "\t-m : toggles preserving the current mapping [default = %s]\n", fMapped? "yes": "no" );
Abc_Print( -2, "\t-n : toggles saving CI/CO names of the AIG [default = %s]\n", fNames? "yes": "no" );
Abc_Print( -2, "\t-v : toggles additional verbose output [default = %s]\n", fVerbose? "yes": "no" );

259
src/base/abci/abcDress3.c Normal file
View File

@ -0,0 +1,259 @@
/**CFile****************************************************************
FileName [abcDress3.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Network and node package.]
Synopsis [Transfers names from one netlist to the other.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: abcDress3.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "base/abc/abc.h"
#include "base/io/ioAbc.h"
#include "proof/cec/cec.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Compute equivalence classes of nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkComputeGiaEquivs( Gia_Man_t * pGia, int nConfs, int fVerbose )
{
Gia_Man_t * pTemp;
Cec_ParFra_t ParsFra, * pPars = &ParsFra;
Cec_ManFraSetDefaultParams( pPars );
pPars->fUseOrigIds = 1;
pPars->fSatSweeping = 1;
pPars->nBTLimit = nConfs;
pPars->fVerbose = fVerbose;
pTemp = Cec_ManSatSweeping( pGia, pPars, 0 );
Gia_ManStop( pTemp );
pTemp = Gia_ManOrigIdsReduce( pGia, pGia->vIdsEquiv );
Gia_ManStop( pTemp );
}
/**Function*************************************************************
Synopsis [Add logic from pNtk to the AIG manager p.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkAigToGiaOne( Gia_Man_t * p, Abc_Ntk_t * pNtk )
{
extern int Abc_ConvertAigToGia( Gia_Man_t * p, Hop_Obj_t * pRoot );
Hop_Man_t * pHopMan;
Hop_Obj_t * pHopObj;
Vec_Ptr_t * vNodes;
Abc_Obj_t * pNode, * pFanin;
int i, k;
assert( Abc_NtkIsAigLogic(pNtk) );
pHopMan = (Hop_Man_t *)pNtk->pManFunc;
Hop_ManConst1(pHopMan)->iData = 1;
// image primary inputs
Abc_NtkCleanCopy( pNtk );
Abc_NtkForEachCi( pNtk, pNode, i )
pNode->iTemp = Gia_ManCiLit(p, i);
// iterate through nodes used in the mapping
vNodes = Abc_NtkDfs( pNtk, 0 );
Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
{
Abc_ObjForEachFanin( pNode, pFanin, k )
Hop_ManPi(pHopMan, k)->iData = pFanin->iTemp;
pHopObj = Hop_Regular( (Hop_Obj_t *)pNode->pData );
assert( Abc_ObjFaninNum(pNode) <= Hop_ManPiNum(pHopMan) );
if ( Hop_DagSize(pHopObj) > 0 )
Abc_ConvertAigToGia( p, pHopObj );
pNode->iTemp = Abc_LitNotCond( pHopObj->iData, Hop_IsComplement( (Hop_Obj_t *)pNode->pData ) );
}
Vec_PtrFree( vNodes );
// create primary outputs
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 * p;
Gia_Obj_t * pObj;
Abc_Obj_t * pNode;
int i;
assert( Abc_NtkIsAigLogic(pNtk1) );
assert( Abc_NtkIsAigLogic(pNtk2) );
// 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 )
Gia_ManAppendCi(p);
// add logic
Gia_ManHashAlloc( p );
Abc_NtkAigToGiaOne( p, pNtk1 );
Abc_NtkAigToGiaOne( p, pNtk2 );
Gia_ManHashStop( p );
// add extra POs to dangling nodes
Gia_ManCreateValueRefs( p );
Gia_ManForEachAnd( p, pObj, i )
if ( pObj->Value == 0 )
Gia_ManAppendCo( p, Abc_Var2Lit(i, 0) );
return p;
}
/**Function*************************************************************
Synopsis [Collect equivalence class information.]
Description [Each class is represented as follows:
<num_entries><entry1><entry2>...<entryN>
where <entry> is nodeId with 1-bit for complement and 1-bit for network.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Abc_NtkCollectAddOne( int iNtk, int iObj, int iGiaLit, Gia_Man_t * pGia, Vec_Int_t * vGia2Cla, Vec_Int_t * vNexts[2] )
{
int iRepr = Gia_ObjReprSelf( pGia, Abc_Lit2Var(iGiaLit) );
int Compl = Abc_LitIsCompl(iGiaLit) ^ Gia_ObjPhase(Gia_ManObj(pGia, iRepr)) ^ Gia_ObjPhase(Gia_ManObj(pGia, Abc_Lit2Var(iGiaLit)));
int Added = Abc_Var2Lit( Abc_Var2Lit(iObj, Compl), iNtk );
int Entry = Vec_IntEntry( vGia2Cla, iRepr );
Vec_IntWriteEntry( vNexts[iNtk], iObj, Entry );
Vec_IntWriteEntry( vGia2Cla, iRepr, Added );
}
Vec_Int_t * Abc_NtkCollectEquivClasses( Abc_Ntk_t * pNtks[2], Gia_Man_t * pGia )
{
Vec_Int_t * vClass = Vec_IntAlloc( 100 );
Vec_Int_t * vClasses = Vec_IntAlloc( 1000 );
Vec_Int_t * vGia2Cla = Vec_IntStartFull( Gia_ManObjNum(pGia) ); // mapping objId into classId
Vec_Int_t * vNexts[2] = { Vec_IntStartFull(Abc_NtkObjNumMax(pNtks[0])), Vec_IntStartFull(Abc_NtkObjNumMax(pNtks[1])) };
Abc_Obj_t * pObj;
int n, i, k, Entry, fCompl;
Abc_NtkForEachCi( pNtks[0], pObj, i )
Abc_NtkCollectAddOne( 0, Abc_ObjId(pObj), pObj->iTemp, pGia, vGia2Cla, vNexts );
for ( n = 0; n < 2; n++ )
Abc_NtkForEachNode( pNtks[n], pObj, i )
Abc_NtkCollectAddOne( n, Abc_ObjId(pObj), pObj->iTemp, pGia, vGia2Cla, vNexts );
Vec_IntForEachEntry( vGia2Cla, Entry, i )
{
Vec_IntClear( vClass );
for ( ; Entry >= 0; Entry = Vec_IntEntry(vNexts[Entry&1], Entry>>2) )
Vec_IntPush( vClass, Entry );
if ( Vec_IntSize(vClass) < 2 )
continue;
Vec_IntReverseOrder( vClass );
fCompl = 2 & Vec_IntEntry( vClass, 0 );
Vec_IntForEachEntry( vClass, Entry, k )
Vec_IntWriteEntry( vClass, k, Entry ^ fCompl );
Vec_IntPush( vClasses, Vec_IntSize(vClass) );
Vec_IntAppend( vClasses, vClass );
}
Vec_IntFree( vGia2Cla );
Vec_IntFree( vNexts[0] );
Vec_IntFree( vNexts[1] );
Vec_IntFree( vClass );
return vClasses;
}
/**Function*************************************************************
Synopsis [Write the output file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkDumpEquivFile( char * pFileName, Vec_Int_t * vClasses, Abc_Ntk_t * pNtks[2] )
{
int i, c, k, Entry;
FILE * pFile = fopen( pFileName, "wb" );
if ( pFile == NULL ) { printf( "Cannot open file %s for writing.\n", pFileName ); return; }
fprintf( pFile, "# Node equivalences computed by ABC for networks \"%s\" and \"%s\" on %s\n\n", Abc_NtkName(pNtks[0]), Abc_NtkName(pNtks[1]), Extra_TimeStamp() );
for ( i = c = 0; i < Vec_IntSize(vClasses); c++, i += 1 + Vec_IntEntry(vClasses, i) )
{
Vec_IntForEachEntryStartStop( vClasses, Entry, k, i + 1, i + 1 + Vec_IntEntry(vClasses, i) )
{
Abc_Ntk_t * pNtk = pNtks[Entry & 1];
char * pObjName = Abc_ObjName( Abc_NtkObj(pNtk, Entry>>2) );
fprintf( pFile, "%d:%s:%s%s\n", c+1, Abc_NtkName(pNtk), (Entry&2) ? "NOT:":"", pObjName );
}
fprintf( pFile, "\n" );
}
fclose( pFile );
}
/**Function*************************************************************
Synopsis [Compute and dump equivalent name classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkDumpEquiv( Abc_Ntk_t * pNtks[2], char * pFileName, int nConfs, 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] );
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
Abc_NtkComputeGiaEquivs( pGia, nConfs, fVerbose );
//if ( fVerbose )
// Abc_PrintTime( 1, "Equivalence computation time", Abc_Clock() - clk );
if ( fVerbose )
Gia_ManPrintStats( pGia, NULL );
// collect equivalence class information
vClasses = Abc_NtkCollectEquivClasses( pNtks, pGia );
Gia_ManStop( pGia );
// dump information into the output file
Abc_NtkDumpEquivFile( pFileName, vClasses, pNtks );
Vec_IntFree( vClasses );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

1
src/base/abci/module.make
View File

@ -15,6 +15,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcDetect.c \
src/base/abci/abcDress.c \
src/base/abci/abcDress2.c \
src/base/abci/abcDress3.c \
src/base/abci/abcDsd.c \
src/base/abci/abcExact.c \
src/base/abci/abcExtract.c \

1
src/proof/cec/cec.h
View File

@ -108,6 +108,7 @@ struct Cec_ParFra_t_
int fColorDiff; // miter with separate outputs
int fSatSweeping; // enable SAT sweeping
int fRunCSat; // enable another solver
int fUseOrigIds; // enable recording of original IDs
int fVeryVerbose; // verbose stats
int fVerbose; // verbose stats
int iOutFail; // the failed output

10
src/proof/cec/cecCore.c
View File

@ -236,7 +236,7 @@ Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
Gia_Man_t * pNew;
Cec_ManPat_t * pPat;
pPat = Cec_ManPatStart();
Cec_ManSatSolve( pPat, pAig, pPars );
Cec_ManSatSolve( pPat, pAig, pPars, NULL, NULL, NULL );
// pNew = Gia_ManDupDfsSkip( pAig );
pNew = Gia_ManDup( pAig );
Cec_ManPatStop( pPat );
@ -351,6 +351,12 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars, int fSil
pIni = Gia_ManDup(pAig);
pIni->pReprs = pAig->pReprs; pAig->pReprs = NULL;
pIni->pNexts = pAig->pNexts; pAig->pNexts = NULL;
if ( pPars->fUseOrigIds )
{
Gia_ManOrigIdsInit( pIni );
Vec_IntFreeP( &pAig->vIdsEquiv );
pAig->vIdsEquiv = Vec_IntAlloc( 1000 );
}
// prepare the managers
// SAT sweeping
@ -429,7 +435,7 @@ clk = Abc_Clock();
if ( pPars->fRunCSat )
Cec_ManSatSolveCSat( pPat, pSrm, pParsSat );
else
Cec_ManSatSolve( pPat, pSrm, pParsSat );
Cec_ManSatSolve( pPat, pSrm, pParsSat, p->pAig->vIdsOrig, p->vXorNodes, pAig->vIdsEquiv );
p->timeSat += Abc_Clock() - clk;
if ( Cec_ManFraClassesUpdate( p, pSim, pPat, pSrm ) )
{

2
src/proof/cec/cecInt.h
View File

@ -201,7 +201,7 @@ extern int Cec_ManCountNonConstOutputs( Gia_Man_t * pAig );
extern int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig );
/*=== cecSolve.c ============================================================*/
extern int Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pObj );
extern void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars );
extern void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Int_t * vIdsOrig, Vec_Int_t * vMiterPairs, Vec_Int_t * vEquivPairs );
extern void Cec_ManSatSolveCSat( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars );
extern Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats );
extern Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Str_t ** pvStatus );

12
src/proof/cec/cecSolve.c
View File

@ -673,7 +673,7 @@ p->timeSatUndec += Abc_Clock() - clk;
SeeAlso []
***********************************************************************/
void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars )
void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Int_t * vIdsOrig, Vec_Int_t * vMiterPairs, Vec_Int_t * vEquivPairs )
{
Bar_Progress_t * pProgress = NULL;
Cec_ManSat_t * p;
@ -706,6 +706,16 @@ clk2 = Abc_Clock();
status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) );
pObj->fMark0 = (status == 0);
pObj->fMark1 = (status == 1);
if ( status == 1 && vIdsOrig )
{
int iObj1 = Vec_IntEntry(vMiterPairs, 2*i);
int iObj2 = Vec_IntEntry(vMiterPairs, 2*i+1);
int OrigId1 = Vec_IntEntry(vIdsOrig, iObj1);
int OrigId2 = Vec_IntEntry(vIdsOrig, iObj2);
assert( OrigId1 >= 0 && OrigId2 >= 0 );
Vec_IntPushTwo( vEquivPairs, OrigId1, OrigId2 );
}
/*
if ( status == -1 )
{