Skip to content

A
abc
Commit 9b059e30 by Alan Mishchenko
Options

Version abc80315

parent ff6f0943
Showing with 90 additions and 22 deletions
src/aig/aig/aigInter.c
......@@ -143,7 +143,7 @@ void Aig_ManInterFast( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose )
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose )
Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fRelation, int fVerbose )
{
void * pSatCnf = NULL;
Inta_Man_t * pManInter;
......@@ -187,9 +187,10 @@ clk = clock();
sat_solver_store_mark_clauses_a( pSat );
// update the last clause
if ( fRelation )
{
extern int sat_solver_store_change_last( sat_solver * pSat );
// iLast = sat_solver_store_change_last( pSat );
iLast = sat_solver_store_change_last( pSat );
}
// add clauses of B
......@@ -207,7 +208,8 @@ clk = clock();
// add PI clauses
// collect the common variables
vVarsAB = Vec_IntAlloc( Aig_ManPiNum(pManOn) );
// Vec_IntPush( vVarsAB, iLast );
if ( fRelation )
Vec_IntPush( vVarsAB, iLast );
Aig_ManForEachPi( pManOn, pObj, i )
{
......
src/aig/bdc/bdcCore.c
......@@ -44,7 +44,7 @@ Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars )
Bdc_Man_t * p;
p = ALLOC( Bdc_Man_t, 1 );
memset( p, 0, sizeof(Bdc_Man_t) );
assert( pPars->nVarsMax > 3 && pPars->nVarsMax < 16 );
assert( pPars->nVarsMax > 2 && pPars->nVarsMax < 16 );
p->pPars = pPars;
p->nWords = Kit_TruthWordNum( pPars->nVarsMax );
p->nDivsLimit = 200;
......
src/base/abci/abc.c
......@@ -6809,24 +6809,29 @@ usage:
int Abc_CommandInter( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes, * pNtk1, * pNtk2;
Abc_Ntk_t * pNtk, * pNtk1, * pNtk2, * pNtkRes = NULL;
char ** pArgvNew;
int nArgcNew;
int c, fDelete1, fDelete2;
int fRelation;
int fVerbose;
extern Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose );
extern Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fRelation, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
fRelation = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "rvh" ) ) != EOF )
{
switch ( c )
{
case 'r':
fRelation ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
......@@ -6843,10 +6848,19 @@ int Abc_CommandInter( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
if ( nArgcNew == 0 )
{
Abc_Obj_t * pObj;
int i;
printf( "Deriving new circuit structure for the current network.\n" );
Abc_ObjXorFaninC( Abc_NtkPo(pNtk2,0), 0 );
Abc_NtkForEachPo( pNtk2, pObj, i )
Abc_ObjXorFaninC( pObj, 0 );
}
if ( fRelation && Abc_NtkCoNum(pNtk1) != 1 )
{
printf( "Computation of interplants as a relation only works for single-output functions.\n" );
printf( "Use command \"cone\" to extract one output cone from the multi-output network.\n" );
}
pNtkRes = Abc_NtkInter( pNtk1, pNtk2, fVerbose );
else
pNtkRes = Abc_NtkInter( pNtk1, pNtk2, fRelation, fVerbose );
if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
......@@ -6859,10 +6873,26 @@ int Abc_CommandInter( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: inter [-vh] <fileOnSet> <fileOffSet>\n" );
fprintf( pErr, "\t derives interpolant of two networks (onset and offset)\n" );
fprintf( pErr, "usage: inter [-rvh] <onset.blif> <offset.blif>\n" );
fprintf( pErr, "\t derives interpolant of two networks representing onset and offset;\n" );
fprintf( pErr, "\t-r : toggle computing interpolant as a relation [default = %s]\n", fRelation? "yes": "no" );
fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
fprintf( pErr, "\t \n" );
fprintf( pErr, "\t Comments:\n" );
fprintf( pErr, "\t \n" );
fprintf( pErr, "\t The networks given on the command line should have the same CIs/COs.\n" );
fprintf( pErr, "\t If only one network is given on the command line, this network\n" );
fprintf( pErr, "\t is assumed to be the offset, while the current network is the onset.\n" );
fprintf( pErr, "\t If no network is given on the command line, the current network is\n" );
fprintf( pErr, "\t assumed to be the onset and its complement is taken to be the offset.\n" );
fprintf( pErr, "\t The resulting interpolant is stored as the current network.\n" );
fprintf( pErr, "\t To verify that the interpolant agrees with the onset and the offset,\n" );
fprintf( pErr, "\t save it in file \"inter.blif\" and run the following:\n" );
fprintf( pErr, "\t (a) \"miter -i <onset.blif> <inter.blif>; iprove\"\n" );
fprintf( pErr, "\t (b) \"miter -i <inter.blif> <offset_inv.blif>; iprove\"\n" );
fprintf( pErr, "\t where <offset_inv.blif> is the network derived by complementing the\n" );
fprintf( pErr, "\t outputs of <offset.blif>: \"r <onset.blif>; st -i; w <offset_inv.blif>\"\n" );
return 1;
}
......
src/base/abci/abcDar.c
......@@ -1530,14 +1530,14 @@ Abc_Ntk_t * Abc_NtkDarEnlarge( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkInterOne( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose )
Abc_Ntk_t * Abc_NtkInterOne( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fRelation, int fVerbose )
{
extern Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose );
extern Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fRelation, int fVerbose );
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pManOn, * pManOff, * pManAig;
if ( Abc_NtkCoNum(pNtkOn) != 1 || Abc_NtkCoNum(pNtkOff) != 1 )
{
printf( "Currently works only for single output networks.\n" );
printf( "Currently works only for single-output networks.\n" );
return NULL;
}
if ( Abc_NtkCiNum(pNtkOn) != Abc_NtkCiNum(pNtkOff) )
......@@ -1553,7 +1553,7 @@ Abc_Ntk_t * Abc_NtkInterOne( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbo
if ( pManOff == NULL )
return NULL;
// derive the interpolant
pManAig = Aig_ManInter( pManOn, pManOff, fVerbose );
pManAig = Aig_ManInter( pManOn, pManOff, fRelation, fVerbose );
if ( pManAig == NULL )
{
printf( "Interpolant computation failed.\n" );
......@@ -1561,8 +1561,15 @@ Abc_Ntk_t * Abc_NtkInterOne( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbo
}
Aig_ManStop( pManOn );
Aig_ManStop( pManOff );
// for the relation, add an extra input
if ( fRelation )
{
Abc_Obj_t * pObj;
pObj = Abc_NtkCreatePi( pNtkOff );
Abc_ObjAssignName( pObj, "New", NULL );
}
// create logic network
pNtkAig = Abc_NtkFromDar( pNtkOn, pManAig );
pNtkAig = Abc_NtkFromDar( pNtkOff, pManAig );
Aig_ManStop( pManAig );
return pNtkAig;
}
......@@ -1609,7 +1616,7 @@ int timeInt;
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose )
Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fRelation, int fVerbose )
{
Abc_Ntk_t * pNtkOn1, * pNtkOff1, * pNtkInter1, * pNtkInter;
Abc_Obj_t * pObj;
......@@ -1623,7 +1630,7 @@ Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose
// Abc_NtkInterFast( pNtkOn, pNtkOff, fVerbose );
// consider the case of one output
if ( Abc_NtkCoNum(pNtkOn) == 1 )
return Abc_NtkInterOne( pNtkOn, pNtkOff, fVerbose );
return Abc_NtkInterOne( pNtkOn, pNtkOff, fRelation, fVerbose );
// start the new newtork
pNtkInter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
pNtkInter->pName = Extra_UtilStrsav(pNtkOn->pName);
......@@ -1652,7 +1659,7 @@ timeInt = 0;
Abc_ObjXorFaninC( Abc_NtkPo(pNtkInter1, 0), 0 );
}
else
pNtkInter1 = Abc_NtkInterOne( pNtkOn1, pNtkOff1, fVerbose );
pNtkInter1 = Abc_NtkInterOne( pNtkOn1, pNtkOff1, 0, fVerbose );
if ( pNtkInter1 )
{
Abc_NtkAppend( pNtkInter, pNtkInter1, 1 );
......
src/base/abci/abcDelay.c
......@@ -566,7 +566,7 @@ Abc_Ntk_t * Abc_NtkSpeedup( Abc_Ntk_t * pNtk, int fUseLutLib, int Percentage, in
if ( !fVeryVerbose && nTimeCris == 0 )
continue;
Counter++;
// count the total number of timingn critical second-generation nodes
// count the total number of timing critical second-generation nodes
Vec_PtrClear( vTimeCries );
if ( nTimeCris )
{
......@@ -602,6 +602,35 @@ Abc_Ntk_t * Abc_NtkSpeedup( Abc_Ntk_t * pNtk, int fUseLutLib, int Percentage, in
// add the node to choices
if ( Vec_PtrSize(vTimeCries) == 0 || Vec_PtrSize(vTimeCries) > Degree )
continue;
// order the fanins in the increasing order of criticalily
if ( Vec_PtrSize(vTimeCries) > 1 )
{
pFanin = Vec_PtrEntry( vTimeCries, 0 );
pFanin2 = Vec_PtrEntry( vTimeCries, 1 );
if ( Abc_ObjSlack(pFanin) < Abc_ObjSlack(pFanin2) )
{
Vec_PtrWriteEntry( vTimeCries, 0, pFanin2 );
Vec_PtrWriteEntry( vTimeCries, 1, pFanin );
}
}
if ( Vec_PtrSize(vTimeCries) > 2 )
{
pFanin = Vec_PtrEntry( vTimeCries, 1 );
pFanin2 = Vec_PtrEntry( vTimeCries, 2 );
if ( Abc_ObjSlack(pFanin) < Abc_ObjSlack(pFanin2) )
{
Vec_PtrWriteEntry( vTimeCries, 1, pFanin2 );
Vec_PtrWriteEntry( vTimeCries, 2, pFanin );
}
pFanin = Vec_PtrEntry( vTimeCries, 0 );
pFanin2 = Vec_PtrEntry( vTimeCries, 1 );
if ( Abc_ObjSlack(pFanin) < Abc_ObjSlack(pFanin2) )
{
Vec_PtrWriteEntry( vTimeCries, 0, pFanin2 );
Vec_PtrWriteEntry( vTimeCries, 1, pFanin );
}
}
// add choice
Abc_NtkSpeedupNode( pNtk, pNtkNew, pNode, vTimeFanins, vTimeCries );
}
Vec_PtrFree( vTimeCries );
......
src/base/io/io.c
......@@ -825,7 +825,7 @@ int IoCommandReadTruth( Abc_Frame_t * pAbc, int argc, char ** argv )
pSopCover = Abc_SopFromTruthHex(argv[globalUtilOptind]);
else
pSopCover = Abc_SopFromTruthBin(argv[globalUtilOptind]);
if ( pSopCover == NULL )
if ( pSopCover == NULL || pSopCover[0] == 0 )
{
fprintf( pAbc->Err, "Reading truth table has failed.\n" );
return 1;
......
src/sat/bsat/satInterA.c
......@@ -947,7 +947,7 @@ void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in
if ( fVerbose )
{
PRT( "Interpo", clock() - clkTotal );
// PRT( "Interpo", clock() - clkTotal );
printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f Mb\n",
p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,
1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots),
......
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