From 51a646a355c78cf0f4cf104d6316706653b24008 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 22 Jun 2015 23:05:13 -0700 Subject: Version abc90901 committer: Baruch Sterin --- abc.rc | 50 ++++++++- abclib.dsp | 48 ++++++++- src/aig/aig/aig.h | 1 + src/aig/aig/aigMan.c | 1 + src/aig/bbr/bbrCex.c | 1 + src/aig/bbr/bbrImage.c | 38 ++++++- src/aig/cnf/cnf.h | 2 + src/aig/cnf/cnfUtil.c | 44 ++++++++ src/aig/gia/gia.h | 34 +++++-- src/aig/gia/giaAig.c | 24 +++++ src/aig/gia/giaAig.h | 1 + src/aig/gia/module.make | 2 + src/aig/ntl/ntlReadBlif.c | 12 +-- src/aig/saig/saig.h | 3 +- src/aig/saig/saigAbs.c | 122 ++++++++++++++++------ src/aig/saig/saigBmc.c | 251 ++++++++++++++++++++++++++++++++++++++-------- src/aig/saig/saigDup.c | 121 +++++++++++++++++----- src/aig/saig/saigSimExt.c | 10 +- src/aig/ssw/sswSim.c | 2 +- src/base/abci/abc.c | 132 +++++++++++------------- src/base/abci/abcDar.c | 97 +++++++++++++++++- src/misc/vec/vecAtt.h | 4 +- src/misc/vec/vecInt.h | 38 +++++++ src/opt/mfs/mfsStrash.c | 54 ++++++++++ 24 files changed, 890 insertions(+), 202 deletions(-) diff --git a/abc.rc b/abc.rc index d618ea34..b2247204 100644 --- a/abc.rc +++ b/abc.rc @@ -2,8 +2,8 @@ set check # checks intermediate networks #set checkfio # prints warnings when fanins/fanouts are duplicated set checkread # checks new networks after reading from file -set backup # saves backup networks retrived by "undo" and "recall" -set savesteps 1 # sets the maximum number of backup networks to save +#set backup # saves backup networks retrived by "undo" and "recall" +#set savesteps 1 # sets the maximum number of backup networks to save set progressbar # display the progress bar # program names for internal calls @@ -138,9 +138,51 @@ alias pjsolve "scl; dc2; fr; dc2; ic; ic -t; if -a; cs tacas/005_care.aig; mfs alias t0 "r test/mc1.blif; st; test" alias t1 "r s27mc2.blif; st; test" alias t2 "r i/intel_001.aig; ps; indcut -v" -alias t "r c\s\0\000.aig; int" +#alias t "r c\s\0\000.aig; int" #alias t "r test/interpol.blif; st; int" +alias t "&r s444.aig; &ps; &era -v" -#read_library at\syn\brdcm.genlib + +alias spec "&r 1.aig;&srm -s;r gsrm.aig; bmc2 -F 1000 -C 10000; &resim; &w 1.aig; &ps " +alias spech "&r 1.aig;&srm -s;r gsrm.aig;scl;ps; bmc2 -F 1000 -C 25000; &resim; &w 1.aig; &ps " +alias spechx "&r 1.aig;&srm ;r gsrm.aig;smp;bmc2 -F 5000 -C 75000; &resim; &w 1.aig; &ps " +alias specb "&r 1.aig;&srm ;r gsrm.aig;smp;ps; reach -o -B 1000000 -F 2000; &resim; &w 1.aig; &ps " +alias specp "&r 1.aig;&srm ;r gsrm.aig;scorr -F 2;ps; simpk ; &resim; &w 1.aig; &ps " +alias sprb "ua; &get; eclassh; specb" +alias sprh "ua; &get; eclassh; spech" + +alias eclass "&equiv -smf -W 255 -F 1000; &w 1.aig" +alias transfer "w 1.aig; &r 1.aig" +alias &ua "set autoexec " +alias scr "&get; &scorr; &put" +alias lcr "&get; &lcorr; &put" +alias trm "logic;trim;st;ps" +alias inth "int -rv -C 25000" + +alias spr "ua; &get; eclass; spech" +alias reachx "reach -o -B 1000000000 -F 5000" +alias dc2rs "ua; compress2rs; ps" +alias simp "dprove -vrcbju -C 5000 -V 1" +alias simpk "dprove -vrcbkmfiu -B 10 -D 1000" +alias indh "ind -v -F 50 -C 10000" + +alias eclassh "&equiv -smf -W 512 -F 2000; &w 1.aig" +alias ffx "ps;orpos;qua_ffix" +alias bfx "ps;orpos;qua_bfix" +alias smp "ua;ps;scl;rw;dr;lcorr;rw;dr;scorr;fraig;dc2;dr;scorr -F 2;dc2rs;w temp.aig" + +alias s "w temp.aig" + +alias absh "abs -se -D 25000" +alias absr "abs -ser -G 2000" +alias absp "abs -sep -G 2000" + +alias spechi "ua; &get; &equiv -smf -W 512 -F 2000; &ps; &speci; &srm; r gsrm.aig;&ps;&w 1.aig" +alias spechis "ua; &get; &equiv -s -W 512 -F 2000; &ps; &speci; &srm -s; r gsrm.aig; &ps; &w 1.aig" +alias absh1 "absh -R 1" +alias simpkh "simpk -D 25000" + +alias spechisf "ua; &get; &equiv -smf -W 512 -F 2000; &ps; &semi -R 5; &srm; r gsrm.aig;&ps;&w 1.aig" +alias spechissf "ua; &get; &equiv -s -W 512 -F 2000; &ps; ; &srm -s; r gsrm.aig; &ps; &w 1.aig" diff --git a/abclib.dsp b/abclib.dsp index 9aa8d573..72e14fc1 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -41,7 +41,7 @@ RSC=rc.exe # PROP Intermediate_Dir "ReleaseLib" # PROP Target_Dir "" # ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_MBCS" /D "_LIB" /YX /FD /c -# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/sat/nsat" /I "src/sat/psat" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /I "src/aig/int" /I "src/aig/dch" /I "src/aig/ssw" /I "src/sat/lsat" /I "src/aig/cec" /I "src/aig/cgt" /I "src/aig/sec" /I "src/map/amap" /I "src/aig/fsim" /I "src/aig/gia" /I "src/aig/bbl" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /c +# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/sat/nsat" /I "src/sat/psat" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /I "src/aig/int" /I "src/aig/dch" /I "src/aig/ssw" /I "src/sat/lsat" /I "src/aig/cec" /I "src/aig/cgt" /I "src/aig/sec" /I "src/map/amap" /I "src/aig/fsim" /I "src/aig/gia" /I "src/aig/bbl" /I "src/aig/sky" /I "src/aig/nal2" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /c # ADD BASE RSC /l 0x409 /d "NDEBUG" # ADD RSC /l 0x409 /d "NDEBUG" BSC32=bscmake.exe @@ -64,7 +64,7 @@ LIB32=link.exe -lib # PROP Intermediate_Dir "DebugLib" # PROP Target_Dir "" # ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_MBCS" /D "_LIB" /YX /FD /GZ /c -# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/sat/nsat" /I "src/sat/psat" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /I "src/aig/int" /I "src/aig/dch" /I "src/aig/ssw" /I "src/sat/lsat" /I "src/aig/cec" /I "src/aig/cgt" /I "src/aig/sec" /I "src/map/amap" /I "src/aig/fsim" /I "src/aig/gia" /I "src/aig/bbl" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /GZ /c +# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/sat/nsat" /I "src/sat/psat" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /I "src/aig/int" /I "src/aig/dch" /I "src/aig/ssw" /I "src/sat/lsat" /I "src/aig/cec" /I "src/aig/cgt" /I "src/aig/sec" /I "src/map/amap" /I "src/aig/fsim" /I "src/aig/gia" /I "src/aig/bbl" /I "src/aig/sky" /I "src/aig/nal2" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /GZ /c # ADD BASE RSC /l 0x409 /d "_DEBUG" # ADD RSC /l 0x409 /d "_DEBUG" BSC32=bscmake.exe @@ -3703,6 +3703,10 @@ SOURCE=.\src\aig\gia\gia.h # End Source File # Begin Source File +SOURCE=.\src\aig\gia\giaAbs.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\gia\giaAig.c # End Source File # Begin Source File @@ -3755,6 +3759,10 @@ SOURCE=.\src\aig\gia\giaEra.c # End Source File # Begin Source File +SOURCE=.\src\aig\gia\giaEra2.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\gia\giaFanout.c # End Source File # Begin Source File @@ -3850,6 +3858,42 @@ SOURCE=.\src\aig\live\liveness.c SOURCE=.\src\aig\live\liveness_sim.c # End Source File # End Group +# Begin Group "sky" + +# PROP Default_Filter "" +# Begin Source File + +SOURCE=.\src\aig\sky\sky.c +# End Source File +# Begin Source File + +SOURCE=.\src\aig\sky\sky.h +# End Source File +# Begin Source File + +SOURCE=.\src\aig\sky\skyCheck.c +# End Source File +# Begin Source File + +SOURCE=.\src\aig\sky\skyMan.c +# End Source File +# Begin Source File + +SOURCE=.\src\aig\sky\skyName.c +# End Source File +# Begin Source File + +SOURCE=.\src\aig\sky\skyObj.c +# End Source File +# Begin Source File + +SOURCE=.\src\aig\sky\skyReadBlif.c +# End Source File +# Begin Source File + +SOURCE=.\src\aig\sky\skyUtil.c +# End Source File +# End Group # End Group # End Group # Begin Group "Header Files" diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 56e2336a..45b509dc 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -156,6 +156,7 @@ struct Aig_Man_t_ Vec_Int_t * vEquPairs; Vec_Vec_t * vClockDoms; Vec_Int_t * vProbs; // probability of node being 1 + Vec_Int_t * vCiNumsOrig; // original CI names // timing statistics int time1; int time2; diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c index 11d3f3d7..01b29f5f 100644 --- a/src/aig/aig/aigMan.c +++ b/src/aig/aig/aigMan.c @@ -211,6 +211,7 @@ void Aig_ManStop( Aig_Man_t * p ) if ( p->vOnehots ) Vec_VecFree( (Vec_Vec_t *)p->vOnehots ); if ( p->vClockDoms) Vec_VecFree( p->vClockDoms ); if ( p->vProbs ) Vec_IntFree( p->vProbs ); + if ( p->vCiNumsOrig)Vec_IntFree( p->vCiNumsOrig ); ABC_FREE( p->pFastSim ); ABC_FREE( p->pData ); ABC_FREE( p->pSeqModel ); diff --git a/src/aig/bbr/bbrCex.c b/src/aig/bbr/bbrCex.c index 4555570a..947c393c 100644 --- a/src/aig/bbr/bbrCex.c +++ b/src/aig/bbr/bbrCex.c @@ -54,6 +54,7 @@ Ssw_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd, int i, v, RetValue, nPiOffset; char * pValues; int clk = clock(); +//printf( "\nDeriving counter-example.\n" ); // allocate room for the counter-example pCex = Ssw_SmlAllocCounterExample( Saig_ManRegNum(p), Saig_ManPiNum(p), Vec_PtrSize(vOnionRings)+1 ); diff --git a/src/aig/bbr/bbrImage.c b/src/aig/bbr/bbrImage.c index aed302eb..c16a8ff4 100644 --- a/src/aig/bbr/bbrImage.c +++ b/src/aig/bbr/bbrImage.c @@ -232,6 +232,7 @@ Bbr_ImageTree_t * Bbr_bddImageStart( // clean the partitions Bbr_DeleteParts_rec( pTree->pRoot ); ABC_FREE( pParts ); + return pTree; } @@ -729,13 +730,26 @@ int Bbr_BuildTreeNode( DdManager * dd, iVarBest = Bbr_FindBestVariable( dd, nNodes, pNodes, nVars, pVars ); if ( iVarBest == -1 ) return 0; - +/* +for ( v = 0; v < nVars; v++ ) +{ + DdNode * bSupp; + if ( pVars[v] == NULL ) + continue; + printf( "%3d :", v ); + printf( "%3d ", pVars[v]->nParts ); + bSupp = Cudd_Support( dd, pVars[v]->bParts ); Cudd_Ref( bSupp ); + Bbr_bddPrint( dd, bSupp ); printf( "\n" ); + Cudd_RecursiveDeref( dd, bSupp ); +} +*/ pVar = pVars[iVarBest]; // this var cannot appear in one partition only nSupp = Cudd_SupportSize( dd, pVar->bParts ); assert( nSupp == pVar->nParts ); assert( nSupp != 1 ); +//printf( "var = %d supp = %d\n\n", iVarBest, nSupp ); // if it appears in only two partitions, quantify it if ( pVar->nParts == 2 ) @@ -773,6 +787,7 @@ int Bbr_BuildTreeNode( DdManager * dd, Bbr_FindBestPartitions( dd, pVar->bParts, nNodes, pNodes, &iNode1, &iNode2 ); pNode1 = pNodes[iNode1]; pNode2 = pNodes[iNode2]; +//printf( "smallest bdds with this var: %d %d\n", iNode1, iNode2 ); /* // it is not possible that a var appears only in these two // otherwise, it would have a different cost @@ -789,6 +804,7 @@ int Bbr_BuildTreeNode( DdManager * dd, // clean the old nodes pNodes[iNode1] = pNode; pNodes[iNode2] = NULL; +//printf( "Removing node %d (leaving node %d)\n", iNode2, iNode1 ); // update the variables that appear in pNode[iNode2] for ( bSuppTemp = pNode2->pPart->bSupp; bSuppTemp != b1; bSuppTemp = cuddT(bSuppTemp) ) @@ -941,9 +957,29 @@ int Bbr_FindBestVariable( DdManager * dd, CostBest = 100000000000000.0; iVarBest = -1; + + // check if there are two-variable partitions + for ( v = 0; v < nVars; v++ ) + if ( pVars[v] && pVars[v]->nParts == 2 ) + { + CostCur = 0; + for ( bTemp = pVars[v]->bParts; bTemp != b1; bTemp = cuddT(bTemp) ) + CostCur += pNodes[bTemp->index]->pPart->nNodes * + pNodes[bTemp->index]->pPart->nNodes; + if ( CostBest > CostCur ) + { + CostBest = CostCur; + iVarBest = v; + } + } + if ( iVarBest >= 0 ) + return iVarBest; + + // find other partition for ( v = 0; v < nVars; v++ ) if ( pVars[v] ) { + assert( pVars[v]->nParts > 1 ); CostCur = 0; for ( bTemp = pVars[v]->bParts; bTemp != b1; bTemp = cuddT(bTemp) ) CostCur += pNodes[bTemp->index]->pPart->nNodes * diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h index 4343bf9a..f7d1d38c 100644 --- a/src/aig/cnf/cnf.h +++ b/src/aig/cnf/cnf.h @@ -157,6 +157,8 @@ extern void Cnf_ManPostprocess( Cnf_Man_t * p ); /*=== cnfUtil.c ========================================================*/ extern Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect ); extern Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder ); +extern Vec_Int_t * Cnf_DataCollectCiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p ); +extern Vec_Int_t * Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p ); /*=== cnfWrite.c ========================================================*/ extern void Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover ); extern Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ); diff --git a/src/aig/cnf/cnfUtil.c b/src/aig/cnf/cnfUtil.c index 3738fee5..7da9fb47 100644 --- a/src/aig/cnf/cnfUtil.c +++ b/src/aig/cnf/cnfUtil.c @@ -182,6 +182,50 @@ Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder ) return vMapped; } +/**Function************************************************************* + + Synopsis [Returns the array of CI IDs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Cnf_DataCollectCiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p ) +{ + Vec_Int_t * vCiIds; + Aig_Obj_t * pObj; + int i; + vCiIds = Vec_IntAlloc( Aig_ManPiNum(p) ); + Aig_ManForEachPi( p, pObj, i ) + Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] ); + return vCiIds; +} + +/**Function************************************************************* + + Synopsis [Returns the array of CI IDs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p ) +{ + Vec_Int_t * vCoIds; + Aig_Obj_t * pObj; + int i; + vCoIds = Vec_IntAlloc( Aig_ManPoNum(p) ); + Aig_ManForEachPo( p, pObj, i ) + Vec_IntPush( vCoIds, pCnf->pVarNums[pObj->Id] ); + return vCoIds; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index f8c1fe91..f023366a 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -136,6 +136,7 @@ struct Gia_Man_t_ unsigned char* pSwitching; // switching activity for each object Gia_Plc_t * pPlacement; // placement of the objects int * pTravIds; // separate traversal ID representation + int nTravIdsAlloc; // the number of trav IDs allocated Vec_Ptr_t * vNamesIn; // the input names Vec_Ptr_t * vNamesOut; // the output names }; @@ -167,7 +168,6 @@ struct Gia_ParFra_t_ }; - // simulation parameters typedef struct Gia_ParSim_t_ Gia_ParSim_t; struct Gia_ParSim_t_ @@ -197,6 +197,7 @@ static inline void Gia_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= static inline void Gia_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); } static inline unsigned Gia_InfoMask( int nVar ) { return (~(unsigned)0) >> (32-nVar); } static inline unsigned Gia_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId & 31)); } +static inline int Gia_WordHasOneBit( unsigned uWord ) { return (uWord & (uWord-1)) == 0; } static inline int Gia_WordCountOnes( unsigned uWord ) { uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555); @@ -320,14 +321,29 @@ static inline void Gia_ObjSetTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * static inline int Gia_ObjIsTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj ) { return ((int)pObj->Value == p->nTravIds); } static inline int Gia_ObjIsTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { return ((int)pObj->Value == p->nTravIds - 1); } -static inline void Gia_ManResetTravIdArray( Gia_Man_t * p ) { ABC_FREE( p->pTravIds ); p->pTravIds = ABC_CALLOC( int, Gia_ManObjNum(p) ); p->nTravIds = 1; } -static inline void Gia_ManIncrementTravIdArray( Gia_Man_t * p ) { p->nTravIds++; } -static inline void Gia_ObjSetTravIdCurrentArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { p->pTravIds[Gia_ObjId(p, pObj)] = p->nTravIds; } -static inline void Gia_ObjSetTravIdPreviousArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { p->pTravIds[Gia_ObjId(p, pObj)] = p->nTravIds - 1; } -static inline int Gia_ObjIsTravIdCurrentArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds); } -static inline int Gia_ObjIsTravIdPreviousArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds - 1); } -static inline void Gia_ObjSetTravIdCurrentArrayId( Gia_Man_t * p, int Id ) { p->pTravIds[Id] = p->nTravIds; } -static inline int Gia_ObjIsTravIdCurrentArrayId( Gia_Man_t * p, int Id ) { return (p->pTravIds[Id] == p->nTravIds); } +static inline void Gia_ManResetTravIdArray( Gia_Man_t * p ) +{ + ABC_FREE( p->pTravIds ); + p->nTravIdsAlloc = Gia_ManObjNum(p); + p->pTravIds = ABC_CALLOC( int, p->nTravIdsAlloc ); + p->nTravIds = 1; +} +static inline void Gia_ManIncrementTravIdArray( Gia_Man_t * p ) +{ + while ( p->nTravIdsAlloc < Gia_ManObjNum(p) ) + { + p->nTravIdsAlloc *= 2; + p->pTravIds = ABC_REALLOC( int, p->pTravIds, p->nTravIdsAlloc ); + memset( p->pTravIds + p->nTravIdsAlloc/2, 0, sizeof(int) * p->nTravIdsAlloc/2 ); + } + p->nTravIds++; +} +static inline void Gia_ObjSetTravIdCurrentArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); p->pTravIds[Gia_ObjId(p, pObj)] = p->nTravIds; } +static inline void Gia_ObjSetTravIdPreviousArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); p->pTravIds[Gia_ObjId(p, pObj)] = p->nTravIds - 1; } +static inline int Gia_ObjIsTravIdCurrentArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds); } +static inline int Gia_ObjIsTravIdPreviousArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds - 1); } +static inline void Gia_ObjSetTravIdCurrentArrayId( Gia_Man_t * p, int Id ) { assert( Id < p->nTravIdsAlloc ); p->pTravIds[Id] = p->nTravIds; } +static inline int Gia_ObjIsTravIdCurrentArrayId( Gia_Man_t * p, int Id ) { assert( Id < p->nTravIdsAlloc ); return (p->pTravIds[Id] == p->nTravIds); } // AIG construction extern void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout ); diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c index 07e74e34..fa9030c5 100644 --- a/src/aig/gia/giaAig.c +++ b/src/aig/gia/giaAig.c @@ -361,6 +361,30 @@ void Gia_ManReprToAigRepr( Aig_Man_t * p, Gia_Man_t * pGia ) } } +/**Function************************************************************* + + Synopsis [Applied DC2 to the GIA manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManCompress2( Gia_Man_t * p ) +{ + extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose ); + Gia_Man_t * pGia; + Aig_Man_t * pNew, * pTemp; + pNew = Gia_ManToAig( p, 0 ); + pNew = Dar_ManCompress2( pTemp = pNew, 1, 0, 1, 0, 0 ); + Aig_ManStop( pTemp ); + pGia = Gia_ManFromAig( pNew ); + Aig_ManStop( pNew ); + return pGia; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaAig.h b/src/aig/gia/giaAig.h index 0e29bf06..8cef5c7e 100644 --- a/src/aig/gia/giaAig.h +++ b/src/aig/gia/giaAig.h @@ -52,6 +52,7 @@ extern Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p ); extern Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices ); extern Aig_Man_t * Gia_ManToAigSkip( Gia_Man_t * p, int nOutDelta ); extern void Gia_ManReprToAigRepr( Aig_Man_t * p, Gia_Man_t * pGia ); +extern Gia_Man_t * Gia_ManCompress2( Gia_Man_t * p ); #ifdef __cplusplus } diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index 79bfa2fb..0245b0f1 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -1,4 +1,5 @@ SRC += src/aig/gia/gia.c \ + src/aig/gia/giaAbs.c \ src/aig/gia/giaAig.c \ src/aig/gia/giaAiger.c \ src/aig/gia/giaCof.c \ @@ -11,6 +12,7 @@ SRC += src/aig/gia/gia.c \ src/aig/gia/giaEnable.c \ src/aig/gia/giaEquiv.c \ src/aig/gia/giaEra.c \ + src/aig/gia/giaEra2.c \ src/aig/gia/giaFanout.c \ src/aig/gia/giaForce.c \ src/aig/gia/giaFrames.c \ diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c index f94595b8..2e8a8096 100644 --- a/src/aig/ntl/ntlReadBlif.c +++ b/src/aig/ntl/ntlReadBlif.c @@ -272,12 +272,12 @@ static Ioa_ReadMod_t * Ioa_ReadModAlloc() Ioa_ReadMod_t * p; p = ABC_ALLOC( Ioa_ReadMod_t, 1 ); memset( p, 0, sizeof(Ioa_ReadMod_t) ); - p->vInputs = Vec_PtrAlloc( 8 ); - p->vOutputs = Vec_PtrAlloc( 8 ); - p->vLatches = Vec_PtrAlloc( 8 ); - p->vNames = Vec_PtrAlloc( 8 ); - p->vSubckts = Vec_PtrAlloc( 8 ); - p->vDelays = Vec_PtrAlloc( 8 ); + p->vInputs = Vec_PtrAlloc( 8 ); + p->vOutputs = Vec_PtrAlloc( 8 ); + p->vLatches = Vec_PtrAlloc( 8 ); + p->vNames = Vec_PtrAlloc( 8 ); + p->vSubckts = Vec_PtrAlloc( 8 ); + p->vDelays = Vec_PtrAlloc( 8 ); p->vTimeInputs = Vec_PtrAlloc( 8 ); p->vTimeOutputs = Vec_PtrAlloc( 8 ); return p; diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index b77a4292..f72a3074 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -26,6 +26,7 @@ //////////////////////////////////////////////////////////////////////// #include "aig.h" +#include "giaAbs.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// @@ -90,7 +91,7 @@ static inline Aig_Obj_t * Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj ) { //////////////////////////////////////////////////////////////////////// /*=== sswAbs.c ==========================================================*/ -extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fUseBdds, int fUseDprove, int fUseStart, int fVerbose ); +extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, Gia_ParAbs_t * pPars ); /*=== saigBmc.c ==========================================================*/ extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit ); extern void Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite ); diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c index 844d6f24..2fac60f5 100644 --- a/src/aig/saig/saigAbs.c +++ b/src/aig/saig/saigAbs.c @@ -684,6 +684,30 @@ Ssw_Cex_t * Saig_ManCexShrink( Aig_Man_t * p, Aig_Man_t * pAbs, Ssw_Cex_t * pCex return pCex; } +/**Function************************************************************* + + Synopsis [Find the first PI corresponding to the flop.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManFirstFlopPi( Aig_Man_t * p, Aig_Man_t * pAbs ) +{ + Aig_Obj_t * pObj; + int i; + assert( pAbs->vCiNumsOrig != NULL ); + Aig_ManForEachPi( p, pObj, i ) + { + if ( Vec_IntEntry(pAbs->vCiNumsOrig, i) >= Saig_ManPiNum(p) ) + return i; + } + return -1; +} + /**Function************************************************************* Synopsis [Performs proof-based abstraction using BMC of the given depth.] @@ -701,9 +725,9 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF extern Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, void * pCex, int fVerbose ); extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent ); - Vec_Int_t * vFlopsNew, * vPiToReg; - Aig_Obj_t * pObj; - int i, Entry, iFlop; + Vec_Int_t * vFlopsNew;//, * vPiToReg; +// Aig_Obj_t * pObj; + int i, Entry;//, iFlop; if ( fUseDprove && Aig_ManRegNum(pAbs) > 0 ) { Fra_Sec_t SecPar, * pSecPar = &SecPar; @@ -727,8 +751,8 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF return NULL; if ( pnUseStart ) *pnUseStart = ((Fra_Cex_t *)pAbs->pSeqModel)->iFrame; -// Saig_ManExtendCounterExampleTest( p->pAig, 0, p->pAig->pSeqModel ); - vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManPiNum(p), pAbs->pSeqModel, fVerbose ); +// vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManPiNum(p), pAbs->pSeqModel, fVerbose ); + vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManFirstFlopPi(p, pAbs), pAbs->pSeqModel, fVerbose ); if ( Vec_IntSize(vFlopsNew) == 0 ) { printf( "Discovered a true counter-example!\n" ); @@ -739,7 +763,7 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF if ( fVerbose ) printf( "Adding %d registers to the abstraction.\n", Vec_IntSize(vFlopsNew) ); // vFlopsNew contains PI number that should be kept in pAbs - +/* // for each additional PI, collect the number of a register it stands for Vec_IntForEachEntry( vFlops, Entry, i ) { @@ -770,6 +794,20 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF Vec_IntFree( vPiToReg ); Vec_IntFree( vFlopsNew ); + Vec_IntSort( vFlops, 0 ); + Vec_IntForEachEntryStart( vFlops, Entry, i, 1 ) + assert( Vec_IntEntry(vFlops, i-1) != Entry ); +*/ + // add to the abstraction + Vec_IntForEachEntry( vFlopsNew, Entry, i ) + { + Entry = Vec_IntEntry(pAbs->vCiNumsOrig, Entry); + assert( Entry >= Saig_ManPiNum(p) ); + assert( Entry < Aig_ManPiNum(p) ); + Vec_IntPush( vFlops, Entry-Saig_ManPiNum(p) ); + } + Vec_IntFree( vFlopsNew ); + Vec_IntSort( vFlops, 0 ); Vec_IntForEachEntryStart( vFlops, Entry, i, 1 ) assert( Vec_IntEntry(vFlops, i-1) != Entry ); @@ -788,7 +826,7 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fUseBdds, int fUseDprove, int fUseStart, int fVerbose ) +Vec_Int_t * Saig_ManProofAbstraction_int( Aig_Man_t * p, Gia_ParAbs_t * pPars ) { Aig_Man_t * pResult, * pTemp; Cnf_Dat_t * pCnf; @@ -800,10 +838,10 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, assert( Aig_ManRegNum(p) > 0 ); Aig_ManSetPioNumbers( p ); - if ( fSkipProof ) + if ( pPars->fSkipProof ) { // assert( 0 ); - if ( fVerbose ) + if ( pPars->fVerbose ) printf( "Performing counter-example-based refinement.\n" ); // vFlops = Vec_IntStartNatural( 100 ); // Vec_IntPush( vFlops, 0 ); @@ -811,12 +849,12 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, } else { - if ( fVerbose ) - printf( "Performing proof-based abstraction with %d frames and %d max conflicts.\n", nFrames, nConfMax ); - if ( fDynamic ) + if ( pPars->fVerbose ) + printf( "Performing proof-based abstraction with %d frames and %d max conflicts.\n", pPars->nFramesMax, pPars->nConfMax ); + if ( pPars->fDynamic ) { // create CNF for the frames - vFrames = Saig_AbsCreateFrames( p, nFrames, fVerbose ); + vFrames = Saig_AbsCreateFrames( p, pPars->nFramesMax, pPars->fVerbose ); // create dynamic solver pSat = Saig_AbsCreateSolverDyn( p, vFrames ); } @@ -825,15 +863,15 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, // create CNF for the AIG pCnf = Cnf_DeriveSimple( p, Aig_ManPoNum(p) ); // create SAT solver for the unrolled AIG - pSat = Saig_AbsCreateSolver( pCnf, nFrames ); + pSat = Saig_AbsCreateSolver( pCnf, pPars->nFramesMax ); } - if ( fVerbose ) + if ( pPars->fVerbose ) { printf( "SAT solver: Vars = %7d. Clauses = %7d. ", pSat->size, pSat->stats.clauses ); ABC_PRT( "Time", clock() - clk2 ); } // compute UNSAT core - vCore = Saig_AbsSolverUnsatCore( pSat, nConfMax, fVerbose ); + vCore = Saig_AbsSolverUnsatCore( pSat, pPars->nConfMax, pPars->fVerbose ); sat_solver_delete( pSat ); if ( vCore == NULL ) { @@ -841,18 +879,18 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, return NULL; } // collect registers - if ( fDynamic ) + if ( pPars->fDynamic ) { vFlops = Saig_AbsCollectRegistersDyn( p, vFrames, vCore ); Saig_AbsFreeCnfs( vFrames ); } else { - vFlops = Saig_AbsCollectRegisters( pCnf, nFrames, vCore ); + vFlops = Saig_AbsCollectRegisters( pCnf, pPars->nFramesMax, vCore ); Cnf_DataFree( pCnf ); } Vec_IntFree( vCore ); - if ( fVerbose ) + if ( pPars->fVerbose ) { printf( "The number of relevant registers is %d (out of %d). ", Vec_IntSize(vFlops), Aig_ManRegNum(p) ); ABC_PRT( "Time", clock() - clk ); @@ -872,10 +910,10 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, // create the resulting AIG pResult = Saig_ManAbstraction( p, vFlops ); - if ( fExtend ) + if ( pPars->fExtend ) { int nUseStart = 0; - if ( !fVerbose ) + if ( !pPars->fVerbose ) { printf( "Init : " ); Aig_ManPrintStats( pResult ); @@ -883,13 +921,13 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, printf( "Refining abstraction...\n" ); for ( Iter = 0; ; Iter++ ) { - pTemp = Saig_ManProofRefine( p, pResult, vFlops, nFramesBmc, nConfMaxBmc, fUseBdds, fUseDprove, fUseStart?&nUseStart:NULL, fVerbose ); + pTemp = Saig_ManProofRefine( p, pResult, vFlops, pPars->nFramesBmc, pPars->nConfMaxBmc, pPars->fUseBdds, pPars->fUseDprove, pPars->fUseStart?&nUseStart:NULL, pPars->fVerbose ); if ( pTemp == NULL ) break; Aig_ManStop( pResult ); pResult = pTemp; printf( "ITER %4d : ", Iter ); - if ( !fVerbose ) + if ( !pPars->fVerbose ) Aig_ManPrintStats( pResult ); // else // printf( " -----------------------------------------------------\n" ); @@ -897,26 +935,52 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, Ioa_WriteAiger( pResult, "gabs.aig", 0, 0 ); // printf( "Intermediate abstracted model was written into file \"%s\".\n", "gabs.aig" ); // check if the ratio is reached - if ( 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pTemp))/Aig_ManRegNum(p) < 1.0*nRatio ) + if ( 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pTemp))/Aig_ManRegNum(p) < 1.0*pPars->nRatio ) { - printf( "Refinements is stopped because flop reduction is less than %d%%\n", nRatio ); + printf( "Refinements is stopped because flop reduction is less than %d%%\n", pPars->nRatio ); Aig_ManStop( pResult ); pResult = NULL; break; } } } - Vec_IntFree( vFlops ); // write the final result if ( pResult ) + Aig_ManStop( pResult ); + else { - Ioa_WriteAiger( pResult, "gabs.aig", 0, 0 ); - printf( "Final abstracted model was written into file \"%s\".\n", "gabs.aig" ); + Vec_IntFree( vFlops ); + vFlops = NULL; } - return pResult; + return vFlops; } +/**Function************************************************************* + Synopsis [Performs proof-based abstraction using BMC of the given depth.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, Gia_ParAbs_t * pPars ) +{ + Vec_Int_t * vFlops; + Aig_Man_t * pAbs = NULL; + vFlops = Saig_ManProofAbstraction_int( p, pPars ); + // write the final result + if ( vFlops ) + { + pAbs = Saig_ManAbstraction( p, vFlops ); + Ioa_WriteAiger( pAbs, "gabs.aig", 0, 0 ); + printf( "Final abstracted model was written into file \"%s\".\n", "gabs.aig" ); + Vec_IntFree( vFlops ); + } + return pAbs; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c index a37be3ad..ac1cbe5b 100644 --- a/src/aig/saig/saigBmc.c +++ b/src/aig/saig/saigBmc.c @@ -45,6 +45,7 @@ struct Saig_Bmc_t_ // node mapping int nObjs; // the largest number of an AIG object Vec_Ptr_t * vAig2Frm; // mapping of AIG nodees into Frames nodes +// Vec_Str_t * vAig2Frm2; // mapping of AIG nodees into Frames nodes // SAT solver sat_solver * pSat; // SAT solver int nSatVars; // the number of used SAT variables @@ -71,6 +72,170 @@ static inline Aig_Obj_t * Saig_BmcObjChild1( Saig_Bmc_t * p, Aig_Obj_t * pObj, i /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +#define ABS_ZER 1 +#define ABS_ONE 2 +#define ABS_UND 3 + +static inline int Abs_ManSimInfoNot( int Value ) +{ + if ( Value == ABS_ZER ) + return ABS_ONE; + if ( Value == ABS_ONE ) + return ABS_ZER; + return ABS_UND; +} + +static inline int Abs_ManSimInfoAnd( int Value0, int Value1 ) +{ + if ( Value0 == ABS_ZER || Value1 == ABS_ZER ) + return ABS_ZER; + if ( Value0 == ABS_ONE && Value1 == ABS_ONE ) + return ABS_ONE; + return ABS_UND; +} + +static inline int Abs_ManSimInfoGet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame ) +{ + unsigned * pInfo = Vec_PtrEntry( vSimInfo, iFrame ); + return 3 & (pInfo[Aig_ObjId(pObj) >> 4] >> ((Aig_ObjId(pObj) & 15) << 1)); +} + +static inline void Abs_ManSimInfoSet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame, int Value ) +{ + unsigned * pInfo = Vec_PtrEntry( vSimInfo, iFrame ); + assert( Value >= ABS_ZER && Value <= ABS_UND ); + Value ^= Abs_ManSimInfoGet( vSimInfo, pObj, iFrame ); + pInfo[Aig_ObjId(pObj) >> 4] ^= (Value << ((Aig_ObjId(pObj) & 15) << 1)); +} + +/**Function************************************************************* + + Synopsis [Performs ternary simulation for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abs_ManExtendOneEval_rec( Vec_Ptr_t * vSimInfo, Aig_Man_t * p, Aig_Obj_t * pObj, int iFrame ) +{ + int Value0, Value1, Value; + Value = Abs_ManSimInfoGet( vSimInfo, pObj, iFrame ); + if ( Value ) + return Value; + if ( Aig_ObjIsPi(pObj) ) + { + assert( Saig_ObjIsLo(p, pObj) ); + Value = Abs_ManExtendOneEval_rec( vSimInfo, p, Saig_ObjLoToLi(p, pObj), iFrame-1 ); + Abs_ManSimInfoSet( vSimInfo, pObj, iFrame, Value ); + return Value; + } + Value0 = Abs_ManExtendOneEval_rec( vSimInfo, p, Aig_ObjFanin0(pObj), iFrame ); + if ( Aig_ObjFaninC0(pObj) ) + Value0 = Abs_ManSimInfoNot( Value0 ); + if ( Aig_ObjIsPo(pObj) ) + { + Abs_ManSimInfoSet( vSimInfo, pObj, iFrame, Value0 ); + return Value0; + } + assert( Aig_ObjIsNode(pObj) ); + if ( Value0 == ABS_ZER ) + Value = ABS_ZER; + else + { + Value1 = Abs_ManExtendOneEval_rec( vSimInfo, p, Aig_ObjFanin1(pObj), iFrame ); + if ( Aig_ObjFaninC1(pObj) ) + Value1 = Abs_ManSimInfoNot( Value1 ); + Value = Abs_ManSimInfoAnd( Value0, Value1 ); + } + Abs_ManSimInfoSet( vSimInfo, pObj, iFrame, Value ); + assert( Value ); + return Value; +} + +/**Function************************************************************* + + Synopsis [Performs ternary simulation for one design.] + + Description [The returned array contains the result of ternary + simulation for all the frames where the output could be proved 0.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abs_ManTernarySimulate( Aig_Man_t * p, int nFramesMax, int fVerbose ) +{ + Vec_Ptr_t * vSimInfo; + Aig_Obj_t * pObj; + int i, f, nFramesLimit, nFrameWords; + int clk = clock(); + assert( Aig_ManRegNum(p) > 0 ); + // the maximum number of frames will be determined to use at most 200Mb of RAM + nFramesLimit = 1 + (200000000 * 4)/Aig_ManObjNum(p); + nFramesLimit = ABC_MIN( nFramesLimit, nFramesMax ); + nFrameWords = Aig_BitWordNum( 2 * Aig_ManObjNum(p) ); + // allocate simulation info + vSimInfo = Vec_PtrAlloc( nFramesLimit ); + for ( f = 0; f < nFramesLimit; f++ ) + { + Vec_PtrPush( vSimInfo, ABC_CALLOC(unsigned, nFrameWords) ); + if ( f == 0 ) + { + Saig_ManForEachLo( p, pObj, i ) + Abs_ManSimInfoSet( vSimInfo, pObj, 0, ABS_ZER ); + } + Abs_ManSimInfoSet( vSimInfo, Aig_ManConst1(p), f, ABS_ONE ); + Saig_ManForEachPi( p, pObj, i ) + Abs_ManSimInfoSet( vSimInfo, pObj, f, ABS_UND ); + Saig_ManForEachPo( p, pObj, i ) + Abs_ManExtendOneEval_rec( vSimInfo, p, pObj, f ); + // check if simulation has derived at least one fail or unknown + Saig_ManForEachPo( p, pObj, i ) + if ( Abs_ManSimInfoGet(vSimInfo, pObj, f) != ABS_ZER ) + { + if ( fVerbose ) + { + printf( "Ternary sim found non-zero output in frame %d. Used %5.2f Mb. ", + f, 0.25 * (f+1) * Aig_ManObjNum(p) / (1<<20) ); + ABC_PRT( "Time", clock() - clk ); + } + return vSimInfo; + } + } + if ( fVerbose ) + { + printf( "Ternary sim proved all outputs in the first %d frames. Used %5.2f Mb. ", + nFramesLimit, 0.25 * nFramesLimit * Aig_ManObjNum(p) / (1<<20) ); + ABC_PRT( "Time", clock() - clk ); + } + return vSimInfo; +} + +/**Function************************************************************* + + Synopsis [Free the array of simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abs_ManFreeAray( Vec_Ptr_t * p ) +{ + void * pTemp; + int i; + Vec_PtrForEachEntry( p, pTemp, i ) + ABC_FREE( pTemp ); + Vec_PtrFree( p ); +} + + /**Function************************************************************* Synopsis [Create manager.] @@ -135,8 +300,32 @@ Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, ***********************************************************************/ void Saig_BmcManStop( Saig_Bmc_t * p ) { +// Aig_Obj_t * pObj; +// int i, f, Counter = 0; +// int i, Counter = 0; +// for ( i = 0; i < p->vAig2Frm2->nSize; i++ ) +// Counter += (p->vAig2Frm2->pArray[i] != 0); +// for ( i = 0; i < p->vAig2Frm->nSize; i++ ) +// Counter += (p->vAig2Frm->pArray[i] != NULL); +// printf( "Objs = %d. Nodes = %d. Frames = %d. Used = %d. Non-empty = %d.\n", +// p->nObjs, Aig_ManNodeNum(p->pAig), p->iFrameLast, p->vAig2Frm->nSize, Counter ); + +/* + Aig_ManForEachObj( p->pAig, pObj, i ) + { + int Last = -1; + for ( f = 0; f <= p->iFrameLast; f++ ) + if ( Saig_BmcObjFrame( p, pObj, f ) ) + Last = f; + if ( i % 50 == 0 ) + printf( "%d ", Last ); + } + printf( "\n" ); +*/ + Aig_ManStop( p->pFrm ); Vec_PtrFree( p->vAig2Frm ); +// Vec_StrFree( p->vAig2Frm2 ); Vec_IntFree( p->vObj2Var ); sat_solver_delete( p->pSat ); Vec_PtrFree( p->vTargets ); @@ -196,44 +385,6 @@ Aig_Obj_t * Saig_BmcIntervalExplore_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i return pRes; } -/**Function************************************************************* - - Synopsis [Performs the actual construction of the output.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Obj_t * Saig_BmcIntervalConstruct_rec_OLD( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i ) -{ - Aig_Obj_t * pRes; - pRes = Saig_BmcObjFrame( p, pObj, i ); - assert( pRes != NULL ); - if ( pRes != AIG_VISITED ) - return pRes; - if ( Saig_ObjIsPi( p->pAig, pObj ) ) - pRes = Aig_ObjCreatePi(p->pFrm); - else if ( Saig_ObjIsLo( p->pAig, pObj ) ) - pRes = Saig_BmcIntervalConstruct_rec_OLD( p, Saig_ObjLoToLi(p->pAig, pObj), i-1 ); - else if ( Aig_ObjIsPo( pObj ) ) - { - Saig_BmcIntervalConstruct_rec_OLD( p, Aig_ObjFanin0(pObj), i ); - pRes = Saig_BmcObjChild0( p, pObj, i ); - } - else - { - Saig_BmcIntervalConstruct_rec_OLD( p, Aig_ObjFanin0(pObj), i ); - Saig_BmcIntervalConstruct_rec_OLD( p, Aig_ObjFanin1(pObj), i ); - pRes = Aig_And( p->pFrm, Saig_BmcObjChild0(p, pObj, i), Saig_BmcObjChild1(p, pObj, i) ); - } - assert( pRes != AIG_VISITED ); - Saig_BmcObjSetFrame( p, pObj, i, pRes ); - return pRes; -} - /**Function************************************************************* Synopsis [Performs the actual construction of the output.] @@ -263,8 +414,13 @@ Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int else { Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin0(pObj), i, vVisited ); - Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin1(pObj), i, vVisited ); - pRes = Aig_And( p->pFrm, Saig_BmcObjChild0(p, pObj, i), Saig_BmcObjChild1(p, pObj, i) ); + if ( Saig_BmcObjChild0(p, pObj, i) == Aig_ManConst0(p->pFrm) ) + pRes = Aig_ManConst0(p->pFrm); + else + { + Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin1(pObj), i, vVisited ); + pRes = Aig_And( p->pFrm, Saig_BmcObjChild0(p, pObj, i), Saig_BmcObjChild1(p, pObj, i) ); + } } assert( pRes != NULL ); Saig_BmcObjSetFrame( p, pObj, i, pRes ); @@ -288,7 +444,7 @@ void Saig_BmcInterval( Saig_Bmc_t * p ) { Aig_Obj_t * pTarget; Aig_Obj_t * pObj, * pRes; - int i, iFrame; + int i, iFrame, Counter; int nNodes = Aig_ManObjNum( p->pFrm ); Vec_PtrClear( p->vTargets ); p->iFramePrev = p->iFrameLast; @@ -309,13 +465,18 @@ void Saig_BmcInterval( Saig_Bmc_t * p ) Aig_ObjCreatePo( p->pFrm, pTarget ); Aig_ManCleanup( p->pFrm ); // check if the node is gone + Counter = 0; Vec_PtrForEachEntry( p->vVisited, pObj, i ) { iFrame = (int)(ABC_PTRINT_T)Vec_PtrEntry( p->vVisited, 1+i++ ); pRes = Saig_BmcObjFrame( p, pObj, iFrame ); if ( Aig_ObjIsNone( Aig_Regular(pRes) ) ) + { Saig_BmcObjSetFrame( p, pObj, iFrame, NULL ); + Counter++; + } } +// printf( "%d ", Counter ); } } } @@ -564,7 +725,7 @@ void Saig_BmcAddTargetsAsPos( Saig_Bmc_t * p ) Aig_ManPrintStats( p->pFrm ); Aig_ManCleanup( p->pFrm ); Aig_ManPrintStats( p->pFrm ); -} +} /**Function************************************************************* @@ -584,6 +745,11 @@ void Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMa Cnf_Dat_t * pCnf; int nOutsSolved = 0; int Iter, RetValue, clk = clock(), clk2; +/* + Vec_Ptr_t * vSimInfo; + vSimInfo = Abs_ManTernarySimulate( pAig, nFramesMax, fVerbose ); + Abs_ManFreeAray( vSimInfo ); +*/ p = Saig_BmcManStart( pAig, nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll, fVerbose ); if ( fVerbose ) { @@ -593,6 +759,7 @@ void Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMa printf( "Params: FramesMax = %d. NodesDelta = %d. ConfMaxOne = %d. ConfMaxAll = %d.\n", nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll ); } + for ( Iter = 0; ; Iter++ ) { clk2 = clock(); diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c index e6534a1f..e261fca1 100644 --- a/src/aig/saig/saigDup.c +++ b/src/aig/saig/saigDup.c @@ -70,7 +70,7 @@ Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * pAig ) /**Function************************************************************* - Synopsis [Numbers of flops included in the abstraction.] + Synopsis [Duplicates the AIG manager recursively.] Description [] @@ -79,55 +79,130 @@ Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * pAig ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops ) +Aig_Obj_t * Saig_ManAbstractionDfs_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj ) { - Aig_Man_t * pAigNew;//, * pTemp; + if ( pObj->pData ) + return pObj->pData; + Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) ); + Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin1(pObj) ); + return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Trims the model by removing PIs without fanout.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManTrimPis( Aig_Man_t * p ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj; + int i, fAllPisHaveNoRefs; + // check the refs of PIs + fAllPisHaveNoRefs = 1; + Saig_ManForEachPi( p, pObj, i ) + if ( pObj->nRefs ) + fAllPisHaveNoRefs = 0; + // start the new manager + pNew = Aig_ManStart( Aig_ManObjNum(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); + // start mapping of the CI numbers + pNew->vCiNumsOrig = Vec_IntAlloc( Aig_ManPiNum(p) ); + // map const and primary inputs + Aig_ManCleanData( p ); + Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); + Aig_ManForEachPi( p, pObj, i ) + if ( fAllPisHaveNoRefs || pObj->nRefs || Saig_ObjIsLo(p, pObj) ) + { + pObj->pData = Aig_ObjCreatePi( pNew ); + Vec_IntPush( pNew->vCiNumsOrig, Vec_IntEntry(p->vCiNumsOrig, i) ); + } + Aig_ManForEachNode( p, pObj, i ) + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + Aig_ManForEachPo( p, pObj, i ) + pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Performs abstraction of the AIG to preserve the included flops.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManAbstraction( Aig_Man_t * p, Vec_Int_t * vFlops ) +{ + Aig_Man_t * pNew, * pTemp; Aig_Obj_t * pObj, * pObjLi, * pObjLo; int i, Entry; + Aig_ManCleanData( p ); // start the new manager - pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) ); - pAigNew->pName = Aig_UtilStrsav( pAig->pName ); + pNew = Aig_ManStart( Aig_ManNodeNum(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); // map the constant node - Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew ); + Aig_ManConst1(p)->pData = Aig_ManConst1( pNew ); // label included flops Vec_IntForEachEntry( vFlops, Entry, i ) { - pObjLi = Saig_ManLi( pAig, Entry ); + pObjLi = Saig_ManLi( p, Entry ); assert( pObjLi->fMarkA == 0 ); pObjLi->fMarkA = 1; - pObjLo = Saig_ManLo( pAig, Entry ); + pObjLo = Saig_ManLo( p, Entry ); assert( pObjLo->fMarkA == 0 ); pObjLo->fMarkA = 1; } // create variables for PIs - Aig_ManForEachPi( pAig, pObj, i ) + assert( p->vCiNumsOrig == NULL ); + pNew->vCiNumsOrig = Vec_IntAlloc( Aig_ManPiNum(p) ); + Aig_ManForEachPi( p, pObj, i ) if ( !pObj->fMarkA ) - pObj->pData = Aig_ObjCreatePi( pAigNew ); + { + pObj->pData = Aig_ObjCreatePi( pNew ); + Vec_IntPush( pNew->vCiNumsOrig, i ); + } // create variables for LOs - Aig_ManForEachPi( pAig, pObj, i ) + Aig_ManForEachPi( p, pObj, i ) if ( pObj->fMarkA ) { pObj->fMarkA = 0; - pObj->pData = Aig_ObjCreatePi( pAigNew ); + pObj->pData = Aig_ObjCreatePi( pNew ); + Vec_IntPush( pNew->vCiNumsOrig, i ); } // add internal nodes - Aig_ManForEachNode( pAig, pObj, i ) - pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); +// Aig_ManForEachNode( p, pObj, i ) +// pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); // create POs - Saig_ManForEachPo( pAig, pObj, i ) - Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) ); + Saig_ManForEachPo( p, pObj, i ) + { + Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) ); + Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + } // create LIs - Aig_ManForEachPo( pAig, pObj, i ) + Aig_ManForEachPo( p, pObj, i ) if ( pObj->fMarkA ) { pObj->fMarkA = 0; - Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) ); + Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) ); + Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); } - Aig_ManSetRegNum( pAigNew, Vec_IntSize(vFlops) ); - Aig_ManSeqCleanup( pAigNew ); -// pAigNew = Aig_ManDupSimpleDfs( pTemp = pAigNew ); -// Aig_ManStop( pTemp ); - return pAigNew; + Aig_ManSetRegNum( pNew, Vec_IntSize(vFlops) ); + Aig_ManSeqCleanup( pNew ); + // remove PIs without fanout + pNew = Saig_ManTrimPis( pTemp = pNew ); + Aig_ManStop( pTemp ); + return pNew; } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/saig/saigSimExt.c b/src/aig/saig/saigSimExt.c index 97b91b1d..22d5d6b8 100644 --- a/src/aig/saig/saigSimExt.c +++ b/src/aig/saig/saigSimExt.c @@ -247,7 +247,7 @@ void Saig_ManExtendUndo( Aig_Man_t * p, Vec_Ptr_t * vSimInfo, Vec_Int_t * vUndo SeeAlso [] ***********************************************************************/ -Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstPi, Ssw_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose ) +Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstFlopPi, Ssw_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose ) { Vec_Int_t * vRes, * vResInv, * vUndo, * vVis, * vVis2; int i, f, Value; @@ -262,7 +262,7 @@ Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstPi, Ssw_Cex_t vVis = Vec_IntAlloc( 1000 ); vVis2 = Vec_IntAlloc( 1000 ); vUndo = Vec_IntAlloc( 1000 ); - for ( i = iFirstPi; i < Saig_ManPiNum(p); i++ ) + for ( i = iFirstFlopPi; i < Saig_ManPiNum(p); i++ ) { Vec_IntClear( vUndo ); for ( f = pCex->iFrame; f >= 0; f-- ) @@ -297,7 +297,7 @@ Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstPi, Ssw_Cex_t SeeAlso [] ***********************************************************************/ -Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, Ssw_Cex_t * pCex, int fVerbose ) +Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstFlopPi, Ssw_Cex_t * pCex, int fVerbose ) { Vec_Int_t * vRes; Vec_Ptr_t * vSimInfo; @@ -305,10 +305,10 @@ Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, Ssw_C Aig_ManFanoutStart( p ); vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p), Aig_BitWordNum(2*(pCex->iFrame+1)) ); clk = clock(); - vRes = Saig_ManExtendCounterExample( p, iFirstPi, pCex, vSimInfo, fVerbose ); + vRes = Saig_ManExtendCounterExample( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); if ( fVerbose ) { - printf( "Total new PIs = %3d. Non-removable PIs = %3d. ", Saig_ManPiNum(p)-iFirstPi, Vec_IntSize(vRes) ); + printf( "Total new PIs = %3d. Non-removable PIs = %3d. ", Saig_ManPiNum(p)-iFirstFlopPi, Vec_IntSize(vRes) ); ABC_PRT( "Time", clock() - clk ); } Vec_PtrFree( vSimInfo ); diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c index 0e99b1e8..cf5270dd 100644 --- a/src/aig/ssw/sswSim.c +++ b/src/aig/ssw/sswSim.c @@ -1285,7 +1285,7 @@ int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p ) Aig_Obj_t * pObj; int RetValue, i, k, iBit; // assert( Aig_ManRegNum(pAig) > 0 ); - assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) ); +// assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) ); // start a new sequential simulator pSml = Ssw_SmlStart( pAig, 0, p->iFrame+1, 1 ); // assign simulation info for the registers diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 789d2714..f7caad5d 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -40,6 +40,7 @@ #include "cgt.h" #include "amap.h" #include "cec.h" +#include "giaAbs.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -322,6 +323,8 @@ extern int Abc_CommandAbcLivenessToSafetySim ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbcTestNew ( Abc_Frame_t * pAbc, int argc, char ** argv ); +extern Aig_Man_t * Ntl_ManExtract( void * p ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -18807,40 +18810,18 @@ usage: ***********************************************************************/ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) { + Gia_ParAbs_t Pars, * pPars = &Pars; FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; - int nFramesMax; - int nConfMax; - int fDynamic; - int fExtend; - int fSkipProof; - int nFramesBmc; - int nConfMaxBmc; - int nRatio; - int fUseBdds; - int fUseDprove; - int fUseStart; - int fVerbose; int c; - extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fUseBdds, int fUseDprove, int fUseStart, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, Gia_ParAbs_t * pPars ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - nFramesMax = 10; - nConfMax = 10000; - fDynamic = 1; - fExtend = 0; - fSkipProof = 0; - nFramesBmc = 2000; - nConfMaxBmc = 5000; - nRatio = 10; - fUseBdds = 0; - fUseDprove = 0; - fUseStart = 1; - fVerbose = 0; + Gia_ManAbsSetDefaultParams( pPars ); Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "FCGDRdesrpfvh" ) ) != EOF ) { @@ -18852,9 +18833,9 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); goto usage; } - nFramesMax = atoi(argv[globalUtilOptind]); + pPars->nFramesMax = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nFramesMax < 0 ) + if ( pPars->nFramesMax < 0 ) goto usage; break; case 'C': @@ -18863,9 +18844,9 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); goto usage; } - nConfMax = atoi(argv[globalUtilOptind]); + pPars->nConfMax = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nConfMax < 0 ) + if ( pPars->nConfMax < 0 ) goto usage; break; case 'G': @@ -18874,9 +18855,9 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Command line switch \"-G\" should be followed by an integer.\n" ); goto usage; } - nFramesBmc = atoi(argv[globalUtilOptind]); + pPars->nFramesBmc = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nFramesBmc < 0 ) + if ( pPars->nFramesBmc < 0 ) goto usage; break; case 'D': @@ -18885,9 +18866,9 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" ); goto usage; } - nConfMaxBmc = atoi(argv[globalUtilOptind]); + pPars->nConfMaxBmc = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nConfMaxBmc < 0 ) + if ( pPars->nConfMaxBmc < 0 ) goto usage; break; case 'R': @@ -18896,31 +18877,31 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Command line switch \"-R\" should be followed by an integer.\n" ); goto usage; } - nRatio = atoi(argv[globalUtilOptind]); + pPars->nRatio = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nRatio < 0 ) + if ( pPars->nRatio < 0 ) goto usage; break; case 'd': - fDynamic ^= 1; + pPars->fDynamic ^= 1; break; case 'e': - fExtend ^= 1; + pPars->fExtend ^= 1; break; case 's': - fSkipProof ^= 1; + pPars->fSkipProof ^= 1; break; case 'r': - fUseBdds ^= 1; + pPars->fUseBdds ^= 1; break; case 'p': - fUseDprove ^= 1; + pPars->fUseDprove ^= 1; break; case 'f': - fUseStart ^= 1; + pPars->fUseStart ^= 1; break; case 'v': - fVerbose ^= 1; + pPars->fVerbose ^= 1; break; case 'h': goto usage; @@ -18943,18 +18924,18 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( stdout, "Currently only works for structurally hashed circuits.\n" ); return 0; } - if ( !(0 <= nRatio && nRatio <= 100) ) + if ( !(0 <= pPars->nRatio && pPars->nRatio <= 100) ) { fprintf( stdout, "Wrong value of parameter \"-R \".\n" ); return 0; } // modify the current network - pNtkRes = Abc_NtkDarPBAbstraction( pNtk, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, nRatio, fUseBdds, fUseDprove, fUseStart, fVerbose ); + pNtkRes = Abc_NtkDarPBAbstraction( pNtk, pPars ); if ( pNtkRes == NULL ) { if ( pNtk->pSeqModel == NULL ) - printf( "Proof-based abstraction has failed.\n" ); + printf( "Abstraction has failed.\n" ); return 0; } // replace the current network @@ -18964,18 +18945,18 @@ usage: fprintf( pErr, "usage: abs [-FCGDR num] [-desrpfvh]\n" ); fprintf( pErr, "\t proof-based abstraction (PBA) using UNSAT core of BMC\n" ); fprintf( pErr, "\t followed by counter-example-based abstraction\n" ); - fprintf( pErr, "\t-F num : the max number of timeframes for PBA [default = %d]\n", nFramesMax ); - fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver for PBA [default = %d]\n", nConfMax ); - fprintf( pErr, "\t-G num : the max number of timeframes for BMC [default = %d]\n", nFramesBmc ); - fprintf( pErr, "\t-D num : the max number of conflicts by SAT solver for BMC [default = %d]\n", nConfMaxBmc ); - fprintf( pErr, "\t-R num : the %% of abstracted flops when refinement stops (0<=num<=100) [default = %d]\n", nRatio ); - fprintf( pErr, "\t-d : toggle dynamic unrolling of timeframes [default = %s]\n", fDynamic? "yes": "no" ); - fprintf( pErr, "\t-e : toggle extending abstraction using COI of flops [default = %s]\n", fExtend? "yes": "no" ); - fprintf( pErr, "\t-s : toggle skipping proof-based abstraction [default = %s]\n", fSkipProof? "yes": "no" ); - fprintf( pErr, "\t-r : toggle using BDD-based reachability for filtering [default = %s]\n", fUseBdds? "yes": "no" ); - fprintf( pErr, "\t-p : toggle using \"dprove\" for filtering [default = %s]\n", fUseDprove? "yes": "no" ); - fprintf( pErr, "\t-f : toggle starting BMC from a later frame [default = %s]\n", fUseStart? "yes": "no" ); - fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-F num : the max number of timeframes for PBA [default = %d]\n", pPars->nFramesMax ); + fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver for PBA [default = %d]\n", pPars->nConfMax ); + fprintf( pErr, "\t-G num : the max number of timeframes for BMC [default = %d]\n", pPars->nFramesBmc ); + fprintf( pErr, "\t-D num : the max number of conflicts by SAT solver for BMC [default = %d]\n", pPars->nConfMaxBmc ); + fprintf( pErr, "\t-R num : the %% of abstracted flops when refinement stops (0<=num<=100) [default = %d]\n", pPars->nRatio ); + fprintf( pErr, "\t-d : toggle dynamic unrolling of timeframes [default = %s]\n", pPars->fDynamic? "yes": "no" ); + fprintf( pErr, "\t-e : toggle extending abstraction using COI of flops [default = %s]\n", pPars->fExtend? "yes": "no" ); + fprintf( pErr, "\t-s : toggle skipping proof-based abstraction [default = %s]\n", pPars->fSkipProof? "yes": "no" ); + fprintf( pErr, "\t-r : toggle using BDD-based reachability for filtering [default = %s]\n", pPars->fUseBdds? "yes": "no" ); + fprintf( pErr, "\t-p : toggle using \"dprove\" for filtering [default = %s]\n", pPars->fUseDprove? "yes": "no" ); + fprintf( pErr, "\t-f : toggle starting BMC from a later frame [default = %s]\n", pPars->fUseStart? "yes": "no" ); + fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -19129,7 +19110,6 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv ) int fAlter; extern void * Ioa_ReadBlif( char * pFileName, int fCheck ); extern void Ioa_WriteBlif( void * p, char * pFileName ); - extern Aig_Man_t * Ntl_ManExtract( void * p ); extern void * Ntl_ManExtractNwk( void * p, Aig_Man_t * pAig, Tim_Man_t * pManTime ); extern void Ntl_ManPrintStats( void * p ); @@ -21083,7 +21063,6 @@ int Abc_CommandAbc8Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) int nConfLimit; int nLevelMax; int fUseCSat; - extern Aig_Man_t * Ntl_ManExtract( void * p ); extern void * Ntl_ManFraig( void * p, int nPartSize, int nConfLimit, int nLevelMax, int fUseCSat, int fVerbose ); extern void Ntl_ManFree( void * p ); @@ -21204,7 +21183,6 @@ int Abc_CommandAbc8Scl( Abc_Frame_t * pAbc, int argc, char ** argv ) int fLatchConst; int fLatchEqual; int fVerbose; - extern Aig_Man_t * Ntl_ManExtract( void * p ); extern void * Ntl_ManScl( void * p, int fLatchConst, int fLatchEqual, int fVerbose ); extern int Ntl_ManIsComb( void * p ); @@ -21300,7 +21278,6 @@ int Abc_CommandAbc8Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv ) int nFramesP; int nConfMax; int fVerbose; - extern Aig_Man_t * Ntl_ManExtract( void * p ); extern void * Ntl_ManLcorr( void * p, int nConfMax, int fScorrGia, int fUseCSat, int fVerbose ); extern int Ntl_ManIsComb( void * p ); @@ -21417,7 +21394,6 @@ int Abc_CommandAbc8Ssw( Abc_Frame_t * pAbc, int argc, char ** argv ) void * pNtlNew, * pNtlOld; Fra_Ssw_t Pars, * pPars = &Pars; int c; - extern Aig_Man_t * Ntl_ManExtract( void * p ); extern void * Ntl_ManSsw( void * p, Fra_Ssw_t * pPars ); extern int Ntl_ManIsComb( void * p ); @@ -21632,7 +21608,6 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) void * pNtlNew, * pNtlOld; Ssw_Pars_t Pars, * pPars = &Pars; int c; - extern Aig_Man_t * Ntl_ManExtract( void * p ); extern void * Ntl_ManScorr( void * p, Ssw_Pars_t * pPars ); extern int Ntl_ManIsComb( void * p ); @@ -25186,11 +25161,14 @@ int Abc_CommandAbc9Era( Abc_Frame_t * pAbc, int argc, char ** argv ) { Gia_Man_t * pTemp = NULL; int c, fVerbose = 0; + int fUseCubes = 1; int fMiter = 0; - int nStatesMax = 10000000; + int nStatesMax = 1000000000; extern void Gia_ManCollectReachable( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbose ); + extern void Gia_ManArePerform( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbose ); + Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Smvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Smcvh" ) ) != EOF ) { switch ( c ) { @@ -25208,6 +25186,9 @@ int Abc_CommandAbc9Era( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'm': fMiter ^= 1; break; + case 'c': + fUseCubes ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -25222,24 +25203,31 @@ int Abc_CommandAbc9Era( Abc_Frame_t * pAbc, int argc, char ** argv ) printf( "Abc_CommandAbc9Era(): There is no AIG.\n" ); return 1; } - if ( Gia_ManPiNum(pAbc->pAig) > 12 ) + if ( Gia_ManRegNum(pAbc->pAig) == 0 ) { - printf( "Abc_CommandAbc9Era(): The number of PIs (%d) should be no more than 12.\n", Gia_ManPiNum(pAbc->pAig) ); + printf( "Abc_CommandAbc9Era(): The network is combinational.\n" ); return 1; } - if ( Gia_ManRegNum(pAbc->pAig) == 0 ) + if ( !fUseCubes && Gia_ManPiNum(pAbc->pAig) > 12 ) { - printf( "Abc_CommandAbc9Era(): The network is combinational.\n" ); + printf( "Abc_CommandAbc9Era(): The number of PIs (%d) should be no more than 12 when cubes are not used.\n", Gia_ManPiNum(pAbc->pAig) ); return 1; } - Gia_ManCollectReachable( pAbc->pAig, nStatesMax, fMiter, fVerbose ); + if ( fUseCubes ) + Gia_ManArePerform( pAbc->pAig, nStatesMax, fMiter, fVerbose ); + else + Gia_ManCollectReachable( pAbc->pAig, nStatesMax, fMiter, fVerbose ); + pAbc->pCex = ((Gia_Man_t *)pAbc->pAig)->pCexSeq; // temporary ??? + ((Gia_Man_t *)pAbc->pAig)->pCexSeq = NULL; return 0; usage: - fprintf( stdout, "usage: &era [-S num] [-mvh]\n" ); + fprintf( stdout, "usage: &era [-S num] [-mcvh]\n" ); +// fprintf( stdout, "usage: &era [-S num] [-mvh]\n" ); fprintf( stdout, "\t explicit reachability analysis for small sequential AIGs\n" ); - fprintf( stdout, "\t-S num : the max number of states to traverse (num > 0) [default = %d]\n", nStatesMax ); + fprintf( stdout, "\t-S num : the max number of states (num > 0) [default = %d]\n", nStatesMax ); fprintf( stdout, "\t-m : stop when the miter output is 1 [default = %s]\n", fMiter? "yes": "no" ); + fprintf( stdout, "\t-c : use state cubes instead of state minterms [default = %s]\n", fUseCubes? "yes": "no" ); fprintf( stdout, "\t-v : print verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( stdout, "\t-h : print the command usage\n"); return 1; diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 790a9028..dbe98631 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -32,6 +32,7 @@ //#include "fsim.h" #include "gia.h" #include "cec.h" +#include "giaAbs.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -463,6 +464,92 @@ Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan ) return pNtkNew; } +/**Function************************************************************* + + Synopsis [Converts the network from the AIG manager into ABC.] + + Description [This procedure should be called after seq sweeping, + which changes the number of registers.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkAfterTrim( Aig_Man_t * pMan, Abc_Ntk_t * pNtkOld ) +{ + Vec_Ptr_t * vNodes; + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObjNew, * pObjOld; + Aig_Obj_t * pObj, * pObjLo, * pObjLi; + int i; + assert( pMan->nAsserts == 0 ); + assert( Aig_ManRegNum(pMan) <= Abc_NtkLatchNum(pNtkOld) ); + assert( Saig_ManPiNum(pMan) <= Abc_NtkCiNum(pNtkOld) ); + assert( Saig_ManPoNum(pMan) == Abc_NtkPoNum(pNtkOld) ); + assert( pMan->vCiNumsOrig != NULL ); + // perform strashing + pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); + // duplicate the name and the spec +// pNtkNew->pName = Extra_UtilStrsav(pMan->pName); +// pNtkNew->pSpec = Extra_UtilStrsav(pMan->pSpec); + Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew); + // create PIs + Aig_ManForEachPiSeq( pMan, pObj, i ) + { + pObjNew = Abc_NtkCreatePi( pNtkNew ); + pObj->pData = pObjNew; + // find the name + pObjOld = Abc_NtkCi( pNtkOld, Vec_IntEntry(pMan->vCiNumsOrig, i) ); + Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjOld), NULL ); + } + // create POs + Aig_ManForEachPoSeq( pMan, pObj, i ) + { + pObjNew = Abc_NtkCreatePo( pNtkNew ); + pObj->pData = pObjNew; + // find the name + pObjOld = Abc_NtkCo( pNtkOld, i ); + Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjOld), NULL ); + } + assert( Abc_NtkCiNum(pNtkNew) == Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan) ); + assert( Abc_NtkCoNum(pNtkNew) == Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan) ); + // create as many latches as there are registers in the manager + Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i ) + { + pObjNew = Abc_NtkCreateLatch( pNtkNew ); + pObjLi->pData = Abc_NtkCreateBi( pNtkNew ); + pObjLo->pData = Abc_NtkCreateBo( pNtkNew ); + Abc_ObjAddFanin( pObjNew, pObjLi->pData ); + Abc_ObjAddFanin( pObjLo->pData, pObjNew ); + Abc_LatchSetInit0( pObjNew ); + // find the name + pObjOld = Abc_NtkCi( pNtkOld, Vec_IntEntry(pMan->vCiNumsOrig, Saig_ManPiNum(pMan)+i) ); + Abc_ObjAssignName( pObjLo->pData, Abc_ObjName(pObjOld), NULL ); + // find the name + pObjOld = Abc_NtkCo( pNtkOld, Saig_ManPoNum(pMan)+i ); + Abc_ObjAssignName( pObjLi->pData, Abc_ObjName(pObjOld), NULL ); + } + // rebuild the AIG + vNodes = Aig_ManDfs( pMan, 1 ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + if ( Aig_ObjIsBuf(pObj) ) + pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj); + else + pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) ); + Vec_PtrFree( vNodes ); + // connect the PO nodes + Aig_ManForEachPo( pMan, pObj, i ) + { + pObjNew = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj); + Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjNew ); + } + // check the resulting AIG + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Abc_NtkFromAigPhase(): Network check has failed.\n" ); + return pNtkNew; +} + /**Function************************************************************* Synopsis [Converts the network from the AIG manager into ABC.] @@ -1633,12 +1720,12 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int printf( "No output was asserted in %d frames. Reached conflict limit (%d). ", iFrame, nBTLimit ); else // if ( RetValue == 0 ) { - extern void Aig_ManCounterExampleValueTest( Aig_Man_t * pAig, Fra_Cex_t * pCex ); +// extern void Aig_ManCounterExampleValueTest( Aig_Man_t * pAig, Fra_Cex_t * pCex ); Fra_Cex_t * pCex = pNtk->pSeqModel; printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame ); - Aig_ManCounterExampleValueTest( pMan, pCex ); +// Aig_ManCounterExampleValueTest( pMan, pCex ); } } else @@ -2714,7 +2801,7 @@ ABC_PRT( "Time", clock() - clkTotal ); SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fUseBdds, int fUseDprove, int fUseStart, int fVerbose ) +Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, Gia_ParAbs_t * pPars ) { Abc_Ntk_t * pNtkAig; Aig_Man_t * pMan, * pTemp; @@ -2724,7 +2811,7 @@ Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConf return NULL; Aig_ManSetRegNum( pMan, pMan->nRegs ); - pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, nRatio, fUseBdds, fUseDprove, fUseStart, fVerbose ); + pMan = Saig_ManProofAbstraction( pTemp = pMan, pPars ); if ( pTemp->pSeqModel ) { ABC_FREE( pNtk->pModel ); @@ -2735,7 +2822,7 @@ Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConf if ( pMan == NULL ) return NULL; - pNtkAig = Abc_NtkFromAigPhase( pMan ); + pNtkAig = Abc_NtkAfterTrim( pMan, pNtk ); // pNtkAig->pName = Extra_UtilStrsav(pNtk->pName); // pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec); Aig_ManStop( pMan ); diff --git a/src/misc/vec/vecAtt.h b/src/misc/vec/vecAtt.h index 983b7c1c..74379bf6 100644 --- a/src/misc/vec/vecAtt.h +++ b/src/misc/vec/vecAtt.h @@ -18,8 +18,8 @@ ***********************************************************************/ -#ifndef __Vec_Att_H__ -#define __Vec_Att_H__ +#ifndef __VEC_ATT_H__ +#define __VEC_ATT_H__ //////////////////////////////////////////////////////////////////////// /// INCLUDES /// diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h index c3c92f09..966f5ac9 100644 --- a/src/misc/vec/vecInt.h +++ b/src/misc/vec/vecInt.h @@ -302,6 +302,23 @@ static inline int Vec_IntEntry( Vec_Int_t * p, int i ) return p->pArray[i]; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int * Vec_IntEntryP( Vec_Int_t * p, int i ) +{ + assert( i >= 0 && i < p->nSize ); + return p->pArray + i; +} + /**Function************************************************************* Synopsis [] @@ -762,6 +779,27 @@ static inline void Vec_IntReverseOrder( Vec_Int_t * p ) } } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Vec_Int_t * Vec_IntInvert( Vec_Int_t * p ) +{ + Vec_Int_t * vRes; + int Entry, i; + vRes = Vec_IntStart( Vec_IntFindMax(p) + 1 ); + Vec_IntForEachEntry( p, Entry, i ) + Vec_IntWriteEntry( vRes, Entry, i ); + return vRes; +} + /**Function************************************************************* Synopsis [Comparison procedure for two integers.] diff --git a/src/opt/mfs/mfsStrash.c b/src/opt/mfs/mfsStrash.c index 578c2fbe..7e6c25da 100644 --- a/src/opt/mfs/mfsStrash.c +++ b/src/opt/mfs/mfsStrash.c @@ -28,6 +28,60 @@ /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [Recursively converts AIG from Aig_Man_t into Hop_Obj_t.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_MfsConvertAigToHop_rec( Aig_Obj_t * pObj, Hop_Man_t * pHop ) +{ + assert( !Aig_IsComplement(pObj) ); + if ( pObj->pData ) + return; + Abc_MfsConvertAigToHop_rec( Aig_ObjFanin0(pObj), pHop ); + Abc_MfsConvertAigToHop_rec( Aig_ObjFanin1(pObj), pHop ); + pObj->pData = Hop_And( pHop, (Hop_Obj_t *)Aig_ObjChild0Copy(pObj), (Hop_Obj_t *)Aig_ObjChild1Copy(pObj) ); + assert( !Hop_IsComplement(pObj->pData) ); +} + +/**Function************************************************************* + + Synopsis [Converts AIG from Aig_Man_t into Hop_Obj_t.] + + Description [Assumes that Aig_Man_t has exactly one primary outputs. + Returns the pointer to the root node (Hop_Obj_t) in Hop_Man_t.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Abc_MfsConvertAigToHop( Aig_Man_t * pMan, Hop_Man_t * pHop ) +{ + Aig_Obj_t * pRoot, * pObj; + int i; + assert( Aig_ManPoNum(pMan) == 1 ); + pRoot = Aig_ManPo( pMan, 0 ); + // check the case of a constant + if ( Aig_ObjIsConst1( Aig_ObjFanin0(pRoot) ) ) + return Hop_NotCond( Hop_ManConst1(pHop), Aig_ObjFaninC0(pRoot) ); + // set the PI mapping + Aig_ManCleanData( pMan ); + Aig_ManForEachPi( pMan, pObj, i ) + pObj->pData = Hop_IthVar( pHop, i ); + // construct the AIG + Abc_MfsConvertAigToHop_rec( Aig_ObjFanin0(pRoot), pHop ); + return Hop_NotCond( Aig_ObjFanin0(pRoot)->pData, Aig_ObjFaninC0(pRoot) ); +} + +// should be called as follows: pNodeNew->pData = Abc_MfsConvertAigToHop( pAigManInterpol, pNodeNew->pNtk->pManFunc ); + /**Function************************************************************* Synopsis [Construct BDDs and mark AIG nodes.] -- cgit v1.2.3