From 6074fa3a1e76d846b1abd6674891ff7ed5b78175 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 16 Mar 2008 08:01:00 -0700 Subject: Version abc80316 --- src/aig/fra/fra.h | 2 +- src/aig/fra/fraSec.c | 5 ++++- src/base/abci/abc.c | 36 ++++++++++++++++++++++++------------ src/base/abci/abcDar.c | 8 ++++---- 4 files changed, 33 insertions(+), 18 deletions(-) diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index e7583b4b..ee4e9115 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -328,7 +328,7 @@ extern int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig extern int Fra_NodesAreClause( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR ); extern int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew ); /*=== fraSec.c ========================================================*/ -extern int Fra_FraigSec( Aig_Man_t * p, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose ); +extern int Fra_FraigSec( Aig_Man_t * p, int nFrames, int fRetimeFirst, int fFraiging, int fVerbose, int fVeryVerbose ); /*=== fraSim.c ========================================================*/ extern int Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize ); extern int Fra_SmlNodeIsConst( Aig_Obj_t * pObj ); diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 75d297cf..bbad2a6e 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -40,7 +40,7 @@ SeeAlso [] ***********************************************************************/ -int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fVerbose, int fVeryVerbose ) +int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fFraiging, int fVerbose, int fVeryVerbose ) { Fra_Ssw_t Pars, * pPars = &Pars; Fra_Sml_t * pSml; @@ -113,6 +113,8 @@ PRT( "Time", clock() - clk ); } // perform fraiging + if ( fFraiging ) + { clk = clock(); pNew = Fra_FraigEquivence( pTemp = pNew, 100, 0 ); Aig_ManStop( pTemp ); @@ -122,6 +124,7 @@ clk = clock(); Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); PRT( "Time", clock() - clk ); } + } // perform seq sweeping while increasing the number of frames RetValue = Fra_FraigMiterStatus( pNew ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 204525d9..91133b2a 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -13390,23 +13390,25 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv ) int nArgcNew; int c; int fRetimeFirst; + int fFraiging; int fVerbose; int fVeryVerbose; int nFrames; - extern int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose ); + extern int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetimeFirst, int fFraiging, int fVerbose, int fVeryVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - nFrames =16; - fRetimeFirst = 1; - fVerbose = 0; - fVeryVerbose = 0; + nFrames = 16; + fRetimeFirst = 1; + fFraiging = 1; + fVerbose = 0; + fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Krwvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Krfwvh" ) ) != EOF ) { switch ( c ) { @@ -13424,6 +13426,9 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'r': fRetimeFirst ^= 1; break; + case 'f': + fFraiging ^= 1; + break; case 'w': fVeryVerbose ^= 1; break; @@ -13447,17 +13452,18 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv ) } // perform verification - Abc_NtkDarSec( pNtk1, pNtk2, nFrames, fRetimeFirst, fVerbose, fVeryVerbose ); + Abc_NtkDarSec( pNtk1, pNtk2, nFrames, fRetimeFirst, fFraiging, fVerbose, fVeryVerbose ); if ( fDelete1 ) Abc_NtkDelete( pNtk1 ); if ( fDelete2 ) Abc_NtkDelete( pNtk2 ); return 0; usage: - fprintf( pErr, "usage: dsec [-K num] [-rwvh] \n" ); + fprintf( pErr, "usage: dsec [-K num] [-rfwvh] \n" ); fprintf( pErr, "\t performs inductive sequential equivalence checking\n" ); fprintf( pErr, "\t-K num : the limit on the depth of induction [default = %d]\n", nFrames ); fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" ); + fprintf( pErr, "\t-f : toggles the internal use of fraiging [default = %s]\n", fFraiging? "yes": "no" ); fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); @@ -13485,11 +13491,12 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk; int c; int fRetimeFirst; + int fFraiging; int fVerbose; int fVeryVerbose; int nFrames; - extern int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose ); + extern int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fFraiging, int fVerbose, int fVeryVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -13498,10 +13505,11 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults nFrames = 16; fRetimeFirst = 1; + fFraiging = 1; fVerbose = 0; fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Frwvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Frfwvh" ) ) != EOF ) { switch ( c ) { @@ -13519,6 +13527,9 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'r': fRetimeFirst ^= 1; break; + case 'f': + fFraiging ^= 1; + break; case 'w': fVeryVerbose ^= 1; break; @@ -13542,14 +13553,15 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) } // perform verification - Abc_NtkDarProve( pNtk, nFrames, fRetimeFirst, fVerbose, fVeryVerbose ); + Abc_NtkDarProve( pNtk, nFrames, fRetimeFirst, fFraiging, fVerbose, fVeryVerbose ); return 0; usage: - fprintf( pErr, "usage: dprove [-F num] [-rwvh]\n" ); + fprintf( pErr, "usage: dprove [-F num] [-rfwvh]\n" ); fprintf( pErr, "\t performs SEC on the sequential miter\n" ); fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", nFrames ); fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" ); + fprintf( pErr, "\t-f : toggles the internal use of fraiging [default = %s]\n", fFraiging? "yes": "no" ); fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 367ba727..78f43aac 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -1186,7 +1186,7 @@ PRT( "Time", clock() - clk ); SeeAlso [] ***********************************************************************/ -int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose ) +int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fFraiging, int fVerbose, int fVeryVerbose ) { Aig_Man_t * pMan; int RetValue; @@ -1199,7 +1199,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fVerbo } assert( pMan->nRegs > 0 ); // perform verification - RetValue = Fra_FraigSec( pMan, nFrames, fRetimeFirst, fVerbose, fVeryVerbose ); + RetValue = Fra_FraigSec( pMan, nFrames, fRetimeFirst, fFraiging, fVerbose, fVeryVerbose ); pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; if ( pNtk->pSeqModel ) { @@ -1221,7 +1221,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fVerbo SeeAlso [] ***********************************************************************/ -int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose ) +int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetimeFirst, int fFraiging, int fVerbose, int fVeryVerbose ) { // Fraig_Params_t Params; Aig_Man_t * pMan; @@ -1293,7 +1293,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetim assert( pMan->nRegs > 0 ); // perform verification - RetValue = Fra_FraigSec( pMan, nFrames, fRetimeFirst, fVerbose, fVeryVerbose ); + RetValue = Fra_FraigSec( pMan, nFrames, fRetimeFirst, fFraiging, fVerbose, fVeryVerbose ); Aig_ManStop( pMan ); return RetValue; } -- cgit v1.2.3