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

&brecover done

This commit is contained in:
Allen Ho 2024-03-04 00:54:23 +08:00
parent a747f46292
commit bcf04fadb6
3 changed files with 287 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -1806,6 +1806,8 @@ extern void Bnd_ManFindBound( Gia_Man_t *p );
extern Gia_Man_t* Bnd_ManGenSpecOut( Gia_Man_t *p );
extern Gia_Man_t* Bnd_ManGenImplOut( Gia_Man_t *p );
extern Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPatch );
extern Gia_Man_t* Bnd_ManGenPatched1( Gia_Man_t *pOut, Gia_Man_t *pSpec );
extern Gia_Man_t* Bnd_ManGenPatched2( Gia_Man_t *p, Gia_Man_t *pPatch );
extern void Bnd_ManSetEqOut( int eq );
extern void Bnd_ManSetEqRes( int eq );
extern void Bnd_ManPrintStats();

111
src/aig/gia/giaBound.c
View File

@ -572,7 +572,7 @@ void Bnd_ManFindBound( Gia_Man_t * p )
{
if ( cnt < pBnd -> nBI )
{
Vec_IntPush( vBI, Gia_ObjId(p, pObj) );
Vec_IntPush( vBI, Gia_ObjId(p, Gia_ObjFanin0(pObj) ) );
}
else
{
@ -884,27 +884,32 @@ Gia_Man_t* Bnd_ManGenImplOut( Gia_Man_t* p )
return pNew;
}
void Bnd_AddNodeRec( Gia_Man_t *p, Gia_Man_t *pNew, Gia_Obj_t *pObj )
void Bnd_AddNodeRec( Gia_Man_t *p, Gia_Man_t *pNew, Gia_Obj_t *pObj, int fSkipStrash )
{
// TODO does this mean constant zero node?
if ( pObj -> Value != ~0 ) return;
for( int i = 0; i < Gia_ObjFaninNum(p, pObj); i++ )
{
Bnd_AddNodeRec( p, pNew, Gia_ObjFanin(pObj, i) );
Bnd_AddNodeRec( p, pNew, Gia_ObjFanin(pObj, i), fSkipStrash );
}
if ( Gia_ObjIsAnd(pObj) )
{
pObj -> Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
if ( fSkipStrash )
{
if ( Gia_ObjIsBuf(pObj) ) pObj -> Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
else pObj -> Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
else
{
pObj -> Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
}
else
{
if ( Gia_ObjIsCi(pObj) )
{
printf("Ci with value 0 encountered (id = %d)\n", Gia_ObjId(p, pObj) );
}
assert( Gia_ObjIsCo(pObj) );
// if ( Gia_ObjIsCi(pObj) ) printf("Ci with value ~0 encountered (id = %d)\n", Gia_ObjId(p, pObj) );
pObj -> Value = Gia_ObjFanin0Copy(pObj);
}
}
@ -963,7 +968,7 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat
for ( i = 0; i < Vec_IntSize( pBnd -> vEI_spec ); i++ )
{
pObj = Gia_ManCo(pOut, i + Gia_ManCoNum(pSpec) );
Bnd_AddNodeRec( pOut, pNew, pObj );
Bnd_AddNodeRec( pOut, pNew, pObj, 0 );
// set Spec EI
Gia_ManObj( pSpec, Vec_IntEntry(pBnd -> vEI_spec, i) ) -> Value = pObj -> Value;
@ -976,7 +981,7 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat
Vec_IntForEachEntry( pBnd -> vBI, id, i )
{
pObj = Gia_ManObj( pSpec, id );
Bnd_AddNodeRec( pSpec, pNew, pObj );
Bnd_AddNodeRec( pSpec, pNew, pObj, 0 );
// set patch bi
Gia_ManObj( pPatch, Vec_IntEntry( vBI_patch, i) ) -> Value = pObj -> Value;
@ -989,7 +994,7 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat
Vec_IntForEachEntry( vBO_patch, id, i )
{
pObj = Gia_ManObj( pPatch, id );
Bnd_AddNodeRec( pPatch, pNew, pObj );
Bnd_AddNodeRec( pPatch, pNew, pObj, 0 );
// set spec bo
Gia_ManObj( pSpec, Vec_IntEntry( pBnd -> vBO, i) ) -> Value = pObj -> Value;
@ -1002,7 +1007,7 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat
Vec_IntForEachEntry( pBnd -> vEO_spec, id, i )
{
pObj = Gia_ManObj( pSpec, id );
Bnd_AddNodeRec( pSpec, pNew, pObj );
Bnd_AddNodeRec( pSpec, pNew, pObj, 0 );
// set impl EO (PI)
Gia_ManCi( pOut, i + Gia_ManCiNum(pSpec) ) -> Value = pObj -> Value;
@ -1015,7 +1020,7 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat
for ( i = 0; i < Gia_ManCoNum(pSpec); i++ )
{
pObj = Gia_ManCo( pOut, i );
Bnd_AddNodeRec( pOut, pNew, pObj );
Bnd_AddNodeRec( pOut, pNew, pObj, 0 );
Gia_ManAppendCo( pNew, pObj->Value );
// printf(" %d",pObj -> Value);
}
@ -1036,7 +1041,87 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat
return pNew;
}
Gia_Man_t* Bnd_ManGenPatched1( Gia_Man_t *pOut, Gia_Man_t *pSpec )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, id;
pNew = Gia_ManStart( Gia_ManObjNum(pOut) + Gia_ManObjNum( pSpec ) );
pNew -> pName = ABC_ALLOC( char, strlen(pOut->pName)+3);
sprintf( pNew -> pName, "%s_p", pOut -> pName );
Gia_ManFillValue(pOut);
Gia_ManFillValue(pSpec);
Gia_ManConst0(pOut)->Value = 0;
Gia_ManConst0(pSpec)->Value = 0;
// add Impl (real) PI
for ( i = 0; i < Gia_ManCiNum(pSpec); i++ )
{
pObj = Gia_ManCi(pOut, i);
pObj -> Value = Gia_ManAppendCi( pNew );
}
// add Impl EI to CI
printf("adding EI to CI in Impl\n");
for ( i = 0; i < Vec_IntSize( pBnd -> vEI_spec ); i++ )
{
pObj = Gia_ManCo(pOut, i + Gia_ManCoNum(pSpec) );
Bnd_AddNodeRec( pOut, pNew, pObj, 1 );
// set Spec EI
Gia_ManObj( pSpec, Vec_IntEntry(pBnd -> vEI_spec, i) ) -> Value = pObj -> Value;
printf(" %d",pObj -> Value);
}
printf("\n");
// add Spec EO to EI
// add BI -> BO -> EO to maintain the order of bufs
Vec_IntForEachEntry( pBnd -> vBI, id, i )
{
pObj = Gia_ManObj( pSpec, id );
Bnd_AddNodeRec( pSpec, pNew, pObj, 1 );
}
Vec_IntForEachEntry( pBnd -> vBO, id, i )
{
pObj = Gia_ManObj( pSpec, id );
Bnd_AddNodeRec( pSpec, pNew, pObj, 1 );
}
Vec_IntForEachEntry( pBnd -> vEO_spec, id, i )
{
pObj = Gia_ManObj( pSpec, id );
Bnd_AddNodeRec( pSpec, pNew, pObj, 1 );
// set impl EO (PI)
Gia_ManCi( pOut, i + Gia_ManCiNum(pSpec) ) -> Value = pObj -> Value;
// printf(" %d",pObj -> Value);
}
// printf("\n");
// add Impl (real) PO to EO
// printf("adding CO to EO in Impl\n");
for ( i = 0; i < Gia_ManCoNum(pSpec); i++ )
{
pObj = Gia_ManCo( pOut, i );
Bnd_AddNodeRec( pOut, pNew, pObj, 1 );
Gia_ManAppendCo( pNew, pObj->Value );
// printf(" %d",pObj -> Value);
}
// printf("\n");
// clean up
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
pBnd -> nNode_patched = Gia_ManAndNum( pNew );
pBnd -> status = 3;
return pNew;
}

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

@ -599,6 +599,7 @@ static int Abc_CommandAbc9ProdAdd ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9AddFlop ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9BMiter ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9GenHie ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9BRecover ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9StrEco ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -1381,6 +1382,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&addflop", Abc_CommandAbc9AddFlop, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&bmiter", Abc_CommandAbc9BMiter, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&gen_hie", Abc_CommandAbc9GenHie, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&brecover", Abc_CommandAbc9BRecover, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&str_eco", Abc_CommandAbc9StrEco, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 );
@ -52092,6 +52094,191 @@ usage:
***********************************************************************/
extern Bnd_Man_t* pBnd;
int Abc_CommandAbc9BRecover( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
extern void Cec4_ManSetParams( Cec_ParFra_t * pPars );
extern Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose );
Gia_Man_t *pSpec, *pImpl_out = 0, *pSpec_out = 0, *pMiter, *pPatched, *pTemp, *pBmiter;
char * FileName = NULL;
FILE * pFile = NULL;
int c, fVerbose = 0, success = 1;
// params
Gps_Par_t Pars, * pPars = &Pars;
memset( pPars, 0, sizeof(Gps_Par_t) );
Cec_ParCec_t ParsCec, *pParsCec = &ParsCec;
Cec_ManCecSetDefaultParams( pParsCec );
Cec_ParFra_t ParsFra, *pParsFra = &ParsFra;
Cec4_ManSetParams( pParsFra );
pParsFra -> fBMiterInfo = 1;
// parse options
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
{
switch ( c )
{
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9BRecover(): There is no AIG.\n" );
return 0;
}
if ( argc != globalUtilOptind + 1 )
{
printf("%d\n", argc-globalUtilOptind);
Abc_Print( -1, "Abc_CommandAbc9BRecover(): AIG should be given on the command line.\n" );
return 0;
}
// read spec
FileName = argv[globalUtilOptind];
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
Abc_Print( -1, "Cannot open input file \"%s\". ", FileName );
if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", ".blif", ".pla", ".eqn", ".bench" )) )
Abc_Print( 1, "Did you mean \"%s\"?", FileName );
Abc_Print( 1, "\n" );
return 1;
}
fclose( pFile );
pSpec = Gia_AigerRead( FileName, 0, 1, 0 );
if ( pSpec == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9BRecover(): Cannot read the file name on the command line.\n" );
return 0;
}
if ( Gia_ManBufNum(pSpec) == 0 )
{
Abc_Print( -1, "Abc_CommandAbc9BRecover(): The given spec should be hierarchical.\n" );
Gia_ManStop(pSpec);
return 0;
}
// start boundary manager
pBnd = Bnd_ManStart( pSpec, pAbc->pGia );
// verify if spec eq impl
pMiter = Gia_ManMiter( pAbc->pGia, pSpec, 0, 1, 0, 0, 0 );
if ( !Cec_ManVerify( pMiter, pParsCec ) )
{
Abc_Print( -1, "Abc_CommandAbc9BRecover(): The given spec is not equivalent to current impl.\n" );
success = 0;
}
Gia_ManStop(pMiter);
// check boundary
if ( success )
{
if ( 0 == Bnd_ManCheckBound( pSpec ) )
{
Abc_Print( -1, "Abc_CommandAbc9BRecover(): The given spec has invalid boundary.\n" );
success = 0;
}
}
if ( success )
{
// create bmiter, run fraig, record mapping
pBmiter = Gia_ManBoundaryMiter( pSpec, pAbc->pGia, 0 );
pTemp = Cec4_ManSimulateTest( pBmiter, pParsFra );
Gia_ManStop(pBmiter);
Gia_ManStop(pTemp);
// find
Bnd_ManFindBound( pSpec );
// create spec_out and
pSpec_out = Bnd_ManGenSpecOut( pSpec );
if ( !pSpec_out ) success = 0;
pImpl_out = Bnd_ManGenImplOut( pAbc->pGia );
if ( !pImpl_out ) success = 0;
// Gia_AigerWrite( pSpec_out, "spec_out.aig", 0, 0, 0 );
// Gia_AigerWrite( pImpl_out, "impl_out.aig", 0, 0, 0 );
// Gia_ManPrintStats( pSpec_out, pPars );
// Gia_ManPrintStats( pImpl_out, pPars );
}
if ( success )
{
// check if spec_out and imnpl_out are equivalent
printf("Checking the equivalence of spec_out and impl_out\n");
pMiter = Gia_ManMiter( pSpec_out, pImpl_out, 0, 1, 0, 0, 0 );
Bnd_ManSetEqOut( Cec_ManVerify( pMiter, pParsCec ) );
Gia_ManStop( pMiter );
// generate patched impl
printf("Generating patched impl\n");
pPatched = Bnd_ManGenPatched1( pImpl_out, pSpec );
// // generate patched spec just for debugging
// printf("Generating patched spec\n");
// pTemp = Bnd_ManGenPatched( pSpec_out, pAbc->pGia, pPatch );
// printf("Checking the equivalence of patched spec and patched impl\n");
// pMiter = Gia_ManMiter( pTemp, pPatched, 0, 1, 0, 0, 0 );
// Cec_ManVerify( pMiter, pParsCec );
// Gia_ManStop( pMiter );
// printf("Checking the equivalence of patched spec and patch\n");
// pMiter = Gia_ManMiter( pTemp, pPatch, 0, 1, 0, 0, 0 );
// Cec_ManVerify( pMiter, pParsCec );
// Gia_ManStop( pMiter );
// Gia_ManStop( pTemp );
// check if patched is equiv to spec
printf("Checking the equivalence of patched impl and patch\n");
pMiter = Gia_ManMiter( pSpec, pPatched, 0, 1, 0, 0, 0 );
Bnd_ManSetEqRes( Cec_ManVerify( pMiter, pParsCec ) );
Gia_ManStop( pMiter );
}
Bnd_ManPrintStats();
Gia_ManStop( pSpec );
if ( pSpec_out ) Gia_ManStop( pSpec_out );
if ( pImpl_out ) Gia_ManStop( pImpl_out );
if ( success )
{
Abc_FrameUpdateGia( pAbc, pPatched );
}
Bnd_ManStop();
return 0;
usage:
Abc_Print( -2, "usage: &str_eco -I <biNum> [-vh] <impl> <patch>\n" );
Abc_Print( -2, "\t SAT-sweeping-based ECO\n" );
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\t<impl> : the implementation aig. (should be equivalent to spec)\n");
Abc_Print( -2, "\t<patch> : the modified spec. (should be a hierarchical AIG)\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
@ -52111,8 +52298,6 @@ int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv )
Cec4_ManSetParams( pParsFra );
pParsFra -> fBMiterInfo = 1;
// TODO: save return value and return at the end of the function
// parse options
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )