diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-09 16:38:08 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-09 16:38:08 -0800 |
commit | 7a2984bbe9e2d9e76851c0ce440e08f6788fcb70 (patch) | |
tree | 1a881ad856e68b06971fa439f6467274954d7924 /src/base/wlc/wlcCom.c | |
parent | 2fe17c1f4bf2a4df4076ad2fee336f568c52786f (diff) | |
download | abc-7a2984bbe9e2d9e76851c0ce440e08f6788fcb70.tar.gz abc-7a2984bbe9e2d9e76851c0ce440e08f6788fcb70.tar.bz2 abc-7a2984bbe9e2d9e76851c0ce440e08f6788fcb70.zip |
Word-level abstraction.
Diffstat (limited to 'src/base/wlc/wlcCom.c')
-rw-r--r-- | src/base/wlc/wlcCom.c | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index cc69c636..346a9076 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -423,7 +423,7 @@ int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv ) printf( "Extracting output %d as a %s word-level network.\n", iOutput, fSeq ? "sequential" : "combinational" ); pName = Wlc_NtkNewName( pNtk, iOutput, fSeq ); Wlc_NtkMarkCone( pNtk, iOutput, Range, fSeq, fAllPis ); - pNtk = Wlc_NtkDupDfs( pNtk, 1, fSeq, NULL ); + pNtk = Wlc_NtkDupDfs( pNtk, 1, fSeq ); ABC_FREE( pNtk->pName ); pNtk->pName = Abc_UtilStrsav( pName ); Wlc_AbcUpdateNtk( pAbc, pNtk ); @@ -941,6 +941,7 @@ usage: ******************************************************************************/ int Abc_CommandInvCheck( Abc_Frame_t * pAbc, int argc, char ** argv ) { + abctime clk = Abc_Clock(); extern int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ); int c, nFailed, fVerbose = 0; Extra_UtilGetoptReset(); @@ -974,9 +975,10 @@ int Abc_CommandInvCheck( Abc_Frame_t * pAbc, int argc, char ** argv ) } nFailed = Pdr_InvCheck( pAbc->pGia, Wlc_AbcGetInv(pAbc), fVerbose ); if ( nFailed ) - printf( "Invariant verification failed for %d clauses (out of %d).\n", nFailed, Vec_IntEntry(Wlc_AbcGetInv(pAbc),0) ); + printf( "Invariant verification failed for %d clauses (out of %d). ", nFailed, Vec_IntEntry(Wlc_AbcGetInv(pAbc),0) ); else - printf( "Invariant verification succeeded.\n" ); + printf( "Invariant verification succeeded. " ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); return 0; usage: Abc_Print( -2, "usage: inv_check [-vh]\n" ); |