Skip to content

A
abc
Commit 9d09f583 by Alan Mishchenko
Options

Version abc80610

parent 9604ecb1
Showing with 1067 additions and 239 deletions
Makefile
......@@ -24,7 +24,9 @@ MODULES := src/base/abc src/base/abci src/base/cmd \
default: $(PROG)
#OPTFLAGS := -DNDEBUG -O3
#OPTFLAGS := -DNDEBUG -O3 -DLIN
#OPTFLAGS := -DNDEBUG -O3 -DLIN64
#OPTFLAGS := -g -O -DLIN
OPTFLAGS := -g -O -DLIN64
CFLAGS += -Wall -Wno-unused-function $(OPTFLAGS) $(patsubst %, -I%, $(MODULES))
......
abc.dsp
......@@ -3294,6 +3294,10 @@ SOURCE=.\src\aig\saig\saigIoa.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigMiter.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigPhase.c
# End Source File
# Begin Source File
......
abctestlib.dsw deleted 100644 → 0
Microsoft Developer Studio Workspace File, Format Version 6.00
# WARNING: DO NOT EDIT OR DELETE THIS WORKSPACE FILE!
###############################################################################
Project: "abctestlib"=.\abctestlib.dsp - Package Owner=<4>
Package=<5>
{{{
}}}
Package=<4>
{{{
}}}
###############################################################################
Global:
Package=<5>
{{{
}}}
Package=<3>
{{{
}}}
###############################################################################
readme
Often the code comes directly from a Windows computer.
The following steps may be needed to compile it on UNIX:
Modify Makefile to have -DLIN (for 32-bits) or -DLIN64 (for 64-bits)
>> dos2unix Makefile Makefile
>> dos2unix depends.sh depends.sh
>> chmod 755 depends.sh
......
readmeaig 0 → 100644
Using AIG Package in ABC
- Download the latest snapshot of ABC
- Compile the code found in "abc\src\aig\aig", "abc\src\aig\saig", and "abc\src\misc\vec" as a static library.
- Link the library to the project.
- Add #include "saig.h".
- Start the AIG package using Aig_ManStart().
- Assign primary inputs using Aig_ObjCreatePi().
- Assign register outputs using Aig_ObjCreatePi().
(it is important to create all PIs first, before creating register outputs).
- Construct AIG in the topological order using Aig_And(), Aig_Or(), Aig_Not(), etc.
- If constant-0/1 AIG nodes are needed, use Aig_ManConst0() or Aig_ManConst1()
- Create primary outputs using Aig_ObjCreatePo().
- Create register inputs using Aig_ObjCreatePo().
(it is important to create all POs first, before creating register inputs).
- Set the number of registers by calling Aig_ManSetRegNum().
- Remove dangling AIG nodes (produced by structural hashing) using Aig_ManCleanup().
- Call the consistency checking procedure Aig_ManCheck().
- Dump AIG into a file using the new BLIF dumper Saig_ManDumpBlif().
- For each object in the design annotated with the constructed AIG node (pNode), remember its AIG node ID by calling Aig_ObjId( Aig_Regular(pNode) ). To check whether the corresponding AIG node is complemented use Aig_IsComplement(pNode).
- Quit the AIG package using Aig_ManStop().
The above process should not produce memory leaks.
src/aig/aig/aigScl.c
......@@ -591,10 +591,11 @@ void Aig_ManComputeSccs( Aig_Man_t * p )
Aig_Man_t * Aig_ManScl( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int fVerbose )
{
extern void Saig_ManReportUselessRegisters( Aig_Man_t * pAig );
extern int Saig_ManReportComplements( Aig_Man_t * p );
Aig_Man_t * pAigInit, * pAigNew;
Aig_Obj_t * pFlop1, * pFlop2;
int i, Entry1, Entry2, nTruePis;
int i, Entry1, Entry2, nTruePis;//, nRegs;
// store the original AIG
assert( pAig->vFlopNums == NULL );
pAigInit = pAig;
......@@ -627,6 +628,11 @@ Aig_Man_t * Aig_ManScl( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int
Aig_ManSeqCleanup( pAigNew );
Saig_ManReportUselessRegisters( pAigNew );
if ( Aig_ManRegNum(pAigNew) == 0 )
return pAigNew;
// nRegs = Saig_ManReportComplements( pAigNew );
// if ( nRegs )
// printf( "The number of complemented registers = %d.\n", nRegs );
return pAigNew;
}
......
src/aig/bbr/bbr.h
......@@ -74,7 +74,7 @@ extern void Aig_ManFreeGlobalBdds( Aig_Man_t * p, DdManager * dd );
extern int Aig_ManSizeOfGlobalBdds( Aig_Man_t * p );
extern DdManager * Aig_ManComputeGlobalBdds( Aig_Man_t * p, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose );
/*=== bbrReach.c ==========================================================*/
extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent );
#ifdef __cplusplus
}
......
src/aig/bbr/bbrReach.c
......@@ -203,7 +203,7 @@ DdNode ** Aig_ManCreatePartitions( DdManager * dd, Aig_Man_t * p, int fReorder,
SeeAlso []
***********************************************************************/
int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, DdNode * bInitial, DdNode ** pbOutputs, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose )
int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, DdNode * bInitial, DdNode ** pbOutputs, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent )
{
int fInternalReorder = 0;
Bbr_ImageTree_t * pTree;
......@@ -231,6 +231,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
free( pbVarsY );
if ( pTree == NULL )
{
if ( !fSilent )
printf( "BDDs blew up during qualitification scheduling. " );
return -1;
}
......@@ -247,6 +248,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
bNext = Bbr_bddImageCompute2( pTree2, bCurrent );
if ( bNext == NULL )
{
if ( !fSilent )
printf( "BDDs blew up during image computation. " );
if ( fPartition )
Bbr_bddImageTreeDelete( pTree );
......@@ -271,6 +273,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
{
if ( !Cudd_bddLeq( dd, bNext, Cudd_Not(pbOutputs[i]) ) )
{
if ( !fSilent )
printf( "Output %d was asserted in frame %d. ", i, nIters );
Cudd_RecursiveDeref( dd, bReached );
bReached = NULL;
......@@ -326,9 +329,11 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
Cudd_RecursiveDeref( dd, bReached );
if ( nIters > nIterMax || Cudd_DagSize(bReached) > nBddMax )
{
if ( !fSilent )
printf( "Verified only for states reachable in %d frames. ", nIters );
return -1; // undecided
}
if ( !fSilent )
printf( "The miter is proved unreachable after %d iterations. ", nIters );
return 1; // unreachable
}
......@@ -344,7 +349,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
SeeAlso []
***********************************************************************/
int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose )
int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent )
{
DdManager * dd;
DdNode ** pbParts, ** pbOutputs;
......@@ -357,6 +362,7 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fParti
dd = Aig_ManComputeGlobalBdds( p, nBddMax, 1, fReorder, fVerbose );
if ( dd == NULL )
{
if ( !fSilent )
printf( "The number of intermediate BDD nodes exceeded the limit (%d).\n", nBddMax );
return -1;
}
......@@ -378,6 +384,7 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fParti
{
if ( !Cudd_bddLeq( dd, bInitial, Cudd_Not(pbOutputs[i]) ) )
{
if ( !fSilent )
printf( "The miter output %d is proved REACHABLE in the initial state. ", i );
RetValue = 0;
break;
......@@ -385,7 +392,7 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fParti
}
// explore reachable states
if ( RetValue == -1 )
RetValue = Aig_ManComputeReachable( dd, p, pbParts, bInitial, pbOutputs, nBddMax, nIterMax, fPartition, fReorder, fVerbose );
RetValue = Aig_ManComputeReachable( dd, p, pbParts, bInitial, pbOutputs, nBddMax, nIterMax, fPartition, fReorder, fVerbose, fSilent );
// cleanup
Cudd_RecursiveDeref( dd, bInitial );
......@@ -401,8 +408,11 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fParti
Bbr_StopManager( dd );
// report the runtime
if ( !fSilent )
{
PRT( "Time", clock() - clk );
fflush( stdout );
}
return RetValue;
}
......
src/aig/cnf/cnf.h
......@@ -139,7 +139,7 @@ extern void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus );
extern void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable );
extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable );
extern void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit );
extern void Cnf_DataWriteOrClause( void * pSat, Cnf_Dat_t * pCnf );
extern int Cnf_DataWriteOrClause( void * pSat, Cnf_Dat_t * pCnf );
/*=== cnfMap.c ========================================================*/
extern void Cnf_DeriveMapping( Cnf_Man_t * p );
extern int Cnf_ManMapForCnf( Cnf_Man_t * p );
......
src/aig/cnf/cnfMan.c
......@@ -362,7 +362,7 @@ void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit )
SeeAlso []
***********************************************************************/
void Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf )
int Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf )
{
sat_solver * pSat = p;
Aig_Obj_t * pObj;
......@@ -371,8 +371,12 @@ void Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf )
Aig_ManForEachPo( pCnf->pMan, pObj, i )
pLits[i] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
if ( !sat_solver_addclause( pSat, pLits, pLits + Aig_ManPoNum(pCnf->pMan) ) )
assert( 0 );
{
free( pLits );
return 0;
}
free( pLits );
return 1;
}
////////////////////////////////////////////////////////////////////////
......
src/aig/fra/fra.h
......@@ -104,6 +104,7 @@ struct Fra_Ssw_t_
int fWriteImps; // write implications into a file
int fUse1Hot; // use one-hotness constraints
int fVerbose; // enable verbose output
int fSilent; // disable any output
int nIters; // the number of iterations performed
float TimeLimit; // the runtime budget for this call
};
......@@ -121,6 +122,7 @@ struct Fra_Sec_t_
int fInterpolation; // enables interpolation
int fReachability; // enables BDD based reachability
int fStopOnFirstFail; // enables stopping after first output of a miter has failed to prove
int fSilent; // disables all output
int fVerbose; // enables verbose reporting of statistics
int fVeryVerbose; // enables very verbose reporting
int TimeLimit; // enables the timeout
......
src/aig/fra/fraCec.c
......@@ -53,19 +53,22 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVe
// derive CNF
pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) );
// pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) );
// convert into the SAT solver
// convert into SAT solver
pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
// add the OR clause for the outputs
Cnf_DataWriteOrClause( pSat, pCnf );
vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
Cnf_DataFree( pCnf );
// solve SAT
if ( pSat == NULL )
{
Vec_IntFree( vCiIds );
// printf( "Trivially unsat\n" );
Cnf_DataFree( pCnf );
return 1;
}
// add the OR clause for the outputs
if ( !Cnf_DataWriteOrClause( pSat, pCnf ) )
{
sat_solver_delete( pSat );
Cnf_DataFree( pCnf );
return 1;
}
vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
Cnf_DataFree( pCnf );
// printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
......
src/aig/fra/fraInd.c
......@@ -422,6 +422,7 @@ PRT( "Time", clock() - clk );
if ( pParams->TimeLimit != 0.0 && clock() > TimeToStop )
{
if ( !pParams->fSilent )
printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" );
goto finish;
}
......@@ -452,6 +453,7 @@ PRT( "Time", clock() - clk );
if ( pParams->TimeLimit != 0.0 && clock() > TimeToStop )
{
if ( !pParams->fSilent )
printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" );
goto finish;
}
......
src/aig/fra/fraSec.c
......@@ -53,11 +53,12 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p )
p->fInterpolation = 1; // enables interpolation
p->fReachability = 1; // enables BDD based reachability
p->fStopOnFirstFail = 1; // enables stopping after first output of a miter has failed to prove
p->fSilent = 0; // disables all output
p->fVerbose = 0; // enables verbose reporting of statistics
p->fVeryVerbose = 0; // enables very verbose reporting
p->TimeLimit = 0; // enables the timeout
// internal parameters
p->fReportSolution = 1; // enables specialized format for reporting solution
p->fReportSolution = 0; // enables specialized format for reporting solution
}
/**Function*************************************************************
......@@ -158,6 +159,7 @@ clk = clock();
TimeLeft = AIG_MAX( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 )
{
if ( !pParSec->fSilent )
printf( "Runtime limit exceeded.\n" );
RetValue = -1;
TimeOut = 1;
......@@ -166,14 +168,16 @@ clk = clock();
}
pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, pParSec->fVeryVerbose, &nIter, TimeLeft );
p->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
Aig_ManStop( pTemp );
if ( pNew == NULL )
{
if ( p->pSeqModel )
{
RetValue = 0;
if ( !pParSec->fSilent )
{
printf( "Networks are NOT EQUIVALENT after simulation. " );
PRT( "Time", clock() - clkTotal );
}
if ( pParSec->fReportSolution && !pParSec->fRecursive )
{
printf( "SOLUTION: FAIL " );
......@@ -186,6 +190,7 @@ PRT( "Time", clock() - clkTotal );
TimeOut = 1;
goto finish;
}
Aig_ManStop( pTemp );
if ( pParSec->fVerbose )
{
......@@ -201,6 +206,7 @@ PRT( "Time", clock() - clk );
TimeLeft = AIG_MAX( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 )
{
if ( !pParSec->fSilent )
printf( "Runtime limit exceeded.\n" );
RetValue = -1;
TimeOut = 1;
......@@ -235,6 +241,7 @@ PRT( "Time", clock() - clk );
TimeLeft = AIG_MAX( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 )
{
if ( !pParSec->fSilent )
printf( "Runtime limit exceeded.\n" );
RetValue = -1;
TimeOut = 1;
......@@ -273,6 +280,7 @@ PRT( "Time", clock() - clk );
TimeLeft = AIG_MAX( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 )
{
if ( !pParSec->fSilent )
printf( "Runtime limit exceeded.\n" );
RetValue = -1;
TimeOut = 1;
......@@ -283,6 +291,7 @@ PRT( "Time", clock() - clk );
clk = clock();
pPars->nFramesK = nFrames;
pPars->TimeLimit = TimeLeft;
pPars->fSilent = pParSec->fSilent;
pNew = Fra_FraigInduction( pTemp = pNew, pPars );
if ( pNew == NULL )
{
......@@ -357,8 +366,11 @@ PRT( "Time", clock() - clk );
Fra_SmlStop( pSml );
Aig_ManStop( pNew );
RetValue = 0;
if ( !pParSec->fSilent )
{
printf( "Networks are NOT EQUIVALENT after simulation. " );
PRT( "Time", clock() - clkTotal );
}
if ( pParSec->fReportSolution && !pParSec->fRecursive )
{
printf( "SOLUTION: FAIL " );
......@@ -399,10 +411,10 @@ PRT( "Time", clock() - clk );
// try reachability analysis
if ( pParSec->fReachability && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManRegNum(pNew) < 150 )
{
extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent );
pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew);
pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew);
RetValue = Aig_ManVerifyUsingBdds( pNew, 100000, 1000, 1, 1, 0 );
RetValue = Aig_ManVerifyUsingBdds( pNew, 100000, 1000, 1, 1, 0, pParSec->fSilent );
}
// try one-output at a time
......@@ -414,6 +426,7 @@ PRT( "Time", clock() - clk );
for ( i = 0; i < Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew); i++ )
if ( !Aig_ObjIsConst1( Aig_ObjFanin0(Aig_ManPo(pNew,i)) ) )
Counter++;
if ( !pParSec->fSilent )
printf( "*** The miter has %d outputs (out of %d total) unsolved in the multi-output form.\n",
Counter, Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) );
iCount = 0;
......@@ -427,6 +440,7 @@ PRT( "Time", clock() - clk );
TimeLeft = AIG_MAX( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 )
{
if ( !pParSec->fSilent )
printf( "Runtime limit exceeded.\n" );
TimeOut = 1;
goto finish;
......@@ -438,6 +452,7 @@ PRT( "Time", clock() - clk );
if ( Aig_ObjIsConst1( Aig_ObjFanin0(Aig_ManPo(pNew,i)) ) )
continue;
iCount++;
if ( !pParSec->fSilent )
printf( "*** Running output %d of the miter (number %d out of %d unsolved).\n", i, iCount, Counter );
pNew2 = Aig_ManDupOneOutput( pNew, i );
......@@ -462,6 +477,7 @@ PRT( "Time", clock() - clk );
RetValue = -1;
else
RetValue = 1;
if ( !pParSec->fSilent )
printf( "*** Finished running separate outputs of the miter.\n" );
}
......@@ -469,8 +485,11 @@ finish:
// report the miter
if ( RetValue == 1 )
{
if ( !pParSec->fSilent )
{
printf( "Networks are equivalent. " );
PRT( "Time", clock() - clkTotal );
}
if ( pParSec->fReportSolution && !pParSec->fRecursive )
{
printf( "SOLUTION: PASS " );
......@@ -479,8 +498,11 @@ PRT( "Time", clock() - clkTotal );
}
else if ( RetValue == 0 )
{
if ( !pParSec->fSilent )
{
printf( "Networks are NOT EQUIVALENT. " );
PRT( "Time", clock() - clkTotal );
}
if ( pParSec->fReportSolution && !pParSec->fRecursive )
{
printf( "SOLUTION: FAIL " );
......@@ -489,14 +511,17 @@ PRT( "Time", clock() - clkTotal );
}
else
{
if ( !pParSec->fSilent )
{
printf( "Networks are UNDECIDED. " );
PRT( "Time", clock() - clkTotal );
}
if ( pParSec->fReportSolution && !pParSec->fRecursive )
{
printf( "SOLUTION: UNDECIDED " );
PRT( "Time", clock() - clkTotal );
}
if ( !TimeOut )
if ( !TimeOut && !pParSec->fSilent )
{
static int Counter = 1;
char pFileName[1000];
......
src/aig/fra/fraSim.c
......@@ -1119,20 +1119,22 @@ int Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Fra_Cex_t * p )
RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) );
// write the output file
fprintf( pFile, "1\n" );
for ( i = 0; i <= p->iFrame; i++ )
{
/*
Aig_ManForEachLoSeq( pAig, pObj, k )
{
pSims = Fra_ObjSim(pSml, pObj->Id);
fprintf( pFile, "%d", (int)(pSims[i] != 0) );
}
fprintf( pFile, " " );
*/
Aig_ManForEachPiSeq( pAig, pObj, k )
{
pSims = Fra_ObjSim(pSml, pObj->Id);
fprintf( pFile, "%d", (int)(pSims[i] != 0) );
}
/*
fprintf( pFile, " " );
Aig_ManForEachPoSeq( pAig, pObj, k )
{
......@@ -1145,6 +1147,7 @@ int Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Fra_Cex_t * p )
pSims = Fra_ObjSim(pSml, pObj->Id);
fprintf( pFile, "%d", (int)(pSims[i] != 0) );
}
*/
fprintf( pFile, "\n" );
}
......
src/aig/ivy/ivyFraig.c
......@@ -2260,8 +2260,8 @@ p->timeSat += clock() - clk;
{
p->timeSatUnsat += clock() - clk;
pLits[0] = lit_neg( pLits[0] );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
assert( RetValue );
// RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
// assert( RetValue );
// continue solving the other implication
p->nSatCallsUnsat++;
}
......
src/aig/ntl/ntlCheck.c
......@@ -40,11 +40,100 @@
SeeAlso []
***********************************************************************/
int Ntl_ModelCheck( Ntl_Mod_t * pModel )
int Ntl_ModelCheck( Ntl_Mod_t * pModel, int fMain )
{
Ntl_Obj_t * pObj;
Ntl_Net_t * pNet;
int i, k, fStatus = 1;
// check root level model
if ( fMain )
{
if ( Ntl_ModelLatchNum(pModel) > 0 )
{
printf( "Root level model has %d registers.\n", pModel->pName, Ntl_ModelLatchNum(pModel) );
fStatus = 0;
}
goto checkobjs;
}
// check delay information
if ( pModel->attrBox && pModel->attrComb )
{
if ( pModel->vDelays == NULL )
{
printf( "Warning: Comb model %s does not have delay info. Default 1.0 delays are assumed.\n", pModel->pName );
pModel->vDelays = Vec_IntAlloc( 3 );
Vec_IntPush( pModel->vDelays, -1 );
Vec_IntPush( pModel->vDelays, -1 );
Vec_IntPush( pModel->vDelays, Aig_Float2Int(1.0) );
}
if ( pModel->vTimeInputs != NULL )
{
printf( "Combinational model %s has input arrival/required time information.\n", pModel->pName );
fStatus = 0;
}
if ( pModel->vTimeOutputs != NULL )
{
printf( "Combinational model %s has output arrival/required time information.\n", pModel->pName );
fStatus = 0;
}
}
if ( pModel->attrBox && !pModel->attrComb )
{
if ( pModel->vDelays != NULL )
{
printf( "Sequential model %s has delay info.\n", pModel->pName );
fStatus = 0;
}
if ( pModel->vTimeInputs == NULL )
{
printf( "Warning: Seq model %s does not have input arrival/required time info. Default 0.0 is assumed.\n", pModel->pName );
pModel->vTimeInputs = Vec_IntAlloc( 2 );
Vec_IntPush( pModel->vTimeInputs, -1 );
Vec_IntPush( pModel->vTimeInputs, Aig_Float2Int(1.0) );
}
if ( pModel->vTimeOutputs == NULL )
{
printf( "Warning: Seq model %s does not have output arrival/required time info. Default 0.0 is assumed.\n", pModel->pName );
pModel->vTimeOutputs = Vec_IntAlloc( 2 );
Vec_IntPush( pModel->vTimeOutputs, -1 );
Vec_IntPush( pModel->vTimeOutputs, Aig_Float2Int(1.0) );
}
}
// check box attributes
if ( pModel->attrBox )
{
if ( !pModel->attrWhite )
{
if ( Ntl_ModelNodeNum(pModel) + Ntl_ModelLut1Num(pModel) > 0 )
{
printf( "Model %s is a blackbox, yet it has %d nodes.\n", pModel->pName, Ntl_ModelNodeNum(pModel) + Ntl_ModelLut1Num(pModel) );
fStatus = 0;
}
if ( Ntl_ModelLatchNum(pModel) > 0 )
{
printf( "Model %s is a blackbox, yet it has %d registers.\n", pModel->pName, Ntl_ModelLatchNum(pModel) );
fStatus = 0;
}
return fStatus;
}
// this is a white box
if ( pModel->attrComb && Ntl_ModelNodeNum(pModel) + Ntl_ModelLut1Num(pModel) == 0 )
{
printf( "Model %s is a comb blackbox, yet it has no nodes.\n", pModel->pName );
fStatus = 0;
}
if ( !pModel->attrComb && Ntl_ModelLatchNum(pModel) == 0 )
{
printf( "Model %s is a seq blackbox, yet it has no registers.\n", pModel->pName );
fStatus = 0;
}
}
checkobjs:
// check nets
Ntl_ModelForEachNet( pModel, pNet, i )
{
if ( pNet->pName == NULL )
......@@ -58,6 +147,8 @@ int Ntl_ModelCheck( Ntl_Mod_t * pModel )
fStatus = 0;
}
}
// check objects
Ntl_ModelForEachObj( pModel, pObj, i )
{
Ntl_ObjForEachFanin( pObj, pNet, k )
......@@ -89,8 +180,8 @@ int Ntl_ModelCheck( Ntl_Mod_t * pModel )
***********************************************************************/
int Ntl_ManCheck( Ntl_Man_t * pMan )
{
Ntl_Mod_t * pMod1, * pMod2;
int i, k, fStatus = 1;
Ntl_Mod_t * pMod1;
int i, fStatus = 1;
// check that the models have unique names
Ntl_ManForEachModel( pMan, pMod1, i )
{
......@@ -99,16 +190,6 @@ int Ntl_ManCheck( Ntl_Man_t * pMan )
printf( "Model %d does not have a name\n", i );
fStatus = 0;
}
Ntl_ManForEachModel( pMan, pMod2, k )
{
if ( i >= k )
continue;
if ( strcmp(pMod1->pName, pMod2->pName) == 0 )
{
printf( "Models %d and %d have the same name (%s).\n", i, k, pMod1->pName );
fStatus = 0;
}
}
}
// check that the models (except the first one) do not have boxes
Ntl_ManForEachModel( pMan, pMod1, i )
......@@ -124,9 +205,8 @@ int Ntl_ManCheck( Ntl_Man_t * pMan )
// check models
Ntl_ManForEachModel( pMan, pMod1, i )
{
if ( !Ntl_ModelCheck( pMod1 ) )
if ( !Ntl_ModelCheck( pMod1, i==0 ) )
fStatus = 0;
break;
}
return fStatus;
}
......@@ -150,7 +230,7 @@ void Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel )
Ntl_Obj_t * pNode;
int i;
if ( Ntl_ModelIsBlackBox(pModel) )
if ( !pModel->attrWhite )
return;
// check for non-driven nets
......@@ -186,6 +266,37 @@ void Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel )
Vec_PtrFree( vNets );
}
/**Function*************************************************************
Synopsis [Fixed problems with non-driven nets in the model.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ntl_ModelTransformLatches( Ntl_Mod_t * pModel )
{
Ntl_Mod_t * pMod[3] = { NULL };
Ntl_Obj_t * pLatch;
int i, Init;
if ( Ntl_ModelLatchNum(pModel) == 0 )
return;
Ntl_ModelForEachLatch( pModel, pLatch, i )
{
Init = pLatch->LatchId.regInit;
if ( pMod[Init] == NULL )
pMod[Init] = Ntl_ManCreateLatchModel( pModel->pMan, Init );
pLatch->pImplem = pMod[Init];
pLatch->Type = NTL_OBJ_BOX;
}
printf( "Root level model %s: %d registers turned into white seq boxes.\n", pModel->pName, Ntl_ModelLatchNum(pModel) );
pModel->nObjs[NTL_OBJ_BOX] += Ntl_ModelLatchNum(pModel);
pModel->nObjs[NTL_OBJ_LATCH] = 0;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
......
src/aig/ntl/ntlFraig.c
......@@ -203,7 +203,7 @@ void Ntl_ManResetComplemented( Ntl_Man_t * p, Aig_Man_t * pAigCol )
pRoot = Ntl_ManRootModel(p);
Ntl_ModelForEachLatch( pRoot, pObj, i )
{
if ( (pObj->LatchId & 3) == 1 )
if ( Ntl_ObjIsInit1( pObj ) )
{
pObjCol = Ntl_ObjFanout0(pObj)->pCopy;
assert( pObjCol->fPhase == 0 );
......@@ -275,7 +275,7 @@ Ntl_Man_t * Ntl_ManFraig( Ntl_Man_t * p, int nPartSize, int nConfLimit, int nLev
// collapse the AIG
pAig = Ntl_ManExtract( p );
pNew = Ntl_ManInsertAig( p, pAig );
pAigCol = Ntl_ManCollapse( pNew, 0 );
pAigCol = Ntl_ManCollapseComb( pNew );
// perform fraiging for the given design
nPartSize = nPartSize? nPartSize : Aig_ManPoNum(pAigCol);
......@@ -309,7 +309,7 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe
// collapse the AIG
pAig = Ntl_ManExtract( p );
pNew = Ntl_ManInsertAig( p, pAig );
pAigCol = Ntl_ManCollapse( pNew, 1 );
pAigCol = Ntl_ManCollapseSeq( pNew );
// perform SCL for the given design
Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) );
......@@ -343,7 +343,7 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose )
// collapse the AIG
pAig = Ntl_ManExtract( p );
pNew = Ntl_ManInsertAig( p, pAig );
pAigCol = Ntl_ManCollapse( pNew, 1 );
pAigCol = Ntl_ManCollapseSeq( pNew );
// perform SCL for the given design
Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) );
......@@ -377,7 +377,7 @@ Ntl_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Fra_Ssw_t * pPars )
// collapse the AIG
pAig = Ntl_ManExtract( p );
pNew = Ntl_ManInsertAig( p, pAig );
pAigCol = Ntl_ManCollapse( pNew, 1 );
pAigCol = Ntl_ManCollapseSeq( pNew );
// perform SCL for the given design
Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) );
......@@ -502,7 +502,7 @@ void Ntl_ManFlipEdges( Ntl_Man_t * p, Aig_Man_t * pAigCol )
iLatch = 0;
Ntl_ModelForEachLatch( pRoot, pObj, i )
{
if ( (pObj->LatchId & 3) == 1 )
if ( Ntl_ObjIsInit1( pObj ) )
{
pObjCol = Aig_ManPi( pAigCol, Ntl_ModelPiNum(pRoot) + iLatch );
assert( pObjCol->fMarkA == 0 );
......@@ -524,7 +524,7 @@ void Ntl_ManFlipEdges( Ntl_Man_t * p, Aig_Man_t * pAigCol )
iLatch = 0;
Ntl_ModelForEachLatch( pRoot, pObj, i )
{
if ( (pObj->LatchId & 3) == 1 )
if ( Ntl_ObjIsInit1( pObj ) )
{
// flip the latch input
pObjCol = Aig_ManPo( pAigCol, Ntl_ModelPoNum(pRoot) + iLatch );
......@@ -554,7 +554,7 @@ Ntl_Man_t * Ntl_ManSsw2( Ntl_Man_t * p, Fra_Ssw_t * pPars )
Ntl_Man_t * pNew;
Aig_Man_t * pAigRed, * pAigCol;
// collapse the AIG
pAigCol = Ntl_ManCollapse( p, 1 );
pAigCol = Ntl_ManCollapseSeq( p );
Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) );
// transform the collapsed AIG
pAigRed = Fra_FraigInduction( pAigCol, pPars );
......
src/aig/ntl/ntlMan.c
......@@ -50,9 +50,14 @@ Ntl_Man_t * Ntl_ManAlloc()
p->vCos = Vec_PtrAlloc( 1000 );
p->vNodes = Vec_PtrAlloc( 1000 );
p->vBox1Cos = Vec_IntAlloc( 1000 );
p->vLatchIns = Vec_PtrAlloc( 1000 );
// start the manager
p->pMemObjs = Aig_MmFlexStart();
p->pMemSops = Aig_MmFlexStart();
// allocate model table
p->nModTableSize = Aig_PrimeCudd( 100 );
p->pModTable = ALLOC( Ntl_Mod_t *, p->nModTableSize );
memset( p->pModTable, 0, sizeof(Ntl_Mod_t *) * p->nModTableSize );
return p;
}
......@@ -189,10 +194,12 @@ void Ntl_ManFree( Ntl_Man_t * p )
if ( p->vCos ) Vec_PtrFree( p->vCos );
if ( p->vNodes ) Vec_PtrFree( p->vNodes );
if ( p->vBox1Cos ) Vec_IntFree( p->vBox1Cos );
if ( p->vLatchIns ) Vec_PtrFree( p->vLatchIns );
if ( p->pMemObjs ) Aig_MmFlexStop( p->pMemObjs, 0 );
if ( p->pMemSops ) Aig_MmFlexStop( p->pMemSops, 0 );
if ( p->pAig ) Aig_ManStop( p->pAig );
if ( p->pManTime ) Tim_ManStop( p->pManTime );
FREE( p->pModTable );
free( p );
}
......@@ -239,7 +246,7 @@ int Ntl_ManLatchNum( Ntl_Man_t * p )
SeeAlso []
***********************************************************************/
Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName )
Ntl_Mod_t * Ntl_ManFindModel_old( Ntl_Man_t * p, char * pName )
{
Ntl_Mod_t * pModel;
int i;
......@@ -276,6 +283,8 @@ void Ntl_ManPrintStats( Ntl_Man_t * p )
printf( "\n" );
fflush( stdout );
assert( Ntl_ModelLut1Num(pRoot) == Ntl_ModelCountLut1(pRoot) );
Ntl_ManPrintTypes( p );
fflush( stdout );
}
/**Function*************************************************************
......@@ -296,6 +305,67 @@ Tim_Man_t * Ntl_ManReadTimeMan( Ntl_Man_t * p )
/**Function*************************************************************
Synopsis [Saves the model type.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ntl_ManSaveBoxType( Ntl_Obj_t * pObj )
{
Ntl_Mod_t * pModel = pObj->pImplem;
int Number = 0;
assert( Ntl_ObjIsBox(pObj) );
Number |= (pModel->attrWhite << 0);
Number |= (pModel->attrBox << 1);
Number |= (pModel->attrComb << 2);
Number |= (pModel->attrKeep << 3);
pModel->pMan->BoxTypes[Number]++;
}
/**Function*************************************************************
Synopsis [Saves the model type.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ntl_ManPrintTypes( Ntl_Man_t * p )
{
Ntl_Mod_t * pModel;
Ntl_Obj_t * pObj;
int i;
pModel = Ntl_ManRootModel( p );
if ( Ntl_ModelBoxNum(pModel) == 0 )
return;
printf( "BOX STATISTICS:\n" );
Ntl_ModelForEachBox( pModel, pObj, i )
Ntl_ManSaveBoxType( pObj );
for ( i = 0; i < 15; i++ )
{
if ( !p->BoxTypes[i] )
continue;
printf( "%5d :", p->BoxTypes[i] );
printf( " %s", ((i & 1) > 0)? "white": "black" );
printf( " %s", ((i & 2) > 0)? "box ": "logic" );
printf( " %s", ((i & 4) > 0)? "comb ": "seq " );
printf( " %s", ((i & 8) > 0)? "keep ": "sweep" );
printf( "\n" );
}
printf( "Total box instances = %6d.\n\n", Ntl_ModelBoxNum(pModel) );
for ( i = 0; i < 15; i++ )
p->BoxTypes[i] = 0;
}
/**Function*************************************************************
Synopsis [Allocates the model.]
Description []
......@@ -311,16 +381,25 @@ Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName )
// start the manager
p = ALLOC( Ntl_Mod_t, 1 );
memset( p, 0, sizeof(Ntl_Mod_t) );
p->attrBox = 1;
p->attrComb = 1;
p->attrWhite = 1;
p->attrKeep = 0;
p->pMan = pMan;
p->pName = Ntl_ManStoreName( p->pMan, pName );
Vec_PtrPush( pMan->vModels, p );
p->vObjs = Vec_PtrAlloc( 1000 );
p->vPis = Vec_PtrAlloc( 100 );
p->vPos = Vec_PtrAlloc( 100 );
p->vObjs = Vec_PtrAlloc( 100 );
p->vPis = Vec_PtrAlloc( 10 );
p->vPos = Vec_PtrAlloc( 10 );
// start the table
p->nTableSize = Aig_PrimeCudd( 1000 );
p->nTableSize = Aig_PrimeCudd( 100 );
p->pTable = ALLOC( Ntl_Net_t *, p->nTableSize );
memset( p->pTable, 0, sizeof(Ntl_Net_t *) * p->nTableSize );
// add model to the table
if ( !Ntl_ManAddModel( pMan, p ) )
{
Ntl_ModelFree( p );
return NULL;
}
return p;
}
......@@ -371,11 +450,14 @@ Ntl_Mod_t * Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
if ( pNet->pCopy != NULL )
Ntl_ObjSetFanout( pObj->pCopy, pNet->pCopy, k );
if ( Ntl_ObjIsLatch(pObj) )
{
((Ntl_Obj_t *)pObj->pCopy)->LatchId = pObj->LatchId;
((Ntl_Obj_t *)pObj->pCopy)->pClock = pObj->pClock->pCopy;
}
}
pModelNew->vDelays = pModelOld->vDelays? Vec_IntDup( pModelOld->vDelays ) : NULL;
pModelNew->vArrivals = pModelOld->vArrivals? Vec_IntDup( pModelOld->vArrivals ) : NULL;
pModelNew->vRequireds = pModelOld->vRequireds? Vec_IntDup( pModelOld->vRequireds ) : NULL;
pModelNew->vTimeInputs = pModelOld->vTimeInputs? Vec_IntDup( pModelOld->vTimeInputs ) : NULL;
pModelNew->vTimeOutputs = pModelOld->vTimeOutputs? Vec_IntDup( pModelOld->vTimeOutputs ) : NULL;
return pModelNew;
}
......@@ -397,11 +479,20 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
Ntl_Obj_t * pObj;
int i, k;
pModelNew = Ntl_ModelAlloc( pManNew, pModelOld->pName );
pModelNew->attrWhite = pModelOld->attrWhite;
pModelNew->attrBox = pModelOld->attrBox;
pModelNew->attrComb = pModelOld->attrComb;
pModelNew->attrKeep = pModelOld->attrKeep;
Ntl_ModelForEachObj( pModelOld, pObj, i )
pObj->pCopy = Ntl_ModelDupObj( pModelNew, pObj );
Ntl_ModelForEachNet( pModelOld, pNet, i )
{
pNet->pCopy = Ntl_ModelFindOrCreateNet( pModelNew, pNet->pName );
if ( pNet->pDriver == NULL )
{
assert( !pModelOld->attrWhite );
continue;
}
((Ntl_Net_t *)pNet->pCopy)->pDriver = pNet->pDriver->pCopy;
assert( pNet->pDriver->pCopy != NULL );
}
......@@ -412,13 +503,16 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
Ntl_ObjForEachFanout( pObj, pNet, k )
Ntl_ObjSetFanout( pObj->pCopy, pNet->pCopy, k );
if ( Ntl_ObjIsLatch(pObj) )
{
((Ntl_Obj_t *)pObj->pCopy)->LatchId = pObj->LatchId;
((Ntl_Obj_t *)pObj->pCopy)->pClock = pObj->pClock->pCopy;
}
if ( Ntl_ObjIsNode(pObj) )
((Ntl_Obj_t *)pObj->pCopy)->pSop = Ntl_ManStoreSop( pManNew->pMemSops, pObj->pSop );
}
pModelNew->vDelays = pModelOld->vDelays? Vec_IntDup( pModelOld->vDelays ) : NULL;
pModelNew->vArrivals = pModelOld->vArrivals? Vec_IntDup( pModelOld->vArrivals ) : NULL;
pModelNew->vRequireds = pModelOld->vRequireds? Vec_IntDup( pModelOld->vRequireds ) : NULL;
pModelNew->vTimeInputs = pModelOld->vTimeInputs? Vec_IntDup( pModelOld->vTimeInputs ) : NULL;
pModelNew->vTimeOutputs = pModelOld->vTimeOutputs? Vec_IntDup( pModelOld->vTimeOutputs ) : NULL;
return pModelNew;
}
......@@ -435,9 +529,9 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
***********************************************************************/
void Ntl_ModelFree( Ntl_Mod_t * p )
{
assert( Ntl_ManCheckNetsAreNotMarked(p) );
if ( p->vRequireds ) Vec_IntFree( p->vRequireds );
if ( p->vArrivals ) Vec_IntFree( p->vArrivals );
assert( Ntl_ModelCheckNetsAreNotMarked(p) );
if ( p->vTimeOutputs ) Vec_IntFree( p->vTimeOutputs );
if ( p->vTimeInputs ) Vec_IntFree( p->vTimeInputs );
if ( p->vDelays ) Vec_IntFree( p->vDelays );
Vec_PtrFree( p->vObjs );
Vec_PtrFree( p->vPis );
......@@ -446,6 +540,45 @@ void Ntl_ModelFree( Ntl_Mod_t * p )
free( p );
}
/**Function*************************************************************
Synopsis [Create model equal to the latch with the given init value.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ntl_Mod_t * Ntl_ManCreateLatchModel( Ntl_Man_t * pMan, int Init )
{
char Name[100];
Ntl_Mod_t * pModel;
Ntl_Obj_t * pObj;
Ntl_Net_t * pNetLi, * pNetLo;
// create model
sprintf( Name, "%s%d", "latch", Init );
pModel = Ntl_ModelAlloc( pMan, Name );
pModel->attrWhite = 1;
pModel->attrBox = 1;
pModel->attrComb = 0;
pModel->attrKeep = 0;
// create primary input
pObj = Ntl_ModelCreatePi( pModel );
pNetLi = Ntl_ModelFindOrCreateNet( pModel, "li" );
Ntl_ModelSetNetDriver( pObj, pNetLi );
// create latch
pObj = Ntl_ModelCreateLatch( pModel );
pObj->LatchId.regInit = Init;
pObj->pFanio[0] = pNetLi;
// create primary output
pNetLo = Ntl_ModelFindOrCreateNet( pModel, "lo" );
Ntl_ModelSetNetDriver( pObj, pNetLo );
pObj = Ntl_ModelCreatePo( pModel, pNetLo );
return pModel;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/aig/ntl/ntlSweep.c
......@@ -79,7 +79,7 @@ void Ntl_ManSweepMark( Ntl_Man_t * p )
Ntl_ManSweepMark_rec( p, pObj );
// start from the persistant boxes
Ntl_ModelForEachBox( pRoot, pObj, i )
if ( pObj->pImplem->fKeep )
if ( pObj->pImplem->attrKeep )
Ntl_ManSweepMark_rec( p, pObj );
}
......
src/aig/ntl/ntlTable.c
......@@ -189,7 +189,7 @@ Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName )
SeeAlso []
***********************************************************************/
int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber )
int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * pName, int * pNumber )
{
Ntl_Net_t * pNet;
Ntl_Obj_t * pObj;
......@@ -198,6 +198,30 @@ int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber )
pNet = Ntl_ModelFindNet( p, pName );
if ( pNet == NULL )
return 0;
if ( fPiOnly )
{
Ntl_ModelForEachPi( p, pObj, i )
{
if ( Ntl_ObjFanout0(pObj) == pNet )
{
*pNumber = i;
return -1;
}
}
return 0;
}
if ( fPoOnly )
{
Ntl_ModelForEachPo( p, pObj, i )
{
if ( Ntl_ObjFanin0(pObj) == pNet )
{
*pNumber = i;
return 1;
}
}
return 0;
}
Ntl_ModelForEachPo( p, pObj, i )
{
if ( Ntl_ObjFanin0(pObj) == pNet )
......@@ -281,6 +305,97 @@ int Ntl_ModelCountNets( Ntl_Mod_t * p )
return Counter;
}
/**Function*************************************************************
Synopsis [Resizes the table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ntl_ManModelTableResize( Ntl_Man_t * p )
{
Ntl_Mod_t ** pModTableNew, ** ppSpot, * pEntry, * pEntry2;
int nModTableSizeNew, Counter, e, clk;
clk = clock();
// get the new table size
nModTableSizeNew = Aig_PrimeCudd( 3 * p->nModTableSize );
// allocate a new array
pModTableNew = ALLOC( Ntl_Mod_t *, nModTableSizeNew );
memset( pModTableNew, 0, sizeof(Ntl_Mod_t *) * nModTableSizeNew );
// rehash entries
Counter = 0;
for ( e = 0; e < p->nModTableSize; e++ )
for ( pEntry = p->pModTable[e], pEntry2 = pEntry? pEntry->pNext : NULL;
pEntry; pEntry = pEntry2, pEntry2 = pEntry? pEntry->pNext : NULL )
{
ppSpot = pModTableNew + Ntl_HashString( pEntry->pName, nModTableSizeNew );
pEntry->pNext = *ppSpot;
*ppSpot = pEntry;
Counter++;
}
assert( Counter == p->nModEntries );
// printf( "Increasing the structural table size from %6d to %6d. ", p->nTableSize, nTableSizeNew );
// PRT( "Time", clock() - clk );
// replace the table and the parameters
free( p->pModTable );
p->pModTable = pModTableNew;
p->nModTableSize = nModTableSizeNew;
}
/**Function*************************************************************
Synopsis [Finds or creates the net.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ManAddModel( Ntl_Man_t * p, Ntl_Mod_t * pModel )
{
Ntl_Mod_t * pEnt;
unsigned Key = Ntl_HashString( pModel->pName, p->nModTableSize );
for ( pEnt = p->pModTable[Key]; pEnt; pEnt = pEnt->pNext )
if ( !strcmp( pEnt->pName, pModel->pName ) )
return 0;
pModel->pNext = p->pModTable[Key];
p->pModTable[Key] = pModel;
if ( ++p->nModEntries > 2 * p->nModTableSize )
Ntl_ManModelTableResize( p );
Vec_PtrPush( p->vModels, pModel );
return 1;
}
/**Function*************************************************************
Synopsis [Finds or creates the net.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName )
{
Ntl_Mod_t * pEnt;
unsigned Key = Ntl_HashString( pName, p->nModTableSize );
for ( pEnt = p->pModTable[Key]; pEnt; pEnt = pEnt->pNext )
if ( !strcmp( pEnt->pName, pName ) )
return pEnt;
return NULL;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/aig/ntl/ntlTime.c
......@@ -88,13 +88,27 @@ Tim_Man_t * Ntl_ManCreateTiming( Ntl_Man_t * p )
// start the timing manager
pMan = Tim_ManStart( Aig_ManPiNum(p->pAig), Aig_ManPoNum(p->pAig) );
// unpack the data in the arrival times
if ( pRoot->vArrivals )
Vec_IntForEachEntry( pRoot->vArrivals, Entry, i )
Tim_ManInitCiArrival( pMan, Entry, Aig_Int2Float(Vec_IntEntry(pRoot->vArrivals,++i)) );
if ( pRoot->vTimeInputs )
{
Vec_IntForEachEntry( pRoot->vTimeInputs, Entry, i )
{
if ( Entry == -1 )
Tim_ManSetCiArrivalAll( pMan, Aig_Int2Float(Vec_IntEntry(pRoot->vTimeInputs,++i)) );
else
Tim_ManInitCiArrival( pMan, Entry, Aig_Int2Float(Vec_IntEntry(pRoot->vTimeInputs,++i)) );
}
}
// unpack the data in the required times
if ( pRoot->vRequireds )
Vec_IntForEachEntry( pRoot->vRequireds, Entry, i )
Tim_ManInitCoRequired( pMan, Entry, Aig_Int2Float(Vec_IntEntry(pRoot->vRequireds,++i)) );
if ( pRoot->vTimeOutputs )
{
Vec_IntForEachEntry( pRoot->vTimeOutputs, Entry, i )
{
if ( Entry == -1 )
Tim_ManSetCoRequiredAll( pMan, Aig_Int2Float(Vec_IntEntry(pRoot->vTimeOutputs,++i)) );
else
Tim_ManInitCoRequired( pMan, Entry, Aig_Int2Float(Vec_IntEntry(pRoot->vTimeOutputs,++i)) );
}
}
// derive timing tables
vDelayTables = Vec_PtrAlloc( Vec_PtrSize(p->vModels) );
Ntl_ManForEachModel( p, pModel, i )
......@@ -106,7 +120,7 @@ Tim_Man_t * Ntl_ManCreateTiming( Ntl_Man_t * p )
Tim_ManSetDelayTables( pMan, vDelayTables );
// set up the boxes
iBox = 0;
curPi = Ntl_ModelCiNum(pRoot);
curPi = p->iLastCi;
Ntl_ManForEachBox( p, pObj, i )
{
Tim_ManCreateBoxFirst( pMan, Vec_IntEntry(p->vBox1Cos, iBox), Ntl_ObjFaninNum(pObj), curPi, Ntl_ObjFanoutNum(pObj), pObj->pImplem->pDelayTable );
......
src/aig/ntl/ntlUtil.c
......@@ -238,26 +238,6 @@ void Ntl_ManUnmarkCiCoNets( Ntl_Man_t * p )
/**Function*************************************************************
Synopsis [Unmarks the CI/CO nets.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ManCheckNetsAreNotMarked( Ntl_Mod_t * pModel )
{
Ntl_Net_t * pNet;
int i;
Ntl_ModelForEachNet( pModel, pNet, i )
assert( pNet->fMark == 0 );
return 1;
}
/**Function*************************************************************
Synopsis [Convert initial values of registers to be zero.]
Description []
......@@ -274,7 +254,7 @@ void Ntl_ManSetZeroInitValues( Ntl_Man_t * p )
int i;
pRoot = Ntl_ManRootModel(p);
Ntl_ModelForEachLatch( pRoot, pObj, i )
pObj->LatchId &= ~3;
pObj->LatchId.regInit = 0;
}
/**Function*************************************************************
......@@ -296,7 +276,7 @@ void Ntl_ManAddInverters( Ntl_Obj_t * pObj )
Ntl_Net_t * pNetLo, * pNetLi, * pNetLoInv, * pNetLiInv;
Ntl_Obj_t * pNode;
int nLength, RetValue;
assert( (pObj->LatchId & 3) == 1 );
assert( Ntl_ObjIsInit1( pObj ) );
// get the nets
pNetLi = Ntl_ObjFanin0(pObj);
pNetLo = Ntl_ObjFanout0(pObj);
......@@ -362,11 +342,132 @@ void Ntl_ManTransformInitValues( Ntl_Man_t * p )
pRoot = Ntl_ManRootModel(p);
Ntl_ModelForEachLatch( pRoot, pObj, i )
{
if ( (pObj->LatchId & 3) == 1 )
if ( Ntl_ObjIsInit1( pObj ) )
Ntl_ManAddInverters( pObj );
pObj->LatchId &= ~3;
pObj->LatchId.regInit = 0;
}
}
/**Function*************************************************************
Synopsis [Counts the number of CIs in the model.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ModelCombLeafNum( Ntl_Mod_t * p )
{
Ntl_Obj_t * pObj;
int i, Counter = 0;
Ntl_ModelForEachCombLeaf( p, pObj, i )
Counter += Ntl_ObjFanoutNum( pObj );
return Counter;
}
/**Function*************************************************************
Synopsis [Counts the number of COs in the model.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ModelCombRootNum( Ntl_Mod_t * p )
{
Ntl_Obj_t * pObj;
int i, Counter = 0;
Ntl_ModelForEachCombRoot( p, pObj, i )
Counter += Ntl_ObjFaninNum( pObj );
return Counter;
}
/**Function*************************************************************
Synopsis [Counts the number of CIs in the model.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ModelSeqLeafNum( Ntl_Mod_t * p )
{
Ntl_Obj_t * pObj;
int i, Counter = 0;
Ntl_ModelForEachSeqLeaf( p, pObj, i )
Counter += Ntl_ObjFanoutNum( pObj );
return Counter;
}
/**Function*************************************************************
Synopsis [Counts the number of COs in the model.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ModelSeqRootNum( Ntl_Mod_t * p )
{
Ntl_Obj_t * pObj;
int i, Counter = 0;
Ntl_ModelForEachSeqRoot( p, pObj, i )
Counter += Ntl_ObjFaninNum( pObj );
return Counter;
}
/**Function*************************************************************
Synopsis [Unmarks the CI/CO nets.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ModelCheckNetsAreNotMarked( Ntl_Mod_t * pModel )
{
Ntl_Net_t * pNet;
int i;
Ntl_ModelForEachNet( pModel, pNet, i )
assert( pNet->fMark == 0 );
return 1;
}
/**Function*************************************************************
Synopsis [Unmarks the CI/CO nets.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ntl_ModelClearNets( Ntl_Mod_t * pModel )
{
Ntl_Net_t * pNet;
int i;
Ntl_ModelForEachNet( pModel, pNet, i )
{
pNet->nVisits = 0;
pNet->pCopy = NULL;
}
}
////////////////////////////////////////////////////////////////////////
......
src/aig/ntl/ntlWriteBlif.c
......@@ -40,15 +40,22 @@
SeeAlso []
***********************************************************************/
void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel, int fMain )
{
Ntl_Obj_t * pObj;
Ntl_Net_t * pNet;
float Delay;
int i, k, fClockAdded = 0;
int i, k;
fprintf( pFile, ".model %s\n", pModel->pName );
if ( pModel->fKeep )
fprintf( pFile, ".attrib keep\n" );
if ( pModel->attrWhite || pModel->attrBox || pModel->attrComb || pModel->attrKeep )
{
fprintf( pFile, ".attrib" );
fprintf( pFile, " %s", pModel->attrWhite? "white": "black" );
fprintf( pFile, " %s", pModel->attrBox? "box" : "logic" );
fprintf( pFile, " %s", pModel->attrComb? "comb" : "seq" );
// fprintf( pFile, " %s", pModel->attrKeep? "keep" : "sweep" );
fprintf( pFile, "\n" );
}
fprintf( pFile, ".inputs" );
Ntl_ModelForEachPi( pModel, pObj, i )
fprintf( pFile, " %s", Ntl_ObjFanout0(pObj)->pName );
......@@ -63,19 +70,25 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
for ( i = 0; i < Vec_IntSize(pModel->vDelays); i += 3 )
{
fprintf( pFile, ".delay" );
if ( Vec_IntEntry(pModel->vDelays,i) != -1 )
fprintf( pFile, " %s", Ntl_ObjFanout0(Ntl_ModelPi(pModel, Vec_IntEntry(pModel->vDelays,i)))->pName );
if ( Vec_IntEntry(pModel->vDelays,i+1) != -1 )
fprintf( pFile, " %s", Ntl_ObjFanin0(Ntl_ModelPo(pModel, Vec_IntEntry(pModel->vDelays,i+1)))->pName );
fprintf( pFile, " %.3f", Aig_Int2Float(Vec_IntEntry(pModel->vDelays,i+2)) );
fprintf( pFile, "\n" );
}
}
if ( pModel->vArrivals )
if ( pModel->vTimeInputs )
{
for ( i = 0; i < Vec_IntSize(pModel->vArrivals); i += 2 )
for ( i = 0; i < Vec_IntSize(pModel->vTimeInputs); i += 2 )
{
if ( fMain )
fprintf( pFile, ".input_arrival" );
fprintf( pFile, " %s", Ntl_ObjFanout0(Ntl_ModelPi(pModel, Vec_IntEntry(pModel->vArrivals,i)))->pName );
Delay = Aig_Int2Float(Vec_IntEntry(pModel->vArrivals,i+1));
else
fprintf( pFile, ".input_required" );
if ( Vec_IntEntry(pModel->vTimeInputs,i) != -1 )
fprintf( pFile, " %s", Ntl_ObjFanout0(Ntl_ModelPi(pModel, Vec_IntEntry(pModel->vTimeInputs,i)))->pName );
Delay = Aig_Int2Float(Vec_IntEntry(pModel->vTimeInputs,i+1));
if ( Delay == -TIM_ETERNITY )
fprintf( pFile, " -inf" );
else if ( Delay == TIM_ETERNITY )
......@@ -85,13 +98,17 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
fprintf( pFile, "\n" );
}
}
if ( pModel->vRequireds )
if ( pModel->vTimeOutputs )
{
for ( i = 0; i < Vec_IntSize(pModel->vRequireds); i += 2 )
for ( i = 0; i < Vec_IntSize(pModel->vTimeOutputs); i += 2 )
{
if ( fMain )
fprintf( pFile, ".output_required" );
fprintf( pFile, " %s", Ntl_ObjFanin0(Ntl_ModelPo(pModel, Vec_IntEntry(pModel->vRequireds,i)))->pName );
Delay = Aig_Int2Float(Vec_IntEntry(pModel->vRequireds,i+1));
else
fprintf( pFile, ".output_arrival" );
if ( Vec_IntEntry(pModel->vTimeOutputs,i) != -1 )
fprintf( pFile, " %s", Ntl_ObjFanin0(Ntl_ModelPo(pModel, Vec_IntEntry(pModel->vTimeOutputs,i)))->pName );
Delay = Aig_Int2Float(Vec_IntEntry(pModel->vTimeOutputs,i+1));
if ( Delay == -TIM_ETERNITY )
fprintf( pFile, " -inf" );
else if ( Delay == TIM_ETERNITY )
......@@ -117,13 +134,27 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
fprintf( pFile, ".latch" );
fprintf( pFile, " %s", Ntl_ObjFanin0(pObj)->pName );
fprintf( pFile, " %s", Ntl_ObjFanout0(pObj)->pName );
if ( pObj->LatchId >> 2 )
fprintf( pFile, " %d", pObj->LatchId >> 2 );
if ( Ntl_ObjFanin(pObj, 1) != NULL )
fprintf( pFile, " %s", Ntl_ObjFanin(pObj, 1)->pName );
else if ( pObj->LatchId >> 2 )
fprintf( pFile, " clock99" ), fClockAdded = 1;
fprintf( pFile, " %d", pObj->LatchId & 3 );
assert( pObj->LatchId.regType == 0 || pObj->LatchId.regClass == 0 );
if ( pObj->LatchId.regType )
{
if ( pObj->LatchId.regType == 1 )
fprintf( pFile, " fe" );
else if ( pObj->LatchId.regType == 2 )
fprintf( pFile, " re" );
else if ( pObj->LatchId.regType == 3 )
fprintf( pFile, " ah" );
else if ( pObj->LatchId.regType == 4 )
fprintf( pFile, " al" );
else if ( pObj->LatchId.regType == 5 )
fprintf( pFile, " as" );
else
assert( 0 );
}
else if ( pObj->LatchId.regClass )
fprintf( pFile, " %d", pObj->LatchId.regClass );
if ( pObj->pClock )
fprintf( pFile, " %s", pObj->pClock->pName );
fprintf( pFile, " %d", pObj->LatchId.regInit );
fprintf( pFile, "\n" );
}
else if ( Ntl_ObjIsBox(pObj) )
......@@ -136,8 +167,6 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
fprintf( pFile, "\n" );
}
}
if ( fClockAdded )
fprintf( pFile, ".names clock99\n 0\n" );
fprintf( pFile, ".end\n\n" );
}
......@@ -167,7 +196,7 @@ void Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName )
fprintf( pFile, "# Benchmark \"%s\" written by ABC-8 on %s\n", p->pName, Ioa_TimeStamp() );
// write the models
Ntl_ManForEachModel( p, pModel, i )
Ioa_WriteBlifModel( pFile, pModel );
Ioa_WriteBlifModel( pFile, pModel, i==0 );
// close the file
fclose( pFile );
}
......
src/aig/saig/module.make
......@@ -3,6 +3,7 @@ SRC += src/aig/saig/saigBmc.c \
src/aig/saig/saigHaig.c \
src/aig/saig/saigInter.c \
src/aig/saig/saigIoa.c \
src/aig/saig/saigMiter.c \
src/aig/saig/saigPhase.c \
src/aig/saig/saigRetFwd.c \
src/aig/saig/saigRetMin.c \
......
src/aig/saig/saig.h
......@@ -86,6 +86,8 @@ extern void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
extern Aig_Man_t * Saig_ManReadBlif( char * pFileName );
/*=== saigInter.c ==========================================================*/
extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fVerbose, int * pDepth );
/*=== saigMiter.c ==========================================================*/
extern Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper );
/*=== saigPhase.c ==========================================================*/
extern Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int fIgnore, int fPrint, int fVerbose );
/*=== saigRetFwd.c ==========================================================*/
......
src/aig/saig/saigBmc.c
......@@ -277,6 +277,8 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
free( pModel );
Vec_IntFree( vCiIds );
// if ( piFrame )
// *piFrame = i / Saig_ManPoNum(pAig);
RetValue = 0;
break;
}
......
src/aig/saig/saigMiter.c 0 → 100644
/**CFile****************************************************************
FileName [saigMiter.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Sequential AIG package.]
Synopsis [Computes sequential miter of two sequential AIGs.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: saigMiter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "saig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper )
{
Aig_Man_t * pNew;
Aig_Obj_t * pObj;
int i;
assert( Saig_ManRegNum(p1) > 0 || Saig_ManRegNum(p2) > 0 );
assert( Saig_ManPiNum(p1) == Saig_ManPiNum(p2) );
assert( Saig_ManPoNum(p1) == Saig_ManPoNum(p2) );
pNew = Aig_ManStart( Aig_ManObjNumMax(p1) + Aig_ManObjNumMax(p2) );
// map constant nodes
Aig_ManConst1(p1)->pData = Aig_ManConst1(pNew);
Aig_ManConst1(p2)->pData = Aig_ManConst1(pNew);
// map primary inputs
Saig_ManForEachPi( p1, pObj, i )
pObj->pData = Aig_ObjCreatePi( pNew );
Saig_ManForEachPi( p2, pObj, i )
pObj->pData = Aig_ManPi( pNew, i );
// map register outputs
Saig_ManForEachLo( p1, pObj, i )
pObj->pData = Aig_ObjCreatePi( pNew );
Saig_ManForEachLo( p2, pObj, i )
pObj->pData = Aig_ObjCreatePi( pNew );
// map internal nodes
Aig_ManForEachNode( p1, pObj, i )
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
Aig_ManForEachNode( p2, pObj, i )
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
// create primary outputs
Saig_ManForEachPo( p1, pObj, i )
{
if ( Oper == 0 ) // XOR
pObj = Aig_Exor( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild0Copy(Aig_ManPo(p2,0)) );
else if ( Oper == 1 ) // implication is PO(p1) -> PO(p2) ... complement is PO(p1) & !PO(p2)
pObj = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_Not(Aig_ObjChild0Copy(Aig_ManPo(p2,0))) );
else
assert( 0 );
}
// create register inputs
Saig_ManForEachLi( p1, pObj, i )
pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
Saig_ManForEachLi( p2, pObj, i )
pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
// cleanup
Aig_ManSetRegNum( pNew, Saig_ManRegNum(p1) + Saig_ManRegNum(p2) );
Aig_ManCleanup( pNew );
return pNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/saig/saigScl.c
......@@ -67,6 +67,42 @@ void Saig_ManReportUselessRegisters( Aig_Man_t * pAig )
printf( "Network has %d (out of %d) registers driven by PIs.\n", Counter2, Saig_ManRegNum(pAig) );
}
/**Function*************************************************************
Synopsis [Report the number of pairs of complemented registers.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_ManReportComplements( Aig_Man_t * p )
{
Aig_Obj_t * pObj, * pFanin;
int i, Counter = 0, Diffs = 0;
assert( Aig_ManRegNum(p) > 0 );
Aig_ManForEachObj( p, pObj, i )
assert( !pObj->fMarkA );
Aig_ManForEachLiSeq( p, pObj, i )
{
pFanin = Aig_ObjFanin0(pObj);
if ( pFanin->fMarkA )
Counter++;
else
pFanin->fMarkA = 1;
}
// count fanins that have both attributes
Aig_ManForEachLiSeq( p, pObj, i )
{
pFanin = Aig_ObjFanin0(pObj);
pFanin->fMarkA = 0;
}
return Counter;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/aig/tim/tim.c
......@@ -554,6 +554,8 @@ void Tim_ManCreateBoxFirst( Tim_Man_t * p, int firstIn, int nIns, int firstOut,
pBox = (Tim_Box_t *)Mem_FlexEntryFetch( p->pMemObj, sizeof(Tim_Box_t) + sizeof(int) * (nIns+nOuts) );
memset( pBox, 0, sizeof(Tim_Box_t) );
pBox->iBox = Vec_PtrSize( p->vBoxes );
//printf( "Creating box %d: First in = %d. (%d) First out = %d. (%d)\n", pBox->iBox,
// firstIn, nIns, firstOut, nOuts );
Vec_PtrPush( p->vBoxes, pBox );
pBox->pDelayTable = pDelayTable;
pBox->nInputs = nIns;
......@@ -704,6 +706,25 @@ void Tim_ManSetCoRequired( Tim_Man_t * p, int iCo, float Delay )
SeeAlso []
***********************************************************************/
void Tim_ManSetCiArrivalAll( Tim_Man_t * p, float Delay )
{
Tim_Obj_t * pObj;
int i;
Tim_ManForEachCi( p, pObj, i )
Tim_ManInitCiArrival( p, i, Delay );
}
/**Function*************************************************************
Synopsis [Sets the correct required times for all POs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Tim_ManSetCoRequiredAll( Tim_Man_t * p, float Delay )
{
Tim_Obj_t * pObj;
......
src/aig/tim/tim.h
......@@ -81,6 +81,7 @@ extern void Tim_ManInitCoRequired( Tim_Man_t * p, int iCo, float Dela
extern void Tim_ManSetCoArrival( Tim_Man_t * p, int iCo, float Delay );
extern void Tim_ManSetCiRequired( Tim_Man_t * p, int iCi, float Delay );
extern void Tim_ManSetCoRequired( Tim_Man_t * p, int iCo, float Delay );
extern void Tim_ManSetCiArrivalAll( Tim_Man_t * p, float Delay );
extern void Tim_ManSetCoRequiredAll( Tim_Man_t * p, float Delay );
extern float Tim_ManGetCiArrival( Tim_Man_t * p, int iCi );
extern float Tim_ManGetCoRequired( Tim_Man_t * p, int iCo );
......
src/base/abci/abc.c
......@@ -9298,7 +9298,7 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Prove_Params_t Params, * pParams = &Params;
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkTemp;
int c, clk, RetValue;
int c, clk, RetValue, iOut = -1;
extern int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars );
......@@ -9351,8 +9351,16 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv )
// verify that the pattern is correct
if ( RetValue == 0 )
{
Abc_Obj_t * pObj;
int i;
int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pNtkTemp->pModel );
if ( pSimInfo[0] != 1 )
Abc_NtkForEachCo( pNtk, pObj, i )
if ( pSimInfo[i] == 1 )
{
iOut = i;
break;
}
if ( i == Abc_NtkCoNum(pNtk) )
printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" );
free( pSimInfo );
}
......@@ -9360,7 +9368,7 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( RetValue == -1 )
printf( "UNDECIDED " );
else if ( RetValue == 0 )
printf( "SATISFIABLE " );
printf( "SATISFIABLE (output = %d) ", iOut );
else
printf( "UNSATISFIABLE " );
//printf( "\n" );
......@@ -15634,6 +15642,7 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
int fMapped;
int fTest;
extern void * Ioa_ReadBlif( char * pFileName, int fCheck );
extern void Ioa_WriteBlif( void * p, char * pFileName );
extern Aig_Man_t * Ntl_ManExtract( void * p );
extern void * Ntl_ManExtractNwk( void * p, Aig_Man_t * pAig, Tim_Man_t * pManTime );
......@@ -15678,6 +15687,7 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pTemp )
{
Ntl_ManPrintStats( pTemp );
// Ioa_WriteBlif( pTemp, "test_boxes.blif" );
Ntl_ManFree( pTemp );
}
return 0;
......@@ -17888,6 +17898,8 @@ int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
printf( "Currently *cec works only for two designs given on command line.\n" );
/*
// derive AIGs
pAig1 = Ntl_ManCollapse( pAbc->pAbc8Ntl, 0 );
pTemp = Ntl_ManInsertNtk( pAbc->pAbc8Ntl, pAbc->pAbc8Nwk );
......@@ -17903,6 +17915,7 @@ int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
Fra_FraigCecTop( pAig1, pAig2, nConfLimit, nPartSize, fSmart, fVerbose );
Aig_ManStop( pAig1 );
Aig_ManStop( pAig2 );
*/
return 0;
usage:
......
src/base/main/mainMC.c
......@@ -45,29 +45,36 @@
***********************************************************************/
int main( int argc, char * argv[] )
{
int fEnableBmcOnly = 0; // enable to make it BMC-only
int fEnableCounter = 1; // should be 1 in the final version
int fEnableComment = 0; // should be 0 in the final version
Fra_Sec_t SecPar, * pSecPar = &SecPar;
FILE * pFile;
Aig_Man_t * pAig;
int RetValue;
int RetValue = -1;
int Depth = -1;
// BMC parameters
int nFrames = 30;
int nSizeMax = 200000;
int nFrames = 50;
int nSizeMax = 500000;
int nBTLimit = 10000;
int fRewrite = 0;
int fNewAlgo = 1;
int fVerbose = 0;
int clkTotal = clock();
if ( argc != 2 )
{
printf( " Expecting one command-line argument (an input file in AIGER format).\n" );
printf( " usage: %s <file.aig>", argv[0] );
printf( " usage: %s <file.aig>\n", argv[0] );
return 0;
}
pFile = fopen( argv[1], "r" );
if ( pFile == NULL )
{
printf( " Cannot open input AIGER file \"%s\".\n", argv[1] );
printf( " usage: %s <file.aig>", argv[0] );
printf( " usage: %s <file.aig>\n", argv[0] );
return 0;
}
fclose( pFile );
......@@ -75,12 +82,15 @@ int main( int argc, char * argv[] )
if ( pAig == NULL )
{
printf( " Parsing the AIGER file \"%s\" has failed.\n", argv[1] );
printf( " usage: %s <file.aig>", argv[0] );
printf( " usage: %s <file.aig>\n", argv[0] );
return 0;
}
// perform BMC
Aig_ManSetRegNum( pAig, pAig->nRegs );
if ( !fEnableBmcOnly )
{
// perform BMC
if ( pAig->nRegs != 0 )
RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, NULL );
// perform full-blown SEC
......@@ -91,17 +101,28 @@ int main( int argc, char * argv[] )
extern void Cnf_ClearMemory();
Fra_SecSetDefaultParams( pSecPar );
pSecPar->nFramesMax = 2; // the max number of frames used for induction
pSecPar->TimeLimit = 600;
pSecPar->nFramesMax = 4; // the max number of frames used for induction
pSecPar->fPhaseAbstract = 0; // disable phase-abstraction
pSecPar->fSilent = 1; // disable phase-abstraction
Dar_LibStart();
RetValue = Fra_FraigSec( pAig, pSecPar );
Dar_LibStop();
Cnf_ClearMemory();
}
}
// perform BMC again
if ( RetValue == -1 )
if ( RetValue == -1 && pAig->nRegs != 0 )
{
int nFrames = 200;
int nSizeMax = 500000;
int nBTLimit = 10000000;
int fRewrite = 0;
RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &Depth );
if ( RetValue != 0 )
RetValue = -1;
}
// decide how to report the output
......@@ -111,7 +132,20 @@ int main( int argc, char * argv[] )
if ( RetValue == 0 )
{
// fprintf(stdout, "s SATIFIABLE\n");
fprintf( pFile, "1" );
if ( fEnableCounter )
{
printf( "\n" );
if ( pAig->pSeqModel )
Fra_SmlWriteCounterExample( pFile, pAig, pAig->pSeqModel );
}
if ( fEnableComment )
{
printf( " # File %10s. ", argv[1] );
PRT( "Time", clock() - clkTotal );
}
if ( pFile != stdout )
fclose(pFile);
Aig_ManStop( pAig );
......@@ -120,7 +154,15 @@ int main( int argc, char * argv[] )
else if ( RetValue == 1 )
{
// fprintf(stdout, "s UNSATISFIABLE\n");
fprintf( pFile, "0\n" );
fprintf( pFile, "0" );
if ( fEnableComment )
{
printf( " # File %10s. ", argv[1] );
PRT( "Time", clock() - clkTotal );
}
printf( "\n" );
if ( pFile != stdout )
fclose(pFile);
Aig_ManStop( pAig );
......@@ -129,6 +171,15 @@ int main( int argc, char * argv[] )
else // if ( RetValue == -1 )
{
// fprintf(stdout, "s UNKNOWN\n");
fprintf( pFile, "2" );
if ( fEnableComment )
{
printf( " # File %10s. ", argv[1] );
PRT( "Time", clock() - clkTotal );
}
printf( "\n" );
if ( pFile != stdout )
fclose(pFile);
Aig_ManStop( pAig );
......
src/bdd/parse/parseCore.c
......@@ -58,7 +58,9 @@
#define PARSE_SYM_XOR1 '<' // logic EXOR (the 1st symbol)
#define PARSE_SYM_XOR2 '+' // logic EXOR (the 2nd symbol)
#define PARSE_SYM_XOR3 '>' // logic EXOR (the 3rd symbol)
#define PARSE_SYM_OR '+' // logic OR
#define PARSE_SYM_XOR '^' // logic XOR
#define PARSE_SYM_OR1 '+' // logic OR
#define PARSE_SYM_OR2 '|' // logic OR
#define PARSE_SYM_EQU1 '<' // equvalence (the 1st symbol)
#define PARSE_SYM_EQU2 '=' // equvalence (the 2nd symbol)
#define PARSE_SYM_EQU3 '>' // equvalence (the 3rd symbol)
......@@ -220,7 +222,9 @@ DdNode * Parse_FormulaParser( FILE * pOutput, char * pFormulaInit, int nVars, in
case PARSE_SYM_AND1:
case PARSE_SYM_AND2:
case PARSE_SYM_OR:
case PARSE_SYM_OR1:
case PARSE_SYM_OR2:
case PARSE_SYM_XOR:
if ( Flag != PARSE_FLAG_VAR )
{
fprintf( pOutput, "Parse_FormulaParser(): There is no variable before AND, EXOR, or OR.\n" );
......@@ -229,8 +233,10 @@ DdNode * Parse_FormulaParser( FILE * pOutput, char * pFormulaInit, int nVars, in
}
if ( *pTemp == PARSE_SYM_AND1 || *pTemp == PARSE_SYM_AND2 )
Parse_StackOpPush( pStackOp, PARSE_OPER_AND );
else //if ( Str[Pos] == PARSE_SYM_OR )
else if ( *pTemp == PARSE_SYM_OR1 || *pTemp == PARSE_SYM_OR2 )
Parse_StackOpPush( pStackOp, PARSE_OPER_OR );
else //if ( Str[Pos] == PARSE_SYM_XOR )
Parse_StackOpPush( pStackOp, PARSE_OPER_XOR );
Flag = PARSE_FLAG_OPER;
break;
......
src/map/if/ifMap.c
......@@ -296,6 +296,7 @@ int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fPrepr
}
else if ( If_ObjIsCi(pObj) )
{
//printf( "processing CI %d\n", pObj->Id );
arrTime = Tim_ManGetCiArrival( p->pManTim, pObj->IdPio );
If_ObjSetArrTime( pObj, arrTime );
}
......
src/map/mio/mioFunc.c
......@@ -25,7 +25,9 @@
// these symbols (and no other) can appear in the formulas
#define MIO_SYMB_AND '*'
#define MIO_SYMB_OR '+'
#define MIO_SYMB_OR1 '+'
#define MIO_SYMB_OR2 '|'
#define MIO_SYMB_XOR '^'
#define MIO_SYMB_NOT '!'
#define MIO_SYMB_AFTNOT '\''
#define MIO_SYMB_OPEN '('
......@@ -239,8 +241,9 @@ int Mio_GateCollectNames( char * pFormula, char * pPinNames[] )
// remove the non-name symbols
for ( pTemp = Buffer; *pTemp; pTemp++ )
if ( *pTemp == MIO_SYMB_AND || *pTemp == MIO_SYMB_OR || *pTemp == MIO_SYMB_NOT
|| *pTemp == MIO_SYMB_OPEN || *pTemp == MIO_SYMB_CLOSE || *pTemp == MIO_SYMB_AFTNOT )
if ( *pTemp == MIO_SYMB_AND || *pTemp == MIO_SYMB_OR1 || *pTemp == MIO_SYMB_OR2
|| *pTemp == MIO_SYMB_XOR || *pTemp == MIO_SYMB_NOT || *pTemp == MIO_SYMB_OPEN
|| *pTemp == MIO_SYMB_CLOSE || *pTemp == MIO_SYMB_AFTNOT )
*pTemp = ' ';
// save the names
......
src/map/mio/mioRead.c
......@@ -265,7 +265,7 @@ Mio_Gate_t * Mio_LibraryReadGate( char ** ppToken, bool fExtendedFormat )
// then rest of the expression
pToken = strtok( NULL, ";" );
pGate->pForm = Extra_UtilStrsav( pToken );
pGate->pForm = chomp( pToken );
// read the pin info
// start the linked list of pins
......@@ -392,21 +392,27 @@ Mio_Pin_t * Mio_LibraryReadPin( char ** ppToken, bool fExtendedFormat )
SeeAlso []
***********************************************************************/
char *chomp( char *s )
char * chomp( char *s )
{
char *b = ALLOC(char, strlen(s)+1), *c = b;
while (*s && isspace(*s))
++s;
while (*s && !isspace(*s))
*c++ = *s++;
char *a, *b, *c;
// remove leading spaces
for ( b = s; *b; b++ )
if ( !isspace(*b) )
break;
// strsav the string
a = strcpy( ALLOC(char, strlen(b)+1), b );
// remove trailing spaces
for ( c = a+strlen(a); c > a; c-- )
if ( *c == 0 || isspace(*c) )
*c = 0;
return b;
else
break;
return a;
}
/**Function*************************************************************
Synopsis [Duplicates string and returns it with leading and
trailing spaces removed.]
Synopsis []
Description []
......
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