summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/gia.h2
-rw-r--r--src/aig/gia/giaDup.c25
-rw-r--r--src/aig/gia/giaMan.c89
-rw-r--r--src/aig/gia/giaUtil.c102
-rw-r--r--src/base/abci/abc.c28
-rw-r--r--src/base/abci/abcTiming.c58
-rw-r--r--src/base/io/ioReadBlif.c19
-rw-r--r--src/base/wlc/wlcAbc.c14
-rw-r--r--src/base/wlc/wlcCom.c38
9 files changed, 322 insertions, 53 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 3517502d..8a5137fe 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1488,7 +1488,7 @@ extern void Gia_ManPrintStatsMiter( Gia_Man_t * p, int fVerbose )
extern void Gia_ManSetRegNum( Gia_Man_t * p, int nRegs );
extern void Gia_ManReportImprovement( Gia_Man_t * p, Gia_Man_t * pNew );
extern void Gia_ManPrintNpnClasses( Gia_Man_t * p );
-extern void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs );
+extern void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs, int fVerBufs );
/*=== giaMem.c ===========================================================*/
extern Gia_MmFixed_t * Gia_MmFixedStart( int nEntrySize, int nEntriesMax );
extern void Gia_MmFixedStop( Gia_MmFixed_t * p, int fVerbose );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 326bbedb..a2ed4942 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -2320,6 +2320,31 @@ Gia_Man_t * Gia_ManDupTrimmed2( Gia_Man_t * p )
assert( !Gia_ManHasDangling( pNew ) );
return pNew;
}
+Gia_Man_t * Gia_ManDupTrimmed3( Gia_Man_t * p )
+{
+ Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) );
+ Gia_Man_t * pNew;
+ Gia_Obj_t * pObj;
+ int i;
+ pNew = Gia_ManStart( Gia_ManObjNum(p) );
+ pNew->pName = Abc_UtilStrsav( p->pName );
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ Gia_ManFillValue( p );
+ Gia_ManConst0(p)->Value = 0;
+ Gia_ManForEachCi( p, pObj, i )
+ pObj->Value = Gia_ManAppendCi(pNew);
+ Gia_ManForEachAnd( p, pObj, i )
+ pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ // mark duplicated POs
+ Gia_ManForEachPo( p, pObj, i )
+ Vec_IntWriteEntry( vMap, Gia_ObjFaninId0p(p, pObj), i );
+ Gia_ManForEachPo( p, pObj, i )
+ if ( Vec_IntEntry(vMap, Gia_ObjFaninId0p(p, pObj)) == i )
+ Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ Vec_IntFree( vMap );
+ Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+ return pNew;
+}
/**Function*************************************************************
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index b5748401..e4c9afd0 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -1270,13 +1270,14 @@ void Gia_ManWriteNames( FILE * pFile, char c, int n, Vec_Ptr_t * vNames, int Sta
fFirst = 0;
}
}
-void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs )
+void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs, int fVerBufs )
{
FILE * pFile;
Gia_Obj_t * pObj;
Vec_Bit_t * vInvs, * vUsed;
- int nDigits = Abc_Base10Log( Gia_ManObjNum(p) );
- int nDigits2 = Abc_Base10Log( Gia_ManPiNum(p) );
+ int nDigits = Abc_Base10Log( Gia_ManObjNum(p) );
+ int nDigitsI = Abc_Base10Log( Gia_ManPiNum(p) );
+ int nDigitsO = Abc_Base10Log( Gia_ManPoNum(p) );
int i, k, iObj;
if ( Gia_ManRegNum(p) )
{
@@ -1301,20 +1302,63 @@ void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs )
fprintf( pFile, "%c", p->pName[i] );
else
fprintf( pFile, "_" );
- fprintf( pFile, " (\n " );
- Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 4, 4, NULL );
- fprintf( pFile, ",\n " );
- Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 4, 4, NULL );
- fprintf( pFile, "\n );\n\n" );
+ if ( fVerBufs )
+ {
+ fprintf( pFile, " (\n " );
+ Gia_ManWriteNames( pFile, 'a', Gia_ManPiNum(p), NULL, 4, 4, NULL );
+ fprintf( pFile, ",\n " );
+
+ Gia_ManWriteNames( pFile, 'y', Gia_ManPoNum(p), NULL, 4, 4, NULL );
+ fprintf( pFile, "\n );\n\n" );
+
+ fprintf( pFile, " input " );
+ Gia_ManWriteNames( pFile, 'a', Gia_ManPiNum(p), NULL, 8, 4, NULL );
+ fprintf( pFile, ";\n\n" );
+
+ fprintf( pFile, " output " );
+ Gia_ManWriteNames( pFile, 'y', Gia_ManPoNum(p), NULL, 9, 4, NULL );
+ fprintf( pFile, ";\n\n" );
+
+ fprintf( pFile, " wire " );
+ Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL );
+ fprintf( pFile, ";\n\n" );
- fprintf( pFile, " input " );
- Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL );
- fprintf( pFile, ";\n\n" );
+ fprintf( pFile, " wire " );
+ Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL );
+ fprintf( pFile, ";\n\n" );
- fprintf( pFile, " output " );
- Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL );
- fprintf( pFile, ";\n\n" );
+ Gia_ManForEachPi( p, pObj, i )
+ {
+ fprintf( pFile, " buf ( %s,", Gia_ObjGetDumpName(p->vNamesIn, 'x', i, nDigitsI) );
+ fprintf( pFile, " %s );\n", Gia_ObjGetDumpName(NULL, 'a', i, nDigitsI) );
+ }
+ fprintf( pFile, "\n" );
+
+ Gia_ManForEachPo( p, pObj, i )
+ {
+ fprintf( pFile, " buf ( %s,", Gia_ObjGetDumpName(NULL, 'y', i, nDigitsO) );
+ fprintf( pFile, " %s );\n", Gia_ObjGetDumpName(p->vNamesOut, 'z', i, nDigitsO) );
+ }
+ fprintf( pFile, "\n" );
+ }
+ else
+ {
+ fprintf( pFile, " (\n " );
+ Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 4, 4, NULL );
+ fprintf( pFile, ",\n " );
+
+ Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 4, 4, NULL );
+ fprintf( pFile, "\n );\n\n" );
+
+ fprintf( pFile, " input " );
+ Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL );
+ fprintf( pFile, ";\n\n" );
+
+ fprintf( pFile, " output " );
+ Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL );
+ fprintf( pFile, ";\n\n" );
+ }
if ( Vec_BitCount(vUsed) )
{
@@ -1338,7 +1382,7 @@ void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs )
fprintf( pFile, ";\n\n" );
Vec_IntForEachEntry( vObjs, iObj, i )
{
- fprintf( pFile, " buf( %s,", Gia_ObjGetDumpName(NULL, 'n', iObj, nDigits) );
+ fprintf( pFile, " buf ( %s,", Gia_ObjGetDumpName(NULL, 'n', iObj, nDigits) );
fprintf( pFile, " t_%d );\n", i );
}
fprintf( pFile, "\n" );
@@ -1349,13 +1393,13 @@ void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs )
{
if ( Vec_BitEntry(vUsed, Gia_ObjId(p, pObj)) )
{
- fprintf( pFile, " buf( %s,", Gia_ObjGetDumpName(NULL, 'n', Gia_ObjId(p, pObj), nDigits) );
- fprintf( pFile, " %s );\n", Gia_ObjGetDumpName(p->vNamesIn, 'x', i, nDigits2) );
+ fprintf( pFile, " buf ( %s,", Gia_ObjGetDumpName(NULL, 'n', Gia_ObjId(p, pObj), nDigits) );
+ fprintf( pFile, " %s );\n", Gia_ObjGetDumpName(p->vNamesIn, 'x', i, nDigitsI) );
}
if ( Vec_BitEntry(vInvs, Gia_ObjId(p, pObj)) )
{
- fprintf( pFile, " not( %s,", Gia_ObjGetDumpName(NULL, 'i', Gia_ObjId(p, pObj), nDigits) );
- fprintf( pFile, " %s );\n", Gia_ObjGetDumpName(p->vNamesIn, 'x', i, nDigits2) );
+ fprintf( pFile, " not ( %s,", Gia_ObjGetDumpName(NULL, 'i', Gia_ObjId(p, pObj), nDigits) );
+ fprintf( pFile, " %s );\n", Gia_ObjGetDumpName(p->vNamesIn, 'x', i, nDigitsI) );
}
}
@@ -1374,20 +1418,19 @@ void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs )
}
if ( !fSkip )
{
- fprintf( pFile, " and( %s,", Gia_ObjGetDumpName(NULL, 'n', i, nDigits) );
+ fprintf( pFile, " and ( %s,", Gia_ObjGetDumpName(NULL, 'n', i, nDigits) );
fprintf( pFile, " %s,", Gia_ObjGetDumpName(NULL, (char)(Gia_ObjFaninC0(pObj)? 'i':'n'), Gia_ObjFaninId0(pObj, i), nDigits) );
fprintf( pFile, " %s );\n", Gia_ObjGetDumpName(NULL, (char)(Gia_ObjFaninC1(pObj)? 'i':'n'), Gia_ObjFaninId1(pObj, i), nDigits) );
}
if ( Vec_BitEntry(vInvs, i) )
{
- fprintf( pFile, " not( %s,", Gia_ObjGetDumpName(NULL, 'i', i, nDigits) );
+ fprintf( pFile, " not ( %s,", Gia_ObjGetDumpName(NULL, 'i', i, nDigits) );
fprintf( pFile, " %s );\n", Gia_ObjGetDumpName(NULL, 'n', i, nDigits) );
}
}
// output drivers
fprintf( pFile, "\n" );
- nDigits2 = Abc_Base10Log( Gia_ManPoNum(p) );
Gia_ManForEachPo( p, pObj, i )
{
/*
@@ -1397,7 +1440,7 @@ void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs )
else
fprintf( pFile, "%s;\n", Gia_ObjGetDumpName(NULL, (char)(Gia_ObjFaninC0(pObj)? 'i':'n'), Gia_ObjFaninId0p(p, pObj), nDigits) );
*/
- fprintf( pFile, " buf( %s, ", Gia_ObjGetDumpName(p->vNamesOut, 'z', i, nDigits2) );
+ fprintf( pFile, " buf ( %s, ", Gia_ObjGetDumpName(p->vNamesOut, 'z', i, nDigitsO) );
if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
fprintf( pFile, "1\'b%d );\n", Gia_ObjFaninC0(pObj) );
else
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index d5a39f79..efc866b8 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -2821,6 +2821,108 @@ void Gia_ManDumpSuppFileTest( Gia_Man_t * p, char * pFileName )
Vec_StrFree( vRes );
}
+
+/**Function*************************************************************
+
+ Synopsis [Compute support diffs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManConvertSupp_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+ if ( !Gia_ObjIsAnd(pObj) )
+ return;
+ if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+ return;
+ Gia_ObjSetTravIdCurrent(p, pObj);
+ Gia_ManConvertSupp_rec( pNew, p, Gia_ObjFanin0(pObj) );
+ Gia_ManConvertSupp_rec( pNew, p, Gia_ObjFanin1(pObj) );
+ pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+}
+Gia_Man_t * Gia_ManConvertSupp( Gia_Man_t * p )
+{
+ int fOnly1 = 0;
+ int fVerbose = 1;
+ abctime clk = Abc_Clock();
+ Gia_Man_t * pNew, * pTemp;
+ Gia_Obj_t * pObjPi, * pObjRi, * pObjRo;
+ Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
+ Vec_Int_t * vAnds = Vec_IntAlloc( 100 );
+ int i, n, iLits[2];
+ assert( Gia_ManRegNum(p) && Gia_ManRegNum(p) % 8 == 0 );
+ pNew = Gia_ManStart( Gia_ManObjNum(p) );
+ pNew->pName = Abc_UtilStrsav( p->pName );
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ Gia_ManFillValue(p);
+ Gia_ManConst0(p)->Value = 0;
+ Gia_ManForEachPi( p, pObjPi, i )
+ pObjPi->Value = Gia_ManAppendCi( pNew );
+ Gia_ManHashAlloc( pNew );
+ Gia_ManForEachRi( p, pObjRi, i )
+ {
+ pObjRo = Gia_ObjRiToRo(p, pObjRi);
+ if ( (i - Gia_ManPoNum(p)) % 8 != 0 )
+ continue;
+ if ( fOnly1 )
+ {
+ assert( pObjRo->Value == ~0 );
+ for ( n = 0; n < 2; n++ )
+ {
+ pObjRo->Value = n;
+ Gia_ManIncrementTravId( p );
+ Gia_ManConvertSupp_rec( pNew, p, Gia_ObjFanin0(pObjRi) );
+ iLits[n] = Gia_ObjFanin0Copy(pObjRi);
+ }
+ pObjRo->Value = ~0;
+ Gia_ManAppendCo( pNew, Abc_LitNot(Gia_ManHashAnd( pNew, iLits[1], Abc_LitNot(iLits[0]) )) );
+ }
+ else
+ {
+ int Fanin = Gia_ObjFaninId0p( p, pObjRi );
+ Vec_Int_t * vNodes = Gia_ManCollectNodesCis( p, &Fanin, 1 );
+ Gia_Obj_t * pObj; int i, m;
+ Vec_IntClear( vSupp );
+ Vec_IntClear( vAnds );
+ Gia_ManForEachObjVec( vNodes, p, pObj, i )
+ Vec_IntPush( Gia_ObjIsAnd(pObj) ? vAnds : vSupp, Gia_ObjId(p, pObj) );
+ Vec_IntFree( vNodes );
+ Vec_IntSort( vSupp, 0 );
+ for ( m = 0; m < 4; m++ )
+ {
+ Gia_ManForEachObjVec( vSupp, p, pObj, i )
+ if ( i >= Vec_IntSize(vSupp)-5 )
+ pObj->Value = (i == Vec_IntSize(vSupp)-5+m) ? 1 : 0;
+ Gia_ManForEachObjVec( vAnds, p, pObj, i )
+ pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ //if ( m == 4 )
+ // Gia_ManAppendCo( pNew, 0 );
+ //else
+ Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObjRi) );
+ //Gia_ManAppendCo( pNew, Abc_Var2Lit( Vec_IntEntry(vSupp, Vec_IntSize(vSupp)-5+m), 0 ) );
+ Gia_ManForEachObjVec( vSupp, p, pObj, i )
+ if ( i >= Vec_IntSize(vSupp)-5 )
+ pObj->Value = Abc_Var2Lit( 1 + Gia_ObjCioId(pObj), 0 );
+ }
+ }
+ }
+ Vec_IntFree( vSupp );
+ Vec_IntFree( vAnds );
+ Gia_ManHashStop( pNew );
+ //Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+ pNew = Gia_ManCleanup( pTemp = pNew );
+ Gia_ManStop( pTemp );
+ if ( fVerbose )
+ printf( "Transformed %d outputs, ", Gia_ManPoNum(pNew) );
+ if ( fVerbose )
+ Abc_PrintTime( 0, "Time", Abc_Clock() - clk );
+ return pNew;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d6871a3c..6e322b9b 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -31219,12 +31219,13 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
int c, nArgcNew;
int fUnique = 0;
int fVerilog = 0;
+ int fVerBufs = 0;
int fMiniAig = 0;
int fMiniLut = 0;
int fWriteNewLine = 0;
int fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "upmlnvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "upbmlnvh" ) ) != EOF )
{
switch ( c )
{
@@ -31234,6 +31235,9 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'p':
fVerilog ^= 1;
break;
+ case 'b':
+ fVerBufs ^= 1;
+ break;
case 'm':
fMiniAig ^= 1;
break;
@@ -31272,7 +31276,7 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
Gia_ManStop( pGia );
}
else if ( fVerilog )
- Gia_ManDumpVerilog( pAbc->pGia, pFileName, NULL );
+ Gia_ManDumpVerilog( pAbc->pGia, pFileName, NULL, fVerBufs );
else if ( fMiniAig )
Gia_ManWriteMiniAig( pAbc->pGia, pFileName );
else if ( fMiniLut )
@@ -31282,10 +31286,11 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: &w [-upmlnvh] <file>\n" );
+ Abc_Print( -2, "usage: &w [-upbmlnvh] <file>\n" );
Abc_Print( -2, "\t writes the current AIG into the AIGER file\n" );
Abc_Print( -2, "\t-u : toggle writing canonical AIG structure [default = %s]\n", fUnique? "yes" : "no" );
Abc_Print( -2, "\t-p : toggle writing Verilog with 'and' and 'not' [default = %s]\n", fVerilog? "yes" : "no" );
+ Abc_Print( -2, "\t-b : toggle writing additional buffers in Verilog [default = %s]\n", fVerBufs? "yes" : "no" );
Abc_Print( -2, "\t-m : toggle writing MiniAIG rather than AIGER [default = %s]\n", fMiniAig? "yes" : "no" );
Abc_Print( -2, "\t-l : toggle writing MiniLUT rather than AIGER [default = %s]\n", fMiniLut? "yes" : "no" );
Abc_Print( -2, "\t-n : toggle writing \'\\n\' after \'c\' in the AIGER file [default = %s]\n", fWriteNewLine? "yes": "no" );
@@ -32623,8 +32628,9 @@ int Abc_CommandAbc9Trim( Abc_Frame_t * pAbc, int argc, char ** argv )
int fTrimCos = 1;
int fDualOut = 0;
int fPoFedByPi = 0;
+ int fPoFedByPo = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Viocdh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Viocpdh" ) ) != EOF )
{
switch ( c )
{
@@ -32648,6 +32654,9 @@ int Abc_CommandAbc9Trim( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'c':
fPoFedByPi ^= 1;
break;
+ case 'p':
+ fPoFedByPo ^= 1;
+ break;
case 'd':
fDualOut ^= 1;
break;
@@ -32669,16 +32678,23 @@ int Abc_CommandAbc9Trim( Abc_Frame_t * pAbc, int argc, char ** argv )
pTemp = Gia_ManDupTrimmed2( pTemp2 = pTemp );
Gia_ManStop( pTemp2 );
}
+ if ( fPoFedByPo )
+ {
+ extern Gia_Man_t * Gia_ManDupTrimmed3( Gia_Man_t * p );
+ pTemp = Gia_ManDupTrimmed3( pTemp2 = pTemp );
+ Gia_ManStop( pTemp2 );
+ }
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
- Abc_Print( -2, "usage: &trim [-V num] [-iocdh]\n" );
+ Abc_Print( -2, "usage: &trim [-V num] [-iocpdh]\n" );
Abc_Print( -2, "\t removes PIs without fanout and PO driven by constants\n" );
Abc_Print( -2, "\t-V num : the value (0 or 1) of POs to remove [default = both]\n" );
Abc_Print( -2, "\t-i : toggle removing PIs [default = %s]\n", fTrimCis? "yes": "no" );
Abc_Print( -2, "\t-o : toggle removing POs [default = %s]\n", fTrimCos? "yes": "no" );
Abc_Print( -2, "\t-c : toggle additionally removing POs fed by PIs [default = %s]\n", fPoFedByPi? "yes": "no" );
+ Abc_Print( -2, "\t-p : toggle additionally removing duplicated POs [default = %s]\n", fPoFedByPo? "yes": "no" );
Abc_Print( -2, "\t-d : toggle using dual-output miter [default = %s]\n", fDualOut? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
@@ -49286,7 +49302,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Test(): There is no AIG.\n" );
return 1;
}
- Abc_FrameUpdateGia( pAbc, Gia_ManPerformNewResub(pAbc->pGia, 100, 8, 1, 1) );
+ Abc_FrameUpdateGia( pAbc, Gia_ManPerformNewResub(pAbc->pGia, 100, 6, 1, 1) );
// printf( "AIG in \"%s\" has the sum of output support sizes equal to %d.\n", pAbc->pGia->pSpec, Gia_ManSumTotalOfSupportSizes(pAbc->pGia) );
return 0;
usage:
diff --git a/src/base/abci/abcTiming.c b/src/base/abci/abcTiming.c
index ae0e7f45..2777c9f8 100644
--- a/src/base/abci/abcTiming.c
+++ b/src/base/abci/abcTiming.c
@@ -24,9 +24,11 @@
#include "base/main/main.h"
#include "map/mio/mio.h"
+
ABC_NAMESPACE_IMPL_START
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -187,8 +189,11 @@ void Abc_NtkTimeSetDefaultRequired( Abc_Ntk_t * pNtk, float Rise, float Fall )
pNtk->pManTime->tReqDef.Rise = Rise;
pNtk->pManTime->tReqDef.Fall = Fall;
// set the required times for each output
- Abc_NtkForEachCo( pNtk, pObj, i )
- Abc_NtkTimeSetRequired( pNtk, Abc_ObjId(pObj), Rise, Fall );
+ Abc_NtkForEachCo( pNtk, pObj, i ){
+ Abc_NtkTimeSetRequired( pNtk, Abc_ObjId(pObj), Rise, Fall );
+ // printf("Debug: Setting *default* required time on object %d to R %f F %f\n",
+ // Abc_ObjId(pObj),Rise,Fall);
+ }
}
/**Function*************************************************************
@@ -206,6 +211,8 @@ void Abc_NtkTimeSetArrival( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall
{
Vec_Ptr_t * vTimes;
Abc_Time_t * pTime;
+ static int debug;
+ debug++;
if ( pNtk->pManTime == NULL )
pNtk->pManTime = Abc_ManTimeStart(pNtk);
Abc_ManTimeExpand( pNtk->pManTime, ObjId + 1, 1 );
@@ -214,11 +221,16 @@ void Abc_NtkTimeSetArrival( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall
pTime = (Abc_Time_t *)vTimes->pArray[ObjId];
pTime->Rise = Rise;
pTime->Fall = Fall;
+ // printf("Debug:%d Setting arrival time on object %d to R %f and F %f\n",debug,
+ // ObjId, Rise, Fall);
+
}
void Abc_NtkTimeSetRequired( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall )
{
Vec_Ptr_t * vTimes;
Abc_Time_t * pTime;
+ static int debug;
+ debug++;
if ( pNtk->pManTime == NULL )
pNtk->pManTime = Abc_ManTimeStart(pNtk);
Abc_ManTimeExpand( pNtk->pManTime, ObjId + 1, 1 );
@@ -227,6 +239,8 @@ void Abc_NtkTimeSetRequired( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall
pTime = (Abc_Time_t *)vTimes->pArray[ObjId];
pTime->Rise = Rise;
pTime->Fall = Fall;
+ // printf("Debug:%d Setting required time on object %d to R %f and F %f\n",debug,
+ // ObjId, Rise, Fall);
}
/**Function*************************************************************
@@ -471,8 +485,9 @@ void Abc_NtkTimePrepare( Abc_Ntk_t * pNtk )
***********************************************************************/
Abc_ManTime_t * Abc_ManTimeStart( Abc_Ntk_t * pNtk )
{
- int fUseZeroDefaultOutputRequired = 1;
+ //int fUseZeroDefaultOutputRequired = 1;
Abc_ManTime_t * p;
+ Abc_Time_t* pTime;
Abc_Obj_t * pObj; int i;
p = pNtk->pManTime = ABC_ALLOC( Abc_ManTime_t, 1 );
memset( p, 0, sizeof(Abc_ManTime_t) );
@@ -480,16 +495,38 @@ Abc_ManTime_t * Abc_ManTimeStart( Abc_Ntk_t * pNtk )
p->vReqs = Vec_PtrAlloc( 0 );
// set default default input=arrivals (assumed to be 0)
// set default default output-requireds (can be either 0 or +infinity, based on the flag)
- p->tReqDef.Rise = fUseZeroDefaultOutputRequired ? 0 : ABC_INFINITY;
- p->tReqDef.Fall = fUseZeroDefaultOutputRequired ? 0 : ABC_INFINITY;
+
+ //AF: hack support the values read in. Not defaults !
+
+ // p->tReqDef.Rise = fUseZeroDefaultOutputRequired ? 0 : ABC_INFINITY;
+ // p->tReqDef.Fall = fUseZeroDefaultOutputRequired ? 0 : ABC_INFINITY;
+
// extend manager
Abc_ManTimeExpand( p, Abc_NtkObjNumMax(pNtk) + 1, 0 );
// set the default timing for CIs
- Abc_NtkForEachCi( pNtk, pObj, i )
- Abc_NtkTimeSetArrival( pNtk, Abc_ObjId(pObj), p->tArrDef.Rise, p->tArrDef.Rise );
+ Abc_NtkForEachCi( pNtk, pObj, i ){
+ Vec_Ptr_t * vTimes;
+ vTimes = pNtk->pManTime->vArrs;
+ pTime = (Abc_Time_t *)vTimes->pArray[Abc_ObjId(pObj)];
+ if (pTime){
+ p->tArrDef.Fall = pTime -> Fall;
+ p->tArrDef.Rise = pTime -> Rise;
+ }
+
+ Abc_NtkTimeSetArrival( pNtk, Abc_ObjId(pObj), p->tArrDef.Rise, p->tArrDef.Rise );
+ }
+
// set the default timing for COs
- Abc_NtkForEachCo( pNtk, pObj, i )
- Abc_NtkTimeSetRequired( pNtk, Abc_ObjId(pObj), p->tReqDef.Rise, p->tReqDef.Rise );
+ Abc_NtkForEachCo( pNtk, pObj, i ){
+ Vec_Ptr_t * vTimes;
+ vTimes = pNtk->pManTime->vArrs;
+ pTime = (Abc_Time_t *)vTimes->pArray[Abc_ObjId(pObj)];
+ if (pTime){
+ p->tReqDef.Fall = pTime -> Fall;
+ p->tReqDef.Rise = pTime -> Rise;
+ }
+ Abc_NtkTimeSetRequired( pNtk, Abc_ObjId(pObj), p->tReqDef.Rise, p->tReqDef.Rise );
+ }
return p;
}
@@ -571,6 +608,9 @@ void Abc_ManTimeDup( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew )
pNtkNew->pManTime->tOutLoad = ABC_ALLOC( Abc_Time_t, Abc_NtkCiNum(pNtkOld) );
memcpy( pNtkNew->pManTime->tOutLoad, pNtkOld->pManTime->tOutLoad, sizeof(Abc_Time_t) * Abc_NtkCoNum(pNtkOld) );
}
+
+ printf("State of abc timing manager\n");
+ Abc_NtkTimePrint(pNtkNew);
}
/**Function*************************************************************
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index 405b44d6..e8979c9b 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -22,6 +22,9 @@
#include "base/main/main.h"
#include "map/mio/mio.h"
+
+
+
ABC_NAMESPACE_IMPL_START
@@ -877,10 +880,13 @@ int Io_ReadBlifNetworkInputArrival( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
return 1;
}
// set timing info
- //Abc_NtkTimeSetArrival( p->pNtkCur, Abc_ObjFanin0(pNet)->Id, (float)TimeRise, (float)TimeFall );
- Vec_IntPush( p->vInArrs, Abc_ObjFanin0(pNet)->Id );
- Vec_IntPush( p->vInArrs, Abc_Float2Int((float)TimeRise) );
- Vec_IntPush( p->vInArrs, Abc_Float2Int((float)TimeFall) );
+ // printf("Debug: Forcing setting of arrival times\n");
+ if (Abc_ObjFaninNum(pNet) >0){
+ Abc_NtkTimeSetArrival( p->pNtkCur, Abc_ObjFanin0(pNet)->Id, (float)TimeRise, (float)TimeFall );
+ Vec_IntPush( p->vInArrs, Abc_ObjFanin0(pNet)->Id );
+ Vec_IntPush( p->vInArrs, Abc_Float2Int((float)TimeRise) );
+ Vec_IntPush( p->vInArrs, Abc_Float2Int((float)TimeFall) );
+ }
return 0;
}
@@ -928,7 +934,10 @@ int Io_ReadBlifNetworkOutputRequired( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
return 1;
}
// set timing info
-// Abc_NtkTimeSetRequired( p->pNtkCur, Abc_ObjFanout0(pNet)->Id, (float)TimeRise, (float)TimeFall );
+ // printf("Setting required time for object %d to R %f F %f\n",
+ // Abc_ObjFanout0(pNet)->Id, (float)TimeRise, (float)TimeFall );
+
+ Abc_NtkTimeSetRequired( p->pNtkCur, Abc_ObjFanout0(pNet)->Id, (float)TimeRise, (float)TimeFall );
Vec_IntPush( p->vOutReqs, Abc_ObjFanout0(pNet)->Id );
Vec_IntPush( p->vOutReqs, Abc_Float2Int((float)TimeRise) );
Vec_IntPush( p->vOutReqs, Abc_Float2Int((float)TimeFall) );
diff --git a/src/base/wlc/wlcAbc.c b/src/base/wlc/wlcAbc.c
index e1b06ffd..8b7dbfa7 100644
--- a/src/base/wlc/wlcAbc.c
+++ b/src/base/wlc/wlcAbc.c
@@ -140,7 +140,7 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vCounts, int fVerbose )
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv )
+Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Ptr_t * vNamesIn )
{
extern Vec_Int_t * Pdr_InvCounts( Vec_Int_t * vInv );
extern Vec_Str_t * Pdr_InvPrintStr( Vec_Int_t * vInv, Vec_Int_t * vCounts );
@@ -166,8 +166,16 @@ Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv )
if ( Entry == 0 )
continue;
pMainObj = Abc_NtkCreatePi( pMainNtk );
- sprintf( Buffer, "pi%d", i );
- Abc_ObjAssignName( pMainObj, Buffer, NULL );
+ // If vNamesIn is given, take names from there for as many entries as possible
+ // otherwise generate names from counter
+ if (vNamesIn != NULL && i < Vec_PtrSize(vNamesIn)) {
+ Abc_ObjAssignName( pMainObj, (char *)Vec_PtrEntry(vNamesIn, i), NULL );
+ }
+ else
+ {
+ sprintf( Buffer, "pi%d", i );
+ Abc_ObjAssignName( pMainObj, Buffer, NULL );
+ }
}
if ( Abc_NtkPiNum(pMainNtk) != nInputs )
{
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 666a8776..39f1bebd 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -1727,15 +1727,19 @@ usage:
******************************************************************************/
int Abc_CommandInvGet( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- extern Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv );
+ extern Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Ptr_t * vNamesIn );
Abc_Ntk_t * pMainNtk;
Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
- int c, fVerbose = 0;
+ int c, i, fVerbose = 0, fFlopNamesFromGia = 0;
+ Vec_Ptr_t * vNamesIn = NULL;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "fvh" ) ) != EOF )
{
switch ( c )
{
+ case 'f':
+ fFlopNamesFromGia ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -1750,16 +1754,38 @@ int Abc_CommandInvGet( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "Abc_CommandInvGet(): Invariant is not available.\n" );
return 0;
}
+ // See if we shall and can copy the PI names from the current GIA
+ if ( fFlopNamesFromGia )
+ {
+ if ( pAbc->pGia == NULL )
+ {
+ Abc_Print( 1, "Abc_CommandInvGet(): No network in &-space, cannot copy names.\n" );
+ fFlopNamesFromGia = 0;
+ }
+ else
+ {
+ vNamesIn = Vec_PtrStart( Gia_ManRegNum(pAbc->pGia) );
+ for ( i = 0; i < Gia_ManRegNum(pAbc->pGia); ++i )
+ {
+ // Only the registers
+ Vec_PtrSetEntry( vNamesIn, i, Extra_UtilStrsav( (const char*)Vec_PtrEntry( pAbc->pGia->vNamesIn, Gia_ManPiNum(pAbc->pGia)+i ) ) );
+ }
+ }
+ }
// derive the network
- pMainNtk = Wlc_NtkGetInv( pNtk, Wlc_AbcGetInv(pAbc) );
+ pMainNtk = Wlc_NtkGetInv( pNtk, Wlc_AbcGetInv(pAbc), vNamesIn );
+ // Delete names
+ if (vNamesIn)
+ Vec_PtrFree( vNamesIn );
// replace the current network
if ( pMainNtk )
Abc_FrameReplaceCurrentNetwork( pAbc, pMainNtk );
return 0;
usage:
- Abc_Print( -2, "usage: inv_get [-vh]\n" );
+ Abc_Print( -2, "usage: inv_get [-fvh]\n" );
Abc_Print( -2, "\t places invariant found by PDR as the current network in the main-space\n" );
- Abc_Print( -2, "\t (in the case of \'sat\' or \'undecided\', inifity clauses are used)\n" );
+ Abc_Print( -2, "\t (in the case of \'sat\' or \'undecided\', infinity clauses are used)\n" );
+ Abc_Print( -2, "\t-f : toggle reading flop names from the &-space [default = %s]\n", fFlopNamesFromGia? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-17 15:26:49 +0000