Skip to content

A
abc
Commit b288bac6 by Alan Mishchenko
Options

Version abc90807 

committer: Baruch Sterin <baruchs@gmail.com>
parent da65e88e
Showing with 157 additions and 23 deletions
src/aig/cec/cec.h
......@@ -135,6 +135,7 @@ struct Cec_ParCor_t_
int fUseCSat; // use circuit-based solver
// int fFirstStop; // stop on the first sat output
int fUseSmartCnf; // use smart CNF computation
int fVerboseFlops; // verbose stats
int fVeryVerbose; // verbose stats
int fVerbose; // verbose stats
};
......
src/aig/cec/cecCorr.c
......@@ -990,6 +990,39 @@ unsigned * Cec_ManComputeInitState( Gia_Man_t * pAig, int nFrames )
/**Function*************************************************************
Synopsis [Prints flop equivalences.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cec_ManPrintFlopEquivs( Gia_Man_t * p )
{
Gia_Obj_t * pObj, * pRepr;
int i;
assert( p->vNamesIn != NULL );
Gia_ManForEachRo( p, pObj, i )
{
if ( Gia_ObjIsConst(p, Gia_ObjId(p, pObj)) )
printf( "Flop \"%s\" is equivalent to constant 0.\n", Vec_PtrEntry(p->vNamesIn, Gia_ObjCioId(pObj)) );
else if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
{
if ( Gia_ObjIsCi(pRepr) )
printf( "Flop \"%s\" is equivalent to flop \"%s\".\n",
Vec_PtrEntry( p->vNamesIn, Gia_ObjCioId(pObj) ),
Vec_PtrEntry( p->vNamesIn, Gia_ObjCioId(pRepr) ) );
else
printf( "Flop \"%s\" is equivalent to internal node %d.\n",
Vec_PtrEntry( p->vNamesIn, Gia_ObjCioId(pObj) ), Gia_ObjId(p, pRepr) );
}
}
}
/**Function*************************************************************
Synopsis [Top-level procedure for register correspondence.]
Description []
......@@ -1060,6 +1093,14 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
}
if ( pPars->nPrefix && (Gia_ManAndNum(pNew) < Gia_ManAndNum(pAig) || Gia_ManRegNum(pNew) < Gia_ManRegNum(pAig)) )
printf( "The reduced AIG was produced using %d-th invariants and will not verify.\n", pPars->nPrefix );
// print verbose info about equivalences
if ( pPars->fVerboseFlops )
{
if ( pAig->vNamesIn == NULL )
printf( "Flop output names are not available. Use command \"&get -n\".\n" );
else
Cec_ManPrintFlopEquivs( pAig );
}
return pNew;
}
......
src/aig/gia/gia.h
......@@ -136,6 +136,8 @@ struct Gia_Man_t_
unsigned char* pSwitching; // switching activity for each object
Gia_Plc_t * pPlacement; // placement of the objects
int * pTravIds; // separate traversal ID representation
Vec_Ptr_t * vNamesIn; // the input names
Vec_Ptr_t * vNamesOut; // the output names
};
......
src/aig/gia/giaMan.c
......@@ -66,6 +66,8 @@ Gia_Man_t * Gia_ManStart( int nObjsMax )
***********************************************************************/
void Gia_ManStop( Gia_Man_t * p )
{
Vec_PtrFreeFree( p->vNamesIn );
Vec_PtrFreeFree( p->vNamesOut );
if ( p->vFlopClasses )
Vec_IntFree( p->vFlopClasses );
Vec_IntFree( p->vCis );
......
src/base/abci/abc.c
......@@ -609,7 +609,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC8", "*cec", Abc_CommandAbc8Cec, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*dsec", Abc_CommandAbc8DSec, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&get", Abc_CommandAbc9Get, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&put", Abc_CommandAbc9Put, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&r", Abc_CommandAbc9Read, 0 );
......@@ -22299,14 +22299,20 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
extern Aig_Man_t * Abc_NtkToDarChoices( Abc_Ntk_t * pNtk );
extern Vec_Ptr_t * Abc_NtkCollectCiNames( Abc_Ntk_t * pNtk );
extern Vec_Ptr_t * Abc_NtkCollectCoNames( Abc_Ntk_t * pNtk );
Gia_Man_t * pAig;
Aig_Man_t * pMan;
int c, fVerbose = 0;
int fNames = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "nvh" ) ) != EOF )
{
switch ( c )
{
case 'n':
fNames ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
......@@ -22343,11 +22349,17 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pAbc->pAig )
Gia_ManStop( pAbc->pAig );
pAbc->pAig = pAig;
if ( fNames )
{
pAig->vNamesIn = Abc_NtkCollectCiNames( pAbc->pNtkCur );
pAig->vNamesOut = Abc_NtkCollectCoNames( pAbc->pNtkCur );
}
return 0;
usage:
fprintf( stdout, "usage: &get [-vh] <file>\n" );
fprintf( stdout, "\t transfer the current network from the old ABC\n" );
fprintf( stdout, "usage: &get [-nvh] <file>\n" );
fprintf( stdout, "\t converts the network into an AIG and moves to the new ABC\n" );
fprintf( stdout, "\t-n : toggles saving CI/CO names of the AIG [default = %s]\n", fNames? "yes": "no" );
fprintf( stdout, "\t-v : toggles additional verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
fprintf( stdout, "\t<file> : the file name\n");
......@@ -24058,7 +24070,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Cec_ManCorSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FCPrecvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "FCPrecwvh" ) ) != EOF )
{
switch ( c )
{
......@@ -24104,6 +24116,9 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'c':
pPars->fUseCSat ^= 1;
break;
case 'w':
pPars->fVerboseFlops ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
......@@ -24127,7 +24142,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( stdout, "usage: &scorr [-FCP num] [-recvh]\n" );
fprintf( stdout, "usage: &scorr [-FCP num] [-recwvh]\n" );
fprintf( stdout, "\t performs signal correpondence computation\n" );
fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
fprintf( stdout, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames );
......@@ -24135,6 +24150,7 @@ usage:
fprintf( stdout, "\t-r : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" );
fprintf( stdout, "\t-e : toggle using equivalences as choices [default = %s]\n", pPars->fMakeChoices? "yes": "no" );
fprintf( stdout, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" );
fprintf( stdout, "\t-w : toggle printing verbose info about equivalent flops [default = %s]\n", pPars->fVerboseFlops? "yes": "no" );
fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
return 1;
......
src/base/abci/abcDar.c
......@@ -587,6 +587,50 @@ Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
/**Function*************************************************************
Synopsis [Collects CI of the network.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Abc_NtkCollectCiNames( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pObj;
int i;
Vec_Ptr_t * vNames;
vNames = Vec_PtrAlloc( 100 );
Abc_NtkForEachCi( pNtk, pObj, i )
Vec_PtrPush( vNames, Extra_UtilStrsav(Abc_ObjName(pObj)) );
return vNames;
}
/**Function*************************************************************
Synopsis [Collects CO of the network.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Abc_NtkCollectCoNames( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pObj;
int i;
Vec_Ptr_t * vNames;
vNames = Vec_PtrAlloc( 100 );
Abc_NtkForEachCo( pNtk, pObj, i )
Vec_PtrPush( vNames, Extra_UtilStrsav(Abc_ObjName(pObj)) );
return vNames;
}
/**Function*************************************************************
Synopsis [Collect latch values.]
Description []
......
src/base/abci/abcMap.c
......@@ -263,7 +263,12 @@ Abc_Obj_t * Abc_NodeFromMap_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNodeMap, int
// check the case of constant node
if ( Map_NodeIsConst(pNodeMap) )
return fPhase? Abc_NtkCreateNodeConst1(pNtkNew) : Abc_NtkCreateNodeConst0(pNtkNew);
{
pNodeNew = fPhase? Abc_NtkCreateNodeConst1(pNtkNew) : Abc_NtkCreateNodeConst0(pNtkNew);
if ( pNodeNew->pData == NULL )
printf( "Error creating mapped network: Library does not have a constant %d gate.\n", fPhase );
return pNodeNew;
}
// check if the phase is already implemented
pNodeNew = (Abc_Obj_t *)Map_NodeReadData( pNodeMap, fPhase );
......
src/base/main/main.c
......@@ -17,7 +17,7 @@
Revision [$Id: main.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "mainInt.h"
// this line should be included in the library project
......
src/map/super/superGate.c
......@@ -706,7 +706,7 @@ void Super_TranferGatesToArray( Super_Man_t * pMan )
{
stmm_generator * gen;
Super_Gate_t * pGate, * pList;
unsigned Key;
ABC_PTRUINT_T Key;
// put the gates fron the table into the array
ABC_FREE( pMan->pGates );
......@@ -734,10 +734,10 @@ void Super_TranferGatesToArray( Super_Man_t * pMan )
void Super_AddGateToTable( Super_Man_t * pMan, Super_Gate_t * pGate )
{
Super_Gate_t ** ppList;
unsigned Key;
ABC_PTRUINT_T Key;
// Key = pGate->uTruth[0] + 2003 * pGate->uTruth[1];
Key = pGate->uTruth[0] ^ pGate->uTruth[1];
if ( !stmm_find_or_add( pMan->tTable, (char *)(ABC_PTRUINT_T)Key, (char ***)&ppList ) )
if ( !stmm_find_or_add( pMan->tTable, (char *)Key, (char ***)&ppList ) )
*ppList = NULL;
pGate->pNext = *ppList;
*ppList = pGate;
......@@ -761,7 +761,7 @@ bool Super_CompareGates( Super_Man_t * pMan, unsigned uTruth[], float Area, floa
{
Super_Gate_t ** ppList, * pPrev, * pGate, * pGate2;
int i, fNewIsBetter, fGateIsBetter;
unsigned Key;
ABC_PTRUINT_T Key;
// skip constant functions
if ( pMan->nVarsMax < 6 )
......@@ -778,7 +778,7 @@ bool Super_CompareGates( Super_Man_t * pMan, unsigned uTruth[], float Area, floa
// get hold of the place where the entry is stored
// Key = uTruth[0] + 2003 * uTruth[1];
Key = uTruth[0] ^ uTruth[1];
if ( !stmm_find( pMan->tTable, (char *)(ABC_PTRUINT_T)Key, (char ***)&ppList ) )
if ( !stmm_find( pMan->tTable, (char *)Key, (char ***)&ppList ) )
return 1;
// the entry with this truth table is found
pPrev = NULL;
......@@ -918,7 +918,7 @@ void Super_Write( Super_Man_t * pMan )
Super_Gate_t * pGateRoot, * pGate;
stmm_generator * gen;
int fZeroFound, clk, v;
unsigned Key;
ABC_PTRUINT_T Key;
if ( pMan->nGates < 1 )
{
......
src/misc/nm/nmApi.c
......@@ -118,7 +118,8 @@ char * Nm_ManStoreIdName( Nm_Man_t * p, int ObjId, int Type, char * pName, char
}
// create a new entry
nEntrySize = sizeof(Nm_Entry_t) + strlen(pName) + (pSuffix?strlen(pSuffix):0) + 1;
nEntrySize = (nEntrySize / 4 + ((nEntrySize % 4) > 0)) * 4;
// nEntrySize = (nEntrySize / 4 + ((nEntrySize % 4) > 0)) * 4;
nEntrySize = (nEntrySize / 8 + ((nEntrySize % 8) > 0)) * 8;
pEntry = (Nm_Entry_t *)Extra_MmFlexEntryFetch( p->pMem, nEntrySize );
pEntry->pNextI2N = pEntry->pNextN2I = pEntry->pNameSake = NULL;
pEntry->ObjId = ObjId;
......
src/misc/vec/vecPtr.h
......@@ -465,6 +465,27 @@ static inline void Vec_PtrClear( Vec_Ptr_t * p )
/**Function*************************************************************
Synopsis [Deallocates array of memory pointers.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_PtrFreeFree( Vec_Ptr_t * p )
{
void * pTemp;
int i;
if ( p == NULL ) return;
Vec_PtrForEachEntry( p, pTemp, i )
ABC_FREE( pTemp );
Vec_PtrFree( p );
}
/**Function*************************************************************
Synopsis [Copies the interger array.]
Description []
......
src/opt/mfs/mfsCore.c
......@@ -266,7 +266,7 @@ clk = clock();
return 1;
}
clk = clock();
Abc_NtkMfsConstructGia( p );
// Abc_NtkMfsConstructGia( p );
p->timeGia += clock() - clk;
// solve the SAT problem
if ( p->pPars->fPower )
......@@ -280,7 +280,7 @@ p->timeGia += clock() - clk;
Abc_NtkMfsResubNode2( p, pNode );
}
p->timeSat += clock() - clk;
Abc_NtkMfsDeconstructGia( p );
// Abc_NtkMfsDeconstructGia( p );
return 1;
}
......
src/opt/mfs/mfsResub.c
......@@ -99,16 +99,17 @@ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands )
{
unsigned * pData;
int RetValue, iVar, i;
int clk = clock(), RetValue2 = Abc_NtkMfsTryResubOnceGia( p, pCands, nCands );
p->timeGia += clock() - clk;
// int clk = clock(), RetValue2 = Abc_NtkMfsTryResubOnceGia( p, pCands, nCands );
//p->timeGia += clock() - clk;
p->nSatCalls++;
RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
// assert( RetValue == l_False || RetValue == l_True );
if ( RetValue != l_Undef && RetValue2 != -1 )
{
assert( (RetValue == l_False) == (RetValue2 == 1) );
}
// if ( RetValue != l_Undef && RetValue2 != -1 )
// {
// assert( (RetValue == l_False) == (RetValue2 == 1) );
// }
if ( RetValue == l_False )
return 1;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment