From c7b331efcf42c94450d7590eeb0c71c525569c11 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 6 Jul 2008 08:01:00 -0700 Subject: Version abc80706 --- src/base/abci/abc.c | 246 ++++++++++++++++++++++++++++++++++++++++++++++ src/base/abci/abcSense.c | 208 +++++++++++++++++++++++++++++++++++++++ src/base/abci/module.make | 1 + 3 files changed, 455 insertions(+) create mode 100644 src/base/abci/abcSense.c (limited to 'src/base') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 2c34ed67..4fed39ab 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -123,6 +123,7 @@ static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandQuaVar ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandQuaRel ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandQuaReach ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSenseInput ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandIStrash ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandICut ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -228,6 +229,7 @@ static int Abc_CommandAbc8Mfs ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandAbc8Lutpack ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc8Balance ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc8Speedup ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8Merge ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc8Fraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc8Scl ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -380,6 +382,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "qvar", Abc_CommandQuaVar, 1 ); Cmd_CommandAdd( pAbc, "Various", "qrel", Abc_CommandQuaRel, 1 ); Cmd_CommandAdd( pAbc, "Various", "qreach", Abc_CommandQuaReach, 1 ); + Cmd_CommandAdd( pAbc, "Various", "senseinput", Abc_CommandSenseInput, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "istrash", Abc_CommandIStrash, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "icut", Abc_CommandICut, 0 ); @@ -480,6 +483,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC8", "*lp", Abc_CommandAbc8Lutpack, 0 ); Cmd_CommandAdd( pAbc, "ABC8", "*b", Abc_CommandAbc8Balance, 0 ); Cmd_CommandAdd( pAbc, "ABC8", "*speedup", Abc_CommandAbc8Speedup, 0 ); + Cmd_CommandAdd( pAbc, "ABC8", "*merge", Abc_CommandAbc8Merge, 0 ); Cmd_CommandAdd( pAbc, "ABC8", "*fraig", Abc_CommandAbc8Fraig, 0 ); Cmd_CommandAdd( pAbc, "ABC8", "*scl", Abc_CommandAbc8Scl, 0 ); @@ -8096,6 +8100,98 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandSenseInput( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + Vec_Int_t * vResult; + int c, nConfLim, fVerbose; + + extern Vec_Int_t * Abc_NtkSensitivity( Abc_Ntk_t * pNtk, int nConfLim, int fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nConfLim = 1000; + fVerbose = 1; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Cvh" ) ) != EOF ) + { + switch ( c ) + { + case 'C': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nConfLim = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nConfLim < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( Abc_NtkGetChoiceNum( pNtk ) ) + { + fprintf( pErr, "This command cannot be applied to an AIG with choice nodes.\n" ); + return 1; + } + if ( !Abc_NtkIsComb(pNtk) ) + { + fprintf( pErr, "This command works only for combinational transition relations.\n" ); + return 1; + } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for strashed networks.\n" ); + return 1; + } + if ( Abc_NtkPoNum(pNtk) < 2 ) + { + fprintf( pErr, "The network should have at least two outputs.\n" ); + return 1; + } + + vResult = Abc_NtkSensitivity( pNtk, nConfLim, fVerbose ); + Vec_IntFree( vResult ); + return 0; + +usage: + fprintf( pErr, "usage: senseinput [-C num] [-vh]\n" ); + fprintf( pErr, "\t computes sensitivity of POs to PIs under constaint\n" ); + fprintf( pErr, "\t constraint should be represented as the last PO" ); + fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nConfLim ); + fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* @@ -17224,6 +17320,156 @@ usage: return 1; } + +//#include "nwk.h" + +// the LUT merging parameters +typedef struct Nwk_LMPars_t_ Nwk_LMPars_t; +struct Nwk_LMPars_t_ +{ + int nMaxLutSize; // the max LUT size for merging (N=5) + int nMaxSuppSize; // the max total support size after merging (S=5) + int nMaxDistance; // the max number of nodes separating LUTs + int nMaxLevelDiff; // the max difference in levels + int nMaxFanout; // the max number of fanouts to traverse + int fUseTfiTfo; // enables the use of TFO/TFO nodes as candidates + int fVeryVerbose; // enables additional verbose output + int fVerbose; // enables verbose output +}; + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc8Merge( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Nwk_LMPars_t Pars, * pPars = &Pars; + Vec_Int_t * vResult; + int c; + int fUseLutLib = 0; + int Percentage = 100; + int Degree = 5; + int fVerbose = 0; + int fVeryVerbose = 0; + extern Vec_Int_t * Nwk_ManLutMerge( void * pNtk, Nwk_LMPars_t * pPars ); + + // set defaults + memset( pPars, 0, sizeof(Nwk_LMPars_t) ); + pPars->nMaxLutSize = 5; // the max LUT size for merging (N=5) + pPars->nMaxSuppSize = 5; // the max total support size after merging (S=5) + pPars->nMaxDistance = 3; // the max number of nodes separating LUTs + pPars->nMaxLevelDiff = 2; // the max difference in levels + pPars->nMaxFanout = 100; // the max number of fanouts to traverse + pPars->fUseTfiTfo = 0; // enables the use of TFO/TFO nodes as candidates + pPars->fVeryVerbose = 0; // enables additional verbose output + pPars->fVerbose = 1; // enables verbose output + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "NSDLFcvwh" ) ) != EOF ) + { + switch ( c ) + { + case 'N': + if ( globalUtilOptind >= argc ) + { + fprintf( stdout, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nMaxLutSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nMaxLutSize < 2 ) + goto usage; + break; + case 'S': + if ( globalUtilOptind >= argc ) + { + fprintf( stdout, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nMaxSuppSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nMaxSuppSize < 2 ) + goto usage; + break; + case 'D': + if ( globalUtilOptind >= argc ) + { + fprintf( stdout, "Command line switch \"-D\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nMaxDistance = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nMaxDistance < 2 ) + goto usage; + break; + case 'L': + if ( globalUtilOptind >= argc ) + { + fprintf( stdout, "Command line switch \"-L\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nMaxLevelDiff = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nMaxLevelDiff < 2 ) + goto usage; + break; + case 'F': + if ( globalUtilOptind >= argc ) + { + fprintf( stdout, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nMaxFanout = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nMaxFanout < 2 ) + goto usage; + break; + case 'c': + pPars->fUseTfiTfo ^= 1; + break; + case 'w': + pPars->fVeryVerbose ^= 1; + break; + case 'v': + pPars->fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pAbc8Nwk == NULL ) + { + printf( "Abc_CommandAbc8Speedup(): There is no mapped network to merge LUTs.\n" ); + return 1; + } + + vResult = Nwk_ManLutMerge( pAbc->pAbc8Nwk, pPars ); + Vec_IntFree( vResult ); + return 0; + +usage: + fprintf( stdout, "usage: *merge [-NSDLF num] [-cwvh]\n" ); + fprintf( stdout, "\t creates pairs of topologically-related LUTs\n" ); + fprintf( stdout, "\t-N : the max LUT size for merging (1 < num) [default = %d]\n", pPars->nMaxLutSize ); + fprintf( stdout, "\t-S : the max total support size after merging (1 < num) [default = %d]\n", pPars->nMaxSuppSize ); + fprintf( stdout, "\t-D : the max distance in terms of LUTs (0 < num) [default = %d]\n", pPars->nMaxDistance ); + fprintf( stdout, "\t-L : the max difference in levels (0 <= num) [default = %d]\n", pPars->nMaxLevelDiff ); + fprintf( stdout, "\t-F : the max number of fanouts to stop traversal (0 < num) [default = %d]\n", pPars->nMaxFanout ); + fprintf( stdout, "\t-c : toggle the use of TFI/TFO nodes as candidates [default = %s]\n", pPars->fUseTfiTfo? "yes" : "no" ); + fprintf( stdout, "\t-w : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); + fprintf( stdout, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" ); + fprintf( stdout, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/base/abci/abcSense.c b/src/base/abci/abcSense.c new file mode 100644 index 00000000..f3d71a54 --- /dev/null +++ b/src/base/abci/abcSense.c @@ -0,0 +1,208 @@ +/**CFile**************************************************************** + + FileName [abcSense.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abc_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "fraig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Copies the topmost levels of the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_NtkSensitivityMiter_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode ) +{ + assert( !Abc_ObjIsComplement(pNode) ); + if ( pNode->pCopy ) + return pNode->pCopy; + Abc_NtkSensitivityMiter_rec( pNtkNew, Abc_ObjFanin0(pNode) ); + Abc_NtkSensitivityMiter_rec( pNtkNew, Abc_ObjFanin1(pNode) ); + return pNode->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) ); +} + +/**Function************************************************************* + + Synopsis [Creates miter for the sensitivity analysis.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkSensitivityMiter( Abc_Ntk_t * pNtk, int iVar ) +{ + Abc_Ntk_t * pMiter; + Vec_Ptr_t * vNodes; + Abc_Obj_t * pObj, * pNext, * pFanin, * pOutput, * pObjNew; + int i; + assert( Abc_NtkIsStrash(pNtk) ); + assert( iVar < Abc_NtkCiNum(pNtk) ); + + // duplicate the network + pMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); + pMiter->pName = Extra_UtilStrsav(pNtk->pName); + pMiter->pSpec = Extra_UtilStrsav(pNtk->pSpec); + + // assign the PIs + Abc_NtkCleanCopy( pNtk ); + Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pMiter); + Abc_AigConst1(pNtk)->pData = Abc_AigConst1(pMiter); + Abc_NtkForEachCi( pNtk, pObj, i ) + pObj->pCopy = pObj->pData = Abc_NtkCreatePi( pMiter ); + Abc_NtkAddDummyPiNames( pMiter ); + + // assign the cofactors of the CI node to be constants + pObj = Abc_NtkCi( pNtk, iVar ); + pObj->pCopy = Abc_ObjNot( Abc_AigConst1(pMiter) ); + pObj->pData = Abc_AigConst1(pMiter); + + // collect the internal nodes + vNodes = Abc_NtkDfsReverseNodes( pNtk, &pObj, 1 ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + for ( pNext = pObj? pObj->pCopy : pObj; pObj; pObj = pNext, pNext = pObj? pObj->pCopy : pObj ) + { + pFanin = Abc_ObjFanin0(pObj); + if ( !Abc_NodeIsTravIdCurrent(pFanin) ) + pFanin->pData = Abc_NtkSensitivityMiter_rec( pMiter, pFanin ); + pFanin = Abc_ObjFanin1(pObj); + if ( !Abc_NodeIsTravIdCurrent(pFanin) ) + pFanin->pData = Abc_NtkSensitivityMiter_rec( pMiter, pFanin ); + pObj->pCopy = Abc_AigAnd( pMiter->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); + pObj->pData = Abc_AigAnd( pMiter->pManFunc, Abc_ObjChild0Data(pObj), Abc_ObjChild1Data(pObj) ); + } + } + Vec_PtrFree( vNodes ); + + // update the affected COs + pOutput = Abc_ObjNot( Abc_AigConst1(pMiter) ); + Abc_NtkForEachCo( pNtk, pObj, i ) + { + if ( !Abc_NodeIsTravIdCurrent(pObj) ) + continue; + // get the result of quantification + if ( i == Abc_NtkCoNum(pNtk) - 1 ) + { + pOutput = Abc_AigAnd( pMiter->pManFunc, pOutput, Abc_ObjChild0Data(pObj) ); + pOutput = Abc_AigAnd( pMiter->pManFunc, pOutput, Abc_ObjChild0Copy(pObj) ); + } + else + { + pNext = Abc_AigXor( pMiter->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild0Data(pObj) ); + pOutput = Abc_AigOr( pMiter->pManFunc, pOutput, pNext ); + } + } + // add the PO node and name + pObjNew = Abc_NtkCreatePo(pMiter); + Abc_ObjAddFanin( pObjNew, pOutput ); + Abc_ObjAssignName( pObjNew, "miter", NULL ); + // make sure everything is okay + if ( !Abc_NtkCheck( pMiter ) ) + { + printf( "Abc_NtkSensitivityMiter: The network check has failed.\n" ); + Abc_NtkDelete( pMiter ); + return NULL; + } + return pMiter; +} + +/**Function************************************************************* + + Synopsis [Computing sensitivity of POs to POs under constaints.] + + Description [The input network is a combinatonal AIG. The last output + is a constraint. The procedure returns the list of number of PIs, + such that at least one PO depends on this PI, under the constraint.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Abc_NtkSensitivity( Abc_Ntk_t * pNtk, int nConfLim, int fVerbose ) +{ + ProgressBar * pProgress; + Prove_Params_t Params, * pParams = &Params; + Vec_Int_t * vResult = NULL; + Abc_Ntk_t * pMiter; + Abc_Obj_t * pObj; + int RetValue, i; + assert( Abc_NtkIsStrash(pNtk) ); + assert( Abc_NtkLatchNum(pNtk) == 0 ); + // set up solving parameters + Prove_ParamsSetDefault( pParams ); + pParams->nItersMax = 3; + pParams->nMiteringLimitLast = nConfLim; + // iterate through the PIs + vResult = Vec_IntAlloc( 100 ); + pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCiNum(pNtk) ); + Abc_NtkForEachCi( pNtk, pObj, i ) + { + Extra_ProgressBarUpdate( pProgress, i, NULL ); + // generate the sensitivity miter + pMiter = Abc_NtkSensitivityMiter( pNtk, i ); + // solve the miter using CEC engine + RetValue = Abc_NtkIvyProve( &pMiter, pParams ); + if ( RetValue == -1 ) // undecided + Vec_IntPush( vResult, i ); + else if ( RetValue == 0 ) + { + int * pSimInfo = Abc_NtkVerifySimulatePattern( pMiter, pMiter->pModel ); + if ( pSimInfo[0] != 1 ) + printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" ); +// else +// printf( "Networks are NOT EQUIVALENT.\n" ); + free( pSimInfo ); + Vec_IntPush( vResult, i ); + } + Abc_NtkDelete( pMiter ); + } + Extra_ProgressBarStop( pProgress ); + if ( fVerbose ) + { + printf( "The outputs are sensitive to %d (out of %d) inputs:\n", + Vec_IntSize(vResult), Abc_NtkCiNum(pNtk) ); + Vec_IntForEachEntry( vResult, RetValue, i ) + printf( "%d ", RetValue ); + printf( "\n" ); + } + return vResult; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abci/module.make b/src/base/abci/module.make index ca2f2501..777da95b 100644 --- a/src/base/abci/module.make +++ b/src/base/abci/module.make @@ -48,6 +48,7 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcRewrite.c \ src/base/abci/abcRr.c \ src/base/abci/abcSat.c \ + src/base/abci/abcSense.c \ src/base/abci/abcStrash.c \ src/base/abci/abcSweep.c \ src/base/abci/abcSymm.c \ -- cgit v1.2.3