From df6fdd1dffd8ce83dfc4a7868ebdd25241f8f24b Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 8 Apr 2009 08:01:00 -0700 Subject: Version abc90408 --- src/base/abci/abc.c | 152 ++++++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 130 insertions(+), 22 deletions(-) (limited to 'src/base/abci/abc.c') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index ef7969be..c48b7e95 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -27,7 +27,7 @@ #include "if.h" #include "res.h" #include "lpk.h" -#include "aig.h" +#include "giaAig.h" #include "dar.h" #include "mfs.h" #include "mfx.h" @@ -39,7 +39,6 @@ #include "ssw.h" #include "cgt.h" #include "amap.h" -#include "gia.h" #include "cec.h" //////////////////////////////////////////////////////////////////////// @@ -194,6 +193,7 @@ static int Abc_CommandScut ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandInit ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandZero ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandUndc ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandOneHot ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPipe ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSeq ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandUnseq ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -513,6 +513,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Sequential", "init", Abc_CommandInit, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "zero", Abc_CommandZero, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "undc", Abc_CommandUndc, 1 ); + Cmd_CommandAdd( pAbc, "Sequential", "onehot", Abc_CommandOneHot, 1 ); // Cmd_CommandAdd( pAbc, "Sequential", "pipe", Abc_CommandPipe, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "retime", Abc_CommandRetime, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "dretime", Abc_CommandDRetime, 1 ); @@ -598,7 +599,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "AIG", "&psig", Abc_CommandAbc9PSig, 0 ); Cmd_CommandAdd( pAbc, "AIG", "&status", Abc_CommandAbc9Status, 0 ); Cmd_CommandAdd( pAbc, "AIG", "&show", Abc_CommandAbc9Show, 0 ); - Cmd_CommandAdd( pAbc, "AIG", "&hash", Abc_CommandAbc9Hash, 0 ); + Cmd_CommandAdd( pAbc, "AIG", "&st", Abc_CommandAbc9Hash, 0 ); Cmd_CommandAdd( pAbc, "AIG", "&topand", Abc_CommandAbc9Topand, 0 ); Cmd_CommandAdd( pAbc, "AIG", "&cof", Abc_CommandAbc9Cof, 0 ); Cmd_CommandAdd( pAbc, "AIG", "&trim", Abc_CommandAbc9Trim, 0 ); @@ -11945,7 +11946,7 @@ usage: fprintf( pErr, "\t-E float : sets epsilon used for tie-breaking [default = %f]\n", pPars->fEpsilon ); fprintf( pErr, "\t-m : toggles using MUX matching [default = %s]\n", pPars->fUseMuxes? "yes": "no" ); fprintf( pErr, "\t-x : toggles using XOR matching [default = %s]\n", pPars->fUseXors? "yes": "no" ); - fprintf( pErr, "\t-i : toggles assuming inverters are ABC_FREE [default = %s]\n", pPars->fFreeInvs? "yes": "no" ); + fprintf( pErr, "\t-i : toggles assuming inverters are free [default = %s]\n", pPars->fFreeInvs? "yes": "no" ); fprintf( pErr, "\t-s : toggles sweep after mapping [default = %s]\n", fSweep? "yes": "no" ); fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); @@ -13094,7 +13095,74 @@ int Abc_CommandUndc( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: fprintf( pErr, "usage: undc [-h]\n" ); - fprintf( pErr, "\t converts latches with DC init values into ABC_FREE PIs\n" ); + fprintf( pErr, "\t converts latches with DC init values into free PIs\n" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandOneHot( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int c; + extern Abc_Ntk_t * Abc_NtkConvertOnehot( Abc_Ntk_t * pNtk ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( Abc_NtkIsComb(pNtk) ) + { + fprintf( pErr, "The current network is combinational.\n" ); + return 0; + } + if ( !Abc_NtkIsLogic(pNtk) ) + { + fprintf( pErr, "This command works only for logic networks.\n" ); + return 0; + } + // get the new network + pNtkRes = Abc_NtkConvertOnehot( pNtk ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Converting to one-hot encoding has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: onehot [-h]\n" ); + fprintf( pErr, "\t converts natural encoding into one-hot encoding\n" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -15030,7 +15098,7 @@ int Abc_CommandSim( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - fNew = 1; + fNew = 0; fComb = 0; nFrames = 32; nWords = 8; @@ -18381,22 +18449,28 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) int nConfMax; int fDynamic; int fExtend; + int fSkipProof; + int nFramesBmc; + int nConfMaxBmc; int fVerbose; int c; - extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - nFramesMax = 10; - nConfMax = 10000; - fDynamic = 1; - fExtend = 0; - fVerbose = 0; + nFramesMax = 10; + nConfMax = 10000; + fDynamic = 1; + fExtend = 0; + fSkipProof = 0; + nFramesBmc = 2000; + nConfMaxBmc = 5000; + fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FCdevh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FCGDdesvh" ) ) != EOF ) { switch ( c ) { @@ -18422,12 +18496,37 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nConfMax < 0 ) goto usage; break; + case 'G': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-G\" should be followed by an integer.\n" ); + goto usage; + } + nFramesBmc = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nFramesBmc < 0 ) + goto usage; + break; + case 'D': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" ); + goto usage; + } + nConfMaxBmc = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nConfMaxBmc < 0 ) + goto usage; + break; case 'd': fDynamic ^= 1; break; case 'e': fExtend ^= 1; break; + case 's': + fSkipProof ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -18454,7 +18553,7 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) } // modify the current network - pNtkRes = Abc_NtkDarPBAbstraction( pNtk, nFramesMax, nConfMax, fDynamic, fExtend, fVerbose ); + pNtkRes = Abc_NtkDarPBAbstraction( pNtk, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, fVerbose ); if ( pNtkRes == NULL ) { if ( pNtk->pSeqModel == NULL ) @@ -18465,12 +18564,16 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); return 0; usage: - fprintf( pErr, "usage: abs [-FC num] [-devh]\n" ); - fprintf( pErr, "\t proof-based abstraction from UNSAT core of the BMC instance\n" ); - fprintf( pErr, "\t-F num : the max number of timeframes [default = %d]\n", nFramesMax ); - fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver [default = %d]\n", nConfMax ); + fprintf( pErr, "usage: abs [-FCGD num] [-desvh]\n" ); + fprintf( pErr, "\t proof-based abstraction (PBA) using UNSAT core of BMC\n" ); + fprintf( pErr, "\t followed by counter-example-based abstraction\n" ); + fprintf( pErr, "\t-F num : the max number of timeframes for PBA [default = %d]\n", nFramesMax ); + fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver for PBA [default = %d]\n", nConfMax ); + fprintf( pErr, "\t-G num : the max number of timeframes for BMC [default = %d]\n", nFramesBmc ); + fprintf( pErr, "\t-D num : the max number of conflicts by SAT solver for BMC [default = %d]\n", nConfMaxBmc ); fprintf( pErr, "\t-d : toggle dynamic unrolling of timeframes [default = %s]\n", fDynamic? "yes": "no" ); fprintf( pErr, "\t-e : toggle extending abstraction using COI of flops [default = %s]\n", fExtend? "yes": "no" ); + fprintf( pErr, "\t-s : toggle skipping proof-based abstraction [default = %s]\n", fSkipProof? "yes": "no" ); 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; @@ -22128,11 +22231,15 @@ int Abc_CommandAbc9Hash( Abc_Frame_t * pAbc, int argc, char ** argv ) { Gia_Man_t * pTemp; int c; + int fAddStrash = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "ah" ) ) != EOF ) { switch ( c ) { + case 'a': + fAddStrash ^= 1; + break; case 'h': goto usage; default: @@ -22144,13 +22251,14 @@ int Abc_CommandAbc9Hash( Abc_Frame_t * pAbc, int argc, char ** argv ) printf( "Abc_CommandAbc9Hash(): There is no AIG.\n" ); return 1; } - pAbc->pAig = Gia_ManRehash( pTemp = pAbc->pAig ); + pAbc->pAig = Gia_ManRehash( pTemp = pAbc->pAig, fAddStrash ); Gia_ManStop( pTemp ); return 0; usage: - fprintf( stdout, "usage: &hash [-h]\n" ); + fprintf( stdout, "usage: &st [-ah]\n" ); fprintf( stdout, "\t performs structural hashing\n" ); + fprintf( stdout, "\t-a : toggle additional hashing [default = %s]\n", fAddStrash? "yes": "no" ); fprintf( stdout, "\t-h : print the command usage\n"); return 1; } @@ -22186,7 +22294,7 @@ int Abc_CommandAbc9Topand( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( pAbc->pAig == NULL ) { - printf( "Abc_CommandAbc9Hash(): There is no AIG.\n" ); + printf( "Abc_CommandAbc9Topand(): There is no AIG.\n" ); return 1; } if ( Gia_ManRegNum(pAbc->pAig) > 0 ) -- cgit v1.2.3