summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abc/abcDfs.c3
-rw-r--r--src/base/abc/abcNtk.c2
-rw-r--r--src/base/abci/abc.c56
-rw-r--r--src/base/abci/abcDar.c209
-rw-r--r--src/base/abci/abcFraig.c4
-rw-r--r--src/base/abci/abcPart.c55
-rw-r--r--src/base/io/ioReadAiger.c13
-rw-r--r--src/base/io/ioReadBench.c8
-rw-r--r--src/base/io/ioWriteVerilog.c10
-rw-r--r--src/base/io/ioWriteVerilog.zipbin0 -> 3662 bytes
-rw-r--r--src/base/ver/ver.h1
-rw-r--r--src/base/ver/verCore.c173
-rw-r--r--src/base/ver/verCore.zipbin14163 -> 14624 bytes
13 files changed, 410 insertions, 124 deletions
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index b682f8ae..39e985c0 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -55,7 +55,10 @@ void Abc_NtkDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
assert( Abc_ObjIsNode( pNode ) || Abc_ObjIsBox( pNode ) );
// visit the transitive fanin of the node
Abc_ObjForEachFanin( pNode, pFanin, i )
+ {
+// pFanin = Abc_ObjFanin( pNode, Abc_ObjFaninNum(pNode)-1-i );
Abc_NtkDfs_rec( Abc_ObjFanin0Ntk(pFanin), vNodes );
+ }
// add the node after the fanins have been added
Vec_PtrPush( vNodes, pNode );
}
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index ce187f60..7d8d0f0f 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -987,7 +987,7 @@ void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk )
Abc_Obj_t * pNet, * pNode;
int i;
- if ( Abc_NtkNodeNum(pNtk) == 0 )
+ if ( Abc_NtkNodeNum(pNtk) == 0 && Abc_NtkBoxNum(pNtk) == 0 )
return;
// check for non-driven nets
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 1e0fed0c..d5321e6d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -330,7 +330,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
// Kit_TruthCountMintermsPrecomp();
// Kit_DsdPrecompute4Vars();
- Dar_LibStart();
+// Dar_LibStart();
}
/**Function*************************************************************
@@ -346,7 +346,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
***********************************************************************/
void Abc_End()
{
- Dar_LibStop();
+// Dar_LibStop();
Abc_NtkFraigStoreClean();
// Rwt_Man4ExplorePrint();
@@ -5931,7 +5931,7 @@ usage:
int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
- Abc_Ntk_t * pNtk;//, * pNtkRes;
+ Abc_Ntk_t * pNtk, * pNtkRes;
int c;
int nLevels;
// extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk );
@@ -5940,6 +5940,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// extern int Pr_ManProofTest( char * pFileName );
extern void Abc_NtkCompareSupports( Abc_Ntk_t * pNtk );
extern void Abc_NtkCompareCones( Abc_Ntk_t * pNtk );
+ extern Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -6049,8 +6050,21 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// Abc_Ntk4VarTable( pNtk );
// Dat_NtkGenerateArrays( pNtk );
- return 0;
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ fprintf( pErr, "Network should be strashed. Command has failed.\n" );
+ return 1;
+ }
+ pNtkRes = Abc_NtkDar( pNtk );
+ if ( pNtkRes == NULL )
+ {
+ fprintf( pErr, "Command has failed.\n" );
+ return 1;
+ }
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ return 0;
usage:
fprintf( pErr, "usage: test [-h]\n" );
fprintf( pErr, "\t testbench for new procedures\n" );
@@ -7286,6 +7300,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
int fAllNodes;
int fExdc;
int c;
+ int fPartition = 0;
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -7307,7 +7322,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
pParams->fVerbose = 0; // the verbosiness flag
pParams->fVerboseP = 0; // the verbosiness flag
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "RDCrscpvaeh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "RDCrscptvaeh" ) ) != EOF )
{
switch ( c )
{
@@ -7360,6 +7375,9 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'v':
pParams->fVerbose ^= 1;
break;
+ case 't':
+ fPartition ^= 1;
+ break;
case 'a':
fAllNodes ^= 1;
break;
@@ -7388,13 +7406,28 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
pParams->fVerboseP = pParams->fTryProve;
// get the new network
- if ( Abc_NtkIsStrash(pNtk) )
- pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc );
+ if ( fPartition )
+ {
+ pNtkRes = Abc_NtkDup( pNtk );
+ if ( Abc_NtkIsStrash(pNtk) )
+ Abc_NtkFraigPartitionedTime( pNtk, &Params );
+ else
+ {
+ pNtk = Abc_NtkStrash( pNtk, fAllNodes, !fAllNodes, 0 );
+ Abc_NtkFraigPartitionedTime( pNtk, &Params );
+ Abc_NtkDelete( pNtk );
+ }
+ }
else
{
- pNtk = Abc_NtkStrash( pNtk, fAllNodes, !fAllNodes, 0 );
- pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc );
- Abc_NtkDelete( pNtk );
+ if ( Abc_NtkIsStrash(pNtk) )
+ pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc );
+ else
+ {
+ pNtk = Abc_NtkStrash( pNtk, fAllNodes, !fAllNodes, 0 );
+ pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc );
+ Abc_NtkDelete( pNtk );
+ }
}
if ( pNtkRes == NULL )
{
@@ -7411,7 +7444,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
sprintf( Buffer, "%d", pParams->nBTLimit );
- fprintf( pErr, "usage: fraig [-R num] [-D num] [-C num] [-rscpvah]\n" );
+ fprintf( pErr, "usage: fraig [-R num] [-D num] [-C num] [-rscpvtah]\n" );
fprintf( pErr, "\t transforms a logic network into a functionally reduced AIG\n" );
fprintf( pErr, "\t-R num : number of random patterns (127 < num < 32769) [default = %d]\n", pParams->nPatsRand );
fprintf( pErr, "\t-D num : number of systematic patterns (127 < num < 32769) [default = %d]\n", pParams->nPatsDyna );
@@ -7423,6 +7456,7 @@ usage:
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pParams->fVerbose? "yes": "no" );
fprintf( pErr, "\t-e : toggle functional sweeping using EXDC [default = %s]\n", fExdc? "yes": "no" );
fprintf( pErr, "\t-a : toggle between all nodes and DFS nodes [default = %s]\n", fAllNodes? "all": "dfs" );
+ fprintf( pErr, "\t-t : toggle using partitioned representation [default = %s]\n", fPartition? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 0863061b..81278515 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -25,62 +25,12 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static Dar_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk );
-static Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Dar_Man_t * pMan );
-
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
- Synopsis [Gives the current ABC network to AIG manager for processing.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk )
-{
- Abc_Ntk_t * pNtkAig;
- Dar_Man_t * pMan;//, * pTemp;
- assert( Abc_NtkIsStrash(pNtk) );
- // convert to the AIG manager
- pMan = Abc_NtkToDar( pNtk );
- if ( pMan == NULL )
- return NULL;
- if ( !Dar_ManCheck( pMan ) )
- {
- printf( "Abc_NtkDar: AIG check has failed.\n" );
- Dar_ManStop( pMan );
- return NULL;
- }
- // perform balance
- Dar_ManPrintStats( pMan );
-// Dar_ManDumpBlif( pMan, "aig_temp.blif" );
- pMan->pPars = Dar_ManDefaultParams();
- Dar_ManRewrite( pMan );
- Dar_ManPrintStats( pMan );
- // convert from the AIG manager
- pNtkAig = Abc_NtkFromDar( pNtk, pMan );
- if ( pNtkAig == NULL )
- return NULL;
- Dar_ManStop( pMan );
- // make sure everything is okay
- if ( !Abc_NtkCheck( pNtkAig ) )
- {
- printf( "Abc_NtkDar: The network check has failed.\n" );
- Abc_NtkDelete( pNtkAig );
- return NULL;
- }
- return pNtkAig;
-}
-
-/**Function*************************************************************
-
Synopsis [Converts the network from the AIG manager into ABC.]
Description []
@@ -96,7 +46,7 @@ Dar_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk )
Abc_Obj_t * pObj;
int i;
// create the manager
- pMan = Dar_ManStart( Abc_NtkNodeNum(pNtk) );
+ pMan = Dar_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
// transfer the pointers to the basic nodes
Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Dar_ManConst1(pMan);
Abc_NtkForEachCi( pNtk, pObj, i )
@@ -122,14 +72,14 @@ Dar_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtk, Dar_Man_t * pMan )
+Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Dar_Man_t * pMan )
{
Vec_Ptr_t * vNodes;
Abc_Ntk_t * pNtkNew;
Dar_Obj_t * pObj;
int i;
// perform strashing
- pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
+ pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
// transfer the pointers to the basic nodes
Dar_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
Dar_ManForEachPi( pMan, pObj, i )
@@ -147,6 +97,159 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtk, Dar_Man_t * pMan )
return pNtkNew;
}
+/**Function*************************************************************
+
+ Synopsis [Converts the network from the AIG manager into ABC.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Dar_Man_t * pMan )
+{
+ Vec_Ptr_t * vNodes;
+ Abc_Ntk_t * pNtkNew;
+ Abc_Obj_t * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1;
+ Dar_Obj_t * pObj;
+ int i;
+// assert( Dar_ManLatchNum(pMan) > 0 );
+ // perform strashing
+ pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
+ // transfer the pointers to the basic nodes
+ Dar_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
+ Dar_ManForEachPi( pMan, pObj, i )
+ pObj->pData = Abc_NtkPi(pNtkNew, i);
+ // create latches of the new network
+ Dar_ManForEachObj( pMan, pObj, i )
+ {
+ if ( !Dar_ObjIsLatch(pObj) )
+ continue;
+ pObjNew = Abc_NtkCreateLatch( pNtkNew );
+ pFaninNew0 = Abc_NtkCreateBi( pNtkNew );
+ pFaninNew1 = Abc_NtkCreateBo( pNtkNew );
+ Abc_ObjAddFanin( pObjNew, pFaninNew0 );
+ Abc_ObjAddFanin( pFaninNew1, pObjNew );
+ Abc_LatchSetInit0( pObjNew );
+ pObj->pData = Abc_ObjFanout0( pObjNew );
+ }
+ Abc_NtkAddDummyBoxNames( pNtkNew );
+ // rebuild the AIG
+ vNodes = Dar_ManDfs( pMan );
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ {
+ // add the first fanin
+ pObj->pData = pFaninNew0 = (Abc_Obj_t *)Dar_ObjChild0Copy(pObj);
+ if ( Dar_ObjIsBuf(pObj) )
+ continue;
+ // add the second fanin
+ pFaninNew1 = (Abc_Obj_t *)Dar_ObjChild1Copy(pObj);
+ // create the new node
+ if ( Dar_ObjIsExor(pObj) )
+ pObj->pData = pObjNew = Abc_AigXor( pNtkNew->pManFunc, pFaninNew0, pFaninNew1 );
+ else
+ pObj->pData = pObjNew = Abc_AigAnd( pNtkNew->pManFunc, pFaninNew0, pFaninNew1 );
+ }
+ Vec_PtrFree( vNodes );
+ // connect the PO nodes
+ Dar_ManForEachPo( pMan, pObj, i )
+ {
+ pFaninNew = (Abc_Obj_t *)Dar_ObjChild0Copy( pObj );
+ Abc_ObjAddFanin( Abc_NtkPo(pNtkNew, i), pFaninNew );
+ }
+ // connect the latches
+ Dar_ManForEachObj( pMan, pObj, i )
+ {
+ if ( !Dar_ObjIsLatch(pObj) )
+ continue;
+ pFaninNew = (Abc_Obj_t *)Dar_ObjChild0Copy( pObj );
+ Abc_ObjAddFanin( Abc_ObjFanin0(Abc_ObjFanin0(pObj->pData)), pFaninNew );
+ }
+ if ( !Abc_NtkCheck( pNtkNew ) )
+ fprintf( stdout, "Abc_NtkFromIvySeq(): Network check has failed.\n" );
+ return pNtkNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collect latch values.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int * Abc_NtkGetLatchValues( Abc_Ntk_t * pNtk )
+{
+ Abc_Obj_t * pLatch;
+ int i, * pArray;
+ pArray = ALLOC( int, Abc_NtkLatchNum(pNtk) );
+ Abc_NtkForEachLatch( pNtk, pLatch, i )
+ pArray[i] = Abc_LatchIsInit1(pLatch);
+ return pArray;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Gives the current ABC network to AIG manager for processing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk )
+{
+ Abc_Ntk_t * pNtkAig;
+ Dar_Man_t * pMan;//, * pTemp;
+ int * pArray;
+
+ assert( Abc_NtkIsStrash(pNtk) );
+ // convert to the AIG manager
+ pMan = Abc_NtkToDar( pNtk );
+ if ( pMan == NULL )
+ return NULL;
+ if ( !Dar_ManCheck( pMan ) )
+ {
+ printf( "Abc_NtkDar: AIG check has failed.\n" );
+ Dar_ManStop( pMan );
+ return NULL;
+ }
+ // perform balance
+ Dar_ManPrintStats( pMan );
+
+ pArray = Abc_NtkGetLatchValues(pNtk);
+ Dar_ManSeqStrash( pMan, Abc_NtkLatchNum(pNtk), pArray );
+ free( pArray );
+
+// Dar_ManDumpBlif( pMan, "aig_temp.blif" );
+// pMan->pPars = Dar_ManDefaultParams();
+// Dar_ManRewrite( pMan );
+ Dar_ManPrintStats( pMan );
+ // convert from the AIG manager
+ if ( Dar_ManLatchNum(pMan) )
+ pNtkAig = Abc_NtkFromDarSeq( pNtk, pMan );
+ else
+ pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+ if ( pNtkAig == NULL )
+ return NULL;
+ Dar_ManStop( pMan );
+ // make sure everything is okay
+ if ( !Abc_NtkCheck( pNtkAig ) )
+ {
+ printf( "Abc_NtkDar: The network check has failed.\n" );
+ Abc_NtkDelete( pNtkAig );
+ return NULL;
+ }
+ return pNtkAig;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index 30e49af2..fa6771b3 100644
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -687,7 +687,7 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
// set the number of networks stored
Abc_FrameSetNtkStoreSize( Abc_FrameReadNtkStoreSize() + 1 );
}
-// printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pStore) - nAndsOld );
+ printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pStore) - nAndsOld );
return 1;
}
@@ -734,7 +734,7 @@ Abc_Ntk_t * Abc_NtkFraigRestore()
Fraig_ParamsSetDefault( &Params );
Params.nPatsRand = nWordsMin * 32; // the number of words of random simulation info
Params.nPatsDyna = nWordsMin * 32; // the number of words of dynamic simulation info
- Params.nBTLimit = 99; // the max number of backtracks to perform
+ Params.nBTLimit = 999999; // the max number of backtracks to perform
Params.fFuncRed = 1; // performs only one level hashing
Params.fFeedBack = 1; // enables solver feedback
Params.fDist1Pats = 1; // enables distance-1 patterns
diff --git a/src/base/abci/abcPart.c b/src/base/abci/abcPart.c
index 748868de..787e3f88 100644
--- a/src/base/abci/abcPart.c
+++ b/src/base/abci/abcPart.c
@@ -698,12 +698,67 @@ Abc_Ntk_t * Abc_NtkFraigPartitioned( Abc_Ntk_t * pNtk, void * pParams )
// derive the final network
pNtkFraig = Abc_NtkPartStitchChoices( pNtk, vFraigs );
Vec_PtrForEachEntry( vFraigs, pNtkAig, i )
+ {
+// Abc_NtkPrintStats( stdout, pNtkAig, 0 );
Abc_NtkDelete( pNtkAig );
+ }
Vec_PtrFree( vFraigs );
return pNtkFraig;
}
+/**Function*************************************************************
+
+ Synopsis [Stitches together several networks with choice nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkFraigPartitionedTime( Abc_Ntk_t * pNtk, void * pParams )
+{
+ extern int Cmd_CommandExecute( void * pAbc, char * sCommand );
+ extern void * Abc_FrameGetGlobalFrame();
+
+ Vec_Vec_t * vParts;
+ Vec_Ptr_t * vFraigs, * vOne;
+ Abc_Ntk_t * pNtkAig, * pNtkFraig;
+ int i;
+ int clk = clock();
+
+ // perform partitioning
+ assert( Abc_NtkIsStrash(pNtk) );
+// vParts = Abc_NtkPartitionNaive( pNtk, 20 );
+ vParts = Abc_NtkPartitionSmart( pNtk, 0, 0 );
+
+ Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" );
+
+ // fraig each partition
+ vFraigs = Vec_PtrAlloc( Vec_VecSize(vParts) );
+ Vec_VecForEachLevel( vParts, vOne, i )
+ {
+ pNtkAig = Abc_NtkCreateConeArray( pNtk, vOne, 0 );
+ pNtkFraig = Abc_NtkFraig( pNtkAig, pParams, 0, 0 );
+ Vec_PtrPush( vFraigs, pNtkFraig );
+ Abc_NtkDelete( pNtkAig );
+
+ printf( "Finished part %d (out of %d)\r", i+1, Vec_VecSize(vParts) );
+ }
+ Vec_VecFree( vParts );
+
+ Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" );
+
+ // derive the final network
+ Vec_PtrForEachEntry( vFraigs, pNtkAig, i )
+ Abc_NtkDelete( pNtkAig );
+ Vec_PtrFree( vFraigs );
+
+ PRT( "Partitioned fraiging time", clock() - clk );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c
index a54a00fe..fe519476 100644
--- a/src/base/io/ioReadAiger.c
+++ b/src/base/io/ioReadAiger.c
@@ -96,7 +96,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
// prepare the array of nodes
vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds );
- Vec_PtrPush( vNodes, Abc_AigConst1(pNtkNew) );
+ Vec_PtrPush( vNodes, Abc_ObjNot( Abc_AigConst1(pNtkNew) ) );
// create the PIs
for ( i = 0; i < nInputs; i++ )
@@ -122,6 +122,8 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
Vec_PtrPush( vNodes, pNode1 );
// assign names to latch and its input
Abc_ObjAssignName( pObj, Abc_ObjNameDummy("_L", i, nDigits), NULL );
+
+ printf( "Creating latch %s with input %d and output %d.\n", Abc_ObjName(pObj), pNode0->Id, pNode1->Id );
}
// remember the beginning of latch/PO literals
@@ -156,14 +158,17 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
Abc_NtkForEachLatchInput( pNtkNew, pObj, i )
{
uLit0 = atoi( pCur ); while ( *pCur++ != '\n' );
- pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ^ (uLit0 < 2) );
+ pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
Abc_ObjAddFanin( pObj, pNode0 );
+
+ printf( "Adding input %d to latch input %d.\n", pNode0->Id, pObj->Id );
+
}
// read the PO driver literals
Abc_NtkForEachPo( pNtkNew, pObj, i )
{
uLit0 = atoi( pCur ); while ( *pCur++ != '\n' );
- pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ^ (uLit0 < 2) );
+ pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
Abc_ObjAddFanin( pObj, pNode0 );
}
@@ -204,7 +209,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), "L" );
// mark the node as named
pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj);
- }
+ }
// skipping the comments
free( pContents );
Vec_PtrFree( vNodes );
diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c
index 2730ba69..ba622e40 100644
--- a/src/base/io/ioReadBench.c
+++ b/src/base/io/ioReadBench.c
@@ -118,7 +118,13 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
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 );
+// Abc_LatchSetInit0( pNode );
+ if ( pType[3] == '0' )
+ Abc_LatchSetInit0( pNode );
+ else if ( pType[3] == '1' )
+ Abc_LatchSetInit1( pNode );
+ else
+ Abc_LatchSetInitDc( pNode );
}
else if ( strcmp(pType, "LUT") == 0 )
{
diff --git a/src/base/io/ioWriteVerilog.c b/src/base/io/ioWriteVerilog.c
index a02d53fd..a4eeb78f 100644
--- a/src/base/io/ioWriteVerilog.c
+++ b/src/base/io/ioWriteVerilog.c
@@ -113,7 +113,12 @@ void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk )
{
// write inputs and outputs
// fprintf( pFile, "module %s ( gclk,\n ", Abc_NtkName(pNtk) );
- fprintf( pFile, "module %s ( \n ", Abc_NtkName(pNtk) );
+ fprintf( pFile, "module %s ( ", Abc_NtkName(pNtk) );
+ // add the clock signal if it does not exist
+ if ( Abc_NtkLatchNum(pNtk) > 0 && Nm_ManFindIdByName(pNtk->pManName, "clock", ABC_OBJ_PI) == -1 )
+ fprintf( pFile, "clock, " );
+ // write other primary inputs
+ fprintf( pFile, "\n " );
if ( Abc_NtkPiNum(pNtk) > 0 )
{
Io_WriteVerilogPis( pFile, pNtk, 3 );
@@ -435,7 +440,8 @@ void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk )
return;
// write the latches
// fprintf( pFile, " always @(posedge %s) begin\n", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_NtkPi(pNtk,0))) );
- fprintf( pFile, " always begin\n" );
+// fprintf( pFile, " always begin\n" );
+ fprintf( pFile, " always @ (posedge clock) begin\n" );
Abc_NtkForEachLatch( pNtk, pLatch, i )
{
fprintf( pFile, " %s", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch)))) );
diff --git a/src/base/io/ioWriteVerilog.zip b/src/base/io/ioWriteVerilog.zip
new file mode 100644
index 00000000..19e68a89
--- /dev/null
+++ b/src/base/io/ioWriteVerilog.zip
Binary files differ
diff --git a/src/base/ver/ver.h b/src/base/ver/ver.h
index cf2b7497..9c538ac4 100644
--- a/src/base/ver/ver.h
+++ b/src/base/ver/ver.h
@@ -66,6 +66,7 @@ struct Ver_Man_t_
Vec_Ptr_t * vNames;
Vec_Ptr_t * vStackFn;
Vec_Int_t * vStackOp;
+ Vec_Int_t * vPerm;
};
diff --git a/src/base/ver/verCore.c b/src/base/ver/verCore.c
index 12c54dba..6d7d230e 100644
--- a/src/base/ver/verCore.c
+++ b/src/base/ver/verCore.c
@@ -110,6 +110,7 @@ Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Lib_t * pGateLib )
p->vNames = Vec_PtrAlloc( 100 );
p->vStackFn = Vec_PtrAlloc( 100 );
p->vStackOp = Vec_IntAlloc( 100 );
+ p->vPerm = Vec_IntAlloc( 100 );
// create the design library and assign the technology library
p->pDesign = Abc_LibCreate( pFileName );
p->pDesign->pLibrary = pGateLib;
@@ -136,6 +137,7 @@ void Ver_ParseStop( Ver_Man_t * p )
Vec_PtrFree( p->vNames );
Vec_PtrFree( p->vStackFn );
Vec_IntFree( p->vStackOp );
+ Vec_IntFree( p->vPerm );
free( p );
}
@@ -1193,6 +1195,12 @@ int Ver_ParseAssign( Ver_Man_t * pMan, Abc_Ntk_t * pNtk )
pFunc = (Hop_Obj_t *)Mio_LibraryReadConst1(Abc_FrameReadLibGen());
else
{
+ // "assign foo = \bar ;"
+ if ( *pEquation == '\\' )
+ {
+ pEquation++;
+ pEquation[strlen(pEquation) - 1] = 0;
+ }
if ( Ver_ParseFindNet(pNtk, pEquation) == NULL )
{
sprintf( pMan->sError, "Cannot read Verilog with non-trivial assignments in the mapped netlist." );
@@ -1358,6 +1366,29 @@ int Ver_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateType_t Ga
/**Function*************************************************************
+ Synopsis [Returns the index of the given pin the gate.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ver_FindGateInput( Mio_Gate_t * pGate, char * pName )
+{
+ Mio_Pin_t * pGatePin;
+ int i;
+ for ( i = 0, pGatePin = Mio_GateReadPins(pGate); pGatePin != NULL; pGatePin = Mio_PinReadNext(pGatePin), i++ )
+ if ( strcmp(pName, Mio_PinReadName(pGatePin)) == 0 )
+ return i;
+ if ( strcmp(pName, Mio_GateReadOutName(pGate)) == 0 )
+ return i;
+ return -1;
+}
+
+/**Function*************************************************************
+
Synopsis [Parses one directive.]
Description []
@@ -1369,10 +1400,10 @@ int Ver_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateType_t Ga
***********************************************************************/
int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate )
{
- Mio_Pin_t * pGatePin;
Ver_Stream_t * p = pMan->pReader;
Abc_Obj_t * pNetActual, * pNode;
char * pWord, Symbol;
+ int Input, i, nFanins = Mio_GateReadInputs(pGate);
// convert from the blackbox into the network with local functions representated by gates
if ( 1 != pMan->fMapped )
@@ -1404,7 +1435,7 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate )
pNode->pData = pGate;
// parse pairs of formal/actural inputs
- pGatePin = Mio_GateReadPins(pGate);
+ Vec_IntClear( pMan->vPerm );
while ( 1 )
{
// process one pair of formal/actual parameters
@@ -1420,24 +1451,13 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate )
if ( pWord == NULL )
return 0;
- // make sure that the formal name is the same as the gate's
- if ( Mio_GateReadInputs(pGate) == Abc_ObjFaninNum(pNode) )
- {
- if ( strcmp(pWord, Mio_GateReadOutName(pGate)) )
- {
- sprintf( pMan->sError, "Formal output name listed %s is different from the name of the gate output %s.", pWord, Mio_GateReadOutName(pGate) );
- Ver_ParsePrintErrorMessage( pMan );
- return 0;
- }
- }
- else
+ // find the corresponding pin of the gate
+ Input = Ver_FindGateInput( pGate, pWord );
+ if ( Input == -1 )
{
- if ( strcmp(pWord, Mio_PinReadName(pGatePin)) )
- {
- sprintf( pMan->sError, "Formal input name listed %s is different from the name of the corresponding pin %s.", pWord, Mio_PinReadName(pGatePin) );
- Ver_ParsePrintErrorMessage( pMan );
- return 0;
- }
+ sprintf( pMan->sError, "Formal input name %s cannot be found in the gate %s.", pWord, Mio_GateReadOutName(pGate) );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
}
// open the paranthesis
@@ -1482,10 +1502,13 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate )
}
// add the fanin
- if ( Mio_GateReadInputs(pGate) == Abc_ObjFaninNum(pNode) )
- Abc_ObjAddFanin( pNetActual, pNode ); // fanout
- else
+ if ( Input < nFanins )
+ {
+ Vec_IntPush( pMan->vPerm, Input );
Abc_ObjAddFanin( pNode, pNetActual ); // fanin
+ }
+ else
+ Abc_ObjAddFanin( pNetActual, pNode ); // fanout
// check if it is the end of gate
Ver_ParseSkipComments( pMan );
@@ -1501,13 +1524,10 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate )
return 0;
}
Ver_ParseSkipComments( pMan );
-
- // get the next pin
- pGatePin = Mio_PinReadNext(pGatePin);
}
// check that the gate as the same number of input
- if ( !(Abc_ObjFaninNum(pNode) == Mio_GateReadInputs(pGate) && Abc_ObjFanoutNum(pNode) == 1) )
+ if ( !(Abc_ObjFaninNum(pNode) == nFanins && Abc_ObjFanoutNum(pNode) == 1) )
{
sprintf( pMan->sError, "Parsing of gate %s has failed.", Mio_GateReadName(pGate) );
Ver_ParsePrintErrorMessage( pMan );
@@ -1522,6 +1542,20 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate )
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
+
+ // check if we need to permute the inputs
+ Vec_IntForEachEntry( pMan->vPerm, Input, i )
+ if ( Input != i )
+ break;
+ if ( i < Vec_IntSize(pMan->vPerm) )
+ {
+ // add the fanin numnbers to the end of the permuation array
+ for ( i = 0; i < nFanins; i++ )
+ Vec_IntPush( pMan->vPerm, Abc_ObjFaninId(pNode, i) );
+ // write the fanin numbers into their corresponding places (according to the gate)
+ for ( i = 0; i < nFanins; i++ )
+ Vec_IntWriteEntry( &pNode->vFanins, Vec_IntEntry(pMan->vPerm, i), Vec_IntEntry(pMan->vPerm, i+nFanins) );
+ }
return 1;
}
@@ -1546,6 +1580,7 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox )
Abc_Obj_t * pNode;
char * pWord, Symbol;
int fCompl, fFormalIsGiven;
+ int i, k, Bit, Limit, nMsb, nLsb, fQuit, flag;
// gate the name of the box
pWord = Ver_ParseGetName( pMan );
@@ -1613,8 +1648,6 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox )
// consider the case of vector-inputs
if ( Symbol == '{' )
{
- int i, k, Bit, Limit, nMsb, nLsb, fQuit;
-
// skip this char
Ver_StreamPopChar(p);
@@ -1673,7 +1706,8 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox )
pNetActual = Ver_ParseFindNet( pNtk, pWord );
if ( pNetActual == NULL )
{
- if ( !strncmp(pWord, "Open_", 5) )
+ if ( !strncmp(pWord, "Open_", 5) ||
+ !strncmp(pWord, "dct_unconnected", 15) )
pNetActual = Abc_NtkCreateNet( pNtk );
else
{
@@ -1697,7 +1731,8 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox )
pNetActual = Ver_ParseFindNet( pNtk, Buffer );
if ( pNetActual == NULL )
{
- if ( !strncmp(pWord, "Open_", 5) )
+ if ( !strncmp(pWord, "Open_", 5) ||
+ !strncmp(pWord, "dct_unconnected", 15) )
pNetActual = Abc_NtkCreateNet( pNtk );
else
{
@@ -1738,34 +1773,72 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox )
if ( pWord[0] == 0 )
{
pNetActual = Abc_NtkCreateNet( pNtk );
+ Vec_PtrPush( pBundle->vNetsActual, Abc_ObjNotCond( pNetActual, fCompl ) );
}
else
{
-/*
- // check if the name is complemented
- fCompl = (pWord[0] == '~');
- if ( fCompl )
- {
- pWord++;
- if ( pNtk->pData == NULL )
- pNtk->pData = Extra_MmFlexStart();
- }
-*/
// get the actual net
+ flag=0;
pNetActual = Ver_ParseFindNet( pNtk, pWord );
- if ( pNetActual == NULL )
+ if ( pNetActual == NULL )
{
- if ( !strncmp(pWord, "Open_", 5) )
- pNetActual = Abc_NtkCreateNet( pNtk );
- else
+ Ver_ParseLookupSuffix( pMan, pWord, &nMsb, &nLsb );
+ if ( nMsb == -1 && nLsb == -1 )
{
- sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) );
- Ver_ParsePrintErrorMessage( pMan );
- return 0;
+ Ver_ParseSignalSuffix( pMan, pWord, &nMsb, &nLsb );
+ if ( nMsb == -1 && nLsb == -1 )
+ {
+ if ( !strncmp(pWord, "Open_", 5) ||
+ !strncmp(pWord, "dct_unconnected", 15) )
+ {
+ pNetActual = Abc_NtkCreateNet( pNtk );
+ Vec_PtrPush( pBundle->vNetsActual, pNetActual );
+ }
+ else
+ {
+ sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
+ }
+ else
+ {
+ flag=1;
+ }
+ }
+ else
+ {
+ flag=1;
}
+ if (flag)
+ {
+ Limit = (nMsb > nLsb) ? nMsb - nLsb + 1: nLsb - nMsb + 1;
+ for ( Bit = nMsb, k = Limit - 1; k >= 0; Bit = (nMsb > nLsb ? Bit - 1: Bit + 1), k--)
+ {
+ // get the actual net
+ sprintf( Buffer, "%s[%d]", pWord, Bit );
+ pNetActual = Ver_ParseFindNet( pNtk, Buffer );
+ if ( pNetActual == NULL )
+ {
+ if ( !strncmp(pWord, "Open_", 5) ||
+ !strncmp(pWord, "dct_unconnected", 15))
+ pNetActual = Abc_NtkCreateNet( pNtk );
+ else
+ {
+ sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
+ }
+ Vec_PtrPush( pBundle->vNetsActual, pNetActual );
+ }
+ }
+ }
+ else
+ {
+ Vec_PtrPush( pBundle->vNetsActual, Abc_ObjNotCond( pNetActual, fCompl ) );
}
}
- Vec_PtrPush( pBundle->vNetsActual, Abc_ObjNotCond( pNetActual, fCompl ) );
}
if ( fFormalIsGiven )
@@ -2000,8 +2073,8 @@ int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox )
}
if ( pBundle == NULL )
{
- printf( "Warning: The formal output %s is not driven when instantiating network %s in box %s.",
- pNameFormal, pNtkBox->pName, Abc_ObjName(pBox) );
+// printf( "Warning: The formal output %s is not driven when instantiating network %s in box %s.",
+// pNameFormal, pNtkBox->pName, Abc_ObjName(pBox) );
continue;
}
}
diff --git a/src/base/ver/verCore.zip b/src/base/ver/verCore.zip
index 45574008..cdfcf5a4 100644
--- a/src/base/ver/verCore.zip
+++ b/src/base/ver/verCore.zip
Binary files differ
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-05 04:53:54 +0000