summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abci/abc.c78
-rw-r--r--src/base/abci/abcRpo.c442
-rw-r--r--src/base/abci/module.make1
-rw-r--r--src/base/main/mainInit.c2
4 files changed, 522 insertions, 1 deletions
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 <unistd.h>
@@ -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 <num>] [-vh] <file>\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 <num> : the number of support variables (binary files only) [default = unused]\n");
+ Abc_Print(-2, "\t-T <num> : 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<file> : 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 <num> 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
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-16 20:11:51 +0000