From 9eaa290b1f2786a292073711d4389574543932d8 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 22 Jun 2013 11:54:58 -0700 Subject: Limiting runtime limit checks in 'pdr'. --- Makefile | 3 +- abclib.dsp | 4 + src/base/abci/abc.c | 78 ++++++++ src/base/abci/abcRpo.c | 442 ++++++++++++++++++++++++++++++++++++++++++++++ src/base/abci/module.make | 1 + src/base/main/mainInit.c | 2 +- src/bool/rpo/literal.h | 297 +++++++++++++++++++++++++++++++ src/bool/rpo/module.make | 1 + src/bool/rpo/rpo.c | 383 +++++++++++++++++++++++++++++++++++++++ src/bool/rpo/rpo.h | 57 ++++++ 10 files changed, 1266 insertions(+), 2 deletions(-) create mode 100644 src/base/abci/abcRpo.c create mode 100644 src/bool/rpo/literal.h create mode 100644 src/bool/rpo/module.make create mode 100644 src/bool/rpo/rpo.c create mode 100644 src/bool/rpo/rpo.h diff --git a/Makefile b/Makefile index 0950b167..ad1f6691 100644 --- a/Makefile +++ b/Makefile @@ -23,7 +23,8 @@ MODULES := \ src/opt/ret src/opt/res src/opt/lpk src/opt/nwk src/opt/rwt \ src/opt/cgt src/opt/csw src/opt/dar src/opt/dau src/opt/sfm \ src/sat/bsat src/sat/csat src/sat/msat src/sat/psat src/sat/cnf src/sat/bmc \ - src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky src/bool/rsb \ + src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky \ + src/bool/rsb src/bool/rpo \ src/proof/pdr src/proof/int src/proof/bbr src/proof/llb src/proof/live \ src/proof/cec src/proof/dch src/proof/fraig src/proof/fra src/proof/ssw \ src/proof/abs src/proof/ssc \ diff --git a/abclib.dsp b/abclib.dsp index 6175d0fa..d19dfee7 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -3886,6 +3886,10 @@ SOURCE=.\src\bool\rsb\rsbInt.h SOURCE=.\src\bool\rsb\rsbMan.c # End Source File # End Group +# Begin Group "rpo" + +# PROP Default_Filter "" +# End Group # End Group # Begin Group "prove" diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index ef973099..063388f7 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -53,6 +53,7 @@ #include "sat/bmc/bmc.h" #include "proof/ssc/ssc.h" #include "opt/sfm/sfm.h" +#include "bool/rpo/rpo.h" #ifndef _WIN32 #include @@ -113,6 +114,7 @@ static int Abc_CommandAddBuffs ( Abc_Frame_t * pAbc, int argc, cha //static int Abc_CommandMerge ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTestDec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTestNpn ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandTestRPO ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -663,6 +665,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) // Cmd_CommandAdd( pAbc, "Synthesis", "merge", Abc_CommandMerge, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "testdec", Abc_CommandTestDec, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "testnpn", Abc_CommandTestNpn, 0 ); + Cmd_CommandAdd( pAbc, "LogiCS", "testrpo", Abc_CommandTestRPO, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "rewrite", Abc_CommandRewrite, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "refactor", Abc_CommandRefactor, 1 ); @@ -5323,6 +5326,81 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandTestRPO(Abc_Frame_t * pAbc, int argc, char ** argv) { + extern int Abc_RpoTest(char * pFileName, int nVarNum, int nThreshold, int fVerbose); + char * pFileName; + int c; + int nVarNum = -1; + int fVerbose = 0; + int nThreshold = -1; + Extra_UtilGetoptReset(); + while ((c = Extra_UtilGetopt(argc, argv, "TNvh")) != EOF) { + switch (c) { + case 'N': + if (globalUtilOptind >= argc) { + Abc_Print(-1, "Command line switch \"-N\" should be followed by an integer.\n"); + goto usage; + } + nVarNum = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if (nVarNum < 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; + } + nThreshold = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if (nThreshold < 0) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if (argc != globalUtilOptind + 1) + { + Abc_Print(1, "Input file is not given.\n"); + goto usage; + } + // get the output file name + pFileName = argv[globalUtilOptind]; + // call the testbench + Abc_RpoTest( pFileName, nVarNum, nThreshold, fVerbose ); + return 0; + +usage: + Abc_Print(-2, "usage: testrpo [-NT ] [-vh] \n"); + Abc_Print(-2, "\t RPO algorithm developed and implemented by Mayler G. A. Martins,\n"); + Abc_Print(-2, "\t Vinicius Callegaro, Renato P. Ribas and Andre' I. Reis\n"); + Abc_Print(-2, "\t at Federal University of Rio Grande do Sul, Porto Alegre, Brazil\n"); + Abc_Print(-2, "\t-N : the number of support variables (binary files only) [default = unused]\n"); + Abc_Print(-2, "\t-T : the number of recursions accepted before abort [default = INFINITE]\n"); + Abc_Print(-2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose ? "yes" : "no"); + Abc_Print(-2, "\t-h : print the command usage\n"); + Abc_Print(-2, "\t : a text file with truth tables in hexadecimal, listed one per line,\n"); + Abc_Print(-2, "\t or a binary file with an array of truth tables (in this case,\n"); + Abc_Print(-2, "\t -N is required to determine how many functions are stored)\n"); + return 1; +} /**Function************************************************************* diff --git a/src/base/abci/abcRpo.c b/src/base/abci/abcRpo.c new file mode 100644 index 00000000..286ef80b --- /dev/null +++ b/src/base/abci/abcRpo.c @@ -0,0 +1,442 @@ +/**CFile**************************************************************** + + FileName [abcRpo.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Rpo package.] + + Synopsis [Procedures for executing RPO.] + + Author [Mayler G. A. Martins / Vinicius Callegaro] + + Affiliation [UFRGS] + + Date [Ver. 1.0. Started - May 08, 2013.] + + Revision [$Id: abcRpo.c,v 1.00 2013/05/08 00:00:00 mgamartins Exp $] + + ***********************************************************************/ + +#include "misc/extra/extra.h" + +#include "bool/rpo/rpo.h" +#include "bool/rpo/literal.h" + +ABC_NAMESPACE_IMPL_START + + +// data-structure to store a bunch of truth tables +typedef struct Rpo_TtStore_t_ Rpo_TtStore_t; + +struct Rpo_TtStore_t_ { + int nVars; + int nWords; + int nFuncs; + word ** pFuncs; +}; + + +// read/write/flip i-th bit of a bit string table: + +static inline int Abc_TruthGetBit(word * p, int i) { + return (int) (p[i >> 6] >> (i & 63)) & 1; +} + +static inline void Abc_TruthSetBit(word * p, int i) { + p[i >> 6] |= (((word) 1) << (i & 63)); +} + +static inline void Abc_TruthXorBit(word * p, int i) { + p[i >> 6] ^= (((word) 1) << (i & 63)); +} + +// read/write k-th digit d of a hexadecimal number: + +static inline int Abc_TruthGetHex(word * p, int k) { + return (int) (p[k >> 4] >> ((k << 2) & 63)) & 15; +} + +static inline void Abc_TruthSetHex(word * p, int k, int d) { + p[k >> 4] |= (((word) d) << ((k << 2) & 63)); +} + +static inline void Abc_TruthXorHex(word * p, int k, int d) { + p[k >> 4] ^= (((word) d) << ((k << 2) & 63)); +} + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +// read one hex character + +static inline int Abc_TruthReadHexDigit(char HexChar) { + if (HexChar >= '0' && HexChar <= '9') + return HexChar - '0'; + if (HexChar >= 'A' && HexChar <= 'F') + return HexChar - 'A' + 10; + if (HexChar >= 'a' && HexChar <= 'f') + return HexChar - 'a' + 10; + assert(0); // not a hexadecimal symbol + return -1; // return value which makes no sense +} + +// write one hex character + +static inline void Abc_TruthWriteHexDigit(FILE * pFile, int HexDigit) { + assert(HexDigit >= 0 && HexDigit < 16); + if (HexDigit < 10) + fprintf(pFile, "%d", HexDigit); + else + fprintf(pFile, "%c", 'A' + HexDigit - 10); +} + +// read one truth table in hexadecimal + +static void Abc_TruthReadHex(word * pTruth, char * pString, int nVars) { + int nWords = (nVars < 7) ? 1 : (1 << (nVars - 6)); + int k, Digit, nDigits = (nWords << 4); + char EndSymbol; + // skip the first 2 symbols if they are "0x" + if (pString[0] == '0' && pString[1] == 'x') + pString += 2; + // get the last symbol + EndSymbol = pString[nDigits]; + // the end symbol of the TT (the one immediately following hex digits) + // should be one of the following: space, a new-line, or a zero-terminator + // (note that on Windows symbols '\r' can be inserted before each '\n') + assert(EndSymbol == ' ' || EndSymbol == '\n' || EndSymbol == '\r' || EndSymbol == '\0'); + // read hexadecimal digits in the reverse order + // (the last symbol in the string is the least significant digit) + for (k = 0; k < nDigits; k++) { + Digit = Abc_TruthReadHexDigit(pString[nDigits - 1 - k]); + assert(Digit >= 0 && Digit < 16); + Abc_TruthSetHex(pTruth, k, Digit); + } +} + +// write one truth table in hexadecimal (do not add end-of-line!) + +static void Abc_TruthWriteHex(FILE * pFile, word * pTruth, int nVars) { + int nDigits, Digit, k; + nDigits = (1 << (nVars - 2)); + for (k = 0; k < nDigits; k++) { + Digit = Abc_TruthGetHex(pTruth, k); + assert(Digit >= 0 && Digit < 16); + Abc_TruthWriteHexDigit(pFile, Digit); + } +} + + + +/**Function************************************************************* + + Synopsis [Allocate/Deallocate storage for truth tables..] + + Description [] + + SideEffects [] + + SeeAlso [] + + ***********************************************************************/ +static Rpo_TtStore_t * Abc_TruthStoreAlloc(int nVars, int nFuncs) { + Rpo_TtStore_t * p; + int i; + p = (Rpo_TtStore_t *) malloc(sizeof (Rpo_TtStore_t)); + p->nVars = nVars; + p->nWords = (nVars < 7) ? 1 : (1 << (nVars - 6)); + p->nFuncs = nFuncs; + // alloc storage for 'nFuncs' truth tables as one chunk of memory + p->pFuncs = (word **) malloc((sizeof (word *) + sizeof (word) * p->nWords) * p->nFuncs); + // assign and clean the truth table storage + p->pFuncs[0] = (word *) (p->pFuncs + p->nFuncs); + memset(p->pFuncs[0], 0, sizeof (word) * p->nWords * p->nFuncs); + // split it up into individual truth tables + for (i = 1; i < p->nFuncs; i++) + p->pFuncs[i] = p->pFuncs[i - 1] + p->nWords; + return p; +} + +static Rpo_TtStore_t * Abc_TruthStoreAlloc2(int nVars, int nFuncs, word * pBuffer) { + Rpo_TtStore_t * p; + int i; + p = (Rpo_TtStore_t *) malloc(sizeof (Rpo_TtStore_t)); + p->nVars = nVars; + p->nWords = (nVars < 7) ? 1 : (1 << (nVars - 6)); + p->nFuncs = nFuncs; + // alloc storage for 'nFuncs' truth tables as one chunk of memory + p->pFuncs = (word **) malloc(sizeof (word *) * p->nFuncs); + // assign and clean the truth table storage + p->pFuncs[0] = pBuffer; + // split it up into individual truth tables + for (i = 1; i < p->nFuncs; i++) + p->pFuncs[i] = p->pFuncs[i - 1] + p->nWords; + return p; +} + +static void Abc_TtStoreFree(Rpo_TtStore_t * p, int nVarNum) { + if (nVarNum >= 0) + ABC_FREE(p->pFuncs[0]); + ABC_FREE(p->pFuncs); + ABC_FREE(p); +} + +/**Function************************************************************* + + Synopsis [Read file contents.] + + Description [] + + SideEffects [] + + SeeAlso [] + + ***********************************************************************/ +extern int Abc_FileSize(char * pFileName); + +/**Function************************************************************* + + Synopsis [Read file contents.] + + Description [] + + SideEffects [] + + SeeAlso [] + + ***********************************************************************/ +extern char * Abc_FileRead(char * pFileName); + +/**Function************************************************************* + + Synopsis [Determine the number of variables by reading the first line.] + + Description [Determine the number of functions by counting the lines.] + + SideEffects [] + + SeeAlso [] + + ***********************************************************************/ +extern void Abc_TruthGetParams(char * pFileName, int * pnVars, int * pnTruths); + + +/**Function************************************************************* + + Synopsis [Read truth tables from file.] + + Description [] + + SideEffects [] + + SeeAlso [] + + ***********************************************************************/ +static void Abc_TruthStoreRead(char * pFileName, Rpo_TtStore_t * p) { + char * pContents; + int i, nLines; + pContents = Abc_FileRead(pFileName); + if (pContents == NULL) + return; + // here it is assumed (without checking!) that each line of the file + // begins with a string of hexadecimal chars followed by space + + // the file will be read till the first empty line (pContents[i] == '\n') + // (note that Abc_FileRead() added several empty lines at the end of the file contents) + for (nLines = i = 0; pContents[i] != '\n';) { + // read one line + Abc_TruthReadHex(p->pFuncs[nLines++], &pContents[i], p->nVars); + // skip till after the end-of-line symbol + // (note that end-of-line symbol is also skipped) + while (pContents[i++] != '\n'); + } + // adjust the number of functions read + // (we may have allocated more storage because some lines in the file were empty) + assert(p->nFuncs >= nLines); + p->nFuncs = nLines; + ABC_FREE(pContents); +} + +/**Function************************************************************* + + Synopsis [Write truth tables into file.] + + Description [] + + SideEffects [] + + SeeAlso [] + + ***********************************************************************/ +static void Abc_TtStoreWrite(char * pFileName, Rpo_TtStore_t * p, int fBinary) { + FILE * pFile; + int i, nBytes = 8 * Abc_Truth6WordNum(p->nVars); + pFile = fopen(pFileName, "wb"); + if (pFile == NULL) { + printf("Cannot open file \"%s\" for writing.\n", pFileName); + return; + } + for (i = 0; i < p->nFuncs; i++) { + if (fBinary) + fwrite(p->pFuncs[i], nBytes, 1, pFile); + else + Abc_TruthWriteHex(pFile, p->pFuncs[i], p->nVars), fprintf(pFile, "\n"); + } + fclose(pFile); +} + +/**Function************************************************************* + + Synopsis [Read truth tables from input file and write them into output file.] + + Description [] + + SideEffects [] + + SeeAlso [] + + ***********************************************************************/ +static Rpo_TtStore_t * Abc_TtStoreLoad(char * pFileName, int nVarNum) { + Rpo_TtStore_t * p; + if (nVarNum < 0) { + int nVars, nTruths; + // figure out how many truth table and how many variables + Abc_TruthGetParams(pFileName, &nVars, &nTruths); + if (nVars < 2 || nVars > 16 || nTruths == 0) + return NULL; + // allocate data-structure + p = Abc_TruthStoreAlloc(nVars, nTruths); + // read info from file + Abc_TruthStoreRead(pFileName, p); + } else { + char * pBuffer; + int nFileSize = Abc_FileSize(pFileName); + int nBytes = (1 << (nVarNum - 3)); // why mishchencko put -3? ### + int nTruths = nFileSize / nBytes; + //Abc_Print(-2,"nFileSize=%d,nTruths=%d\n",nFileSize, nTruths); + if (nFileSize == -1) + return NULL; + assert(nVarNum >= 6); + if (nFileSize % nBytes != 0) + Abc_Print(0, "The file size (%d) is divided by the truth table size (%d) with remainder (%d).\n", + nFileSize, nBytes, nFileSize % nBytes); + // read file contents + pBuffer = Abc_FileRead(pFileName); + // allocate data-structure + p = Abc_TruthStoreAlloc2(nVarNum, nTruths, (word *) pBuffer); + } + return p; +} + + +/**Function************************************************************* + + Synopsis [Apply decomposition to the truth table.] + + Description [Returns the number of AIG nodes.] + + SideEffects [] + + SeeAlso [] + + ***********************************************************************/ +void Abc_TruthRpoPerform(Rpo_TtStore_t * p, int nThreshold, int fVerbose) { + clock_t clk = clock(); + int i; + int rpoCount = 0; + Literal_t* lit; + float percent; + for (i = 0; i < p->nFuncs; i++) { +// if(i>1000) { +// continue; +// } +//// +// if(i!= 2196 ) { //5886 +// continue; +// } + if(fVerbose) { + Abc_Print(-2,"%d: ", i+1); + } + + lit = Rpo_Factorize((unsigned *) p->pFuncs[i], p->nVars, nThreshold, fVerbose); + if (lit != NULL) { + if(fVerbose) { + Abc_Print(-2, "Solution : %s\n", lit->expression->pArray); + Abc_Print(-2, "\n\n"); + } + Lit_Free(lit); + rpoCount++; + } else { + if(fVerbose) { + Abc_Print(-2, "null\n"); + Abc_Print(-2, "\n\n"); + } + } + } + percent = (rpoCount * 100.0) / p->nFuncs; + Abc_Print(-2,"%d of %d (%.2f %%) functions are RPO.\n", rpoCount,p->nFuncs,percent); + Abc_PrintTime(1, "Time", clock() - clk); +} + +/**Function************************************************************* + + Synopsis [Apply decomposition to truth tables.] + + Description [] + + SideEffects [] + + SeeAlso [] + + ***********************************************************************/ +void Abc_TruthRpoTest(char * pFileName, int nVarNum, int nThreshold, int fVerbose) { + Rpo_TtStore_t * p; + + // allocate data-structure +// if (fVerbose) { +// Abc_Print(-2, "Number of variables = %d\n", nVarNum); +// } + p = Abc_TtStoreLoad(pFileName, nVarNum); + + if (fVerbose) { + Abc_Print(-2, "Number of variables = %d\n", p->nVars); + } + // consider functions from the file + Abc_TruthRpoPerform(p, nThreshold, fVerbose); + + // delete data-structure + Abc_TtStoreFree(p, nVarNum); + // printf( "Finished decomposing truth tables from file \"%s\".\n", pFileName ); +} + +/**Function************************************************************* + + Synopsis [Testbench for decomposition algorithms.] + + Description [] + + SideEffects [] + + SeeAlso [] + + ***********************************************************************/ +int Abc_RpoTest(char * pFileName, int nVarNum,int nThreshold, int fVerbose) { + if (fVerbose) { + printf("Using truth tables from file \"%s\"...\n", pFileName); + } + Abc_TruthRpoTest(pFileName, nVarNum, nThreshold, fVerbose); + fflush(stdout); + return 0; +} + + +/////////////////////ert truth table to /////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + + diff --git a/src/base/abci/module.make b/src/base/abci/module.make index c7645775..5554ea93 100644 --- a/src/base/abci/module.make +++ b/src/base/abci/module.make @@ -55,6 +55,7 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcRestruct.c \ src/base/abci/abcResub.c \ src/base/abci/abcRewrite.c \ + src/base/abci/abcRpo.c \ src/base/abci/abcRr.c \ src/base/abci/abcSat.c \ src/base/abci/abcScorr.c \ diff --git a/src/base/main/mainInit.c b/src/base/main/mainInit.c index bbe0bbd1..bdf0613e 100644 --- a/src/base/main/mainInit.c +++ b/src/base/main/mainInit.c @@ -23,7 +23,7 @@ ABC_NAMESPACE_IMPL_START -//#define USE_ABC2 +#define USE_ABC2 //#define USE_ABC85 //////////////////////////////////////////////////////////////////////// diff --git a/src/bool/rpo/literal.h b/src/bool/rpo/literal.h new file mode 100644 index 00000000..2faf0981 --- /dev/null +++ b/src/bool/rpo/literal.h @@ -0,0 +1,297 @@ +/**CFile**************************************************************** + + FileName [literal.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [RPO] + + Synopsis [Literal structure] + + Author [Mayler G. A. Martins / Vinicius Callegaro] + + Affiliation [UFRGS] + + Date [Ver. 1.0. Started - May 08, 2013.] + + Revision [$Id: literal.h,v 1.00 2013/05/08 00:00:00 mgamartins Exp $] + + ***********************************************************************/ + +#ifndef ABC__bool__rpo__literal_h +#define ABC__bool__rpo__literal_h + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include +#include +#include "bool/kit/kit.h" +#include "misc/vec/vec.h" +#include "misc/util/abc_global.h" + +ABC_NAMESPACE_HEADER_START + + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +// associations +typedef enum { + LIT_NONE = 0, // 0: unknown + LIT_AND, // 1: AND association + LIT_OR, // 2: OR association + LIT_XOR // 3: XOR association (not used yet) +} Operator_t; + + +typedef struct Literal_t_ Literal_t; + +struct Literal_t_ { + unsigned * transition; + unsigned * function; + Vec_Str_t * expression; +}; + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Compute the positive transition] + + Description [The inputs are a function, the number of variables and a variable index and the output is a function] + + SideEffects [Should this function be in kitTruth.c ?] + + SeeAlso [] +// +***********************************************************************/ + +static inline void Lit_TruthPositiveTransition( unsigned * pIn, unsigned * pOut, int nVars, int varIdx ) +{ + unsigned * cof0 = ABC_ALLOC (unsigned, Kit_TruthWordNum(nVars) ); + unsigned * cof1 = ABC_ALLOC (unsigned, Kit_TruthWordNum(nVars) ); + unsigned * ncof0; + Kit_TruthCofactor0New(cof0, pIn,nVars,varIdx); + Kit_TruthCofactor1New(cof1, pIn,nVars,varIdx); + ncof0 = ABC_ALLOC (unsigned, Kit_TruthWordNum(nVars) ); + Kit_TruthNot(ncof0,cof0,nVars); + Kit_TruthAnd(pOut,ncof0,cof1, nVars); + ABC_FREE(cof0); + ABC_FREE(ncof0); + ABC_FREE(cof1); +} + + +/**Function************************************************************* + + Synopsis [Compute the negative transition] + + Description [The inputs are a function, the number of variables and a variable index and the output is a function] + + SideEffects [Should this function be in kitTruth.c ?] + + SeeAlso [] + +***********************************************************************/ + +static inline void Lit_TruthNegativeTransition( unsigned * pIn, unsigned * pOut, int nVars, int varIdx ) +{ + unsigned * cof0 = ABC_ALLOC (unsigned, Kit_TruthWordNum(nVars) ); + unsigned * cof1 = ABC_ALLOC (unsigned, Kit_TruthWordNum(nVars) ); + unsigned * ncof1; + Kit_TruthCofactor0New(cof0, pIn,nVars,varIdx); + Kit_TruthCofactor1New(cof1, pIn,nVars,varIdx); + ncof1 = ABC_ALLOC (unsigned, Kit_TruthWordNum(nVars) ); + Kit_TruthNot(ncof1,cof1,nVars); + Kit_TruthAnd(pOut,ncof1,cof0,nVars); + ABC_FREE(cof0); + ABC_FREE(cof1); + ABC_FREE(ncof1); +} + + +/**Function************************************************************* + + Synopsis [Create a literal given a polarity ] + + Description [The inputs are the function, index and its polarity and a the output is a literal] + + SideEffects [] + + SeeAlso [] + + ***********************************************************************/ + +static inline Literal_t* Lit_Alloc(unsigned* pTruth, int nVars, int varIdx, char pol) { + unsigned * transition; + unsigned * function; + Vec_Str_t * exp; + Literal_t* lit; + assert(pol == '+' || pol == '-'); + transition = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars)); + if (pol == '+') { + Lit_TruthPositiveTransition(pTruth, transition, nVars, varIdx); + } else { + Lit_TruthNegativeTransition(pTruth, transition, nVars, varIdx); + } + if (!Kit_TruthIsConst0(transition,nVars)) { + function = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars)); + Kit_TruthIthVar(function, nVars, varIdx); + //Abc_Print(-2, "Allocating function %X %d %c \n", *function, varIdx, pol); + exp = Vec_StrAlloc(5); + if (pol == '-') { + Kit_TruthNot(function, function, nVars); + Vec_StrPutC(exp, '!'); + } + Vec_StrPutC(exp, (char)('a' + varIdx)); + Vec_StrPutC(exp, '\0'); + lit = ABC_ALLOC(Literal_t, 1); + lit->function = function; + lit->transition = transition; + lit->expression = exp; + return lit; + } else { + ABC_FREE(transition); // free the function. + return NULL; + } +} + + +/**Function************************************************************* + + Synopsis [Group 2 literals using AND or OR] + + Description [] + + SideEffects [] + + SeeAlso [] + + ***********************************************************************/ + +static inline Literal_t* Lit_GroupLiterals(Literal_t* lit1, Literal_t* lit2, Operator_t op, int nVars) { + unsigned * newFunction = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars)); + unsigned * newTransition = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars)); + Vec_Str_t * newExp = Vec_StrAlloc(lit1->expression->nSize + lit2->expression->nSize + 3); + Literal_t* newLiteral; + char opChar = '%'; + switch (op) { + case LIT_AND: + { + //Abc_Print(-2, "Grouping AND %X %X \n", *lit1->function, *lit2->function); + Kit_TruthAnd(newFunction, lit1->function, lit2->function, nVars); + opChar = '*'; + break; + } + case LIT_OR: + { + //Abc_Print(-2, "Grouping OR %X %X \n", *lit1->function, *lit2->function); + Kit_TruthOr(newFunction, lit1->function, lit2->function, nVars); + opChar = '+'; + break; + } + default: + { + Abc_Print(-2, "Lit_GroupLiterals with op not defined."); + //TODO Call ABC Abort + } + } + + Kit_TruthOr(newTransition, lit1->transition, lit2->transition, nVars); + // create a new expression. + Vec_StrPutC(newExp, '('); + Vec_StrAppend(newExp, lit1->expression->pArray); + //Vec_StrPop(newExp); // pop the \0 + Vec_StrPutC(newExp, opChar); + Vec_StrAppend(newExp, lit2->expression->pArray); + //Vec_StrPop(newExp); // pop the \0 + Vec_StrPutC(newExp, ')'); + Vec_StrPutC(newExp, '\0'); + + newLiteral = ABC_ALLOC(Literal_t, 1); + newLiteral->function = newFunction; + newLiteral->transition = newTransition; + newLiteral->expression = newExp; + return newLiteral; +} + + +/**Function************************************************************* + + Synopsis [Create a const literal ] + + Description [] + + SideEffects [] + + SeeAlso [] + + ***********************************************************************/ + +static inline Literal_t* Lit_CreateLiteralConst(unsigned* pTruth, int nVars, int constant) { + Vec_Str_t * exp = Vec_StrAlloc(3); + Literal_t* lit; + Vec_StrPutC(exp, (char)('0' + constant)); + Vec_StrPutC(exp, '\0'); + lit = ABC_ALLOC(Literal_t, 1); + lit->expression = exp; + lit->function = pTruth; + lit->transition = pTruth; // wrong but no effect ### + return lit; +} + +static inline Literal_t* Lit_Copy(Literal_t* lit, int nVars) { + Literal_t* newLit = ABC_ALLOC(Literal_t,1); + newLit->function = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars)); + Kit_TruthCopy(newLit->function,lit->function,nVars); + newLit->transition = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars)); + Kit_TruthCopy(newLit->transition,lit->transition,nVars); + newLit->expression = Vec_StrDup(lit->expression); +// Abc_Print(-2,"Copying: %s\n",newLit->expression->pArray); + return newLit; +} + +static inline void Lit_PrintTT(unsigned* tt, int nVars) { + int w; + for(w=nVars-1; w>=0; w--) { + Abc_Print(-2, "%08X", tt[w]); + } +} + +static inline void Lit_PrintExp(Literal_t* lit) { + Abc_Print(-2, "%s", lit->expression->pArray); +} + +/**Function************************************************************* + + Synopsis [Delete the literal ] + + Description [] + + SideEffects [] + + SeeAlso [] + + ***********************************************************************/ + +static inline void Lit_Free(Literal_t * lit) { + if(lit == NULL) { + return; + } +// Abc_Print(-2,"Freeing: %s\n",lit->expression->pArray); + ABC_FREE(lit->function); + ABC_FREE(lit->transition); + Vec_StrFree(lit->expression); + ABC_FREE(lit); +} + +ABC_NAMESPACE_HEADER_END + +#endif /* LITERAL_H */ + diff --git a/src/bool/rpo/module.make b/src/bool/rpo/module.make new file mode 100644 index 00000000..5c07110c --- /dev/null +++ b/src/bool/rpo/module.make @@ -0,0 +1 @@ +SRC += src/bool/rpo/rpo.c \ No newline at end of file diff --git a/src/bool/rpo/rpo.c b/src/bool/rpo/rpo.c new file mode 100644 index 00000000..5311e107 --- /dev/null +++ b/src/bool/rpo/rpo.c @@ -0,0 +1,383 @@ +/**CFile**************************************************************** + + FileName [rpo.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [RPO] + + Synopsis [Performs read polarity once factorization.] + + Author [Mayler G. A. Martins / Vinicius Callegaro] + + Affiliation [UFRGS] + + Date [Ver. 1.0. Started - May 08, 2013.] + + Revision [$Id: rpo.c,v 1.00 2013/05/08 00:00:00 mgamartins Exp $] + + ***********************************************************************/ + +#include + +#include "literal.h" +#include "rpo.h" +#include "bool/kit/kit.h" +#include "misc/util/abc_global.h" +#include "misc/vec/vec.h" + + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + + +typedef struct Rpo_Man_t_ Rpo_Man_t; + +struct Rpo_Man_t_ { + unsigned * target; + int nVars; + + Literal_t ** literals; + int nLits; + int nLitsMax; + + Rpo_LCI_Edge_t* lci; + int nLCIElems; + + int thresholdMax; + +}; + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Check if two literals are AND-grouped] + + Description [] + + SideEffects [] + + SeeAlso [] + + ***********************************************************************/ +int Rpo_CheckANDGroup(Literal_t* lit1, Literal_t* lit2, int nVars) { + unsigned* notLit1Func = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars)); + unsigned* notLit2Func = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars)); + unsigned* and1; + unsigned* and2; + int isZero; + + Kit_TruthNot(notLit1Func, lit1->function, nVars); + Kit_TruthNot(notLit2Func, lit2->function, nVars); + and1 = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars)); + and2 = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars)); + Kit_TruthAnd(and1, lit1->transition, notLit2Func, nVars); + isZero = Kit_TruthIsConst0(and1, nVars); + if (isZero) { + Kit_TruthAnd(and2, lit2->transition, notLit1Func, nVars); + isZero = Kit_TruthIsConst0(and2, nVars); + } + ABC_FREE(notLit1Func); + ABC_FREE(notLit2Func); + ABC_FREE(and1); + ABC_FREE(and2); + return isZero; +} + +/**Function************************************************************* + + Synopsis [Check if two literals are AND-grouped] + + Description [] + + SideEffects [] + + SeeAlso [] + + ***********************************************************************/ +int Rpo_CheckORGroup(Literal_t* lit1, Literal_t* lit2, int nVars) { + unsigned* and1 = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars)); + unsigned* and2 = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars)); + int isZero; + Kit_TruthAnd(and1, lit1->transition, lit2->function, nVars); + isZero = Kit_TruthIsConst0(and1, nVars); + if (isZero) { + Kit_TruthAnd(and2, lit2->transition, lit1->function, nVars); + isZero = Kit_TruthIsConst0(and2, nVars); + } + ABC_FREE(and1); + ABC_FREE(and2); + return isZero; +} + +Rpo_LCI_Edge_t* Rpo_CreateEdge(Operator_t op, int i, int j, int* vertexDegree) { + Rpo_LCI_Edge_t* edge = ABC_ALLOC(Rpo_LCI_Edge_t, 1); + edge->connectionType = op; + edge->idx1 = i; + edge->idx2 = j; + edge->visited = 0; + vertexDegree[i]++; + vertexDegree[j]++; + return edge; +} + +int Rpo_computeMinEdgeCost(Rpo_LCI_Edge_t** edges, int edgeCount, int* vertexDegree) { + int minCostIndex = -1; + int minVertexIndex = -1; + unsigned int minCost = ~0; + Rpo_LCI_Edge_t* edge; + unsigned int edgeCost; + int minVertex; + int i; + for (i = 0; i < edgeCount; ++i) { + edge = edges[i]; + if (!edge->visited) { + edgeCost = vertexDegree[edge->idx1] + vertexDegree[edge->idx2]; + minVertex = (edge->idx1 < edge->idx2) ? edge->idx1 : edge->idx2; + if (edgeCost < minCost) { + minCost = edgeCost; + minCostIndex = i; + minVertexIndex = minVertex; + } else if ((edgeCost == minCost) && minVertex < minVertexIndex) { + minCost = edgeCost; + minCostIndex = i; + minVertexIndex = minVertex; + } + } + } + return minCostIndex; +} + +void Rpo_PrintEdge(Rpo_LCI_Edge_t* edge) { + Abc_Print(-2, "Edge (%d,%d)/%d\n", edge->idx1, edge->idx2, edge->connectionType); +} + +/**Function************************************************************* + + Synopsis [Test] + + Description [] + + SideEffects [] + + SeeAlso [] + + ***********************************************************************/ +Literal_t* Rpo_Factorize(unsigned* target, int nVars, int nThreshold, int verbose) { + + int nLitCap = nVars * 2; + int nLit = 0; + int w; + Literal_t** vecLit; + Literal_t* lit; + Literal_t* result; + int thresholdCount = 0; + + if (Kit_TruthIsConst0(target, nVars)) { + return Lit_CreateLiteralConst(target, nVars, 0); + } else if (Kit_TruthIsConst1(target, nVars)) { + return Lit_CreateLiteralConst(target, nVars, 1); + } + + // if (nThreshold == -1) { + // nThreshold = nLitCap + nVars; + // } + if (verbose) { + Abc_Print(-2, "Target: "); + Lit_PrintTT(target, nVars); + Abc_Print(-2, "\n"); + } + vecLit = ABC_ALLOC(Literal_t*, nLitCap); + + for (w = nVars - 1; w >= 0; w--) { + lit = Lit_Alloc(target, nVars, w, '+'); + if (lit != NULL) { + vecLit[nLit] = lit; + nLit++; + } + lit = Lit_Alloc(target, nVars, w, '-'); + if (lit != NULL) { + vecLit[nLit] = lit; + nLit++; + } + } + if (verbose) { + Abc_Print(-2, "Allocated %d literal clusters\n", nLit); + } + + result = Rpo_Recursion(target, vecLit, nLit, nLit, nVars, &thresholdCount, nThreshold, verbose); + + //freeing the memory + for (w = 0; w < nLit; ++w) { + Lit_Free(vecLit[w]); + } + ABC_FREE(vecLit); + + return result; + +} + +Literal_t* Rpo_Recursion(unsigned* target, Literal_t** vecLit, int nLit, int nLitCount, int nVars, int* thresholdCount, int thresholdMax, int verbose) { + int i, j, k; + Literal_t* copyResult; + int* vertexDegree; + int v; + int edgeSize; + Rpo_LCI_Edge_t** edges; + int edgeCount = 0; + int isAnd; + int isOr; + Rpo_LCI_Edge_t* edge; + Literal_t* result = NULL; + int edgeIndex; + int minLitIndex; + int maxLitIndex; + Literal_t* oldLit1; + Literal_t* oldLit2; + Literal_t* newLit; + + *thresholdCount = *thresholdCount + 1; + if (*thresholdCount == thresholdMax) { + return NULL; + } + if (verbose) { + Abc_Print(-2, "Entering recursion %d\n", *thresholdCount); + } + // verify if solution is the target or not + if (nLitCount == 1) { + if (verbose) { + Abc_Print(-2, "Checking solution: "); + } + for (k = 0; k < nLit; ++k) { + if (vecLit[k] != NULL) { + if (Kit_TruthIsEqual(target, vecLit[k]->function, nVars)) { + copyResult = Lit_Copy(vecLit[k], nVars); + if (verbose) { + Abc_Print(-2, "FOUND!\n", thresholdCount); + } + thresholdCount = 0; //?? + return copyResult; + } + } + } + if (verbose) { + Abc_Print(-2, "FAILED!\n", thresholdCount); + } + return NULL; + } + + vertexDegree = ABC_ALLOC(int, nLit); + // if(verbose) { + // Abc_Print(-2,"Allocating vertexDegree...\n"); + // } + for (v = 0; v < nLit; v++) { + vertexDegree[v] = 0; + } + // building edges + edgeSize = (nLit * (nLit - 1)) / 2; + edges = ABC_ALLOC(Rpo_LCI_Edge_t*, edgeSize); + if (verbose) { + Abc_Print(-2, "Creating Edges: \n"); + } + + for (i = 0; i < nLit; ++i) { + if (vecLit[i] == NULL) { + continue; + } + for (j = i; j < nLit; ++j) { + if (vecLit[j] == NULL) { + continue; + } + isAnd = Rpo_CheckANDGroup(vecLit[i], vecLit[j], nVars); + isOr = Rpo_CheckORGroup(vecLit[i], vecLit[j], nVars); + if (isAnd) { + if (verbose) { + Abc_Print(-2, "Grouped: "); + Lit_PrintExp(vecLit[j]); + Abc_Print(-2, " AND "); + Lit_PrintExp(vecLit[i]); + Abc_Print(-2, "\n"); + } + // add edge + edge = Rpo_CreateEdge(LIT_AND, i, j, vertexDegree); + edges[edgeCount++] = edge; + } + if (isOr) { + if (verbose) { + Abc_Print(-2, "Grouped: "); + Lit_PrintExp(vecLit[j]); + Abc_Print(-2, " OR "); + Lit_PrintExp(vecLit[i]); + Abc_Print(-2, "\n"); + } + // add edge + edge = Rpo_CreateEdge(LIT_OR, i, j, vertexDegree); + edges[edgeCount++] = edge; + } + } + } + if (verbose) { + Abc_Print(-2, "%d edges created.\n", edgeCount); + } + + + //traverse the edges, grouping new Literal Clusters + do { + edgeIndex = Rpo_computeMinEdgeCost(edges, edgeCount, vertexDegree); + if (edgeIndex < 0) { + if (verbose) { + Abc_Print(-2, "There is no edges unvisited... Exiting recursion.\n"); + //exit(-1); + } + break; + //return NULL; // the graph does not have unvisited edges + } + edge = edges[edgeIndex]; + edge->visited = 1; + //Rpo_PrintEdge(edge); + minLitIndex = (edge->idx1 < edge->idx2) ? edge->idx1 : edge->idx2; + maxLitIndex = (edge->idx1 > edge->idx2) ? edge->idx1 : edge->idx2; + oldLit1 = vecLit[minLitIndex]; + oldLit2 = vecLit[maxLitIndex]; + newLit = Lit_GroupLiterals(oldLit1, oldLit2, edge->connectionType, nVars); + vecLit[minLitIndex] = newLit; + vecLit[maxLitIndex] = NULL; + + if (verbose) { + Abc_Print(-2, "New Literal Cluster found: "); + Lit_PrintExp(newLit); + Abc_Print(-2, " -> "); + Lit_PrintTT(newLit->function, nVars); + Abc_Print(-2, "\n"); + } + result = Rpo_Recursion(target, vecLit, nLit, (nLitCount - 1), nVars, thresholdCount, thresholdMax, verbose); + //independent of result, free the newLit and restore the vector of Literal Clusters + Lit_Free(newLit); + vecLit[minLitIndex] = oldLit1; + vecLit[maxLitIndex] = oldLit2; + if (*thresholdCount == thresholdMax) { + break; + } + } while (result == NULL); + //freeing memory + // if(verbose) { + // Abc_Print(-2,"Freeing vertexDegree...\n"); + // } + ABC_FREE(vertexDegree); + for (i = 0; i < edgeCount; ++i) { + //Abc_Print(-2, "%p ", edges[i]); + ABC_FREE(edges[i]); + } + ABC_FREE(edges); + return result; +} + +ABC_NAMESPACE_IMPL_END \ No newline at end of file diff --git a/src/bool/rpo/rpo.h b/src/bool/rpo/rpo.h new file mode 100644 index 00000000..08f4a479 --- /dev/null +++ b/src/bool/rpo/rpo.h @@ -0,0 +1,57 @@ +/**CFile**************************************************************** + + FileName [rpo.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [RPO] + + Synopsis [Rpo Header] + + Author [Mayler G. A. Martins / Vinicius Callegaro] + + Affiliation [UFRGS] + + Date [Ver. 1.0. Started - May 08, 2013.] + + Revision [$Id: rpo.h,v 1.00 2013/05/08 00:00:00 mgamartins Exp $] + +***********************************************************************/ + +#ifndef ABC__bool__rpo__rpo_h +#define ABC__bool__rpo__rpo_h + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include "literal.h" + +ABC_NAMESPACE_HEADER_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Rpo_LCI_Edge_t_ Rpo_LCI_Edge_t; + +struct Rpo_LCI_Edge_t_ { + unsigned long visited : 1; + unsigned long connectionType : 2; + unsigned long reserved : 1; + unsigned long idx1 : 30; + unsigned long idx2 : 30; +}; + +void Rpo_PrintEdge(Rpo_LCI_Edge_t* edge); +int Rpo_CheckANDGroup(Literal_t* lit1, Literal_t* lit2, int nVars); +int Rpo_CheckORGroup(Literal_t* lit1, Literal_t* lit2, int nVars); +Literal_t* Rpo_Factorize(unsigned* target, int nVars, int nThreshold, int verbose); +Literal_t* Rpo_Recursion(unsigned* target, Literal_t** vecLit, int nLit, int nLitCount, int nVars, int* thresholdCount, int thresholdMax, int verbose); +Rpo_LCI_Edge_t* Rpo_CreateEdge(Operator_t op, int i, int j, int* vertexDegree); +int Rpo_computeMinEdgeCost(Rpo_LCI_Edge_t** edges, int edgeCount, int* vertexDegree); + +ABC_NAMESPACE_HEADER_END + +#endif + \ No newline at end of file -- cgit v1.2.3