From 236d412255e5007adac97c05e759bfd5069bc1c1 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 7 May 2016 19:47:02 -0700 Subject: Experiments with CEC for arithmetic circuits. --- src/base/abci/abc.c | 274 +++++++++++++++++++++++++++++++++++++++++++++- src/base/wlc/wlc.h | 1 + src/base/wlc/wlcBlast.c | 1 + src/base/wlc/wlcNtk.c | 5 + src/base/wlc/wlcReadVer.c | 1 + 5 files changed, 276 insertions(+), 6 deletions(-) (limited to 'src/base') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index b88fa79d..6d6e16f5 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -43,6 +43,7 @@ #include "opt/ret/retInt.h" #include "sat/cnf/cnf.h" #include "proof/cec/cec.h" +#include "proof/acec/acec.h" #include "proof/pdr/pdr.h" #include "misc/tim/tim.h" #include "bdd/llb/llb.h" @@ -464,6 +465,8 @@ static int Abc_CommandAbc9Bmci ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9PoXsim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Demiter ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Fadds ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Polyn ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Acec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Esop ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Exorcism ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Mfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1092,6 +1095,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&poxsim", Abc_CommandAbc9PoXsim, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&demiter", Abc_CommandAbc9Demiter, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&fadds", Abc_CommandAbc9Fadds, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&polyn", Abc_CommandAbc9Polyn, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&acec", Abc_CommandAbc9Acec, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&esop", Abc_CommandAbc9Esop, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&exorcism", Abc_CommandAbc9Exorcism, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&mfs", Abc_CommandAbc9Mfs, 0 ); @@ -27760,6 +27765,7 @@ usage: Abc_Print( -2, "\t-c : toggle collapsing hierarchical AIG [default = %s]\n", fCollapse? "yes": "no" ); Abc_Print( -2, "\t-m : toggle converting to larger gates [default = %s]\n", fAddMuxes? "yes": "no" ); Abc_Print( -2, "\t-L num : create MUX when sum of refs does not exceed this limit [default = %d]\n", Limit ); + Abc_Print( -2, "\t (use L = 1 to create AIG with XORs but without MUXes)\n" ); Abc_Print( -2, "\t-r : toggle rehashing AIG while preserving mapping [default = %s]\n", fRehashMap? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -39054,14 +39060,22 @@ usage: ***********************************************************************/ int Abc_CommandAbc9Demiter( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Gia_Man_t * Gia_ManDupDemiter( Gia_Man_t * p, int fVerbose ); Gia_Man_t * pTemp; - int c, fVerbose = 0; + int c, fDumpFiles = 0, fDumpFilesTwo = 0, fDual = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "ftdvh" ) ) != EOF ) { switch ( c ) { + case 'f': + fDumpFiles ^= 1; + break; + case 't': + fDumpFilesTwo ^= 1; + break; + case 'd': + fDual ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -39076,20 +39090,57 @@ int Abc_CommandAbc9Demiter( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Demiter(): There is no AIG.\n" ); return 0; } + if ( fDumpFiles || fDumpFilesTwo ) + { + char pName0[1000] = "miter_part0.aig"; + char pName1[1000] = "miter_part1.aig"; + Gia_Man_t * pPart1, * pPart2; + if ( Gia_ManPoNum(pAbc->pGia) % 2 != 0 ) + { + Abc_Print( -1, "Abc_CommandAbc9Demiter(): Does not look like a dual-output miter.\n" ); + return 0; + } + if ( fDumpFilesTwo ) + Gia_ManDemiterTwoWords( pAbc->pGia, &pPart1, &pPart2 ); + else + Gia_ManDemiterDual( pAbc->pGia, &pPart1, &pPart2 ); + if ( pAbc->pGia->pSpec ) + { + char * pGen = Extra_FileNameGeneric(pAbc->pGia->pSpec); + sprintf( pName0, "%s_1.aig", pGen ); + sprintf( pName1, "%s_2.aig", pGen ); + ABC_FREE( pGen ); + } + Gia_AigerWrite( pPart1, pName0, 0, 0 ); + Gia_AigerWrite( pPart2, pName1, 0, 0 ); + Gia_ManStop( pPart1 ); + Gia_ManStop( pPart2 ); + if ( fDumpFilesTwo ) + printf( "Two parts of the two-word miter are dumped into files \"%s\" and \"%s\".\n", pName0, pName1 ); + else + printf( "Two parts of the dual-output miter are dumped into files \"%s\" and \"%s\".\n", pName0, pName1 ); + return 0; + } if ( Gia_ManPoNum(pAbc->pGia) != 1 ) { Abc_Print( -1, "Abc_CommandAbc9Demiter(): Miter should have one output.\n" ); return 0; } - pTemp = Gia_ManDupDemiter( pAbc->pGia, fVerbose ); + if ( fDual ) + pTemp = Gia_ManDemiterToDual( pAbc->pGia ); + else + pTemp = Gia_ManDupDemiter( pAbc->pGia, fVerbose ); Abc_FrameUpdateGia( pAbc, pTemp ); if ( fVerbose ) Gia_ManPrintStatsMiter( pTemp, 0 ); return 0; usage: - Abc_Print( -2, "usage: &demiter [-vh]\n" ); - Abc_Print( -2, "\t decomposes a single-output miter\n" ); + Abc_Print( -2, "usage: &demiter [-ftdvh]\n" ); + Abc_Print( -2, "\t decomposes a miter (by default, tries to extract an OR gate)\n" ); + Abc_Print( -2, "\t-f : write files with two sides of a dual-output miter [default = %s]\n", fDumpFiles? "yes": "no" ); + Abc_Print( -2, "\t-t : write files with two sides of a two-word miter [default = %s]\n", fDumpFilesTwo? "yes": "no" ); + Abc_Print( -2, "\t-d : take single-output and decompose into dual-output [default = %s]\n", fDual? "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; @@ -39237,6 +39288,217 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9Polyn( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern void Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fVerbose ); + int c, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9Esop(): There is no AIG.\n" ); + return 0; + } + Gia_PolynBuild( pAbc->pGia, NULL, fVerbose ); + return 0; + +usage: + Abc_Print( -2, "usage: &polyn [-vh]\n" ); + Abc_Print( -2, "\t derives algebraic polynomial from AIG\n" ); + 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; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9Acec( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pFile; + Cec_ParCec_t ParsCec, * pPars = &ParsCec; + Gia_Man_t * pSecond; + char * FileName, * pTemp; + char ** pArgvNew; + int c, nArgcNew, fMiter = 0, fDualOutput = 0, fTwoOutput = 0; + Cec_ManCecSetDefaultParams( pPars ); + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "CTnmdtvh" ) ) != EOF ) + { + switch ( c ) + { + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBTLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBTLimit < 0 ) + goto usage; + break; + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + pPars->TimeLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->TimeLimit < 0 ) + goto usage; + break; + case 'n': + pPars->fNaive ^= 1; + break; + case 'm': + fMiter ^= 1; + break; + case 'd': + fDualOutput ^= 1; + break; + case 't': + fTwoOutput ^= 1; + break; + case 'v': + pPars->fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( fMiter ) + { + Gia_Man_t * pGia0, * pGia1, * pDual; + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9Acec(): There is no AIG.\n" ); + return 1; + } + if ( fDualOutput ) + { + if ( Gia_ManPoNum(pAbc->pGia) & 1 ) + { + Abc_Print( -1, "The dual-output miter should have an even number of outputs.\n" ); + return 1; + } + if ( !pPars->fSilent ) + Abc_Print( 1, "Assuming the current network is a double-output miter. (Conflict limit = %d.)\n", pPars->nBTLimit ); + Gia_ManDemiterDual( pAbc->pGia, &pGia0, &pGia1 ); + pAbc->Status = Gia_PolynCec( pGia0, pGia1, pPars ); + } + else if ( fTwoOutput ) + { + if ( Gia_ManPoNum(pAbc->pGia) & 1 ) + { + Abc_Print( -1, "The dual-output miter should have an even number of outputs.\n" ); + return 1; + } + if ( !pPars->fSilent ) + Abc_Print( 1, "Assuming the current network is a two-word miter. (Conflict limit = %d.)\n", pPars->nBTLimit ); + Gia_ManDemiterTwoWords( pAbc->pGia, &pGia0, &pGia1 ); + pAbc->Status = Gia_PolynCec( pGia0, pGia1, pPars ); + } + else + { + if ( !pPars->fSilent ) + Abc_Print( 1, "Assuming the current network is a single-output miter. (Conflict limit = %d.)\n", pPars->nBTLimit ); + pDual = Gia_ManDemiterToDual( pAbc->pGia ); + Gia_ManDemiterDual( pDual, &pGia0, &pGia1 ); + Gia_ManStop( pDual ); + pAbc->Status = Gia_PolynCec( pGia0, pGia1, pPars ); + } + Abc_FrameReplaceCex( pAbc, &pGia0->pCexComb ); + Gia_ManStop( pGia0 ); + Gia_ManStop( pGia1 ); + return 0; + } + + pArgvNew = argv + globalUtilOptind; + nArgcNew = argc - globalUtilOptind; + if ( nArgcNew != 1 ) + { + if ( pAbc->pGia->pSpec == NULL ) + { + Abc_Print( -1, "File name is not given on the command line.\n" ); + return 1; + } + FileName = pAbc->pGia->pSpec; + } + else + FileName = pArgvNew[0]; + // fix the wrong symbol + for ( pTemp = FileName; *pTemp; pTemp++ ) + if ( *pTemp == '>' ) + *pTemp = '\\'; + if ( (pFile = fopen( FileName, "r" )) == NULL ) + { + Abc_Print( -1, "Cannot open input file \"%s\". ", FileName ); + if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", NULL, NULL, NULL, NULL )) ) + Abc_Print( 1, "Did you mean \"%s\"?", FileName ); + Abc_Print( 1, "\n" ); + return 1; + } + fclose( pFile ); + pSecond = Gia_AigerRead( FileName, 0, 0 ); + if ( pSecond == NULL ) + { + Abc_Print( -1, "Reading AIGER has failed.\n" ); + return 0; + } + pAbc->Status = Gia_PolynCec( pAbc->pGia, pSecond, pPars ); + Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb ); + Gia_ManStop( pSecond ); + return 0; + +usage: + Abc_Print( -2, "usage: &acec [-CT num] [-nmdtvh]\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-n : toggle using naive SAT-based checking [default = %s]\n", pPars->fNaive? "yes":"no"); + Abc_Print( -2, "\t-m : toggle miter vs. two circuits [default = %s]\n", fMiter? "miter":"two circuits"); + Abc_Print( -2, "\t-d : toggle using dual output miter [default = %s]\n", fDualOutput? "yes":"no"); + Abc_Print( -2, "\t-t : toggle using two-word miter [default = %s]\n", fTwoOutput? "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"); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index f3a4f7aa..453cb157 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -125,6 +125,7 @@ typedef struct Wlc_Ntk_t_ Wlc_Ntk_t; struct Wlc_Ntk_t_ { char * pName; // model name + char * pSpec; // input file name Vec_Int_t vPis; // primary inputs Vec_Int_t vPos; // primary outputs Vec_Int_t vCis; // combinational inputs diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c index 3a3d614b..6ddd7a60 100644 --- a/src/base/wlc/wlcBlast.c +++ b/src/base/wlc/wlcBlast.c @@ -1327,6 +1327,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds ) } assert( Vec_PtrSize(pNew->vNamesOut) == Gia_ManCoNum(pNew) ); */ + pNew->pSpec = Abc_UtilStrsav( p->pSpec ? p->pSpec : p->pName ); return pNew; } diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c index 2f3b07bf..442ddb83 100644 --- a/src/base/wlc/wlcNtk.c +++ b/src/base/wlc/wlcNtk.c @@ -223,6 +223,7 @@ void Wlc_NtkFree( Wlc_Ntk_t * p ) ABC_FREE( p->pInits ); ABC_FREE( p->pObjs ); ABC_FREE( p->pName ); + ABC_FREE( p->pSpec ); ABC_FREE( p ); } int Wlc_NtkMemUsage( Wlc_Ntk_t * p ) @@ -587,6 +588,8 @@ Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p ) if ( p->pInits ) pNew->pInits = Abc_UtilStrsav( p->pInits ); Vec_IntFree( vFanins ); + if ( p->pSpec ) + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); return pNew; } void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p ) @@ -658,6 +661,8 @@ Wlc_Ntk_t * Wlc_NtkDupSingleNodes( Wlc_Ntk_t * p ) } Vec_IntFree( vFanins ); Wlc_NtkTransferNames( pNew, p ); + if ( p->pSpec ) + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); return pNew; } diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c index 30525df4..0aedef30 100644 --- a/src/base/wlc/wlcReadVer.c +++ b/src/base/wlc/wlcReadVer.c @@ -1264,6 +1264,7 @@ Wlc_Ntk_t * Wlc_ReadVer( char * pFileName ) finish: Wlc_PrsPrintErrorMessage( p ); Wlc_PrsStop( p ); + pNtk->pSpec = Abc_UtilStrsav( pFileName ); return pNtk; } -- cgit v1.2.3