mirror of https://github.com/YosysHQ/abc.git
Version abc90901
committer: Baruch Sterin <baruchs@gmail.com>
This commit is contained in:
Alan Mishchenko
parent
3270783939
commit
51a646a355
52
abc.rc
52
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"
|
||||
|
||||
#read_library at\syn\brdcm.genlib
|
||||
alias t "&r s444.aig; &ps; &era -v"
|
||||
|
||||
|
||||
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"
|
||||
|
||||
|
||||
|
|
|
|||
48
abclib.dsp
48
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"
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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 );
|
||||
|
|
|
|||
|
|
@ -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 );
|
||||
|
|
|
|||
|
|
@ -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 *
|
||||
|
|
|
|||
|
|
@ -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 );
|
||||
|
|
|
|||
|
|
@ -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 ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -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 );
|
||||
|
|
|
|||
|
|
@ -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 ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -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
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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 \
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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 );
|
||||
|
|
|
|||
|
|
@ -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 ///
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -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 );
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 <num>\".\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 )
|
||||
{
|
||||
printf( "Abc_CommandAbc9Era(): The number of PIs (%d) should be no more than 12.\n", Gia_ManPiNum(pAbc->pAig) );
|
||||
return 1;
|
||||
}
|
||||
if ( Gia_ManRegNum(pAbc->pAig) == 0 )
|
||||
{
|
||||
printf( "Abc_CommandAbc9Era(): The network is combinational.\n" );
|
||||
return 1;
|
||||
}
|
||||
Gia_ManCollectReachable( pAbc->pAig, nStatesMax, fMiter, fVerbose );
|
||||
if ( !fUseCubes && Gia_ManPiNum(pAbc->pAig) > 12 )
|
||||
{
|
||||
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;
|
||||
}
|
||||
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;
|
||||
|
|
|
|||
|
|
@ -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 );
|
||||
|
|
|
|||
|
|
@ -18,8 +18,8 @@
|
|||
|
||||
***********************************************************************/
|
||||
|
||||
#ifndef __Vec_Att_H__
|
||||
#define __Vec_Att_H__
|
||||
#ifndef __VEC_ATT_H__
|
||||
#define __VEC_ATT_H__
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// INCLUDES ///
|
||||
|
|
|
|||
|
|
@ -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.]
|
||||
|
|
|
|||
|
|
@ -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.]
|
||||
|
|
|
|||
Loading…
Reference in New Issue