diff options
Diffstat (limited to 'src/base/abci')
-rw-r--r-- | src/base/abci/abc.c | 93 | ||||
-rw-r--r-- | src/base/abci/abcMiter.c | 14 | ||||
-rw-r--r-- | src/base/abci/abcRefactor.c | 2 | ||||
-rw-r--r-- | src/base/abci/abcRewrite.c | 2 | ||||
-rw-r--r-- | src/base/abci/abcSat.c | 14 |
5 files changed, 105 insertions, 20 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 4745273e..16be21fd 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -86,6 +86,7 @@ static int Abc_CommandFpga ( Abc_Frame_t * pAbc, int argc, char ** argv static int Abc_CommandPga ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSeq ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandUnseq ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRetime ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -163,6 +164,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "FPGA mapping", "pga", Abc_CommandPga, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "seq", Abc_CommandSeq, 1 ); + Cmd_CommandAdd( pAbc, "Sequential", "unseq", Abc_CommandUnseq, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "retime", Abc_CommandRetime, 1 ); Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 ); @@ -949,9 +951,9 @@ int Abc_CommandShowAig( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - if ( !Abc_NtkIsStrash(pNtk) ) + if ( !Abc_NtkHasAig(pNtk) ) { - fprintf( pErr, "Visualizing AIG can only be done for AIGs (run \"strash\").\n" ); + fprintf( pErr, "Visualizing AIG can only be done for AIGs (run \"strash\" or \"seq\").\n" ); return 1; } Abc_NtkShowAig( pNtk ); @@ -3906,7 +3908,6 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; int c; - extern Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk ); pNtk = Abc_FrameReadNet(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -3931,8 +3932,8 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - printf( "This command is not yet implemented.\n" ); - return 0; +// printf( "This command is not yet implemented.\n" ); +// return 0; if ( !Abc_NtkIsStrash(pNtk) ) { @@ -3959,7 +3960,81 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: fprintf( pErr, "usage: seq [-h]\n" ); - fprintf( pErr, "\t converts AIG into sequential AIG (while sweeping latches)\n" ); + fprintf( pErr, "\t converts AIG into sequential AIG\n" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandUnseq( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int c; + int fShare; + + pNtk = Abc_FrameReadNet(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + fShare = 1; + util_getopt_reset(); + while ( ( c = util_getopt( argc, argv, "sh" ) ) != EOF ) + { + switch ( c ) + { + case 's': + fShare ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + + if ( !Abc_NtkIsSeq(pNtk) ) + { + fprintf( pErr, "Works only for sequential AIG (run \"seq\").\n" ); + return 1; + } + + // share the latches on the fanout edges + if ( fShare ) + Abc_NtkSeqShareFanouts(pNtk); + + // get the new network + pNtkRes = Abc_NtkSeqToLogicSop( pNtk ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Converting sequential AIG into an SOP logic network has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: unseq [-sh]\n" ); + fprintf( pErr, "\t converts sequential AIG into an SOP logic network\n" ); + fprintf( pErr, "\t-s : toggle sharing latches [default = %s]\n", fShare? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -3991,7 +4066,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - fForward = 0; + fForward = 1; fBackward = 0; fInitial = 0; util_getopt_reset(); @@ -4021,10 +4096,6 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - printf( "This command is not yet implemented.\n" ); - return 0; - - if ( !Abc_NtkIsSeq(pNtk) ) { fprintf( pErr, "Works only for sequential AIG.\n" ); diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c index 20f41c56..01317d1d 100644 --- a/src/base/abci/abcMiter.c +++ b/src/base/abci/abcMiter.c @@ -501,7 +501,7 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial ) pLatch->pCopy = Abc_ObjNotCond( Abc_AigConst1(pNtkFrames->pManFunc), Abc_LatchIsInit0(pLatch) ); } if ( Counter ) - printf( "Warning: %d uninitialized latches are replaced by free variables.\n", Counter ); + printf( "Warning: %d uninitialized latches are replaced by free PI variables.\n", Counter ); } // create the timeframes @@ -521,12 +521,18 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial ) Abc_NtkForEachLatch( pNtk, pLatch, i ) { pLatchNew = Abc_NtkLatch(pNtkFrames, i); - Abc_ObjAddFanin( pLatchNew, Abc_ObjFanin0(pLatch)->pCopy ); + Abc_ObjAddFanin( pLatchNew, pLatch->pCopy ); Vec_PtrPush( pNtkFrames->vCis, pLatchNew ); Vec_PtrPush( pNtkFrames->vCos, pLatchNew ); Abc_NtkLogicStoreName( pLatchNew, Abc_ObjName(pLatch) ); } } + Abc_NtkForEachLatch( pNtk, pLatch, i ) + pLatch->pNext = NULL; + + // remove dangling nodes + Abc_AigCleanup( pNtkFrames->pManFunc ); + // make sure that everything is okay if ( !Abc_NtkCheck( pNtkFrames ) ) { @@ -586,7 +592,9 @@ void Abc_NtkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_ } // transfer the implementation of the latch drivers to the latches Abc_NtkForEachLatch( pNtk, pLatch, i ) - pLatch->pCopy = Abc_ObjChild0Copy(pLatch); + pLatch->pNext = Abc_ObjChild0Copy(pLatch); + Abc_NtkForEachLatch( pNtk, pLatch, i ) + pLatch->pCopy = pLatch->pNext; } diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c index 3d9534c8..421e3059 100644 --- a/src/base/abci/abcRefactor.c +++ b/src/base/abci/abcRefactor.c @@ -144,6 +144,8 @@ pManRef->timeTotal = clock() - clkStart; Abc_NtkManRefStop( pManRef ); // put the nodes into the DFS order and reassign their IDs Abc_NtkReassignIds( pNtk ); + Abc_AigRehash( pNtk->pManFunc ); +// Abc_AigCheckFaninOrder( pNtk->pManFunc ); // fix the levels if ( fUpdateLevel ) Abc_NtkStopReverseLevels( pNtk ); diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c index 91a99a57..b70d30e6 100644 --- a/src/base/abci/abcRewrite.c +++ b/src/base/abci/abcRewrite.c @@ -115,6 +115,8 @@ Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart ); pNtk->pManCut = NULL; // put the nodes into the DFS order and reassign their IDs Abc_NtkReassignIds( pNtk ); + Abc_AigRehash( pNtk->pManFunc ); +// Abc_AigCheckFaninOrder( pNtk->pManFunc ); // fix the levels if ( fUpdateLevel ) Abc_NtkStopReverseLevels( pNtk ); diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c index b335086f..e5bc2547 100644 --- a/src/base/abci/abcSat.c +++ b/src/base/abci/abcSat.c @@ -52,7 +52,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose ) assert( Abc_NtkLatchNum(pNtk) == 0 ); if ( Abc_NtkPoNum(pNtk) > 1 ) - fprintf( stdout, "Warning: The miter has more than 1 output. SAT will try to prove all of them.\n" ); + fprintf( stdout, "Warning: The miter has %d outputs. SAT will try to prove all of them.\n", Abc_NtkPoNum(pNtk) ); // load clauses into the solver clk = clock(); @@ -65,11 +65,11 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose ) status = solver_simplify(pSat); // printf( "Simplified the problem to %d variables and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) ); // PRT( "Time", clock() - clk ); - if ( status == l_False ) + if ( status == 0 ) { solver_delete( pSat ); - printf( "The problem is UNSATISFIABLE after simplification.\n" ); - return 0; +// printf( "The problem is UNSATISFIABLE after simplification.\n" ); + return -1; } // solve the miter @@ -146,8 +146,10 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk ) Abc_NodeAddClauses( pSat, pSop0, pSop1, pNode, vVars ); } // add clauses for each PO - Abc_NtkForEachPo( pNtk, pNode, i ) - Abc_NodeAddClausesTop( pSat, pNode, vVars ); +// Abc_NtkForEachPo( pNtk, pNode, i ) +// Abc_NodeAddClausesTop( pSat, pNode, vVars ); + + Abc_NodeAddClausesTop( pSat, Abc_NtkPo(pNtk, Abc_NtkPoNum(pNtk)-1), vVars ); // delete Vec_StrFree( vCube ); |