Skip to content

Commit

Permalink
New command &odc to study observability don't-cares.
Browse files Browse the repository at this point in the history
  • Loading branch information
@alanminko
alanminko committed May 14, 2024
1 parent 66c7f67 commit 554da94
Show file tree
Hide file tree
Showing 2 changed files with 126 additions and 1 deletion.
59 changes: 59 additions & 0 deletions src/aig/gia/giaDup.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5823,6 +5823,65 @@ Gia_Man_t * Gia_ManImplFromBMiter( Gia_Man_t * p, int nPo, int nBInput )
return pNew;
}

/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManDupOdc( Gia_Man_t * p, int iObj, int fVerbose )
{
Vec_Int_t * vRoots = Vec_IntAlloc( 1 );
Vec_Int_t * vNodes = Vec_IntAlloc( 100 );
Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
Gia_Obj_t * pObj; int i, iRes = 0;
Vec_IntPush( vRoots, iObj );
Gia_ManStaticFanoutStart( p );
Gia_ManCollectTfo( p, vRoots, vNodes );
Gia_ManStaticFanoutStop( p );
Vec_IntSort(vNodes, 0);
Gia_ManForEachObjVecStart( vNodes, p, pObj, i, 1 ) {
if ( !Gia_ObjIsTravIdCurrent(p, Gia_ObjFanin0(pObj)) )
Vec_IntPushUnique( vSupp, Gia_ObjFaninId0p(p, pObj) );
if ( !Gia_ObjIsTravIdCurrent(p, Gia_ObjFanin1(pObj)) )
Vec_IntPushUnique( vSupp, Gia_ObjFaninId1p(p, pObj) );
}
Vec_IntSort(vSupp, 0);
if ( fVerbose ) Vec_IntPrint( vSupp );
if ( fVerbose ) Vec_IntPrint( vNodes );
Gia_Man_t * pTemp, * pNew = Gia_ManStart( 100 );
pNew->pName = Abc_UtilStrsav( "care" );
Gia_ManFillValue(p);
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachObjVec( vSupp, p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
Gia_ManHashStart(pNew);
Gia_ManObj(p, iObj)->Value = 0;
Gia_ManForEachObjVecStart( vNodes, p, pObj, i, 1 )
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManForEachCo( p, pObj, i )
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
pObj->Value = Gia_ObjFanin0Copy(pObj);
Gia_ManObj(p, iObj)->Value = 1;
Gia_ManForEachObjVecStart( vNodes, p, pObj, i, 1 )
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManForEachCo( p, pObj, i )
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
iRes = Gia_ManHashOr( pNew, iRes, Gia_ManHashXor(pNew, pObj->Value, Gia_ObjFanin0Copy(pObj)) );
Gia_ManAppendCo( pNew, iRes );
Vec_IntFree( vRoots );
Vec_IntFree( vNodes );
Vec_IntFree( vSupp );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;
}

////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
Expand Down
68 changes: 67 additions & 1 deletion src/base/abci/abc.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -606,6 +606,7 @@ static int Abc_CommandAbc9PutOnTop ( Abc_Frame_t * pAbc, int argc, cha
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_CommandAbc9GenCex ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Odc ( Abc_Frame_t * pAbc, int argc, char ** argv );

static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv );

Expand Down Expand Up @@ -1394,6 +1395,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&brecover", Abc_CommandAbc9BRecover, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&str_eco", Abc_CommandAbc9StrEco, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&gencex", Abc_CommandAbc9GenCex, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&odc", Abc_CommandAbc9Odc, 0 );

Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 );
{
Expand Down Expand Up @@ -52952,6 +52954,70 @@ int Abc_CommandAbc9GenCex( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}

/**Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

***********************************************************************/
int Abc_CommandAbc9Odc( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Gia_ManDupOdc( Gia_Man_t * p, int iObj, int fVerbose );
Gia_Man_t * pTemp;
int c, iNode = -1, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Nvh" ) ) != EOF )
{
switch ( c )
{
case 'N':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
iNode = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( iNode < 0 )
goto usage;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Odc(): There is no AIG.\n" );
return 0;
}
if ( !Gia_ObjIsAnd( Gia_ManObj(pAbc->pGia, iNode) ) )
{
Abc_Print( -1, "Abc_CommandAbc9Odc(): Object with ID %d is not an internal node.\n", iNode );
return 0;
}
pTemp = Gia_ManDupOdc( pAbc->pGia, iNode, fVerbose );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;

usage:
Abc_Print( -2, "usage: &odc [-N num] [-vh]\n" );
Abc_Print( -2, "\t generates the complement of the ODC for the node\n" );
Abc_Print( -2, "\t-N num : the node ID [default = undefined]\n" );
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %d]\n", fVerbose ? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}

/**Function*************************************************************

Synopsis []
Expand Down Expand Up @@ -53038,7 +53104,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
Gia_ManStop( pTemp );
return 0;
}
Abc_FrameUpdateGia( pAbc, Gia_ManPerformNewResub(pAbc->pGia, 100, 6, 1, 1) );
//Abc_FrameUpdateGia( pAbc, pNew );
// printf( "AIG in \"%s\" has the sum of output support sizes equal to %d.\n", pAbc->pGia->pSpec, Gia_ManSumTotalOfSupportSizes(pAbc->pGia) );
return 0;
usage:
Expand Down

0 comments on commit 554da94

Please sign in to comment.