summaryrefslogtreecommitdiffstats
path: root/src/base/abci
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/abci')
-rw-r--r--src/base/abci/abc.c241
-rw-r--r--src/base/abci/abcDsd.c2
-rw-r--r--src/base/abci/abcExtract.c51
-rw-r--r--src/base/abci/abcFpgaFast.c141
-rw-r--r--src/base/abci/abcIvy.c83
-rw-r--r--src/base/abci/abcMini.c1
-rw-r--r--src/base/abci/abcNtbdd.c3
-rw-r--r--src/base/abci/abcPrint.c4
-rw-r--r--src/base/abci/abcProve.c23
-rw-r--r--src/base/abci/abcSat.c35
-rw-r--r--src/base/abci/abcVerify.c22
-rw-r--r--src/base/abci/module.make4
12 files changed, 526 insertions, 84 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 2427146c..b25ca2f7 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -117,6 +117,7 @@ static int Abc_CommandSuperChoice ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandSuperChoiceLut ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFpga ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFpgaFast ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPga ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandScut ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -246,6 +247,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "SC mapping", "scl", Abc_CommandSuperChoiceLut, 1 );
Cmd_CommandAdd( pAbc, "FPGA mapping", "fpga", Abc_CommandFpga, 1 );
+ Cmd_CommandAdd( pAbc, "FPGA mapping", "ffpga", Abc_CommandFpgaFast, 1 );
Cmd_CommandAdd( pAbc, "FPGA mapping", "pga", Abc_CommandPga, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "scut", Abc_CommandScut, 0 );
@@ -4007,6 +4009,7 @@ int Abc_CommandOneOutput( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
}
+ pNodeCo = NULL;
if ( argc == globalUtilOptind + 1 )
{
pNode = Abc_NtkFindNode( pNtk, argv[globalUtilOptind] );
@@ -4827,7 +4830,7 @@ usage:
int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
- Abc_Ntk_t * pNtk, * pNtkRes;
+ Abc_Ntk_t * pNtk, * pNtkRes;//, * pNtkTemp;
int c;
int nLutMax;
int nPlaMax;
@@ -4844,13 +4847,13 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- nLutMax = 6;
+ nLutMax = 8;
nPlaMax = 128;
RankCost = 96000;
fFastMode = 1;
fRewriting = 0;
fSynthesis = 0;
- fVerbose = 1;
+ fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "LPRfrsvh" ) ) != EOF )
{
@@ -4927,8 +4930,17 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
*/
// run the command
// pNtkRes = Abc_NtkXyz( pNtk, nPlaMax, 1, 0, fInvs, fVerbose );
- pNtkRes = Abc_NtkPlayer( pNtk, nLutMax, nPlaMax, RankCost, fFastMode, fRewriting, fSynthesis, fVerbose );
-// pNtkRes = NULL;
+/*
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ pNtkTemp = Abc_NtkStrash( pNtk, 0, 1 );
+ pNtkRes = Abc_NtkPlayer( pNtkTemp, nLutMax, nPlaMax, RankCost, fFastMode, fRewriting, fSynthesis, fVerbose );
+ Abc_NtkDelete( pNtkTemp );
+ }
+ else
+ pNtkRes = Abc_NtkPlayer( pNtk, nLutMax, nPlaMax, RankCost, fFastMode, fRewriting, fSynthesis, fVerbose );
+*/
+ pNtkRes = NULL;
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
@@ -5537,10 +5549,10 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
- int c, fUpdateLevel, fVerbose;
+ int c, fProve, fVerbose;
int nConfLimit;
- extern Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose );
+ extern Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fProve, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -5548,10 +5560,10 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
nConfLimit = 100;
- fUpdateLevel = 1;
+ fProve = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Clzvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Cpvh" ) ) != EOF )
{
switch ( c )
{
@@ -5566,8 +5578,8 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nConfLimit < 0 )
goto usage;
break;
- case 'l':
- fUpdateLevel ^= 1;
+ case 'p':
+ fProve ^= 1;
break;
case 'v':
fVerbose ^= 1;
@@ -5589,7 +5601,7 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- pNtkRes = Abc_NtkIvyFraig( pNtk, nConfLimit, fVerbose );
+ pNtkRes = Abc_NtkIvyFraig( pNtk, nConfLimit, fProve, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
@@ -5600,10 +5612,10 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: ifraig [-C num] [-vh]\n" );
+ fprintf( pErr, "usage: ifraig [-C num] [-pvh]\n" );
fprintf( pErr, "\t performs fraiging using a new method\n" );
- fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
-// fprintf( pErr, "\t-l : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
+ fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
+ fprintf( pErr, "\t-p : toggle proving miter outputs [default = %s]\n", fProve? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
@@ -5622,29 +5634,31 @@ usage:
***********************************************************************/
int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv )
{
+ Prove_Params_t Params, * pParams = &Params;
FILE * pOut, * pErr;
- Abc_Ntk_t * pNtk, * pNtkRes;
- int c, fUpdateLevel, fVerbose;
+ Abc_Ntk_t * pNtk, * pNtkTemp;
+ int c, clk, RetValue;
- extern Abc_Ntk_t * Abc_NtkIvyProve( Abc_Ntk_t * pNtk );
+ extern int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- fUpdateLevel = 1;
- fVerbose = 0;
+ Prove_ParamsSetDefault( pParams );
+ pParams->fUseRewriting = 1;
+ pParams->fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "lzvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "rvh" ) ) != EOF )
{
switch ( c )
{
- case 'l':
- fUpdateLevel ^= 1;
+ case 'r':
+ pParams->fUseRewriting ^= 1;
break;
case 'v':
- fVerbose ^= 1;
+ pParams->fVerbose ^= 1;
break;
case 'h':
goto usage;
@@ -5663,21 +5677,43 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- pNtkRes = Abc_NtkIvyProve( pNtk );
- if ( pNtkRes == NULL )
+
+ clk = clock();
+
+ if ( Abc_NtkIsStrash(pNtk) )
+ pNtkTemp = Abc_NtkDup( pNtk );
+ else
+ pNtkTemp = Abc_NtkStrash( pNtk, 0, 0 );
+
+ RetValue = Abc_NtkIvyProve( &pNtkTemp, pParams );
+
+ // verify that the pattern is correct
+ if ( RetValue == 0 )
{
- fprintf( pErr, "Command has failed.\n" );
- return 0;
+ int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pNtkTemp->pModel );
+ if ( pSimInfo[0] != 1 )
+ printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" );
+ free( pSimInfo );
}
+
+ if ( RetValue == -1 )
+ printf( "UNDECIDED " );
+ else if ( RetValue == 0 )
+ printf( "SATISFIABLE " );
+ else
+ printf( "UNSATISFIABLE " );
+ //printf( "\n" );
+
+ PRT( "Time", clock() - clk );
// replace the current network
- Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkTemp );
return 0;
usage:
- fprintf( pErr, "usage: iprove [-h]\n" );
+ fprintf( pErr, "usage: iprove [-rvh]\n" );
fprintf( pErr, "\t performs CEC using a new method\n" );
-// fprintf( pErr, "\t-l : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
-// fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-r : toggle AIG rewriting [default = %s]\n", pParams->fUseRewriting? "yes": "no" );
+ fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pParams->fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
@@ -6932,6 +6968,147 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandFpgaFast( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ char Buffer[100];
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk, * pNtkRes;
+ int c;
+ int fRecovery;
+ int fVerbose;
+ int nLutSize;
+ float DelayTarget;
+
+ extern Abc_Ntk_t * Abc_NtkFpgaFast( Abc_Ntk_t * pNtk, int nLutSize, int fRecovery, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ fRecovery = 1;
+ fVerbose = 0;
+ DelayTarget =-1;
+ nLutSize = 8;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "avhDK" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'a':
+ fRecovery ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ case 'D':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-D\" should be followed by a floating point number.\n" );
+ goto usage;
+ }
+ DelayTarget = (float)atof(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( DelayTarget <= 0.0 )
+ goto usage;
+ break;
+ case 'K':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-K\" should be followed by a positive integer.\n" );
+ goto usage;
+ }
+ nLutSize = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nLutSize < 0 )
+ goto usage;
+ break;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+
+ if ( Abc_NtkIsSeq(pNtk) )
+ {
+ fprintf( pErr, "Cannot FPGA map a sequential AIG.\n" );
+ return 1;
+ }
+
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ // strash and balance the network
+ pNtk = Abc_NtkStrash( pNtk, 0, 0 );
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Strashing before FPGA mapping has failed.\n" );
+ return 1;
+ }
+ pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0, 0, 1 );
+ Abc_NtkDelete( pNtkRes );
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Balancing before FPGA mapping has failed.\n" );
+ return 1;
+ }
+ fprintf( pOut, "The network was strashed and balanced before FPGA mapping.\n" );
+ // get the new network
+ pNtkRes = Abc_NtkFpgaFast( pNtk, nLutSize, fRecovery, fVerbose );
+ if ( pNtkRes == NULL )
+ {
+ Abc_NtkDelete( pNtk );
+ fprintf( pErr, "FPGA mapping has failed.\n" );
+ return 1;
+ }
+ Abc_NtkDelete( pNtk );
+ }
+ else
+ {
+ // get the new network
+ pNtkRes = Abc_NtkFpgaFast( pNtk, nLutSize, fRecovery, fVerbose );
+ if ( pNtkRes == NULL )
+ {
+ fprintf( pErr, "FPGA mapping has failed.\n" );
+ return 1;
+ }
+ }
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ return 0;
+
+usage:
+ if ( DelayTarget == -1 )
+ sprintf( Buffer, "not used" );
+ else
+ sprintf( Buffer, "%.2f", DelayTarget );
+ fprintf( pErr, "usage: ffpga [-K num] [-avh]\n" );
+ fprintf( pErr, "\t performs fast FPGA mapping of the current network\n" );
+ fprintf( pErr, "\t-a : toggles area recovery [default = %s]\n", fRecovery? "yes": "no" );
+// fprintf( pErr, "\t-D float : sets the required time for the mapping [default = %s]\n", Buffer );
+ fprintf( pErr, "\t-K num : the number of LUT inputs (2 < num < 32) [default = %d]\n", nLutSize );
+ fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : prints the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandPga( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c
index cd8f9047..6708217c 100644
--- a/src/base/abci/abcDsd.c
+++ b/src/base/abci/abcDsd.c
@@ -172,7 +172,7 @@ void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t *
int i, nNodesDsd;
// save the CI nodes in the DSD nodes
- Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)Abc_AigConst1(pNtkNew) );
+ Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)Abc_NodeCreateConst1(pNtkNew) );
Abc_NtkForEachCi( pNtk, pNode, i )
{
pNodeDsd = Dsd_ManagerReadInput( pManDsd, i );
diff --git a/src/base/abci/abcExtract.c b/src/base/abci/abcExtract.c
new file mode 100644
index 00000000..52ea03a3
--- /dev/null
+++ b/src/base/abci/abcExtract.c
@@ -0,0 +1,51 @@
+/**CFile****************************************************************
+
+ FileName [abcMvCost.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Calculating the cost of one MV block.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abcMvCost.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_MvCostTest( Abc_Ntk_t * pNtk )
+{
+
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcFpgaFast.c b/src/base/abci/abcFpgaFast.c
index 2d5813c7..b307273f 100644
--- a/src/base/abci/abcFpgaFast.c
+++ b/src/base/abci/abcFpgaFast.c
@@ -19,11 +19,20 @@
***********************************************************************/
#include "abc.h"
+#include "ivy.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+extern Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc );
+
+static Abc_Ntk_t * Ivy_ManFpgaToAbc( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan );
+static Abc_Obj_t * Ivy_ManToAbcFast_rec( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Ivy_Obj_t * pObjIvy, Vec_Int_t * vNodes );
+
+static inline void Abc_ObjSetIvy2Abc( Ivy_Man_t * p, int IvyId, Abc_Obj_t * pObjAbc ) { assert(Vec_PtrEntry(p->pCopy, IvyId) == NULL); assert(!Abc_ObjIsComplement(pObjAbc)); Vec_PtrWriteEntry( p->pCopy, IvyId, pObjAbc ); }
+static inline Abc_Obj_t * Abc_ObjGetIvy2Abc( Ivy_Man_t * p, int IvyId ) { return Vec_PtrEntry( p->pCopy, IvyId ); }
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -43,25 +52,20 @@
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkFpgaFast( Abc_Ntk_t * pNtk, int nLutSize, int fVerbose )
+Abc_Ntk_t * Abc_NtkFpgaFast( Abc_Ntk_t * pNtk, int nLutSize, int fRecovery, int fVerbose )
{
+ Ivy_Man_t * pMan;
Abc_Ntk_t * pNtkNew;
- Abc_Obj_t * pObj;
- int i;
-
// make sure the network is an AIG
assert( Abc_NtkIsStrash(pNtk) );
-
- // iterate over the nodes in the network
- Abc_NtkForEachNode( pNtk, pObj, i )
- {
- }
-
- // create the new network after mapping
- pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
-
- // here we need to create nodes of the new network
-
+ // convert the network into the AIG
+ pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
+ // perform fast FPGA mapping
+ Ivy_FastMapPerform( pMan, nLutSize, fRecovery, fVerbose );
+ // convert back into the ABC network
+ pNtkNew = Ivy_ManFpgaToAbc( pNtk, pMan );
+ Ivy_FastMapStop( pMan );
+ Ivy_ManStop( pMan );
// make sure that the final network passes the test
if ( pNtkNew != NULL && !Abc_NtkCheck( pNtkNew ) )
{
@@ -72,6 +76,113 @@ Abc_Ntk_t * Abc_NtkFpgaFast( Abc_Ntk_t * pNtk, int nLutSize, int fVerbose )
return pNtkNew;
}
+/**Function*************************************************************
+
+ Synopsis [Constructs the ABC network after mapping.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Ivy_ManFpgaToAbc( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan )
+{
+ Abc_Ntk_t * pNtkNew;
+ Abc_Obj_t * pObjAbc, * pObj;
+ Ivy_Obj_t * pObjIvy;
+ Vec_Int_t * vNodes;
+ int i;
+ // start mapping from Ivy into Abc
+ pMan->pCopy = Vec_PtrStart( Ivy_ManObjIdMax(pMan) + 1 );
+ // start the new ABC network
+ pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_AIG );
+ // transfer the pointers to the basic nodes
+ Abc_ObjSetIvy2Abc( pMan, Ivy_ManConst1(pMan)->Id, Abc_NodeCreateConst1(pNtkNew) );
+ Abc_NtkForEachCi( pNtkNew, pObjAbc, i )
+ Abc_ObjSetIvy2Abc( pMan, Ivy_ManPi(pMan, i)->Id, pObjAbc );
+ // recursively construct the network
+ vNodes = Vec_IntAlloc( 100 );
+ Ivy_ManForEachPo( pMan, pObjIvy, i )
+ {
+ // get the new ABC node corresponding to the old fanin of the PO in IVY
+ pObjAbc = Ivy_ManToAbcFast_rec( pNtkNew, pMan, Ivy_ObjFanin0(pObjIvy), vNodes );
+ // consider the case of complemented fanin of the PO
+ if ( Ivy_ObjFaninC0(pObjIvy) ) // complement
+ {
+ if ( Abc_ObjIsCi(pObjAbc) )
+ pObjAbc = Abc_NodeCreateInv( pNtkNew, pObjAbc );
+ else
+ {
+ // clone the node
+ pObj = Abc_NtkCloneObj( pObjAbc );
+ // set complemented functions
+ pObj->pData = Aig_Not( pObjAbc->pData );
+ // return the new node
+ pObjAbc = pObj;
+ }
+ }
+ Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjAbc );
+ }
+ Vec_IntFree( vNodes );
+ Vec_PtrFree( pMan->pCopy );
+ pMan->pCopy = NULL;
+ // remove dangling nodes
+ Abc_NtkCleanup( pNtkNew, 0 );
+ // fix CIs feeding directly into COs
+ Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
+ return pNtkNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Recursively construct the new node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Obj_t * Ivy_ManToAbcFast_rec( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Ivy_Obj_t * pObjIvy, Vec_Int_t * vNodes )
+{
+ Vec_Int_t Supp, * vSupp = &Supp;
+ Abc_Obj_t * pObjAbc, * pFaninAbc;
+ Ivy_Obj_t * pNodeIvy;
+ int i, Entry;
+ // skip the node if it is a constant or already processed
+ pObjAbc = Abc_ObjGetIvy2Abc( pMan, pObjIvy->Id );
+ if ( pObjAbc )
+ return pObjAbc;
+ assert( Ivy_ObjIsAnd(pObjIvy) || Ivy_ObjIsExor(pObjIvy) );
+ // get the support of K-LUT
+ Ivy_FastMapReadSupp( pMan, pObjIvy, vSupp );
+ // create new ABC node and its fanins
+ pObjAbc = Abc_NtkCreateNode( pNtkNew );
+ Vec_IntForEachEntry( vSupp, Entry, i )
+ {
+ pFaninAbc = Ivy_ManToAbcFast_rec( pNtkNew, pMan, Ivy_ManObj(pMan, Entry), vNodes );
+ Abc_ObjAddFanin( pObjAbc, pFaninAbc );
+ }
+ // collect the nodes used in the cut
+ Ivy_ManCollectCut( pMan, pObjIvy, vSupp, vNodes );
+ // create the local function
+ Ivy_ManForEachNodeVec( pMan, vNodes, pNodeIvy, i )
+ {
+ if ( i < Vec_IntSize(vSupp) )
+ pNodeIvy->pEquiv = (Ivy_Obj_t *)Aig_IthVar( pNtkNew->pManFunc, i );
+ else
+ pNodeIvy->pEquiv = (Ivy_Obj_t *)Aig_And( pNtkNew->pManFunc, (Aig_Obj_t *)Ivy_ObjChild0Equiv(pNodeIvy), (Aig_Obj_t *)Ivy_ObjChild1Equiv(pNodeIvy) );
+ }
+ // set the local function
+ pObjAbc->pData = (Abc_Obj_t *)pObjIvy->pEquiv;
+ // set the node
+ Abc_ObjSetIvy2Abc( pMan, pObjIvy->Id, pObjAbc );
+ return pObjAbc;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 320c76dd..82e03119 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -21,6 +21,7 @@
#include "abc.h"
#include "dec.h"
#include "ivy.h"
+#include "fraig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -81,7 +82,7 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )
return NULL;
}
}
- if ( Abc_NtkCountSelfFeedLatches(pNtk) )
+ if ( fSeq && Abc_NtkCountSelfFeedLatches(pNtk) )
{
printf( "Warning: The network has %d self-feeding latches. Quitting.\n", Abc_NtkCountSelfFeedLatches(pNtk) );
return NULL;
@@ -368,7 +369,7 @@ Abc_Ntk_t * Abc_NtkIvySat( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose )
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose )
+Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fProve, int fVerbose )
{
Ivy_FraigParams_t Params, * pParams = &Params;
Abc_Ntk_t * pNtkAig;
@@ -379,6 +380,7 @@ Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose )
Ivy_FraigParamsDefault( pParams );
pParams->nBTLimitNode = nConfLimit;
pParams->fVerbose = fVerbose;
+ pParams->fProve = fProve;
pMan = Ivy_FraigPerform( pTemp = pMan, pParams );
Ivy_ManStop( pTemp );
pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
@@ -394,23 +396,76 @@ Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose )
SideEffects []
- SeeAlso []
+ SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkIvyProve( Abc_Ntk_t * pNtk )
+int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
{
- Ivy_FraigParams_t Params, * pParams = &Params;
- Abc_Ntk_t * pNtkAig;
- Ivy_Man_t * pMan, * pTemp;
+ Prove_Params_t * pParams = pPars;
+ Abc_Ntk_t * pNtk = *ppNtk, * pNtkTemp;
+ Ivy_Man_t * pMan;
+ int RetValue;
+ assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsLogic(pNtk) );
+ // experiment with various parameters settings
+// pParams->fUseBdds = 1;
+// pParams->fBddReorder = 1;
+// pParams->nTotalBacktrackLimit = 10000;
+
+ // strash the network if it is not strashed already
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ pNtk = Abc_NtkStrash( pNtkTemp = pNtk, 0, 1 );
+ Abc_NtkDelete( pNtkTemp );
+ }
+
+ // if SAT only, solve without iteration
+ RetValue = Abc_NtkMiterSat( pNtk, 2*(sint64)pParams->nMiteringLimitStart, (sint64)0, 0, 0, NULL, NULL );
+ if ( RetValue >= 0 )
+ return RetValue;
+
+ // apply AIG rewriting
+ if ( pParams->fUseRewriting && Abc_NtkNodeNum(pNtk) > 500 )
+ {
+ pParams->fUseRewriting = 0;
+ Abc_NtkRewrite( pNtk, 0, 0, 0 );
+ pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );
+ Abc_NtkDelete( pNtkTemp );
+ Abc_NtkRewrite( pNtk, 0, 0, 0 );
+ Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
+ }
+
+ // convert ABC network into IVY network
pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
- if ( pMan == NULL )
- return NULL;
- Ivy_FraigParamsDefault( pParams );
- pMan = Ivy_FraigProve( pTemp = pMan, pParams );
- Ivy_ManStop( pTemp );
- pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
+ // solve the CEC problem
+ RetValue = Ivy_FraigProve( &pMan, pParams );
+ // convert IVY network into ABC network
+ pNtk = Abc_NtkIvyAfter( pNtkTemp = pNtk, pMan, 0, 0 );
+ Abc_NtkDelete( pNtkTemp );
+ // transfer model if given
+ pNtk->pModel = pMan->pData; pMan->pData = NULL;
Ivy_ManStop( pMan );
- return pNtkAig;
+
+ // try to prove it using brute force SAT
+ if ( RetValue < 0 && pParams->fUseBdds )
+ {
+ if ( pParams->fVerbose )
+ {
+ printf( "Attempting BDDs with node limit %d ...\n", pParams->nBddSizeLimit );
+ fflush( stdout );
+ }
+ pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0 );
+ if ( pNtk )
+ {
+ Abc_NtkDelete( pNtkTemp );
+ RetValue = ( (Abc_NtkNodeNum(pNtk) == 1) && (Abc_ObjFanin0(Abc_NtkPo(pNtk,0))->pData == Cudd_ReadLogicZero(pNtk->pManFunc)) );
+ }
+ else
+ pNtk = pNtkTemp;
+ }
+
+ // return the result
+ *ppNtk = pNtk;
+ return RetValue;
}
/**Function*************************************************************
diff --git a/src/base/abci/abcMini.c b/src/base/abci/abcMini.c
index 037f058a..014eafd3 100644
--- a/src/base/abci/abcMini.c
+++ b/src/base/abci/abcMini.c
@@ -59,6 +59,7 @@ Abc_Ntk_t * Abc_NtkMiniBalance( Abc_Ntk_t * pNtk )
}
// perform balance
Aig_ManPrintStats( pMan );
+// Aig_ManDumpBlif( pMan, "aig_temp.blif" );
pMan = Aig_ManBalance( pTemp = pMan, 1 );
Aig_ManStop( pTemp );
Aig_ManPrintStats( pMan );
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index 9a88db99..9b67ab13 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -189,7 +189,6 @@ Abc_Obj_t * Abc_NodeBddToMuxes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew )
// create the table mapping BDD nodes into the ABC nodes
tBdd2Node = st_init_table( st_ptrcmp, st_ptrhash );
// add the constant and the elementary vars
- st_insert( tBdd2Node, (char *)b1, (char *)Abc_AigConst1(pNtkNew) );
Abc_ObjForEachFanin( pNodeOld, pFaninOld, i )
st_insert( tBdd2Node, (char *)Cudd_bddIthVar(dd, i), (char *)pFaninOld->pCopy );
// create the new nodes recursively
@@ -215,6 +214,8 @@ Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t *
{
Abc_Obj_t * pNodeNew, * pNodeNew0, * pNodeNew1, * pNodeNewC;
assert( !Cudd_IsComplement(bFunc) );
+ if ( bFunc == b1 )
+ return Abc_NodeCreateConst1(pNtkNew);
if ( st_lookup( tBdd2Node, (char *)bFunc, (char **)&pNodeNew ) )
return pNodeNew;
// solve for the children nodes
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index c7e2acc0..afc635e9 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -144,7 +144,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
}
*/
-
+/*
// print the statistic into a file
{
FILE * pTable;
@@ -157,7 +157,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
fprintf( pTable, "\n" );
fclose( pTable );
}
-
+*/
/*
// print the statistic into a file
diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c
index f3c1a825..c9e5bfd7 100644
--- a/src/base/abci/abcProve.c
+++ b/src/base/abci/abcProve.c
@@ -314,6 +314,29 @@ void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose
PRT( pString, clock() - clk );
}
+
+/**Function*************************************************************
+
+ Synopsis [Implements resynthesis for CEC.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkMiterRwsat( Abc_Ntk_t * pNtk )
+{
+ Abc_Ntk_t * pNtkTemp;
+ Abc_NtkRewrite( pNtk, 0, 0, 0 );
+ pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 ); Abc_NtkDelete( pNtkTemp );
+ Abc_NtkRewrite( pNtk, 0, 0, 0 );
+ Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
+ return pNtk;
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 3e0d6ba0..8d5dd2a7 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -56,8 +56,8 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int
assert( Abc_NtkIsStrash(pNtk) );
assert( Abc_NtkLatchNum(pNtk) == 0 );
- if ( Abc_NtkPoNum(pNtk) > 1 )
- fprintf( stdout, "Warning: The miter has %d outputs. SAT will try to prove all of them.\n", Abc_NtkPoNum(pNtk) );
+// if ( Abc_NtkPoNum(pNtk) > 1 )
+// fprintf( stdout, "Warning: The miter has %d outputs. SAT will try to prove all of them.\n", Abc_NtkPoNum(pNtk) );
// load clauses into the solver
clk = clock();
@@ -180,6 +180,29 @@ int Abc_NtkClauseTriv( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
SeeAlso []
***********************************************************************/
+int Abc_NtkClauseTop( solver * pSat, Vec_Ptr_t * vNodes, Vec_Int_t * vVars )
+{
+ Abc_Obj_t * pNode;
+ int i;
+//printf( "Adding triv %d. %d\n", Abc_ObjRegular(pNode)->Id, (int)pSat->solver_stats.clauses );
+ vVars->nSize = 0;
+ Vec_PtrForEachEntry( vNodes, pNode, i )
+ Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->pCopy, Abc_ObjIsComplement(pNode) ) );
+// Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->Id, Abc_ObjIsComplement(pNode) ) );
+ return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds trivial clause.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_NtkClauseAnd( solver * pSat, Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, Vec_Int_t * vVars )
{
int fComp1, Var, Var1, i;
@@ -467,8 +490,8 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
Vec_PtrPush( vNodes, pNode );
}
*/
-
// collect the nodes that need clauses and top-level assignments
+ Vec_PtrClear( vSuper );
Abc_NtkForEachCo( pNtk, pNode, i )
{
// get the fanin
@@ -481,9 +504,11 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
Vec_PtrPush( vNodes, pFanin );
}
// add the trivial clause
- if ( !Abc_NtkClauseTriv( pSat, Abc_ObjChild0(pNode), vVars ) )
- goto Quits;
+ Vec_PtrPush( vSuper, Abc_ObjChild0(pNode) );
}
+ if ( !Abc_NtkClauseTop( pSat, vSuper, vVars ) )
+ goto Quits;
+
// add the clauses
Vec_PtrForEachEntry( vNodes, pNode, i )
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 1fddc8cb..622b4103 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -174,7 +174,8 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
// solve the CNF using the SAT solver
Prove_ParamsSetDefault( pParams );
pParams->nItersMax = 5;
- RetValue = Abc_NtkMiterProve( &pMiter, pParams );
+// RetValue = Abc_NtkMiterProve( &pMiter, pParams );
+ RetValue = Abc_NtkIvyProve( &pMiter, pParams );
if ( RetValue == -1 )
printf( "Networks are undecided (resource limits is reached).\n" );
else if ( RetValue == 0 )
@@ -399,12 +400,11 @@ int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk, int nFrames )
SideEffects []
- SeeAlso []
+ SeeAlso []
***********************************************************************/
int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel )
{
- Vec_Ptr_t * vNodes;
Abc_Obj_t * pNode;
int * pValues, Value0, Value1, i;
int fStrashed = 0;
@@ -416,22 +416,16 @@ int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel )
// increment the trav ID
Abc_NtkIncrementTravId( pNtk );
// set the CI values
+ Abc_AigConst1(pNtk)->pCopy = (void *)1;
Abc_NtkForEachCi( pNtk, pNode, i )
pNode->pCopy = (void *)pModel[i];
// simulate in the topological order
- vNodes = Abc_NtkDfs( pNtk, 1 );
- Vec_PtrForEachEntry( vNodes, pNode, i )
+ Abc_NtkForEachNode( pNtk, pNode, i )
{
-// if ( Abc_NodeIsConst(pNode) )
-// pNode->pCopy = NULL;
-// else
- {
- Value0 = ((int)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode);
- Value1 = ((int)Abc_ObjFanin1(pNode)->pCopy) ^ Abc_ObjFaninC1(pNode);
- pNode->pCopy = (void *)(Value0 & Value1);
- }
+ Value0 = ((int)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode);
+ Value1 = ((int)Abc_ObjFanin1(pNode)->pCopy) ^ Abc_ObjFaninC1(pNode);
+ pNode->pCopy = (void *)(Value0 & Value1);
}
- Vec_PtrFree( vNodes );
// fill the output values
pValues = ALLOC( int, Abc_NtkCoNum(pNtk) );
Abc_NtkForEachCo( pNtk, pNode, i )
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index dba9e6fd..bb2ae1a0 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -7,12 +7,16 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcCut.c \
src/base/abci/abcDsd.c \
src/base/abci/abcEspresso.c \
+ src/base/abci/abcExtract.c \
src/base/abci/abcFpga.c \
+ src/base/abci/abcFpgaFast.c \
src/base/abci/abcFraig.c \
src/base/abci/abcFxu.c \
src/base/abci/abcGen.c \
+ src/base/abci/abcIvy.c \
src/base/abci/abcLut.c \
src/base/abci/abcMap.c \
+ src/base/abci/abcMini.c \
src/base/abci/abcMiter.c \
src/base/abci/abcNtbdd.c \
src/base/abci/abcOrder.c \
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-16 22:21:41 +0000