From 79701f8b4603596095d3d04a13018c8e9598f7a0 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 14 Jan 2017 16:11:59 +0700 Subject: Updates to arithmetic verification. --- src/base/abci/abc.c | 20 ++++++++++++++------ src/base/abci/abcDress3.c | 30 +++--------------------------- 2 files changed, 17 insertions(+), 33 deletions(-) (limited to 'src/base') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 910014c6..1e94f28f 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -40543,7 +40543,7 @@ int Abc_CommandAbc9Acec( Abc_Frame_t * pAbc, int argc, char ** argv ) int c, nArgcNew; Acec_ManCecSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CTmdtvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CTmdtbvh" ) ) != EOF ) { switch ( c ) { @@ -40578,6 +40578,9 @@ int Abc_CommandAbc9Acec( Abc_Frame_t * pAbc, int argc, char ** argv ) case 't': pPars->fTwoOutput ^= 1; break; + case 'b': + pPars->fBooth ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -40720,13 +40723,14 @@ int Abc_CommandAbc9Acec( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &acec [-CT num] [-mdtvh] \n" ); + Abc_Print( -2, "usage: &acec [-CT num] [-mdtbvh] \n" ); Abc_Print( -2, "\t combinational equivalence checking for arithmetic circuits\n" ); Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit ); Abc_Print( -2, "\t-m : toggle miter vs. two circuits [default = %s]\n", pPars->fMiter? "miter":"two circuits"); Abc_Print( -2, "\t-d : toggle using dual output miter [default = %s]\n", pPars->fDualOutput? "yes":"no"); Abc_Print( -2, "\t-t : toggle using two-word miter [default = %s]\n", pPars->fTwoOutput? "yes":"no"); + Abc_Print( -2, "\t-b : toggle working with Booth multipliers [default = %s]\n", pPars->fBooth? "yes":"no"); Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes":"no"); Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\tfile1 : (optional) the file with the first network\n"); @@ -40748,12 +40752,15 @@ usage: int Abc_CommandAbc9Anorm( Abc_Frame_t * pAbc, int argc, char ** argv ) { Gia_Man_t * pTemp; - int c, fVerbose = 0; + int c, fBooth = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "bvh" ) ) != EOF ) { switch ( c ) { + case 'b': + fBooth ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -40768,13 +40775,14 @@ int Abc_CommandAbc9Anorm( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Anorm(): There is no AIG.\n" ); return 0; } - pTemp = Acec_Normalize( pAbc->pGia, fVerbose ); + pTemp = Acec_Normalize( pAbc->pGia, fBooth, fVerbose ); Abc_FrameUpdateGia( pAbc, pTemp ); return 0; usage: - Abc_Print( -2, "usage: &anorm [-vh]\n" ); + Abc_Print( -2, "usage: &anorm [-bvh]\n" ); Abc_Print( -2, "\t normalize adder trees in the current AIG\n" ); + Abc_Print( -2, "\t-b : toggles working with Booth multipliers [default = %s]\n", fBooth? "yes": "no" ); 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"); return 1; diff --git a/src/base/abci/abcDress3.c b/src/base/abci/abcDress3.c index 33545f0a..ce0cb7f5 100644 --- a/src/base/abci/abcDress3.c +++ b/src/base/abci/abcDress3.c @@ -33,32 +33,6 @@ ABC_NAMESPACE_IMPL_START /// 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 [Converts AIG from HOP to GIA.] @@ -315,13 +289,15 @@ void Abc_NtkDumpEquivFile( char * pFileName, Vec_Int_t * vClasses, Abc_Ntk_t * p void Abc_NtkDumpEquiv( Abc_Ntk_t * pNtks[2], char * pFileName, int nConfs, int fByName, int fVerbose ) { //abctime clk = Abc_Clock(); + Gia_Man_t * pTemp; Vec_Int_t * vClasses; // derive shared AIG for the two networks 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 - Abc_NtkComputeGiaEquivs( pGia, nConfs, fVerbose ); + pTemp = Gia_ManComputeGiaEquivs( pGia, nConfs, fVerbose ); + Gia_ManStop( pTemp ); //if ( fVerbose ) // Abc_PrintTime( 1, "Equivalence computation time", Abc_Clock() - clk ); if ( fVerbose ) -- cgit v1.2.3