Skip to content

A
abc
Commit 93c05287 by Alan Mishchenko
Options

Version abc70302

parent 81fae91a
Showing with 1133 additions and 37 deletions
abc.dsp
......@@ -310,6 +310,10 @@ SOURCE=.\src\base\abci\abcProve.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcQbf.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcQuant.c
# End Source File
# Begin Source File
......
abc.rc
......@@ -77,7 +77,8 @@ alias tr1 trace_check
alias trt "r c.blif; st; tr0; b; tr1"
alias u undo
alias w write
alias wb write_blif
alias wa write_aiger
alias wb write_bench
alias wh write_hie
alias wl write_blif
alias wp write_pla
......
src/base/abc/abc.h
......@@ -341,6 +341,7 @@ static inline Abc_Obj_t * Abc_ObjNotCond( Abc_Obj_t * p, int c ) { return (A
static inline unsigned Abc_ObjType( Abc_Obj_t * pObj ) { return pObj->Type; }
static inline unsigned Abc_ObjId( Abc_Obj_t * pObj ) { return pObj->Id; }
static inline int Abc_ObjTravId( Abc_Obj_t * pObj ) { return pObj->TravId; }
static inline int Abc_ObjLevel( Abc_Obj_t * pObj ) { return pObj->Level; }
static inline Vec_Int_t * Abc_ObjFaninVec( Abc_Obj_t * pObj ) { return &pObj->vFanins; }
static inline Vec_Int_t * Abc_ObjFanoutVec( Abc_Obj_t * pObj ) { return &pObj->vFanouts; }
static inline Abc_Obj_t * Abc_ObjCopy( Abc_Obj_t * pObj ) { return pObj->pCopy; }
......@@ -609,6 +610,7 @@ extern int Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
extern void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk );
extern int Abc_NtkSopToAig( Abc_Ntk_t * pNtk );
extern int Abc_NtkAigToBdd( Abc_Ntk_t * pNtk );
extern unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth );
extern int Abc_NtkMapToSop( Abc_Ntk_t * pNtk );
extern int Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect );
extern int Abc_NtkToBdd( Abc_Ntk_t * pNtk );
......@@ -637,7 +639,7 @@ extern int Abc_NodeMinimumBase( Abc_Obj_t * pNode );
extern int Abc_NtkRemoveDupFanins( Abc_Ntk_t * pNtk );
extern int Abc_NodeRemoveDupFanins( Abc_Obj_t * pNode );
/*=== abcMiter.c ==========================================================*/
extern Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
extern Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize );
extern void Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * pNode );
extern Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOr, int fCompl2 );
extern Abc_Ntk_t * Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues );
......
src/base/abc/abcAig.c
......@@ -1422,6 +1422,32 @@ void Abc_AigUpdateReset( Abc_Aig_t * pMan )
Vec_PtrClear( pMan->vUpdatedNets );
}
/**Function*************************************************************
Synopsis [Start the update list.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_AigCountNext( Abc_Aig_t * pMan )
{
Abc_Obj_t * pAnd;
int i, Counter = 0, CounterTotal = 0;
// count how many nodes have pNext set
for ( i = 0; i < pMan->nBins; i++ )
Abc_AigBinForEachEntry( pMan->pBins[i], pAnd )
{
Counter += (pAnd->pNext != NULL);
CounterTotal++;
}
printf( "Counter = %d. Nodes = %d. Ave = %6.2f\n", Counter, CounterTotal, 1.0 * CounterTotal/pMan->nBins );
return Counter;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/base/abc/abcFunc.c
......@@ -796,6 +796,131 @@ DdNode * Abc_ConvertAigToBdd( DdManager * dd, Hop_Obj_t * pRoot )
SeeAlso []
***********************************************************************/
int Abc_ConvertAigToTruth_rec1( Hop_Obj_t * pObj )
{
int Counter = 0;
assert( !Hop_IsComplement(pObj) );
if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
return 0;
Counter += Abc_ConvertAigToTruth_rec1( Hop_ObjFanin0(pObj) );
Counter += Abc_ConvertAigToTruth_rec1( Hop_ObjFanin1(pObj) );
assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
Hop_ObjSetMarkA( pObj );
return Counter + 1;
}
/**Function*************************************************************
Synopsis [Computes truth table of the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned * Abc_ConvertAigToTruth_rec2( Hop_Obj_t * pObj, Vec_Int_t * vTruth, int nWords )
{
unsigned * pTruth, * pTruth0, * pTruth1;
int i;
assert( !Hop_IsComplement(pObj) );
if ( !Hop_ObjIsNode(pObj) || !Hop_ObjIsMarkA(pObj) )
return pObj->pData;
// compute the truth tables of the fanins
pTruth0 = Abc_ConvertAigToTruth_rec2( Hop_ObjFanin0(pObj), vTruth, nWords );
pTruth1 = Abc_ConvertAigToTruth_rec2( Hop_ObjFanin1(pObj), vTruth, nWords );
// creat the truth table of the node
pTruth = Vec_IntFetch( vTruth, nWords );
if ( Hop_ObjIsExor(pObj) )
for ( i = 0; i < nWords; i++ )
pTruth[i] = pTruth0[i] ^ pTruth1[i];
else if ( !Hop_ObjFaninC0(pObj) && !Hop_ObjFaninC1(pObj) )
for ( i = 0; i < nWords; i++ )
pTruth[i] = pTruth0[i] & pTruth1[i];
else if ( !Hop_ObjFaninC0(pObj) && Hop_ObjFaninC1(pObj) )
for ( i = 0; i < nWords; i++ )
pTruth[i] = pTruth0[i] & ~pTruth1[i];
else if ( Hop_ObjFaninC0(pObj) && !Hop_ObjFaninC1(pObj) )
for ( i = 0; i < nWords; i++ )
pTruth[i] = ~pTruth0[i] & pTruth1[i];
else // if ( Hop_ObjFaninC0(pObj) && Hop_ObjFaninC1(pObj) )
for ( i = 0; i < nWords; i++ )
pTruth[i] = ~pTruth0[i] & ~pTruth1[i];
assert( Hop_ObjIsMarkA(pObj) ); // loop detection
Hop_ObjClearMarkA( pObj );
pObj->pData = pTruth;
return pTruth;
}
/**Function*************************************************************
Synopsis [Computes truth table of the node.]
Description [Assumes that the structural support is no more than 8 inputs.
Uses array vTruth to store temporary truth tables. The returned pointer should
be used immediately.]
SideEffects []
SeeAlso []
***********************************************************************/
unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth )
{
static unsigned uTruths[8][8] = { // elementary truth tables
{ 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA },
{ 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC },
{ 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 },
{ 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 },
{ 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 },
{ 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF },
{ 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF },
{ 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF }
};
Hop_Obj_t * pObj;
unsigned * pTruth, * pTruth2;
int i, nWords, nNodes;
// clear the data fields and set marks
nNodes = Abc_ConvertAigToTruth_rec1( pRoot );
// prepare memory
nWords = Hop_TruthWordNum( nVars );
Vec_IntClear( vTruth );
Vec_IntGrow( vTruth, nWords * nNodes );
pTruth = Vec_IntFetch( vTruth, nWords );
// check the case of a constant
if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
{
assert( nNodes == 0 );
if ( Hop_IsComplement(pRoot) )
Extra_TruthClear( pTruth, nVars );
else
Extra_TruthFill( pTruth, nVars );
return pTruth;
}
// set elementary truth tables at the leaves
assert( Hop_ManPiNum(p) <= 8 );
Hop_ManForEachPi( p, pObj, i )
pObj->pData = (void *)uTruths[i];
// clear the marks and compute the truth table
pTruth2 = Abc_ConvertAigToTruth_rec2( pRoot, vTruth, nWords );
// copy the result
Extra_TruthCopy( pTruth, pTruth2, nVars );
return pTruth;
}
/**Function*************************************************************
Synopsis [Construct BDDs and mark AIG nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_ConvertAigToAig_rec( Abc_Ntk_t * pNtkAig, Hop_Obj_t * pObj )
{
assert( !Hop_IsComplement(pObj) );
......
src/base/abc/abcObj.c
......@@ -446,7 +446,7 @@ Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName )
// find the internal node
if ( pName[0] != '[' || pName[strlen(pName)-1] != ']' )
{
printf( "Name \"%s\" is not found among CIs/COs (internal names often look as \"[integer]\").\n", pName );
printf( "Name \"%s\" is not found among CO or node names (internal names often look as \"n<num>\").\n", pName );
return NULL;
}
Num = atoi( pName + 1 );
......
src/base/abc/abcUtil.c
......@@ -1294,6 +1294,7 @@ void Abc_NtkReassignIds( Abc_Ntk_t * pNtk )
Abc_Obj_t * pNode, * pTemp, * pConst1;
int i, k;
assert( Abc_NtkIsStrash(pNtk) );
//printf( "Total = %d. Current = %d.\n", Abc_NtkObjNumMax(pNtk), Abc_NtkObjNum(pNtk) );
// start the array of objects with new IDs
vObjsNew = Vec_PtrAlloc( pNtk->nObjs );
// put constant node first
......
src/base/abci/abcGen.c
......@@ -254,6 +254,112 @@ void Abc_WriteFullAdder( FILE * pFile )
fprintf( pFile, "\n" );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_WriteCell( FILE * pFile )
{
fprintf( pFile, ".model cell\n" );
fprintf( pFile, ".inputs px1 px2 py1 py2 x y\n" );
fprintf( pFile, ".outputs fx fy\n" );
fprintf( pFile, ".names x y a\n" );
fprintf( pFile, "11 1\n" );
fprintf( pFile, ".names px1 a x nx\n" );
fprintf( pFile, "11- 1\n" );
fprintf( pFile, "0-1 1\n" );
fprintf( pFile, ".names py1 a y ny\n" );
fprintf( pFile, "11- 1\n" );
fprintf( pFile, "0-1 1\n" );
fprintf( pFile, ".names px2 nx fx\n" );
fprintf( pFile, "10 1\n" );
fprintf( pFile, "01 1\n" );
fprintf( pFile, ".names py2 ny fy\n" );
fprintf( pFile, "10 1\n" );
fprintf( pFile, "01 1\n" );
fprintf( pFile, ".end\n" );
fprintf( pFile, "\n" );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_GenMesh( char * pFileName, int nVars )
{
FILE * pFile;
int i, k;
assert( nVars > 0 );
pFile = fopen( pFileName, "w" );
fprintf( pFile, "# %dx%d mesh generated by ABC on %s\n", nVars, nVars, Extra_TimeStamp() );
fprintf( pFile, ".model mesh%d\n", nVars );
for ( i = 0; i < nVars; i++ )
for ( k = 0; k < nVars; k++ )
{
fprintf( pFile, ".inputs" );
fprintf( pFile, " p%d%dx1", i, k );
fprintf( pFile, " p%d%dx2", i, k );
fprintf( pFile, " p%d%dy1", i, k );
fprintf( pFile, " p%d%dy2", i, k );
fprintf( pFile, "\n" );
}
fprintf( pFile, ".inputs" );
for ( i = 0; i < nVars; i++ )
fprintf( pFile, " v%02d v%02d", 2*i, 2*i+1 );
fprintf( pFile, "\n" );
fprintf( pFile, ".outputs" );
fprintf( pFile, " fx00" );
fprintf( pFile, "\n" );
for ( i = 0; i < nVars; i++ ) // horizontal
for ( k = 0; k < nVars; k++ ) // vertical
{
fprintf( pFile, ".subckt cell" );
fprintf( pFile, " px1=p%d%dx1", i, k );
fprintf( pFile, " px2=p%d%dx2", i, k );
fprintf( pFile, " py1=p%d%dy1", i, k );
fprintf( pFile, " py2=p%d%dy2", i, k );
if ( k == nVars - 1 )
fprintf( pFile, " x=v%02d", i );
else
fprintf( pFile, " x=fx%d%d", i, k+1 );
if ( i == nVars - 1 )
fprintf( pFile, " y=v%02d", nVars+k );
else
fprintf( pFile, " y=fy%d%d", i+1, k );
// outputs
fprintf( pFile, " fx=fx%d%d", i, k );
fprintf( pFile, " fy=fy%d%d", i, k );
fprintf( pFile, "\n" );
}
fprintf( pFile, ".end\n" );
fprintf( pFile, "\n" );
fprintf( pFile, "\n" );
Abc_WriteCell( pFile );
fclose( pFile );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/base/abci/abcMiter.c
......@@ -24,10 +24,10 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
static Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize );
static void Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb );
static void Abc_NtkMiterAddOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter );
static void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb );
static void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize );
static void Abc_NtkAddFrame( Abc_Ntk_t * pNetNew, Abc_Ntk_t * pNet, int iFrame );
// to be exported
......@@ -50,7 +50,7 @@ static void Abc_NtkAddFrame2( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, i
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize )
{
Abc_Ntk_t * pTemp = NULL;
int fRemove1, fRemove2;
......@@ -63,7 +63,7 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
fRemove1 = (!Abc_NtkIsStrash(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0, 0));
fRemove2 = (!Abc_NtkIsStrash(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0, 0));
if ( pNtk1 && pNtk2 )
pTemp = Abc_NtkMiterInt( pNtk1, pNtk2, fComb );
pTemp = Abc_NtkMiterInt( pNtk1, pNtk2, fComb, nPartSize );
if ( fRemove1 ) Abc_NtkDelete( pNtk1 );
if ( fRemove2 ) Abc_NtkDelete( pNtk2 );
return pTemp;
......@@ -80,7 +80,7 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize )
{
char Buffer[1000];
Abc_Ntk_t * pNtkMiter;
......@@ -97,7 +97,7 @@ Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
Abc_NtkMiterPrepare( pNtk1, pNtk2, pNtkMiter, fComb );
Abc_NtkMiterAddOne( pNtk1, pNtkMiter );
Abc_NtkMiterAddOne( pNtk2, pNtkMiter );
Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, fComb );
Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, fComb, nPartSize );
// make sure that everything is okay
if ( !Abc_NtkCheck( pNtkMiter ) )
......@@ -243,7 +243,7 @@ void Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * p
SeeAlso []
***********************************************************************/
void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb )
void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize )
{
Vec_Ptr_t * vPairs;
Abc_Obj_t * pMiter, * pNode;
......@@ -276,9 +276,46 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt
Abc_ObjAddFanin( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjChild0Copy(Abc_ObjFanin0(pNode)) );
}
// add the miter
if ( nPartSize == 0 )
{
pMiter = Abc_AigMiter( pNtkMiter->pManFunc, vPairs );
Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter );
Vec_PtrFree( vPairs );
}
else
{
char Buffer[10];
Vec_Ptr_t * vPairsPart;
int nParts, i, k, iCur;
assert( Vec_PtrSize(vPairs) == 2 * Abc_NtkCoNum(pNtk1) );
// create partitions
nParts = Abc_NtkCoNum(pNtk1) / nPartSize + (int)((Abc_NtkCoNum(pNtk1) % nPartSize) > 0);
vPairsPart = Vec_PtrAlloc( nPartSize );
for ( i = 0; i < nParts; i++ )
{
Vec_PtrClear( vPairsPart );
for ( k = 0; k < nPartSize; k++ )
{
iCur = i * nPartSize + k;
if ( iCur >= Abc_NtkCoNum(pNtk1) )
break;
Vec_PtrPush( vPairsPart, Vec_PtrEntry(vPairs, 2*iCur ) );
Vec_PtrPush( vPairsPart, Vec_PtrEntry(vPairs, 2*iCur+1) );
}
pMiter = Abc_AigMiter( pNtkMiter->pManFunc, vPairsPart );
if ( i == 0 )
Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter );
else
{
sprintf( Buffer, "%d", i );
pNode = Abc_NtkCreatePo( pNtkMiter );
Abc_ObjAssignName( pNode, "miter", Buffer );
Abc_ObjAddFanin( pNode, pMiter );
}
}
Vec_PtrFree( vPairsPart );
Vec_PtrFree( vPairs );
}
}
......
src/base/abci/abcPrint.c
......@@ -52,6 +52,10 @@ int s_MappingMem = 0;
void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
{
int Num;
// if ( Abc_NtkIsStrash(pNtk) )
// Abc_AigCountNext( pNtk->pManFunc );
fprintf( pFile, "%-13s:", pNtk->pName );
if ( Abc_NtkAssertNum(pNtk) )
fprintf( pFile, " i/o/a = %4d/%4d/%4d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk), Abc_NtkAssertNum(pNtk) );
......
src/base/abci/abcQbf.c 0 → 100644
/**CFile****************************************************************
FileName [abcQbf.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Network and node package.]
Synopsis [Implementation of a simple QBF solver.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: abcQbf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "abc.h"
/*
Implementation of a simple QBF solver along the lines of
A. Solar-Lezama, L. Tancau, R. Bodik, V. Saraswat, and S. Seshia,
"Combinatorial sketching for finite programs", 12th International
Conference on Architectural Support for Programming Languages and
Operating Systems (ASPLOS 2006), San Jose, CA, October 2006.
*/
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static void Abc_NtkModelToVector( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues );
static void Abc_NtkVectorClearPars( Vec_Int_t * vPiValues, int nPars );
static void Abc_NtkVectorClearVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int nPars );
static void Abc_NtkVectorPrintPars( Vec_Int_t * vPiValues, int nPars );
static void Abc_NtkVectorPrintVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int nPars );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Solve the QBF problem EpAx[M(p,x)].]
Description [Variables p go first, followed by variable x.
The number of parameters is nPars. The miter is in pNtk.
The miter expresses EQUALITY of the implementation and spec.]
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int fVerbose )
{
Abc_Ntk_t * pNtkVer, * pNtkSyn, * pNtkSyn2, * pNtkTemp;
Vec_Int_t * vPiValues;
int clkTotal = clock(), clkS, clkV;
int nIters, nIterMax = 500, nInputs, RetValue, fFound = 0;
assert( Abc_NtkIsStrash(pNtk) );
assert( Abc_NtkIsComb(pNtk) );
assert( Abc_NtkPoNum(pNtk) == 1 );
assert( nPars > 0 && nPars < Abc_NtkPiNum(pNtk) );
assert( Abc_NtkPiNum(pNtk)-nPars < 32 );
nInputs = Abc_NtkPiNum(pNtk) - nPars;
// initialize the synthesized network with 0000-combination
vPiValues = Vec_IntStart( Abc_NtkPiNum(pNtk) );
Abc_NtkVectorClearPars( vPiValues, nPars );
pNtkSyn = Abc_NtkMiterCofactor( pNtk, vPiValues );
if ( fVerbose )
{
printf( "Iter %2d : ", 0 );
printf( "AIG = %6d ", Abc_NtkNodeNum(pNtkSyn) );
Abc_NtkVectorPrintVars( pNtk, vPiValues, nPars );
printf( "\n" );
}
// iteratively solve
for ( nIters = 0; nIters < nIterMax; nIters++ )
{
// solve the synthesis instance
clkS = clock();
RetValue = Abc_NtkMiterSat( pNtkSyn, 0, 0, 0, NULL, NULL );
clkS = clock() - clkS;
if ( RetValue == 0 )
Abc_NtkModelToVector( pNtkSyn, vPiValues );
if ( RetValue == 1 )
{
break;
}
if ( RetValue == -1 )
{
printf( "Synthesis timed out.\n" );
break;
}
// there is a counter-example
// construct the verification instance
Abc_NtkVectorClearVars( pNtk, vPiValues, nPars );
pNtkVer = Abc_NtkMiterCofactor( pNtk, vPiValues );
// complement the output
Abc_ObjXorFaninC( Abc_NtkPo(pNtkVer,0), 0 );
// solve the verification instance
clkV = clock();
RetValue = Abc_NtkMiterSat( pNtkVer, 0, 0, 0, NULL, NULL );
clkV = clock() - clkV;
if ( RetValue == 0 )
Abc_NtkModelToVector( pNtkVer, vPiValues );
Abc_NtkDelete( pNtkVer );
if ( RetValue == 1 )
{
fFound = 1;
break;
}
if ( RetValue == -1 )
{
printf( "Verification timed out.\n" );
break;
}
// there is a counter-example
// create a new synthesis network
Abc_NtkVectorClearPars( vPiValues, nPars );
pNtkSyn2 = Abc_NtkMiterCofactor( pNtk, vPiValues );
// add to the synthesis instance
pNtkSyn = Abc_NtkMiterAnd( pNtkTemp = pNtkSyn, pNtkSyn2, 0, 0 );
Abc_NtkDelete( pNtkSyn2 );
Abc_NtkDelete( pNtkTemp );
if ( fVerbose )
{
printf( "Iter %2d : ", nIters+1 );
printf( "AIG = %6d ", Abc_NtkNodeNum(pNtkSyn) );
Abc_NtkVectorPrintVars( pNtk, vPiValues, nPars );
printf( " " );
PRTn( "Syn", clkS );
PRT( "Ver", clkV );
}
}
Abc_NtkDelete( pNtkSyn );
// report the results
if ( fFound )
{
printf( "Parameters: " );
Abc_NtkVectorPrintPars( vPiValues, nPars );
printf( "\n" );
printf( "Solved after %d interations. ", nIters );
}
else if ( nIters == nIterMax )
printf( "Unsolved after %d interations. ", nIters );
else
printf( "Implementation does not exist. " );
PRT( "Total runtime", clock() - clkTotal );
Vec_IntFree( vPiValues );
}
/**Function*************************************************************
Synopsis [Translates model into the vector of values.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkModelToVector( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues )
{
int * pModel, i;
pModel = pNtk->pModel;
for ( i = 0; i < Abc_NtkPiNum(pNtk); i++ )
Vec_IntWriteEntry( vPiValues, i, pModel[i] );
}
/**Function*************************************************************
Synopsis [Clears parameters.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkVectorClearPars( Vec_Int_t * vPiValues, int nPars )
{
int i;
for ( i = 0; i < nPars; i++ )
Vec_IntWriteEntry( vPiValues, i, -1 );
}
/**Function*************************************************************
Synopsis [Clears variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkVectorClearVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int nPars )
{
int i;
for ( i = nPars; i < Abc_NtkPiNum(pNtk); i++ )
Vec_IntWriteEntry( vPiValues, i, -1 );
}
/**Function*************************************************************
Synopsis [Clears variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkVectorPrintPars( Vec_Int_t * vPiValues, int nPars )
{
int i;
for ( i = 0; i < nPars; i++ )
printf( "%d", Vec_IntEntry(vPiValues,i) );
}
/**Function*************************************************************
Synopsis [Clears variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkVectorPrintVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int nPars )
{
int i;
for ( i = nPars; i < Abc_NtkPiNum(pNtk); i++ )
printf( "%d", Vec_IntEntry(vPiValues,i) );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/base/abci/abcQuant.c
......@@ -72,7 +72,7 @@ void Abc_NtkSynthesize( Abc_Ntk_t ** ppNtk, int fMoreEffort )
SeeAlso []
***********************************************************************/
int Abc_NtkQuantify( Abc_Ntk_t * pNtk, int iVar, int fVerbose )
int Abc_NtkQuantify( Abc_Ntk_t * pNtk, int fUniv, int iVar, int fVerbose )
{
Vec_Ptr_t * vNodes;
Abc_Obj_t * pObj, * pNext, * pFanin;
......@@ -112,6 +112,9 @@ int Abc_NtkQuantify( Abc_Ntk_t * pNtk, int iVar, int fVerbose )
continue;
pFanin = Abc_ObjFanin0(pObj);
// get the result of quantification
if ( fUniv )
pNext = Abc_AigAnd( pNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild0Data(pObj) );
else
pNext = Abc_AigOr( pNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild0Data(pObj) );
pNext = Abc_ObjNotCond( pNext, Abc_ObjFaninC0(pObj) );
if ( Abc_ObjRegular(pNext) == pFanin )
......@@ -197,7 +200,7 @@ Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose )
for ( i = Abc_NtkPiNum(pNtkNew) - 1; i >= 2*nLatches; i-- )
// for ( i = 2*nLatches; i < Abc_NtkPiNum(pNtkNew); i++ )
{
Abc_NtkQuantify( pNtkNew, i, fVerbose );
Abc_NtkQuantify( pNtkNew, 0, i, fVerbose );
// if ( fSynthesis && (i % 3 == 2) )
if ( fSynthesis )
{
......@@ -339,7 +342,7 @@ Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose )
// quantify the current state variables
for ( v = 0; v < nVars; v++ )
{
Abc_NtkQuantify( pNtkNext, v, fVerbose );
Abc_NtkQuantify( pNtkNext, 0, v, fVerbose );
if ( fSynthesis && (v % 3 == 2) )
{
Abc_NtkCleanData( pNtkNext );
......
src/base/abci/abcRr.c
......@@ -354,7 +354,7 @@ int Abc_NtkRRProve( Abc_RRMan_t * p )
Abc_NtkRRUpdate( pWndCopy, p->pNode->pCopy->pCopy, p->pFanin->pCopy->pCopy, p->pFanout? p->pFanout->pCopy->pCopy : NULL );
if ( !Abc_NtkIsDfsOrdered(pWndCopy) )
Abc_NtkReassignIds(pWndCopy);
p->pMiter = Abc_NtkMiter( p->pWnd, pWndCopy, 1 );
p->pMiter = Abc_NtkMiter( p->pWnd, pWndCopy, 1, 0 );
Abc_NtkDelete( pWndCopy );
clk = clock();
RetValue = Abc_NtkMiterProve( &p->pMiter, p->pParams );
......
src/base/abci/abcVerify.c
......@@ -52,7 +52,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
int RetValue;
// get the miter of the two networks
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1 );
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0 );
if ( pMiter == NULL )
{
printf( "Miter computation has failed.\n" );
......@@ -120,7 +120,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
int RetValue;
// get the miter of the two networks
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1 );
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0 );
if ( pMiter == NULL )
{
printf( "Miter computation has failed.\n" );
......@@ -198,6 +198,108 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
/**Function*************************************************************
Synopsis [Verifies sequential equivalence by fraiging followed by SAT.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nPartSize, int fVerbose )
{
extern int Cmd_CommandExecute( void * pAbc, char * sCommand );
extern void * Abc_FrameGetGlobalFrame();
Prove_Params_t Params, * pParams = &Params;
Abc_Ntk_t * pMiter, * pMiterPart;
Abc_Obj_t * pObj;
int i, RetValue, Status, nOutputs;
// solve the CNF using the SAT solver
Prove_ParamsSetDefault( pParams );
pParams->nItersMax = 5;
// pParams->fVerbose = 1;
assert( nPartSize > 0 );
// get the miter of the two networks
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, nPartSize );
if ( pMiter == NULL )
{
printf( "Miter computation has failed.\n" );
return;
}
RetValue = Abc_NtkMiterIsConstant( pMiter );
if ( RetValue == 0 )
{
printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
// report the error
pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 );
Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
FREE( pMiter->pModel );
Abc_NtkDelete( pMiter );
return;
}
if ( RetValue == 1 )
{
printf( "Networks are equivalent after structural hashing.\n" );
Abc_NtkDelete( pMiter );
return;
}
Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" );
// solve the problem iteratively for each output of the miter
Status = 1;
nOutputs = 0;
Abc_NtkForEachPo( pMiter, pObj, i )
{
// get the cone of this output
pMiterPart = Abc_NtkCreateCone( pMiter, Abc_ObjFanin0(pObj), Abc_ObjName(pObj), 0 );
if ( Abc_ObjFaninC0(pObj) )
Abc_ObjXorFaninC( Abc_NtkPo(pMiterPart,0), 0 );
// solve the cone
// RetValue = Abc_NtkMiterProve( &pMiterPart, pParams );
RetValue = Abc_NtkIvyProve( &pMiterPart, pParams );
if ( RetValue == -1 )
{
printf( "Networks are undecided (resource limits is reached).\r" );
Status = -1;
}
else if ( RetValue == 0 )
{
int * pSimInfo = Abc_NtkVerifySimulatePattern( pMiterPart, pMiterPart->pModel );
if ( pSimInfo[0] != 1 )
printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" );
else
printf( "Networks are NOT EQUIVALENT. \n" );
free( pSimInfo );
Status = 0;
break;
}
else
{
printf( "Finished part %d (out of %d)\r", i+1, Abc_NtkPoNum(pMiter) );
nOutputs += nPartSize;
}
// if ( pMiter->pModel )
// Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
Abc_NtkDelete( pMiterPart );
}
Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" );
if ( Status == 1 )
printf( "Networks are equivalent. \n" );
else if ( Status == -1 )
printf( "Timed out after verifying %d outputs (out of %d).\n", nOutputs, Abc_NtkCoNum(pNtk1) );
Abc_NtkDelete( pMiter );
}
/**Function*************************************************************
Synopsis [Verifies sequential equivalence by brute-force SAT.]
Description []
......@@ -216,7 +318,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
int RetValue;
// get the miter of the two networks
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0 );
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 );
if ( pMiter == NULL )
{
printf( "Miter computation has failed.\n" );
......@@ -298,7 +400,7 @@ int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFr
int RetValue;
// get the miter of the two networks
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0 );
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 );
if ( pMiter == NULL )
{
printf( "Miter computation has failed.\n" );
......
src/base/abci/abc_new.h 0 → 100644
struct Abc_Obj_t_ // 6 words
{
Abc_Obj_t * pCopy; // the copy of this object
Abc_Ntk_t * pNtk; // the host network
int Id; // the object ID
int TravId; // the traversal ID
int nRefs; // the number of fanouts
unsigned Type : 4; // the object type
unsigned fMarkA : 1; // the multipurpose mark
unsigned fMarkB : 1; // the multipurpose mark
unsigned fPhase : 1; // the flag to mark the phase of equivalent node
unsigned fPersist: 1; // marks the persistant AIG node
unsigned nFanins : 24; // the level of the node
Abc_Obj_t * Fanins[0]; // the array of fanins
};
struct Abc_Pin_t_ // 4 words
{
Abc_Pin_t * pNext;
Abc_Pin_t * pPrev;
Abc_Obj_t * pFanin;
Abc_Obj_t * pFanout;
};
src/base/abci/module.make
......@@ -30,6 +30,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcPlace.c \
src/base/abci/abcPrint.c \
src/base/abci/abcProve.c \
src/base/abci/abcQbf.c \
src/base/abci/abcQuant.c \
src/base/abci/abcReconv.c \
src/base/abci/abcRefactor.c \
......
src/base/io/io.c
......@@ -29,6 +29,7 @@ static int IoCommandRead ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadAiger ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadBaf ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadBlif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadBlifMv ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadBench ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadEdif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadEqn ( Abc_Frame_t * pAbc, int argc, char **argv );
......@@ -43,6 +44,7 @@ static int IoCommandWriteHie ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteAiger ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteBaf ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteBlif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteBlifMv ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteBench ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteCellNet( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteCnf ( Abc_Frame_t * pAbc, int argc, char **argv );
......@@ -78,6 +80,7 @@ void Io_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "I/O", "read_aiger", IoCommandReadAiger, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_baf", IoCommandReadBaf, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_blif", IoCommandReadBlif, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_blif_mv", IoCommandReadBlif, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_bench", IoCommandReadBench, 1 );
// Cmd_CommandAdd( pAbc, "I/O", "read_edif", IoCommandReadEdif, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_eqn", IoCommandReadEqn, 1 );
......@@ -92,6 +95,7 @@ void Io_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "I/O", "write_aiger", IoCommandWriteAiger, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_baf", IoCommandWriteBaf, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_blif", IoCommandWriteBlif, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_blif_mv", IoCommandWriteBlifMv, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_bench", IoCommandWriteBench, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_cellnet", IoCommandWriteCellNet, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_counter", IoCommandWriteCounter, 0 );
......@@ -371,6 +375,60 @@ usage:
SeeAlso []
***********************************************************************/
int IoCommandReadBlifMv( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk;
char * pFileName;
int fCheck;
int c;
fCheck = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
{
switch ( c )
{
case 'c':
fCheck ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( argc != globalUtilOptind + 1 )
goto usage;
// get the input file name
pFileName = argv[globalUtilOptind];
// read the file using the corresponding file reader
pNtk = Io_Read( pFileName, IO_FILE_BLIFMV, fCheck );
if ( pNtk == NULL )
return 1;
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
return 0;
usage:
fprintf( pAbc->Err, "usage: read_blif_mv [-ch] <file>\n" );
fprintf( pAbc->Err, "\t read the network in BLIF-MV format\n" );
fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int IoCommandReadBench( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk;
......@@ -988,13 +1046,18 @@ usage:
int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv )
{
char * pFileName;
int fWriteSymbols;
int c;
fWriteSymbols = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "sh" ) ) != EOF )
{
switch ( c )
{
case 's':
fWriteSymbols ^= 1;
break;
case 'h':
goto usage;
default:
......@@ -1006,12 +1069,23 @@ int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv )
// get the output file name
pFileName = argv[globalUtilOptind];
// call the corresponding file writer
if ( fWriteSymbols )
Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_AIGER );
else
{
if ( !Abc_NtkIsStrash(pAbc->pNtkCur) )
{
fprintf( stdout, "Writing this format is only possible for structurally hashed AIGs.\n" );
return 1;
}
Io_WriteAiger( pAbc->pNtkCur, pFileName, 0 );
}
return 0;
usage:
fprintf( pAbc->Err, "usage: write_aiger [-h] <file>\n" );
fprintf( pAbc->Err, "usage: write_aiger [-sh] <file>\n" );
fprintf( pAbc->Err, "\t write the network in the AIGER format (http://fmv.jku.at/aiger)\n" );
fprintf( pAbc->Err, "\t-s : toggle saving I/O names [default = %s]\n", fWriteSymbols? "yes" : "no" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .aig)\n" );
return 1;
......@@ -1096,7 +1170,7 @@ int IoCommandWriteBlif( Abc_Frame_t * pAbc, int argc, char **argv )
return 0;
usage:
fprintf( pAbc->Err, "usage: write_blif [-lh] <file>\n" );
fprintf( pAbc->Err, "usage: write_blif [-h] <file>\n" );
fprintf( pAbc->Err, "\t write the network into a BLIF file\n" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .blif)\n" );
......@@ -1114,16 +1188,64 @@ usage:
SeeAlso []
***********************************************************************/
int IoCommandWriteBlifMv( Abc_Frame_t * pAbc, int argc, char **argv )
{
char * pFileName;
int c;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
case 'h':
goto usage;
default:
goto usage;
}
}
if ( argc != globalUtilOptind + 1 )
goto usage;
// get the output file name
pFileName = argv[globalUtilOptind];
// call the corresponding file writer
Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BLIFMV );
return 0;
usage:
fprintf( pAbc->Err, "usage: write_blif_mv [-h] <file>\n" );
fprintf( pAbc->Err, "\t write the network into a BLIF-MV file\n" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .blif)\n" );
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int IoCommandWriteBench( Abc_Frame_t * pAbc, int argc, char **argv )
{
char * pFileName;
int fUseLuts;
int c;
fUseLuts = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "lh" ) ) != EOF )
{
switch ( c )
{
case 'l':
fUseLuts ^= 1;
break;
case 'h':
goto usage;
default:
......@@ -1135,12 +1257,22 @@ int IoCommandWriteBench( Abc_Frame_t * pAbc, int argc, char **argv )
// get the output file name
pFileName = argv[globalUtilOptind];
// call the corresponding file writer
if ( !fUseLuts )
Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BENCH );
else
{
Abc_Ntk_t * pNtkTemp;
pNtkTemp = Abc_NtkToNetlist( pAbc->pNtkCur );
Abc_NtkToAig( pNtkTemp );
Io_WriteBenchLut( pNtkTemp, pFileName );
Abc_NtkDelete( pNtkTemp );
}
return 0;
usage:
fprintf( pAbc->Err, "usage: write_bench [-h] <file>\n" );
fprintf( pAbc->Err, "usage: write_bench [-lh] <file>\n" );
fprintf( pAbc->Err, "\t write the network in BENCH format\n" );
fprintf( pAbc->Err, "\t-l : toggle using LUTs in the output [default = %s]\n", fUseLuts? "yes" : "no" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .bench)\n" );
return 1;
......
src/base/io/io.h
......@@ -87,7 +87,7 @@ extern Abc_Ntk_t * Io_ReadPla( char * pFileName, int fCheck );
/*=== abcReadVerilog.c ========================================================*/
extern Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck );
/*=== abcWriteAiger.c =========================================================*/
extern void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName );
extern void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols );
/*=== abcWriteBaf.c ===========================================================*/
extern void Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName );
/*=== abcWriteBlif.c ==========================================================*/
......@@ -98,6 +98,7 @@ extern void Io_WriteTimingInfo( FILE * pFile, Abc_Ntk_t * pNtk );
extern void Io_WriteBlifMv( Abc_Ntk_t * pNtk, char * FileName );
/*=== abcWriteBench.c =========================================================*/
extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName );
extern int Io_WriteBenchLut( Abc_Ntk_t * pNtk, char * FileName );
/*=== abcWriteCnf.c ===========================================================*/
extern int Io_WriteCnf( Abc_Ntk_t * pNtk, char * FileName, int fAllPrimes );
/*=== abcWriteDot.c ===========================================================*/
......
src/base/io/ioReadBench.c
......@@ -84,7 +84,8 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
Abc_Ntk_t * pNtk;
Abc_Obj_t * pNode;
Vec_Str_t * vString;
char * pType, ** ppNames;
unsigned uTruth[8];
char * pType, ** ppNames, * pString;
int iLine, nNames;
// allocate the empty network
......@@ -114,11 +115,71 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
{
// get the node name and the node type
pType = vTokens->pArray[1];
if ( strcmp(pType, "DFF") == 0 )
if ( strncmp(pType, "DFF", 3) == 0 ) // works for both DFF and DFFRSE
{
pNode = Io_ReadCreateLatch( pNtk, vTokens->pArray[2], vTokens->pArray[0] );
Abc_LatchSetInit0( pNode );
}
else if ( strcmp(pType, "LUT") == 0 )
{
ppNames = (char **)vTokens->pArray + 3;
nNames = vTokens->nSize - 3;
// check the number of inputs
if ( nNames > 8 )
{
printf( "%s: Currently cannot read truth tables with more than 8 inputs (%d).\n", Extra_FileReaderGetFileName(p), nNames );
Vec_StrFree( vString );
Abc_NtkDelete( pNtk );
return NULL;
}
// get the hex string
pString = vTokens->pArray[2];
if ( strncmp( pString, "0x", 2 ) )
{
printf( "%s: The LUT signature (%s) does not look like a hexadecimal beginning with \"0x\".\n", Extra_FileReaderGetFileName(p), pString );
Vec_StrFree( vString );
Abc_NtkDelete( pNtk );
return NULL;
}
pString += 2;
if ( !Extra_ReadHexadecimal( uTruth, pString, nNames ) )
{
printf( "%s: Reading hexadecimal number (%s) has failed.\n", Extra_FileReaderGetFileName(p), pString );
Vec_StrFree( vString );
Abc_NtkDelete( pNtk );
return NULL;
}
// check if the node is a constant node
if ( Extra_TruthIsConst0(uTruth, nNames) )
{
pNode = Io_ReadCreateNode( pNtk, vTokens->pArray[0], ppNames, 0 );
Abc_ObjSetData( pNode, Abc_SopRegister( pNtk->pManFunc, " 0\n" ) );
}
else if ( Extra_TruthIsConst1(uTruth, nNames) )
{
pNode = Io_ReadCreateNode( pNtk, vTokens->pArray[0], ppNames, 0 );
Abc_ObjSetData( pNode, Abc_SopRegister( pNtk->pManFunc, " 1\n" ) );
}
else
{
// create the node
pNode = Io_ReadCreateNode( pNtk, vTokens->pArray[0], ppNames, nNames );
assert( nNames > 0 );
if ( nNames > 1 )
Abc_ObjSetData( pNode, Abc_SopCreateFromTruth(pNtk->pManFunc, nNames, uTruth) );
else if ( pString[0] == '2' )
Abc_ObjSetData( pNode, Abc_SopCreateBuf(pNtk->pManFunc) );
else if ( pString[0] == '1' )
Abc_ObjSetData( pNode, Abc_SopCreateInv(pNtk->pManFunc) );
else
{
printf( "%s: Reading truth table (%s) of single-input node has failed.\n", Extra_FileReaderGetFileName(p), pString );
Vec_StrFree( vString );
Abc_NtkDelete( pNtk );
return NULL;
}
}
}
else
{
// create a new node and add it to the network
......@@ -144,10 +205,10 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
Abc_ObjSetData( pNode, Abc_SopCreateInv(pNtk->pManFunc) );
else if ( strncmp(pType, "MUX", 3) == 0 )
Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, "1-0 1\n-11 1\n") );
else if ( strncmp(pType, "vdd", 3) == 0 )
Abc_ObjSetData( pNode, Abc_SopRegister( pNtk->pManFunc, " 1\n" ) );
else if ( strncmp(pType, "gnd", 3) == 0 )
Abc_ObjSetData( pNode, Abc_SopRegister( pNtk->pManFunc, " 0\n" ) );
else if ( strncmp(pType, "vdd", 3) == 0 )
Abc_ObjSetData( pNode, Abc_SopRegister( pNtk->pManFunc, " 1\n" ) );
else
{
printf( "Io_ReadBenchNetwork(): Cannot determine gate type \"%s\" in line %d.\n", pType, Extra_FileReaderGetLineNumber(p, 0) );
......
src/base/io/ioUtil.c
......@@ -257,7 +257,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
return;
}
if ( FileType == IO_FILE_AIGER )
Io_WriteAiger( pNtk, pFileName );
Io_WriteAiger( pNtk, pFileName, 1 );
else // if ( FileType == IO_FILE_BAF )
Io_WriteBaf( pNtk, pFileName );
return;
......@@ -310,7 +310,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
{
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( stdout, "Writing BENCH is available for AIGs.\n" );
fprintf( stdout, "Writing traditional BENCH is available for AIGs only (use \"write_bench\").\n" );
return;
}
pNtkTemp = Abc_NtkToNetlistBench( pNtk );
......
src/base/io/ioWriteAiger.c
......@@ -146,7 +146,7 @@ static int Io_WriteAigerEncode( char * pBuffer, int Pos, unsigned x );
SeeAlso []
***********************************************************************/
void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName )
void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols )
{
ProgressBar * pProgress;
FILE * pFile;
......@@ -225,8 +225,10 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName )
// write the buffer
fwrite( pBuffer, 1, Pos, pFile );
free( pBuffer );
/*
// write the symbol table
if ( fWriteSymbols )
{
// write PIs
Abc_NtkForEachPi( pNtk, pObj, i )
fprintf( pFile, "i%d %s\n", i, Abc_ObjName(pObj) );
......@@ -236,7 +238,8 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName )
// write POs
Abc_NtkForEachPo( pNtk, pObj, i )
fprintf( pFile, "o%d %s\n", i, Abc_ObjName(pObj) );
*/
}
// write the comment
fprintf( pFile, "c\n" );
fprintf( pFile, "%s\n", pNtk->pName );
......
src/base/io/ioWriteBench.c
......@@ -24,9 +24,14 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static int Io_WriteBenchCheckNames( Abc_Ntk_t * pNtk );
static int Io_WriteBenchOne( FILE * pFile, Abc_Ntk_t * pNtk );
static int Io_WriteBenchOneNode( FILE * pFile, Abc_Obj_t * pNode );
static int Io_WriteBenchLutOne( FILE * pFile, Abc_Ntk_t * pNtk );
static int Io_WriteBenchLutOneNode( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vTruth );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
......@@ -47,6 +52,11 @@ int Io_WriteBench( Abc_Ntk_t * pNtk, char * pFileName )
Abc_Ntk_t * pExdc;
FILE * pFile;
assert( Abc_NtkIsSopNetlist(pNtk) );
if ( !Io_WriteBenchCheckNames(pNtk) )
{
fprintf( stdout, "Io_WriteBench(): Signal names in this benchmark contain parantheses making them impossible to reproduce in the BENCH format. Use \"short_names\".\n" );
return 0;
}
pFile = fopen( pFileName, "w" );
if ( pFile == NULL )
{
......@@ -148,6 +158,163 @@ int Io_WriteBenchOneNode( FILE * pFile, Abc_Obj_t * pNode )
return 1;
}
/**Function*************************************************************
Synopsis [Writes the network in BENCH format with LUTs and DFFRSE.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Io_WriteBenchLut( Abc_Ntk_t * pNtk, char * pFileName )
{
Abc_Ntk_t * pExdc;
FILE * pFile;
assert( Abc_NtkIsAigNetlist(pNtk) );
if ( !Io_WriteBenchCheckNames(pNtk) )
{
fprintf( stdout, "Io_WriteBenchLut(): Signal names in this benchmark contain parantheses making them impossible to reproduce in the BENCH format. Use \"short_names\".\n" );
return 0;
}
pFile = fopen( pFileName, "w" );
if ( pFile == NULL )
{
fprintf( stdout, "Io_WriteBench(): Cannot open the output file.\n" );
return 0;
}
fprintf( pFile, "# Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
// write the network
Io_WriteBenchLutOne( pFile, pNtk );
// write EXDC network if it exists
pExdc = Abc_NtkExdc( pNtk );
if ( pExdc )
printf( "Io_WriteBench: EXDC is not written (warning).\n" );
// finalize the file
fclose( pFile );
return 1;
}
/**Function*************************************************************
Synopsis [Writes the network in BENCH format.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Io_WriteBenchLutOne( FILE * pFile, Abc_Ntk_t * pNtk )
{
ProgressBar * pProgress;
Abc_Obj_t * pNode;
Vec_Int_t * vMemory;
int i;
// write the PIs/POs/latches
Abc_NtkForEachPi( pNtk, pNode, i )
fprintf( pFile, "INPUT(%s)\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
Abc_NtkForEachPo( pNtk, pNode, i )
fprintf( pFile, "OUTPUT(%s)\n", Abc_ObjName(Abc_ObjFanin0(pNode)) );
Abc_NtkForEachLatch( pNtk, pNode, i )
fprintf( pFile, "%-11s = DFFRSE( %s, gnd, gnd, gnd, gnd )\n",
Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pNode))), Abc_ObjName(Abc_ObjFanin0(Abc_ObjFanin0(pNode))) );
// write internal nodes
vMemory = Vec_IntAlloc( 10000 );
pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
Abc_NtkForEachNode( pNtk, pNode, i )
{
Extra_ProgressBarUpdate( pProgress, i, NULL );
Io_WriteBenchLutOneNode( pFile, pNode, vMemory );
}
Extra_ProgressBarStop( pProgress );
Vec_IntFree( vMemory );
return 1;
}
/**Function*************************************************************
Synopsis [Writes the network in BENCH format.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Io_WriteBenchLutOneNode( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vTruth )
{
Abc_Obj_t * pFanin;
unsigned * pTruth;
int i, nFanins;
assert( Abc_ObjIsNode(pNode) );
nFanins = Abc_ObjFaninNum(pNode);
assert( nFanins <= 8 );
// compute the truth table
pTruth = Abc_ConvertAigToTruth( pNode->pNtk->pManFunc, Hop_Regular(pNode->pData), nFanins, vTruth );
if ( Hop_IsComplement(pNode->pData) )
Extra_TruthNot( pTruth, pTruth, nFanins );
// consider simple cases
if ( Extra_TruthIsConst0(pTruth, nFanins) )
{
fprintf( pFile, "%-11s = gnd\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
return 1;
}
if ( Extra_TruthIsConst1(pTruth, nFanins) )
{
fprintf( pFile, "%-11s = vdd\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
return 1;
}
if ( nFanins == 1 )
{
fprintf( pFile, "%-11s = LUT 0x%d ( %s )\n",
Abc_ObjName(Abc_ObjFanout0(pNode)),
Abc_NodeIsBuf(pNode)? 2 : 1,
Abc_ObjName(Abc_ObjFanin0(pNode)) );
return 1;
}
// write it in the hexadecimal form
fprintf( pFile, "%-11s = LUT 0x", Abc_ObjName(Abc_ObjFanout0(pNode)) );
Extra_PrintHexadecimal( pFile, pTruth, nFanins );
// write the fanins
fprintf( pFile, " (" );
Abc_ObjForEachFanin( pNode, pFanin, i )
fprintf( pFile, " %s%s", Abc_ObjName(pFanin), ((i==nFanins-1)? "" : ",") );
fprintf( pFile, " )\n" );
return 1;
}
/**Function*************************************************************
Synopsis [Returns 1 if the names cannot be written into the bench file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Io_WriteBenchCheckNames( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pObj;
char * pName;
int i;
Abc_NtkForEachObj( pNtk, pObj, i )
for ( pName = Nm_ManFindNameById(pNtk->pManName, i); pName && *pName; pName++ )
if ( *pName == '(' || *pName == ')' )
return 0;
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/map/if/ifMap.c
......@@ -278,7 +278,7 @@ int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fPrepr
if ( p->pPars->fVerbose )
{
char Symb = fPreprocess? 'P' : ((Mode == 0)? 'D' : ((Mode == 1)? 'F' : 'A'));
printf( "%c: Del = %6.2f. Ar = %8.2f. Net = %6d. Cut = %8d. ",
printf( "%c: Del = %7.2f. Ar = %9.1f. Net = %8d. Cut = %8d. ",
Symb, p->RequiredGlo, p->AreaGlo, p->nNets, p->nCutsMerged );
PRT( "T", clock() - clk );
// printf( "Max number of cuts = %d. Average number of cuts = %5.2f.\n",
......
src/map/if/ifReduce.c
......@@ -55,7 +55,7 @@ void If_ManImproveMapping( If_Man_t * p )
If_ManComputeRequired( p );
if ( p->pPars->fVerbose )
{
printf( "E: Del = %6.2f. Ar = %8.2f. Net = %6d. Cut = %8d. ",
printf( "E: Del = %7.2f. Ar = %9.1f. Net = %8d. Cut = %8d. ",
p->RequiredGlo, p->AreaGlo, p->nNets, p->nCutsMerged );
PRT( "T", clock() - clk );
}
......
src/misc/extra/extra.h
......@@ -110,6 +110,7 @@ typedef unsigned long long uint64;
#ifndef PRT
#define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
#define PRTn(a,t) printf("%s = ", (a)); printf("%6.2f sec ", (float)(t)/(float)(CLOCKS_PER_SEC))
#endif
#ifndef PRTP
......
src/misc/extra/extraUtilFile.c
......@@ -324,9 +324,11 @@ void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits )
***********************************************************************/
int Extra_ReadHexadecimal( unsigned Sign[], char * pString, int nVars )
{
int nDigits, Digit, k, c;
Sign[0] = 0;
// write the number into the file
int nWords, nDigits, Digit, k, c;
nWords = Extra_TruthWordNum( nVars );
for ( k = 0; k < nWords; k++ )
Sign[k] = 0;
// read the number from the string
nDigits = (1 << nVars) / 4;
for ( k = 0; k < nDigits; k++ )
{
......
src/misc/vec/vecPtr.h
......@@ -425,6 +425,40 @@ static inline void Vec_PtrFillExtra( Vec_Ptr_t * p, int nSize, void * Entry )
/**Function*************************************************************
Synopsis [Returns the entry even if the place not exist.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void * Vec_PtrGetEntry( Vec_Ptr_t * p, int i )
{
Vec_PtrFillExtra( p, i + 1, NULL );
return Vec_PtrEntry( p, i );
}
/**Function*************************************************************
Synopsis [Inserts the entry even if the place does not exist.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_PtrSetEntry( Vec_Ptr_t * p, int i, void * Entry )
{
Vec_PtrFillExtra( p, i + 1, NULL );
Vec_PtrWriteEntry( p, i, Entry );
}
/**Function*************************************************************
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