merge pyabc changes into mainline

This commit is contained in:
Baruch Sterin 2011-02-01 16:19:38 -08:00
commit 35e05b7e5a
51 changed files with 7900 additions and 2822 deletions

View File

@ -13,6 +13,7 @@ lib/
docs/
src/ext/
src/xxx/
*~
*.orig

View File

@ -37,7 +37,7 @@ default: $(PROG)
#OPTFLAGS := -DNDEBUG -O3 -DLIN
#OPTFLAGS := -DNDEBUG -O3 -DLIN64
#OPTFLAGS := -g -O -DLIN -m32
OPTFLAGS := -g -O -DLIN64 -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8 -DSIZEOF_INT=4 -DABC_NAMESPACE=xxx -fPIC
OPTFLAGS := -g -O -DLIN64 -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8 -DSIZEOF_INT=4 -DABC_NAMESPACE=xxx
CFLAGS += -Wall -Wno-unused-function $(OPTFLAGS) $(patsubst %, -I%, $(MODULES))
CXXFLAGS += $(CFLAGS)
@ -74,7 +74,7 @@ DEP := $(OBJ:.o=.d)
depend: $(DEP)
clean:
rm -rf $(PROG) $(OBJ) $(GARBAGE) $(OBJ:.o=.d)
rm -rf $(PROG) lib$(PROG).a $(OBJ) $(GARBAGE) $(OBJ:.o=.d)
tags:
ctags -R .

View File

@ -1747,10 +1747,6 @@ SOURCE=.\src\opt\mfs\mfsDiv.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\mfs\mfsGia.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\mfs\mfsInt.h
# End Source File
# Begin Source File
@ -3071,6 +3067,10 @@ SOURCE=.\src\aig\aig\aigDfs.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\aig\aigDoms.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\aig\aigDup.c
# End Source File
# Begin Source File
@ -4035,56 +4035,84 @@ SOURCE=.\src\aig\llb\llb.h
# End Source File
# Begin Source File
SOURCE=.\src\aig\llb\llbCex.c
SOURCE=.\src\aig\llb\llb1Cluster.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\llb\llbCluster.c
SOURCE=.\src\aig\llb\llb1Constr.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\llb\llbConstr.c
SOURCE=.\src\aig\llb\llb1Core.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\llb\llbCore.c
SOURCE=.\src\aig\llb\llb1Group.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\llb\llbFlow.c
SOURCE=.\src\aig\llb\llb1Hint.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\llb\llbHint.c
SOURCE=.\src\aig\llb\llb1Man.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\llb\llb1Matrix.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\llb\llb1Pivot.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\llb\llb1Reach.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\llb\llb1Sched.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\llb\llb2Bad.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\llb\llb2Core.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\llb\llb2Driver.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\llb\llb2Dump.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\llb\llb2Flow.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\llb\llb2Image.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\llb\llb3Image.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\llb\llb3Nonlin.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\llb\llbInt.h
# End Source File
# Begin Source File
# End Group
# Begin Group "bll"
SOURCE=.\src\aig\llb\llbMan.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\llb\llbMatrix.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\llb\llbPart.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\llb\llbPivot.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\llb\llbReach.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\llb\llbSched.c
# End Source File
# PROP Default_Filter ""
# End Group
# End Group
# End Group

View File

@ -1,2 +0,0 @@
link.exe @<<
kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib lib\abcd.lib /nologo /subsystem:console /incremental:yes /pdb:".\DebugExe\abc.pdb" /debug /machine:I386 /out:"_TEST/abc.exe" ".\DebugExe\main.obj" ".\lib\abcd.lib"

View File

@ -22,3 +22,24 @@ Using AIG Package in ABC
The above process should not produce memory leaks.
Using GIA Package in ABC
- Add #include "gia.h".
- Start the AIG package using Gia_ManStart( int nObjMax ).
(Parameter 'nNodeMax' should approximately reflect the expected number of objects, including PIs, POs, flop inputs, and flop outputs. If the number of objects is more, memory will be automatically reallocated.)
- Assign primary inputs using Gia_ManAppendCi().
- Assign flop outputs using Gia_ManAppendCi().
(It is important to create all PIs first, before creating flop outputs).
(Flop control logic, if present, should be elaborated into AND gates. For example, to represent a flop enable, create the driver of enable signal, which can be a PI or an internal node, and then add logic for <flop_input_new> = MUX( <enable>, <flop_input>, <flop_output> ). The output of this logic feeds into the flop.
- Construct AIG in the topological order using Gia_ManHashAnd(), Gia_ManHashOr(), Gia_Not(), etc.
- If constant-0/1 AIG nodes are needed, use Gia_ManConst0() or Gia_ManConst1()
- Create primary outputs using Gia_ManAppendCo().
- Create flop inputs using Gia_ManAppendCo().
(it is important to create all POs first, before creating register inputs).
- Set the number of flops by calling Gia_ManSetRegNum().
- Remove dangling AIG nodes (produced by structural hashing) by running Gia_ManCleanup(), which will return a new AIG. If object mapping is defined for the original AIG, it should be remapped into the new AIG.
- Dump AIG into an AIGER file use Gia_DumpAiger().
- For each object in the design annotated with the constructed AIG node (pNode), remember its AIG node ID by calling Gia_ObjId(pNode).
- Quit the AIG package using Gia_ManStop().
The above process should not produce memory leaks.

View File

@ -1,18 +0,0 @@
r examples/apex4.pla; resyn; if; cec; ps; clp; resyn; map; cec; ps
r examples/C2670.blif; st; w 1.aig; cec 1.aig
r examples/C2670.blif; st; short_names; w 1.bench; cec 1.bench
r examples/C2670.blif; st; short_names; ren -s; w 1.eqn; cec 1.eqn
r examples/C2670.blif; resyn2; if -K 8; cec; ps; u; map; cec; ps
r examples/frg2.blif; dsd; muxes; cec; ps; clp; share; resyn; map; cec; ps
r examples/frg2.blif; bdd; muxes; cec; ps; clp; st; ren -b; muxes; cec; ps
r examples/i10.blif; resyn2; fpga; cec; ps; u; map; cec; ps
r examples/i10.blif; choice; fpga; cec; ps; u; map; cec; ps
r examples/pj1.blif; st; if; cec; ps; u; map; cec; ps
r examples/s38417.blif; comb; w 1.blif; resyn; if; cec 1.blif; ps
r examples/s38417.blif; resyn; if; cec; ps; u; map; cec; ps
r examples/s38584.bench; resyn; ren -s; fx; if; cec; ps; u; map; cec; ps
r examples/s444.blif; b; esd -v; print_exdc; dsd; cec; ps
r examples/s444.blif; double; frames -F 5; w 1.blif; ffpga -K 8; cec 1.blif
r examples/s5378.blif; frames -F 5; cycle; w 1.blif; ps; ret; ps; sec 1.blif
r examples/s6669.blif; cycle; w 1.blif; ps; ret -M 3; resyn; ps; sec 1.blif
time

View File

@ -1,194 +0,0 @@
UC Berkeley, ABC 1.01 (compiled Dec 25 2006 17:15:00)
abc 01> so regtest.script
abc - > r examples/apex4.pla; resyn; if; cec; ps; clp; resyn; map; cec; ps
Networks are equivalent.
examples/apex4: i/o = 9/ 19 lat = 0 nd = 1172 aig = 4365 lev = 7
The shared BDD size is 917 nodes. BDD construction time = 0.04 sec
A simple supergate library is derived from gate library "mcnc_temp.genlib".
Loaded 20 unique 5-input supergates from "mcnc_temp.super". Time = 0.02 sec
Networks are equivalent.
examples/apex4: i/o = 9/ 19 lat = 0 nd = 1734 aig = 2576 lev = 12
abc - > r examples/C2670.blif; st; w 1.aig; cec 1.aig
Networks are equivalent after structural hashing.
abc - > r examples/C2670.blif; st; short_names; w 1.bench; cec 1.bench
Networks are equivalent after structural hashing.
abc - > r examples/C2670.blif; st; short_names; ren -s; w 1.eqn; cec 1.eqn
Networks are equivalent.
abc - > r examples/C2670.blif; resyn2; if -K 8; cec; ps; u; map; cec; ps
Networks are equivalent.
C2670.iscas : i/o = 233/ 140 lat = 0 nd = 120 aig = 1056 lev = 4
Networks are equivalent.
C2670.iscas : i/o = 233/ 140 lat = 0 nd = 467 aig = 651 lev = 14
abc - > r examples/frg2.blif; dsd; muxes; cec; ps; clp; share; resyn; map; cec; ps
Networks are equivalent.
frg2 : i/o = 143/ 139 lat = 0 nd = 1648 aig = 2268 lev = 18
The shared BDD size is 1672 nodes. BDD construction time = 0.14 sec
Networks are equivalent.
frg2 : i/o = 143/ 139 lat = 0 nd = 533 aig = 778 lev = 8
abc - > r examples/frg2.blif; bdd; muxes; cec; ps; clp; st; ren -b; muxes; cec; ps
Networks are equivalent.
frg2 : i/o = 143/ 139 lat = 0 nd = 2868 aig = 4221 lev = 38
The shared BDD size is 1684 nodes. BDD construction time = 0.14 sec
Networks are equivalent.
frg2 : i/o = 143/ 139 lat = 0 nd = 2331 aig = 3180 lev = 20
abc - > r examples/i10.blif; resyn2; fpga; cec; ps; u; map; cec; ps
Networks are equivalent.
i10 : i/o = 257/ 224 lat = 0 nd = 808 aig = 2630 lev = 12
Networks are equivalent.
i10 : i/o = 257/ 224 lat = 0 nd = 1555 aig = 1980 lev = 24
abc - > r examples/i10.blif; choice; fpga; cec; ps; u; map; cec; ps
Currently stored 3 networks with 5801 nodes will be fraiged.
Total fraiging time = 0.39 sec
Performing FPGA mapping with choices.
Networks are equivalent.
i10 : i/o = 257/ 224 lat = 0 nd = 798 aig = 2543 lev = 12
Performing mapping with choices.
Networks are equivalent.
i10 : i/o = 257/ 224 lat = 0 nd = 1463 aig = 1993 lev = 23
abc - > r examples/pj1.blif; st; if; cec; ps; u; map; cec; ps
Networks are equivalent after structural hashing.
exCombCkt : i/o = 1769/1063 lat = 0 nd = 5984 aig = 23156 lev = 52
Networks are equivalent.
exCombCkt : i/o = 1769/1063 lat = 0 nd = 11474 aig = 16032 lev = 80
abc - > r examples/s38417.blif; comb; w 1.blif; resyn; if; cec 1.blif; ps
examples/s38417.blif (line 14): Skipping directive ".wire_load_slope".
Networks are equivalent.
s38417 : i/o = 1664/1742 lat = 0 nd = 3479 aig = 10120 lev = 9
abc - > r examples/s38417.blif; resyn; if; cec; ps; u; map; cec; ps
examples/s38417.blif (line 14): Skipping directive ".wire_load_slope".
examples/s38417.blif (line 14): Skipping directive ".wire_load_slope".
Networks are equivalent.
s38417 : i/o = 28/ 106 lat = 1636 nd = 3479 aig = 10120 lev = 9
examples/s38417.blif (line 14): Skipping directive ".wire_load_slope".
Networks are equivalent.
s38417 : i/o = 28/ 106 lat = 1636 nd = 7189 aig = 8689 lev = 17
abc - > r examples/s38584.bench; resyn; ren -s; fx; if; cec; ps; u; map; cec; ps
The network was strashed and balanced before FPGA mapping.
Networks are equivalent.
examples/s38584: i/o = 12/ 278 lat = 1452 nd = 4266 aig = 12569 lev = 10
The network was strashed and balanced before mapping.
Networks are equivalent.
examples/s38584: i/o = 12/ 278 lat = 1452 nd = 8135 aig = 10674 lev = 18
abc - > r examples/s444.blif; b; esd -v; print_exdc; dsd; cec; ps
The shared BDD size is 181 nodes.
BDD nodes in the transition relation before reordering 557.
BDD nodes in the transition relation after reordering 456.
Reachability analysis completed in 151 iterations.
The number of minterms in the reachable state set = 8865.
BDD nodes in the unreachable states before reordering 124.
BDD nodes in the unreachable states after reordering 113.
EXDC network statistics:
exdc : i/o = 21/ 21 lat = 0 nd = 21 cube = 86 lev = 2
Networks are equivalent.
s444 : i/o = 3/ 6 lat = 21 nd = 82 aig = 176 lev = 7
abc - > r examples/s444.blif; double; frames -F 5; w 1.blif; ffpga -K 8; cec 1.blif
Networks are equivalent after structural hashing.
abc - > r examples/s5378.blif; frames -F 5; cycle; w 1.blif; ps; ret; ps; sec 1.blif
s5378_5_frames: i/o = 175/ 245 lat = 164 and = 6629 (exor = 115) lev = 59
s5378_5_frames: i/o = 175/ 245 lat = 182 nd = 6957 cube = 6956 lev = 50
Networks are equivalent after framing.
abc - > r examples/s6669.blif; cycle; w 1.blif; ps; ret -M 3; resyn; ps; sec 1.blif
s6669 : i/o = 83/ 55 lat = 239 nd = 3080 cube = 3080 lev = 93
s6669 : i/o = 83/ 55 lat = 183 and = 1915 (exor = 371) lev = 97
Networks are equivalent after fraiging.
abc - > time
elapse: 44.07 seconds, total: 44.07 seconds
abc 150>
UC Berkeley, ABC 1.01 (compiled Mar 1 2008 16:23:34)
abc 01> so regtest.script
abc - > r examples/apex4.pla; resyn; if; cec; ps; clp; resyn; map; cec; ps
Networks are equivalent.
examples/apex4: i/o = 9/ 19 lat = 0 nd = 1176 edge = 4298 aig = 4314 lev = 7
Shared BDD size = 917 nodes. BDD construction time = 0.04 sec
A simple supergate library is derived from gate library "mcnc_temp.genlib".
Loaded 20 unique 5-input supergates from "mcnc_temp.super". Time = 0.02 sec
Networks are equivalent.
examples/apex4: i/o = 9/ 19 lat = 0 nd = 1734 edge = 4291 aig = 2576 lev = 12
abc - > r examples/C2670.blif; st; w 1.aig; cec 1.aig
Networks are equivalent after structural hashing.
abc - > r examples/C2670.blif; st; short_names; w 1.bench; cec 1.bench
Networks are equivalent after structural hashing.
abc - > r examples/C2670.blif; st; short_names; ren -s; w 1.eqn; cec 1.eqn
Networks are equivalent.
abc - > r examples/C2670.blif; resyn2; if -K 8; cec; ps; u; map; cec; ps
Networks are equivalent.
C2670.iscas : i/o = 233/ 140 lat = 0 nd = 121 edge = 701 aig = 1088 lev = 4
Networks are equivalent.
C2670.iscas : i/o = 233/ 140 lat = 0 nd = 467 edge = 1029 aig = 651 lev = 14
abc - > r examples/frg2.blif; dsd; muxes; cec; ps; clp; share; resyn; map; cec; ps
Networks are equivalent.
frg2 : i/o = 143/ 139 lat = 0 nd = 1648 edge = 2646 aig = 2268 lev = 18
Shared BDD size = 1505 nodes. BDD construction time = 0.13 sec
Networks are equivalent.
frg2 : i/o = 143/ 139 lat = 0 nd = 557 edge = 1295 aig = 748 lev = 9
abc - > r examples/frg2.blif; bdd; muxes; cec; ps; clp; st; ren -b; muxes; cec; ps
Networks are equivalent.
frg2 : i/o = 143/ 139 lat = 0 nd = 2868 edge = 4855 aig = 4221 lev = 38
Shared BDD size = 1555 nodes. BDD construction time = 0.12 sec
Networks are equivalent.
frg2 : i/o = 143/ 139 lat = 0 nd = 2150 edge = 3465 aig = 3075 lev = 19
abc - > r examples/i10.blif; resyn2; fpga; cec; ps; u; map; cec; ps
Networks are equivalent.
i10 : i/o = 257/ 224 lat = 0 nd = 808 edge = 2767 aig = 2630 lev = 12
Networks are equivalent.
i10 : i/o = 257/ 224 lat = 0 nd = 1555 edge = 3379 aig = 1980 lev = 24
abc - > r examples/i10.blif; choice; fpga; cec; ps; u; map; cec; ps
Performing LUT mapping with 548 choices.
Networks are equivalent.
i10 : i/o = 257/ 224 lat = 0 nd = 788 edge = 2722 aig = 2522 lev = 13
Performing mapping with choices.
Networks are equivalent.
i10 : i/o = 257/ 224 lat = 0 nd = 1462 edge = 3271 aig = 1977 lev = 23
abc - > r examples/pj1.blif; st; if; cec; ps; u; map; cec; ps
Networks are equivalent after structural hashing.
exCombCkt : i/o = 1769/ 1063 lat = 0 nd = 5924 edge = 21224 aig = 22799 lev = 52
Networks are equivalent.
exCombCkt : i/o = 1769/ 1063 lat = 0 nd = 11474 edge = 26350 aig = 16032 lev = 80
abc - > r examples/s38417.blif; comb; w 1.blif; resyn; if; cec 1.blif; ps
Line 14: Skipping line ".wire_load_slope 0.00".
Networks are equivalent.
s38417 : i/o = 1664/ 1742 lat = 0 nd = 3502 edge = 11182 aig = 10001 lev = 9
abc - > r examples/s38417.blif; resyn; if; cec; ps; u; map; cec; ps
Line 14: Skipping line ".wire_load_slope 0.00".
Line 14: Skipping line ".wire_load_slope 0.00".
Networks are equivalent.
s38417 : i/o = 28/ 106 lat = 1636 nd = 3502 edge = 11182 aig = 10001 lev = 9
Line 14: Skipping line ".wire_load_slope 0.00".
Networks are equivalent.
s38417 : i/o = 28/ 106 lat = 1636 nd = 7189 edge = 15262 aig = 8689 lev = 17
abc - > r examples/s38584.bench; resyn; ren -s; fx; if; cec; ps; u; map; cec; ps
The network was strashed and balanced before FPGA mapping.
Networks are equivalent.
examples/s38584: i/o = 12/ 278 lat = 1452 nd = 4452 edge = 14910 aig = 12424 lev = 9
The network was strashed and balanced before mapping.
Networks are equivalent.
examples/s38584: i/o = 12/ 278 lat = 1452 nd = 8339 edge = 18690 aig = 10633 lev = 18
abc - > r examples/s444.blif; b; esd -v; print_exdc; dsd; cec; ps
Shared BDD size = 181 nodes.
BDD nodes in the transition relation before reordering 557.
BDD nodes in the transition relation after reordering 456.
Reachability analysis completed in 151 iterations.
The number of minterms in the reachable state set = 8865. ( 0.42 %)
BDD nodes in the unreachable states before reordering 124.
BDD nodes in the unreachable states after reordering 113.
EXDC network statistics:
exdc : i/o = 21/ 21 lat = 0 nd = 21 edge = 41 cube = 86 lev = 2
Networks are equivalent.
s444 : i/o = 3/ 6 lat = 21 nd = 82 edge = 186 aig = 176 lev = 7
abc - > r examples/s444.blif; double; frames -F 5; w 1.blif; ffpga -K 8; cec 1.blif
Networks are equivalent after structural hashing.
abc - > r examples/s5378.blif; frames -F 5; cycle; w 1.blif; ps; ret; ps; sec 1.blif
s5378_5_frames: i/o = 175/ 245 lat = 164 and = 6629 (exor = 115) lev = 59
s5378_5_frames: i/o = 175/ 245 lat = 182 nd = 6957 edge = 13585 cube = 6956 lev = 50
Networks are equivalent after framing.
abc - > r examples/s6669.blif; cycle; w 1.blif; ps; ret -M 3; resyn; ps; sec 1.blif
s6669 : i/o = 83/ 55 lat = 239 nd = 3148 edge = 5411 cube = 3148 lev = 93
s6669 : i/o = 83/ 55 lat = 183 and = 1915 (exor = 371) lev = 97
Networks are equivalent after fraiging.
abc - > time
elapse: 43.01 seconds, total: 43.01 seconds
abc 159>

View File

@ -470,6 +470,7 @@ extern void Aig_ManCutStop( Aig_ManCut_t * p );
/*=== aigDfs.c ==========================================================*/
extern int Aig_ManVerifyTopoOrder( Aig_Man_t * p );
extern Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p, int fNodesOnly );
extern Vec_Ptr_t * Aig_ManDfsAll( Aig_Man_t * p );
extern Vec_Ptr_t * Aig_ManDfsPreorder( Aig_Man_t * p, int fNodesOnly );
extern Vec_Vec_t * Aig_ManLevelize( Aig_Man_t * p );
extern Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes );
@ -501,6 +502,7 @@ extern Vec_Ptr_t * Aig_ManOrderPios( Aig_Man_t * p, Aig_Man_t * pOrder );
extern Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Vec_Ptr_t * vPios );
extern Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupFlopsOnly( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupRepres( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupRepresDfs( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int fImpl );

View File

@ -167,6 +167,70 @@ Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p, int fNodesOnly )
return vNodes;
}
/**Function*************************************************************
Synopsis [Collects internal nodes in the DFS order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManDfsAll_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
{
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
return;
Aig_ObjSetTravIdCurrent(p, pObj);
if ( Aig_ObjIsPi(pObj) )
{
Vec_PtrPush( vNodes, pObj );
return;
}
if ( Aig_ObjIsPo(pObj) )
{
Aig_ManDfsAll_rec( p, Aig_ObjFanin0(pObj), vNodes );
Vec_PtrPush( vNodes, pObj );
return;
}
assert( Aig_ObjIsNode(pObj) );
Aig_ManDfsAll_rec( p, Aig_ObjFanin0(pObj), vNodes );
Aig_ManDfsAll_rec( p, Aig_ObjFanin1(pObj), vNodes );
Vec_PtrPush( vNodes, pObj );
}
/**Function*************************************************************
Synopsis [Collects objects of the AIG in the DFS order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Aig_ManDfsAll( Aig_Man_t * p )
{
Vec_Ptr_t * vNodes;
Aig_Obj_t * pObj;
int i;
Aig_ManIncrementTravId( p );
vNodes = Vec_PtrAlloc( Aig_ManObjNumMax(p) );
// add constant
Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
Vec_PtrPush( vNodes, Aig_ManConst1(p) );
// collect nodes reachable in the DFS order
Aig_ManForEachPo( p, pObj, i )
Aig_ManDfsAll_rec( p, pObj, vNodes );
Aig_ManForEachPi( p, pObj, i )
if ( !Aig_ObjIsTravIdCurrent(p, pObj) )
Vec_PtrPush( vNodes, pObj );
assert( Vec_PtrSize(vNodes) == Aig_ManObjNum(p) );
return vNodes;
}
/**Function*************************************************************
Synopsis [Collects internal nodes in the DFS order.]

959
src/aig/aig/aigDoms.c Normal file
View File

@ -0,0 +1,959 @@
/**CFile****************************************************************
FileName [aigDoms.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [AIG package.]
Synopsis [Computing multi-output dominators.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: aigDoms.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "aig.h"
#include "saig.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Aig_Sto_t_ Aig_Sto_t;
typedef struct Aig_Dom_t_ Aig_Dom_t;
struct Aig_Dom_t_
{
int uSign; // signature
int nNodes; // the number of nodes
int pNodes[0]; // the nodes
};
struct Aig_Sto_t_
{
int Limit;
Aig_Man_t * pAig; // user's AIG
Aig_MmFixed_t * pMem; // memory manager for dominators
Vec_Ptr_t * vDoms; // dominators
Vec_Int_t * vFans; // temporary fanouts
int nDomNodes; // nodes with dominators
int nDomsTotal; // total dominators
int nDomsFilter1; // filtered dominators
int nDomsFilter2; // filtered dominators
};
#define Aig_DomForEachNode( pAig, pDom, pNode, i ) \
for ( i = 0; (i < pDom->nNodes) && ((pNode) = Aig_ManObj(pAig, (pDom)->pNodes[i])); i++ )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Creates dominator manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Sto_t * Aig_ManDomStart( Aig_Man_t * pAig, int Limit )
{
Aig_Sto_t * pSto;
assert( Aig_ManRegNum(pAig) > 0 );
pSto = ABC_CALLOC( Aig_Sto_t, 1 );
pSto->pAig = pAig;
pSto->Limit = Limit;
pSto->pMem = Aig_MmFixedStart( sizeof(Aig_Dom_t) + sizeof(int) * Limit, 10000 );
pSto->vDoms = Vec_PtrStart( Aig_ManObjNumMax(pAig) );
pSto->vFans = Vec_IntAlloc( 100 );
return pSto;
}
/**Function*************************************************************
Synopsis [Adds trivial dominator.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ObjAddTriv( Aig_Sto_t * pSto, int Id, Vec_Ptr_t * vDoms )
{
Aig_Dom_t * pDom;
pDom = (Aig_Dom_t *)Aig_MmFixedEntryFetch( pSto->pMem );
pDom->uSign = (1 << (Id % 63));
pDom->nNodes = 1;
pDom->pNodes[0] = Id;
Vec_PtrPushFirst( vDoms, pDom );
assert( Vec_PtrEntry( pSto->vDoms, Id ) == NULL );
Vec_PtrWriteEntry( pSto->vDoms, Id, vDoms );
}
/**Function*************************************************************
Synopsis [Duplicates vector of doms.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Aig_ObjDomVecDup( Aig_Sto_t * pSto, Vec_Ptr_t * vDoms, int fSkip1 )
{
Vec_Ptr_t * vDoms2;
Aig_Dom_t * pDom, * pDom2;
int i;
vDoms2 = Vec_PtrAlloc( 0 );
Vec_PtrForEachEntryStart( Aig_Dom_t *, vDoms, pDom, i, fSkip1 )
{
pDom2 = (Aig_Dom_t *)Aig_MmFixedEntryFetch( pSto->pMem );
memcpy( pDom2, pDom, sizeof(Aig_Dom_t) + sizeof(int) * pSto->Limit );
Vec_PtrPush( vDoms2, pDom2 );
}
return vDoms2;
}
/**Function*************************************************************
Synopsis [Recycles vector of doms.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ObjDomVecRecycle( Aig_Sto_t * pSto, Vec_Ptr_t * vDoms )
{
Aig_Dom_t * pDom;
int i;
Vec_PtrForEachEntry( Aig_Dom_t *, vDoms, pDom, i )
Aig_MmFixedEntryRecycle( pSto->pMem, (char *)pDom );
Vec_PtrFree( vDoms );
}
/**Function*************************************************************
Synopsis [Duplicates the vector of doms.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ObjDomPrint( Aig_Sto_t * pSto, Aig_Dom_t * pDom, int Num )
{
int k;
printf( "%4d : {", Num );
for ( k = 0; k < pDom->nNodes; k++ )
printf( " %4d", pDom->pNodes[k] );
for ( ; k < pSto->Limit; k++ )
printf( " " );
printf( " }\n" );
}
/**Function*************************************************************
Synopsis [Duplicates the vector of doms.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ObjDomVecPrint( Aig_Sto_t * pSto, Vec_Ptr_t * vDoms )
{
Aig_Dom_t * pDom;
int i;
Vec_PtrForEachEntry( Aig_Dom_t *, vDoms, pDom, i )
Aig_ObjDomPrint( pSto, pDom, i );
}
/**Function*************************************************************
Synopsis [Computes multi-node dominators.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManDomPrint( Aig_Sto_t * pSto )
{
Aig_Obj_t * pObj;
int i;
Saig_ManForEachLo( pSto->pAig, pObj, i )
{
printf( "*** LO %4d %4d :\n", i, pObj->Id );
Aig_ObjDomVecPrint( pSto, (Vec_Ptr_t *)Vec_PtrEntry(pSto->vDoms, pObj->Id) );
}
}
/**Function*************************************************************
Synopsis [Divides the circuit into well-balanced parts.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManDomStop( Aig_Sto_t * pSto )
{
Vec_Ptr_t * vDoms;
int i;
Vec_PtrForEachEntry( Vec_Ptr_t *, pSto->vDoms, vDoms, i )
if ( vDoms )
Aig_ObjDomVecRecycle( pSto, vDoms );
Vec_PtrFree( pSto->vDoms );
Vec_IntFree( pSto->vFans );
Aig_MmFixedStop( pSto->pMem, 0 );
ABC_FREE( pSto );
}
/**Function*************************************************************
Synopsis [Checks correctness of the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ObjDomCheck( Aig_Dom_t * pDom )
{
int i;
for ( i = 1; i < pDom->nNodes; i++ )
{
if ( pDom->pNodes[i-1] >= pDom->pNodes[i] )
{
Abc_Print( -1, "Aig_ObjDomCheck(): Cut has wrong ordering of inputs.\n" );
return 0;
}
assert( pDom->pNodes[i-1] < pDom->pNodes[i] );
}
return 1;
}
/**Function*************************************************************
Synopsis [Returns 1 if pDom is contained in pCut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Aig_ObjDomCheckDominance( Aig_Dom_t * pDom, Aig_Dom_t * pCut )
{
int i, k;
for ( i = 0; i < pDom->nNodes; i++ )
{
for ( k = 0; k < (int)pCut->nNodes; k++ )
if ( pDom->pNodes[i] == pCut->pNodes[k] )
break;
if ( k == (int)pCut->nNodes ) // node i in pDom is not contained in pCut
return 0;
}
// every node in pDom is contained in pCut
return 1;
}
/**Function*************************************************************
Synopsis [Returns 1 if the cut is contained.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ObjDomFilter( Aig_Sto_t * pSto, Vec_Ptr_t * vDoms, Aig_Dom_t * pDom )
{
Aig_Dom_t * pTemp;
int i;
Vec_PtrForEachEntry( Aig_Dom_t *, vDoms, pTemp, i )
{
if ( pTemp->nNodes > pDom->nNodes )
{
// do not fiter the first cut
if ( i == 0 )
continue;
// skip the non-contained cuts
if ( (pTemp->uSign & pDom->uSign) != pDom->uSign )
continue;
// check containment seriously
if ( Aig_ObjDomCheckDominance( pDom, pTemp ) )
{
Vec_PtrRemove( vDoms, pTemp );
Aig_MmFixedEntryRecycle( pSto->pMem, (char *)pTemp );
i--;
pSto->nDomsFilter1++;
}
}
else
{
// skip the non-contained cuts
if ( (pTemp->uSign & pDom->uSign) != pTemp->uSign )
continue;
// check containment seriously
if ( Aig_ObjDomCheckDominance( pTemp, pDom ) )
{
pSto->nDomsFilter2++;
return 1;
}
}
}
return 0;
}
/**Function*************************************************************
Synopsis [Merges two cuts.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Aig_ObjDomMergeOrdered( Aig_Dom_t * pD0, Aig_Dom_t * pD1, Aig_Dom_t * pD, int Limit )
{
int i, k, c;
assert( pD0->nNodes >= pD1->nNodes );
// the case of the largest cut sizes
if ( pD0->nNodes == Limit && pD1->nNodes == Limit )
{
for ( i = 0; i < pD0->nNodes; i++ )
if ( pD0->pNodes[i] != pD1->pNodes[i] )
return 0;
for ( i = 0; i < pD0->nNodes; i++ )
pD->pNodes[i] = pD0->pNodes[i];
pD->nNodes = pD0->nNodes;
return 1;
}
// the case when one of the cuts is the largest
if ( pD0->nNodes == Limit )
{
for ( i = 0; i < pD1->nNodes; i++ )
{
for ( k = pD0->nNodes - 1; k >= 0; k-- )
if ( pD0->pNodes[k] == pD1->pNodes[i] )
break;
if ( k == -1 ) // did not find
return 0;
}
for ( i = 0; i < pD0->nNodes; i++ )
pD->pNodes[i] = pD0->pNodes[i];
pD->nNodes = pD0->nNodes;
return 1;
}
// compare two cuts with different numbers
i = k = 0;
for ( c = 0; c < (int)Limit; c++ )
{
if ( k == pD1->nNodes )
{
if ( i == pD0->nNodes )
{
pD->nNodes = c;
return 1;
}
pD->pNodes[c] = pD0->pNodes[i++];
continue;
}
if ( i == pD0->nNodes )
{
if ( k == pD1->nNodes )
{
pD->nNodes = c;
return 1;
}
pD->pNodes[c] = pD1->pNodes[k++];
continue;
}
if ( pD0->pNodes[i] < pD1->pNodes[k] )
{
pD->pNodes[c] = pD0->pNodes[i++];
continue;
}
if ( pD0->pNodes[i] > pD1->pNodes[k] )
{
pD->pNodes[c] = pD1->pNodes[k++];
continue;
}
pD->pNodes[c] = pD0->pNodes[i++];
k++;
}
if ( i < pD0->nNodes || k < pD1->nNodes )
return 0;
pD->nNodes = c;
return 1;
}
/**Function*************************************************************
Synopsis [Prepares the object for FPGA mapping.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ObjDomMergeTwo( Aig_Dom_t * pDom0, Aig_Dom_t * pDom1, Aig_Dom_t * pDom, int Limit )
{
assert( Limit > 0 );
if ( pDom0->nNodes < pDom1->nNodes )
{
if ( !Aig_ObjDomMergeOrdered( pDom1, pDom0, pDom, Limit ) )
return 0;
}
else
{
if ( !Aig_ObjDomMergeOrdered( pDom0, pDom1, pDom, Limit ) )
return 0;
}
pDom->uSign = pDom0->uSign | pDom1->uSign;
assert( pDom->nNodes <= Limit );
assert( Aig_ObjDomCheck( pDom ) );
return 1;
}
/**Function*************************************************************
Synopsis [Merge two arrays of dominators.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Aig_ObjDomMerge( Aig_Sto_t * pSto, Vec_Ptr_t * vDoms0, Vec_Ptr_t * vDoms1 )
{
Vec_Ptr_t * vDoms;
Aig_Dom_t * pDom0, * pDom1, * pDom;
int i, k;
vDoms = Vec_PtrAlloc( 16 );
Vec_PtrForEachEntry( Aig_Dom_t *, vDoms0, pDom0, i )
Vec_PtrForEachEntry( Aig_Dom_t *, vDoms1, pDom1, k )
{
if ( Aig_WordCountOnes( pDom0->uSign | pDom1->uSign ) > pSto->Limit )
continue;
// check if the cut exists
pDom = (Aig_Dom_t *)Aig_MmFixedEntryFetch( pSto->pMem );
if ( !Aig_ObjDomMergeTwo( pDom0, pDom1, pDom, pSto->Limit ) )
{
Aig_MmFixedEntryRecycle( pSto->pMem, (char *)pDom );
continue;
}
// check if this cut is contained in any of the available cuts
if ( Aig_ObjDomFilter( pSto, vDoms, pDom ) )
{
Aig_MmFixedEntryRecycle( pSto->pMem, (char *)pDom );
continue;
}
Vec_PtrPush( vDoms, pDom );
}
return vDoms;
}
/**Function*************************************************************
Synopsis [Union two arrays of dominators.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ObjDomUnion( Aig_Sto_t * pSto, Vec_Ptr_t * vDoms2, Vec_Ptr_t * vDoms1 )
{
Aig_Dom_t * pDom1, * pDom2;
int i;
Vec_PtrForEachEntry( Aig_Dom_t *, vDoms1, pDom1, i )
{
if ( i == 0 )
continue;
if ( Aig_ObjDomFilter( pSto, vDoms2, pDom1 ) )
continue;
pDom2 = (Aig_Dom_t *)Aig_MmFixedEntryFetch( pSto->pMem );
memcpy( pDom2, pDom1, sizeof(Aig_Dom_t) + sizeof(int) * pSto->Limit );
Vec_PtrPush( vDoms2, pDom2 );
}
}
/**Function*************************************************************
Synopsis [Computes multi-node dominators.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ObjDomCompute( Aig_Sto_t * pSto, Aig_Obj_t * pObj )
{
Vec_Ptr_t * vDoms0, * vDoms1, * vDoms2, * vDomsT;
Aig_Obj_t * pFanout;
int i, iFanout;
pSto->nDomNodes += Aig_ObjIsNode(pObj);
Vec_IntClear( pSto->vFans );
Aig_ObjForEachFanout( pSto->pAig, pObj, pFanout, iFanout, i )
if ( Aig_ObjIsTravIdCurrent(pSto->pAig, pFanout) )
Vec_IntPush( pSto->vFans, iFanout>>1 );
if ( Vec_IntSize(pSto->vFans) == 0 )
return;
vDoms0 = Vec_PtrEntry( pSto->vDoms, Vec_IntEntry(pSto->vFans, 0) );
vDoms2 = Aig_ObjDomVecDup( pSto, vDoms0, 0 );
Vec_IntForEachEntryStart( pSto->vFans, iFanout, i, 1 )
{
vDoms1 = Vec_PtrEntry( pSto->vDoms, iFanout );
vDoms2 = Aig_ObjDomMerge( pSto, vDomsT = vDoms2, vDoms1 );
Aig_ObjDomVecRecycle( pSto, vDomsT );
}
Aig_ObjAddTriv( pSto, pObj->Id, vDoms2 );
pSto->nDomsTotal += Vec_PtrSize(vDoms2);
}
/**Function*************************************************************
Synopsis [Marks the flop TFI with the current traversal ID.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManMarkFlopTfi_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
{
int Count;
assert( !Aig_IsComplement(pObj) );
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
return 0;
Aig_ObjSetTravIdCurrent(p, pObj);
if ( Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) )
return 1;
Count = Aig_ManMarkFlopTfi_rec( p, Aig_ObjFanin0(pObj) );
if ( Aig_ObjIsNode(pObj) )
Count += Aig_ManMarkFlopTfi_rec( p, Aig_ObjFanin1(pObj) );
return Count;
}
/**Function*************************************************************
Synopsis [Marks the flop TFI with the current traversal ID.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManMarkFlopTfi( Aig_Man_t * p )
{
Aig_Obj_t * pObj;
int i;
Aig_ManIncrementTravId( p );
Saig_ManForEachLi( p, pObj, i )
Aig_ManMarkFlopTfi_rec( p, pObj );
}
/**Function*************************************************************
Synopsis [Computes multi-node dominators.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Sto_t * Aig_ManComputeDoms( Aig_Man_t * pAig, int Limit )
{
Aig_Sto_t * pSto;
Vec_Ptr_t * vNodes;
Aig_Obj_t * pObj;
int i, clk = clock();
pSto = Aig_ManDomStart( pAig, Limit );
// initialize flop inputs
Saig_ManForEachLi( pAig, pObj, i )
Aig_ObjAddTriv( pSto, pObj->Id, Vec_PtrAlloc(1) );
// compute internal nodes
vNodes = Aig_ManDfsReverse( pAig );
Aig_ManMarkFlopTfi( pAig );
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
if ( Aig_ObjIsTravIdCurrent(pSto->pAig, pObj) )
Aig_ObjDomCompute( pSto, pObj );
Vec_PtrFree( vNodes );
// compute combinational inputs
Aig_ManForEachPi( pAig, pObj, i )
Aig_ObjDomCompute( pSto, pObj );
// print statistics
printf( "Nodes =%4d. Flops =%4d. Doms =%9d. Ave =%8.2f. ",
pSto->nDomNodes, Aig_ManRegNum(pSto->pAig), pSto->nDomsTotal,
// pSto->nDomsFilter1, pSto->nDomsFilter2,
1.0 * pSto->nDomsTotal / (pSto->nDomNodes + Aig_ManRegNum(pSto->pAig)) );
Abc_PrintTime( 1, "Time", clock() - clk );
return pSto;
}
/**Function*************************************************************
Synopsis [Collects dominators from the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Aig_ObjDomCollect( Aig_Sto_t * pSto, Vec_Int_t * vCut )
{
Vec_Ptr_t * vDoms0, * vDoms1, * vDoms2;
int i, ObjId;
vDoms0 = Vec_PtrEntry( pSto->vDoms, Vec_IntEntry(vCut, 0) );
vDoms2 = Aig_ObjDomVecDup( pSto, vDoms0, 1 );
Vec_IntForEachEntryStart( vCut, ObjId, i, 1 )
{
vDoms1 = Vec_PtrEntry( pSto->vDoms, ObjId );
if ( vDoms1 == NULL )
continue;
Aig_ObjDomUnion( pSto, vDoms2, vDoms1 );
}
return vDoms2;
}
/**Function*************************************************************
Synopsis [Marks the flop TFI with the current traversal ID.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ObjDomVolume_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
{
int Count;
assert( !Aig_IsComplement(pObj) );
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
return 0;
Aig_ObjSetTravIdCurrent(p, pObj);
if ( pObj->fMarkA )
return 1;
// assert( !Aig_ObjIsPi(pObj) && !Aig_ObjIsConst1(pObj) );
if ( Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) )
return 1;
Count = Aig_ObjDomVolume_rec( p, Aig_ObjFanin0(pObj) );
if ( Aig_ObjIsNode(pObj) )
Count += Aig_ObjDomVolume_rec( p, Aig_ObjFanin1(pObj) );
return Count;
}
/**Function*************************************************************
Synopsis [Count the number of nodes in the dominator.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ObjDomVolume( Aig_Sto_t * pSto, Aig_Dom_t * pDom )
{
Aig_Obj_t * pObj;
int i, Counter = 0;
Aig_ManIncrementTravId( pSto->pAig );
Aig_DomForEachNode( pSto->pAig, pDom, pObj, i )
Counter += Aig_ObjDomVolume_rec( pSto->pAig, pObj );
return Counter;
}
/**Function*************************************************************
Synopsis [Dereferences the node's MFFC.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ObjDomDeref_rec( Aig_Obj_t * pNode )
{
int Counter = 0;
assert( pNode->nRefs > 0 );
if ( --pNode->nRefs > 0 )
return 0;
assert( pNode->nRefs == 0 );
if ( pNode->fMarkA )
return 1;
if ( Aig_ObjIsPi(pNode) )
return 0;
Counter += Aig_ObjDomDeref_rec( Aig_ObjFanin0(pNode) );
if ( Aig_ObjIsNode(pNode) )
Counter += Aig_ObjDomDeref_rec( Aig_ObjFanin1(pNode) );
return Counter;
}
/**Function*************************************************************
Synopsis [References the node's MFFC.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ObjDomRef_rec( Aig_Obj_t * pNode )
{
int Counter = 0;
assert( pNode->nRefs >= 0 );
if ( pNode->nRefs++ > 0 )
return 0;
assert( pNode->nRefs == 1 );
if ( pNode->fMarkA )
return 1;
if ( Aig_ObjIsPi(pNode) )
return 0;
Counter += Aig_ObjDomRef_rec( Aig_ObjFanin0(pNode) );
if ( Aig_ObjIsNode(pNode) )
Counter += Aig_ObjDomRef_rec( Aig_ObjFanin1(pNode) );
return Counter;
}
/**Function*************************************************************
Synopsis [Count the number of nodes in the dominator.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ObjDomDomed( Aig_Sto_t * pSto, Aig_Dom_t * pDom )
{
Aig_Obj_t * pObj;
int i, Counter0, Counter1;
Counter0 = 0;
Aig_DomForEachNode( pSto->pAig, pDom, pObj, i )
{
assert( !Aig_ObjIsPi(pObj) );
Counter0 += Aig_ObjDomDeref_rec( Aig_ObjFanin0(pObj) );
if ( Aig_ObjIsNode(pObj) )
Counter0 += Aig_ObjDomDeref_rec( Aig_ObjFanin1(pObj) );
}
Counter1 = 0;
Aig_DomForEachNode( pSto->pAig, pDom, pObj, i )
{
assert( !Aig_ObjIsPi(pObj) );
Counter1 += Aig_ObjDomRef_rec( Aig_ObjFanin0(pObj) );
if ( Aig_ObjIsNode(pObj) )
Counter1 += Aig_ObjDomRef_rec( Aig_ObjFanin1(pObj) );
}
assert( Counter0 == Counter1 );
return Counter0;
}
/**Function*************************************************************
Synopsis [Collects dominators from the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Aig_ObjDomCollectLos( Aig_Sto_t * pSto )
{
Vec_Int_t * vCut;
Aig_Obj_t * pObj;
int i;
vCut = Vec_IntAlloc( Aig_ManRegNum(pSto->pAig) );
Saig_ManForEachLo( pSto->pAig, pObj, i )
{
Vec_IntPush( vCut, pObj->Id );
pObj->fMarkA = 1;
}
return vCut;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ObjPoLogicDeref( Aig_Sto_t * pSto )
{
Aig_Obj_t * pObj;
int i;
Saig_ManForEachPo( pSto->pAig, pObj, i )
Aig_ObjDomDeref_rec( Aig_ObjFanin0(pObj) );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ObjPoLogicRef( Aig_Sto_t * pSto )
{
Aig_Obj_t * pObj;
int i;
Saig_ManForEachPo( pSto->pAig, pObj, i )
Aig_ObjDomRef_rec( Aig_ObjFanin0(pObj) );
}
/**Function*************************************************************
Synopsis [Collects dominators from the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ObjDomFindGood( Aig_Sto_t * pSto )
{
Aig_Dom_t * pDom;
Vec_Int_t * vCut;
Vec_Ptr_t * vDoms;
int i;
vCut = Aig_ObjDomCollectLos( pSto );
vDoms = Aig_ObjDomCollect( pSto, vCut );
Vec_IntFree( vCut );
printf( "The cut has %d non-trivial %d-dominators.\n", Vec_PtrSize(vDoms), pSto->Limit );
Aig_ObjPoLogicDeref( pSto );
Vec_PtrForEachEntry( Aig_Dom_t *, vDoms, pDom, i )
{
// if ( Aig_ObjDomDomed(pSto, pDom) <= 1 )
// continue;
printf( "Vol =%3d. ", Aig_ObjDomVolume(pSto, pDom) );
printf( "Dom =%3d. ", Aig_ObjDomDomed(pSto, pDom) );
Aig_ObjDomPrint( pSto, pDom, i );
}
Aig_ObjPoLogicRef( pSto );
Aig_ObjDomVecRecycle( pSto, vDoms );
Aig_ManCleanMarkA( pSto->pAig );
}
/**Function*************************************************************
Synopsis [Computes multi-node dominators.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManComputeDomsTest( Aig_Man_t * pAig, int Num )
{
Aig_Sto_t * pSto;
// int i;
//Aig_ManShow( pAig, 0, NULL );
Aig_ManFanoutStart( pAig );
// for ( i = 1; i < 9; i++ )
{
printf( "ITERATION %d:\n", Num );
pSto = Aig_ManComputeDoms( pAig, Num );
Aig_ObjDomFindGood( pSto );
// Aig_ManDomPrint( pSto );
Aig_ManDomStop( pSto );
}
Aig_ManFanoutStop( pAig );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

View File

@ -913,6 +913,33 @@ Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p )
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates the AIG manager.]
Description [Assumes topological ordering of nodes.]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_ManDupFlopsOnly( Aig_Man_t * p )
{
Aig_Man_t * pNew;
Aig_Obj_t * pObj;
int i;
pNew = Aig_ManDupWithoutPos( p );
Saig_ManForEachLi( p, pObj, i )
pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
Aig_ManCleanup( pNew );
Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
if ( !Aig_ManCheck(pNew) )
printf( "Aig_ManDupFlopsOnly(): The check has failed.\n" );
return pNew;
}
/**Function*************************************************************

View File

@ -370,6 +370,15 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
if ( pPars->fVerbose )
// fprintf( stdout, "\r" );
fprintf( stdout, "\n" );
if ( pPars->fVerbose )
{
double nMints = Cudd_CountMinterm(dd, bReached, Saig_ManRegNum(p) );
// Extra_bddPrint( dd, bReached );printf( "\n" );
fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p)) );
fflush( stdout );
}
}
Cudd_RecursiveDeref( dd, bNext );
// free the onion rings

File diff suppressed because it is too large Load Diff

View File

@ -31,7 +31,6 @@
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_START
@ -50,11 +49,14 @@ struct Gia_ParLlb_t_
int fUseFlow; // use flow computation
int nVolumeMax; // the largest volume
int nVolumeMin; // the smallest volume
int nPartValue; // partitioning value
int fBackward; // enable backward reachability
int fReorder; // enable dynamic variable reordering
int fIndConstr; // extract inductive constraints
int fUsePivots; // use internal pivot variables
int fCluster; // use partition clustering
int fSchedule; // use cluster scheduling
int fDumpReached; // dump reached states into a file
int fVerbose; // print verbose information
int fVeryVerbose; // print dependency matrices
int fSilent; // do not print any infomation

View File

@ -1,6 +1,6 @@
/**CFile****************************************************************
FileName [llbCluster.c]
FileName [llb1Cluster.c]
SystemName [ABC: Logic synthesis and verification system.]
@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: llbCluster.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
Revision [$Id: llb1Cluster.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/

View File

@ -1,6 +1,6 @@
/**CFile****************************************************************
FileName [llbConstr.c]
FileName [llb1Constr.c]
SystemName [ABC: Logic synthesis and verification system.]
@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: llbConstr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
Revision [$Id: llb1Constr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/

View File

@ -1,6 +1,6 @@
/**CFile****************************************************************
FileName [llbCore.c]
FileName [llb1Core.c]
SystemName [ABC: Logic synthesis and verification system.]
@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: llbCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
Revision [$Id: llb1Core.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
@ -24,11 +24,10 @@
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@ -47,7 +46,7 @@ ABC_NAMESPACE_IMPL_START
void Llb_ManSetDefaultParams( Gia_ParLlb_t * p )
{
memset( p, 0, sizeof(Gia_ParLlb_t) );
p->nBddMax = 1000000;
p->nBddMax = 10000000;
p->nIterMax = 10000000;
p->nClusterMax = 20;
p->nHintDepth = 0;
@ -55,11 +54,14 @@ void Llb_ManSetDefaultParams( Gia_ParLlb_t * p )
p->fUseFlow = 0; // use flow
p->nVolumeMax = 100; // max volume
p->nVolumeMin = 30; // min volume
p->nPartValue = 5; // partitioning value
p->fBackward = 0; // forward by default
p->fReorder = 1;
p->fIndConstr = 0;
p->fUsePivots = 0;
p->fCluster = 0;
p->fSchedule = 0;
p->fDumpReached = 0;
p->fVerbose = 0;
p->fVeryVerbose = 0;
p->fSilent = 0;

View File

@ -1,6 +1,6 @@
/**CFile****************************************************************
FileName [llbPart.c]
FileName [llb1Group.c]
SystemName [ABC: Logic synthesis and verification system.]
@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: llbPart.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
Revision [$Id: llb1Group.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/

View File

@ -1,6 +1,6 @@
/**CFile****************************************************************
FileName [llbHint.c]
FileName [llb1Hint.c]
SystemName [ABC: Logic synthesis and verification system.]
@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: llbHint.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
Revision [$Id: llb1Hint.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
@ -205,8 +205,8 @@ int Llb_ManModelCheckAigWithHints( Aig_Man_t * pAigGlo, Gia_ParLlb_t * pPars )
Finish:
if ( ddGlo )
{
if ( ddGlo->bReached )
Cudd_RecursiveDeref( ddGlo, ddGlo->bReached );
if ( ddGlo->bFunc )
Cudd_RecursiveDeref( ddGlo, ddGlo->bFunc );
Extra_StopManager( ddGlo );
}
Vec_IntFreeP( &vHFCands );

View File

@ -1,6 +1,6 @@
/**CFile****************************************************************
FileName [llbMan.c]
FileName [llb1Man.c]
SystemName [ABC: Logic synthesis and verification system.]
@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: llbMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
Revision [$Id: llb1Man.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
@ -142,8 +142,8 @@ void Llb_ManStop( Llb_Man_t * p )
}
if ( p->ddG )
{
if ( p->ddG->bReached )
Cudd_RecursiveDeref( p->ddG, p->ddG->bReached );
if ( p->ddG->bFunc )
Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc );
Extra_StopManager( p->ddG );
}
Aig_ManStop( p->pAig );

View File

@ -1,6 +1,6 @@
/**CFile****************************************************************
FileName [llbMatrix.c]
FileName [llb1Matrix.c]
SystemName [ABC: Logic synthesis and verification system.]
@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: llbMatrix.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
Revision [$Id: llb1Matrix.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/

View File

@ -1,6 +1,6 @@
/**CFile****************************************************************
FileName [llbPivot.c]
FileName [llb1Pivot.c]
SystemName [ABC: Logic synthesis and verification system.]
@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: llbPivot.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
Revision [$Id: llb1Pivot.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/

View File

@ -1,6 +1,6 @@
/**CFile****************************************************************
FileName [llbReach.c]
FileName [llb1Reach.c]
SystemName [ABC: Logic synthesis and verification system.]
@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: llbReach.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
Revision [$Id: llb1Reach.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
@ -344,6 +344,22 @@ DdNode * Llb_ManCreateConstraints( Llb_Man_t * p, Vec_Int_t * vHints, int fUseNs
return bConstr;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Llb_ManDeriveCex( Llb_Man_t * p, DdNode * bInter, int iOutFail, int iIter )
{
return NULL;
}
/**Function*************************************************************
Synopsis [Perform reachability with hints and returns reached states in ppGlo.]
@ -358,7 +374,6 @@ DdNode * Llb_ManCreateConstraints( Llb_Man_t * p, Vec_Int_t * vHints, int fUseNs
int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo )
{
int fCheckOutputs = !p->pPars->fSkipOutCheck;
int fInternalReorder = 0;
int * pNs2Glo = Vec_IntArray( p->vNs2Glo );
int * pGlo2Cs = Vec_IntArray( p->vGlo2Cs );
DdNode * bCurrent, * bReached, * bNext, * bTemp, * bCube;
@ -403,9 +418,9 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo
// perform reachability analysis
// compute the starting set of states
if ( p->ddG->bReached )
if ( p->ddG->bFunc )
{
bReached = p->ddG->bReached; p->ddG->bReached = NULL;
bReached = p->ddG->bFunc; p->ddG->bFunc = NULL;
bCurrent = Extra_TransferPermute( p->ddG, p->dd, bReached, pGlo2Cs ); Cudd_Ref( bCurrent );
}
else
@ -548,28 +563,22 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo
if ( p->pPars->fVerbose )
{
fprintf( stdout, "F =%3d : ", nIters );
fprintf( stdout, "Image =%6d ", nBddSize );
fprintf( stdout, "%8d (%4d %3d) ",
Cudd_ReadKeys(p->dd), Cudd_ReadReorderings(p->dd), Cudd_ReadGarbageCollections(p->dd) );
fprintf( stdout, "Reach =%6d ", Cudd_DagSize(bReached) );
fprintf( stdout, "%8d (%4d %3d) ",
Cudd_ReadKeys(p->ddG), Cudd_ReadReorderings(p->ddG), Cudd_ReadGarbageCollections(p->ddG) );
}
if ( fInternalReorder && p->pPars->fReorder && nBddSize > nThreshold )
{
if ( p->pPars->fVerbose )
fprintf( stdout, "Reordering... Before = %5d. ", Cudd_DagSize(bReached) );
Cudd_ReduceHeap( p->dd, CUDD_REORDER_SYMM_SIFT, 100 );
// Cudd_AutodynDisable( p->dd );
if ( p->pPars->fVerbose )
fprintf( stdout, "After = %5d.\r", Cudd_DagSize(bReached) );
nThreshold *= 2;
fprintf( stdout, "F =%5d : ", nIters );
fprintf( stdout, "Im =%6d ", nBddSize );
fprintf( stdout, "(%4d %3d) ", Cudd_ReadReorderings(p->dd), Cudd_ReadGarbageCollections(p->dd) );
fprintf( stdout, "Rea =%6d ", Cudd_DagSize(bReached) );
fprintf( stdout, "(%4d%4d) ", Cudd_ReadReorderings(p->ddG), Cudd_ReadGarbageCollections(p->ddG) );
Abc_PrintTime( 1, "Time", clock() - clk2 );
}
/*
if ( p->pPars->fVerbose )
// fprintf( stdout, "\r" );
// fprintf( stdout, "\n" );
Abc_PrintTime( 1, "T", clock() - clk2 );
{
double nMints = Cudd_CountMinterm(p->ddG, bReached, Saig_ManRegNum(p->pAig) );
// Extra_bddPrint( p->ddG, bReached );printf( "\n" );
fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) );
fflush( stdout );
}
*/
}
Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL;
Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL;
@ -598,8 +607,8 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo
}
if ( pddGlo )
{
assert( p->ddG->bReached == NULL );
p->ddG->bReached = bReached; bReached = NULL;
assert( p->ddG->bFunc == NULL );
p->ddG->bFunc = bReached; bReached = NULL;
assert( *pddGlo == NULL );
*pddGlo = p->ddG; p->ddG = NULL;
}

View File

@ -1,12 +1,12 @@
/**CFile****************************************************************
FileName [llb.c]
FileName [llb1Sched.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [BDD based reachability.]
Synopsis []
Synopsis [Partition scheduling algorithm.]
Author [Alan Mishchenko]
@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: llb.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
Revision [$Id: llb1Sched.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/

126
src/aig/llb/llb2Bad.c Normal file
View File

@ -0,0 +1,126 @@
/**CFile****************************************************************
FileName [llb2Bad.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [BDD based reachability.]
Synopsis [Computing bad states.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: llb2Bad.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "llbInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Computes bad in working manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd )
{
Vec_Ptr_t * vNodes;
DdNode * bBdd0, * bBdd1, * bTemp, * bResult;
Aig_Obj_t * pObj;
int i;
assert( Cudd_ReadSize(dd) == Aig_ManPiNum(pInit) );
// initialize elementary variables
Aig_ManConst1(pInit)->pData = Cudd_ReadOne( dd );
Saig_ManForEachLo( pInit, pObj, i )
pObj->pData = Cudd_bddIthVar( dd, i );
Saig_ManForEachPi( pInit, pObj, i )
pObj->pData = Cudd_bddIthVar( dd, Aig_ManRegNum(pInit) + i );
// compute internal nodes
vNodes = Aig_ManDfsNodes( pInit, (Aig_Obj_t **)Vec_PtrArray(pInit->vPos), Saig_ManPoNum(pInit) );
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
{
if ( !Aig_ObjIsNode(pObj) )
continue;
bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( (DdNode *)pObj->pData );
}
// quantify PIs of each PO
bResult = Cudd_ReadLogicZero( dd ); Cudd_Ref( bResult );
Saig_ManForEachPo( pInit, pObj, i )
{
bBdd0 = Cudd_NotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
bResult = Cudd_bddOr( dd, bTemp = bResult, bBdd0 ); Cudd_Ref( bResult );
Cudd_RecursiveDeref( dd, bTemp );
}
// deref
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
{
if ( !Aig_ObjIsNode(pObj) )
continue;
Cudd_RecursiveDeref( dd, pObj->pData );
}
Vec_PtrFree( vNodes );
Cudd_Deref( bResult );
return bResult;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Llb_BddQuantifyPis( Aig_Man_t * pInit, DdManager * dd, DdNode * bFunc )
{
DdNode * bVar, * bCube, * bTemp;
Aig_Obj_t * pObj;
int i;
assert( Cudd_ReadSize(dd) == Aig_ManPiNum(pInit) );
// create PI cube
bCube = Cudd_ReadOne( dd ); Cudd_Ref( bCube );
Saig_ManForEachPi( pInit, pObj, i )
{
bVar = Cudd_bddIthVar( dd, Aig_ManRegNum(pInit) + i );
bCube = Cudd_bddAnd( dd, bTemp = bCube, bVar ); Cudd_Ref( bCube );
Cudd_RecursiveDeref( dd, bTemp );
}
// quantify PI cube
bFunc = Cudd_bddExistAbstract( dd, bFunc, bCube ); Cudd_Ref( bFunc );
Cudd_RecursiveDeref( dd, bCube );
Cudd_Deref( bFunc );
return bFunc;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

638
src/aig/llb/llb2Core.c Normal file
View File

@ -0,0 +1,638 @@
/**CFile****************************************************************
FileName [llb2Core.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [BDD based reachability.]
Synopsis [Core procedure.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: llb2Core.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "llbInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Llb_Img_t_ Llb_Img_t;
struct Llb_Img_t_
{
Aig_Man_t * pInit; // AIG manager
Aig_Man_t * pAig; // AIG manager
Gia_ParLlb_t * pPars; // parameters
DdManager * dd; // BDD manager
DdManager * ddG; // BDD manager
DdManager * ddR; // BDD manager
Vec_Ptr_t * vDdMans; // BDD managers for each partition
Vec_Ptr_t * vRings; // onion rings in ddR
Vec_Int_t * vDriRefs; // driver references
Vec_Int_t * vVarsCs; // cur state variables
Vec_Int_t * vVarsNs; // next state variables
Vec_Int_t * vCs2Glo; // cur state variables into global variables
Vec_Int_t * vNs2Glo; // next state variables into global variables
Vec_Int_t * vGlo2Cs; // global variables into cur state variables
Vec_Int_t * vGlo2Ns; // global variables into next state variables
};
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Computes cube composed of given variables with given values.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Llb_CoreComputeCube( DdManager * dd, Vec_Int_t * vVars, int fUseVarIndex, char * pValues )
{
DdNode * bRes, * bVar, * bTemp;
int i, iVar, Index;
bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes );
Vec_IntForEachEntry( vVars, Index, i )
{
iVar = fUseVarIndex ? Index : i;
bVar = Cudd_NotCond( Cudd_bddIthVar(dd, iVar), (int)(pValues == NULL || pValues[i] != 1) );
bRes = Cudd_bddAnd( dd, bTemp = bRes, bVar ); Cudd_Ref( bRes );
Cudd_RecursiveDeref( dd, bTemp );
}
Cudd_Deref( bRes );
return bRes;
}
/**Function*************************************************************
Synopsis [Derives counter-example by backward reachability.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Llb_CoreDeriveCex( Llb_Img_t * p )
{
extern Abc_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames );
extern int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p );
Abc_Cex_t * pCex;
Aig_Obj_t * pObj;
Vec_Ptr_t * vSupps, * vQuant0, * vQuant1;
DdNode * bState, * bImage, * bOneCube, * bTemp, * bRing;
int i, v, RetValue, nPiOffset;
char * pValues = ABC_ALLOC( char, Cudd_ReadSize(p->ddR) );
assert( Vec_PtrSize(p->vRings) > 0 );
// get supports and quantified variables
Vec_PtrReverseOrder( p->vDdMans );
vSupps = Llb_ImgSupports( p->pAig, p->vDdMans, p->vVarsNs, p->vVarsCs, 1, 0 );
Llb_ImgSchedule( vSupps, &vQuant0, &vQuant1, 0 );
Vec_VecFree( (Vec_Vec_t *)vSupps );
Llb_ImgQuantifyReset( p->vDdMans );
// Llb_ImgQuantifyFirst( p->pAig, p->vDdMans, vQuant0 );
// allocate room for the counter-example
pCex = Ssw_SmlAllocCounterExample( Saig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Vec_PtrSize(p->vRings) );
pCex->iFrame = Vec_PtrSize(p->vRings) - 1;
pCex->iPo = -1;
// get the last cube
bOneCube = Cudd_bddIntersect( p->ddR, Vec_PtrEntryLast(p->vRings), p->ddR->bFunc ); Cudd_Ref( bOneCube );
RetValue = Cudd_bddPickOneCube( p->ddR, bOneCube, pValues );
Cudd_RecursiveDeref( p->ddR, bOneCube );
assert( RetValue );
// write PIs of counter-example
nPiOffset = Saig_ManRegNum(p->pAig) + Saig_ManPiNum(p->pAig) * (Vec_PtrSize(p->vRings) - 1);
Saig_ManForEachPi( p->pAig, pObj, i )
if ( pValues[Saig_ManRegNum(p->pAig)+i] == 1 )
Aig_InfoSetBit( pCex->pData, nPiOffset + i );
// write state in terms of NS variables
if ( Vec_PtrSize(p->vRings) > 1 )
{
bState = Llb_CoreComputeCube( p->dd, p->vVarsNs, 1, pValues ); Cudd_Ref( bState );
}
// perform backward analysis
Vec_PtrForEachEntryReverse( DdNode *, p->vRings, bRing, v )
{
if ( v == Vec_PtrSize(p->vRings) - 1 )
continue;
// compute the next states
bImage = Llb_ImgComputeImage( p->pAig, p->vDdMans, p->dd, bState,
vQuant0, vQuant1, p->vDriRefs, p->pPars->TimeTarget, 1, 0, 0 );
assert( bImage != NULL );
Cudd_Ref( bImage );
Cudd_RecursiveDeref( p->dd, bState );
//Extra_bddPrintSupport( p->dd, bImage ); printf( "\n" );
// move reached states into ring manager
bImage = Extra_TransferPermute( p->dd, p->ddR, bTemp = bImage, Vec_IntArray(p->vCs2Glo) ); Cudd_Ref( bImage );
Cudd_RecursiveDeref( p->dd, bTemp );
// intersect with the previous set
bOneCube = Cudd_bddIntersect( p->ddR, bImage, bRing ); Cudd_Ref( bOneCube );
Cudd_RecursiveDeref( p->ddR, bImage );
// find any assignment of the BDD
RetValue = Cudd_bddPickOneCube( p->ddR, bOneCube, pValues );
Cudd_RecursiveDeref( p->ddR, bOneCube );
assert( RetValue );
// write PIs of counter-example
nPiOffset -= Saig_ManPiNum(p->pAig);
Saig_ManForEachPi( p->pAig, pObj, i )
if ( pValues[Saig_ManRegNum(p->pAig)+i] == 1 )
Aig_InfoSetBit( pCex->pData, nPiOffset + i );
// check that we get the init state
if ( v == 0 )
{
Saig_ManForEachLo( p->pAig, pObj, i )
assert( pValues[i] == 0 );
break;
}
// write state in terms of NS variables
bState = Llb_CoreComputeCube( p->dd, p->vVarsNs, 1, pValues ); Cudd_Ref( bState );
}
assert( nPiOffset == Saig_ManRegNum(p->pAig) );
// update the output number
RetValue = Ssw_SmlFindOutputCounterExample( p->pInit, pCex );
assert( RetValue >= 0 && RetValue < Saig_ManPoNum(p->pInit) ); // invalid CEX!!!
pCex->iPo = RetValue;
// cleanup
ABC_FREE( pValues );
Vec_VecFree( (Vec_Vec_t *)vQuant0 );
Vec_VecFree( (Vec_Vec_t *)vQuant1 );
return pCex;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQuant1 )
{
int * pLoc2Glo = p->pPars->fBackward? Vec_IntArray( p->vCs2Glo ) : Vec_IntArray( p->vNs2Glo );
int * pLoc2GloR = p->pPars->fBackward? Vec_IntArray( p->vNs2Glo ) : Vec_IntArray( p->vCs2Glo );
int * pGlo2Loc = p->pPars->fBackward? Vec_IntArray( p->vGlo2Ns ) : Vec_IntArray( p->vGlo2Cs );
DdNode * bCurrent, * bReached, * bNext, * bTemp;
int clk2, clk = clock(), nIters, nBddSize, iOutFail = -1;
// compute time to stop
if ( p->pPars->TimeLimit )
p->pPars->TimeTarget = clock() + p->pPars->TimeLimit * CLOCKS_PER_SEC;
else
p->pPars->TimeTarget = 0;
// compute initial states
if ( p->pPars->fBackward )
{
// create bad state in the ring manager
p->ddR->bFunc = Llb_CoreComputeCube( p->ddR, p->vVarsCs, 0, NULL ); Cudd_Ref( p->ddR->bFunc );
// create init state in the global manager
bTemp = Llb_BddComputeBad( p->pInit, p->ddR ); Cudd_Ref( bTemp );
bCurrent = Llb_BddQuantifyPis( p->pInit, p->ddR, bTemp ); Cudd_Ref( bCurrent );
Cudd_RecursiveDeref( p->ddR, bTemp );
bReached = Cudd_bddTransfer( p->ddR, p->ddG, bCurrent ); Cudd_Ref( bReached );
Cudd_RecursiveDeref( p->ddR, bCurrent );
// move init state to the working manager
bCurrent = Extra_TransferPermute( p->ddG, p->dd, bReached, pGlo2Loc ); Cudd_Ref( bCurrent );
}
else
{
// create bad state in the ring manager
p->ddR->bFunc = Llb_BddComputeBad( p->pInit, p->ddR ); Cudd_Ref( p->ddR->bFunc );
// create init state in the working and global manager
bCurrent = Llb_CoreComputeCube( p->dd, p->vVarsCs, 1, NULL ); Cudd_Ref( bCurrent );
bReached = Llb_CoreComputeCube( p->ddG, p->vVarsCs, 0, NULL ); Cudd_Ref( bReached );
//Extra_bddPrint( p->dd, bCurrent ); printf( "\n" );
//Extra_bddPrint( p->ddG, bReached ); printf( "\n" );
}
// compute onion rings
for ( nIters = 0; nIters < p->pPars->nIterMax; nIters++ )
{
clk2 = clock();
// check the runtime limit
if ( p->pPars->TimeLimit && clock() >= p->pPars->TimeTarget )
{
if ( !p->pPars->fSilent )
printf( "Reached timeout during image computation (%d seconds).\n", p->pPars->TimeLimit );
p->pPars->iFrame = nIters - 1;
Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
return -1;
}
// save the onion ring
bTemp = Extra_TransferPermute( p->dd, p->ddR, bCurrent, pLoc2GloR ); Cudd_Ref( bTemp );
Vec_PtrPush( p->vRings, bTemp );
// check it for bad states
if ( !p->pPars->fSkipOutCheck && !Cudd_bddLeq( p->ddR, bTemp, Cudd_Not(p->ddR->bFunc) ) )
{
assert( p->pInit->pSeqModel == NULL );
if ( !p->pPars->fBackward )
p->pInit->pSeqModel = Llb_CoreDeriveCex( p );
Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
if ( !p->pPars->fSilent )
{
if ( !p->pPars->fBackward )
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", p->pInit->pSeqModel->iPo, nIters );
else
printf( "Output ??? was asserted in frame %d (counter-example is not produced). ", nIters );
Abc_PrintTime( 1, "Time", clock() - clk );
}
return 0;
}
// compute the next states
bNext = Llb_ImgComputeImage( p->pAig, p->vDdMans, p->dd, bCurrent,
vQuant0, vQuant1, p->vDriRefs, p->pPars->TimeTarget,
p->pPars->fBackward, p->pPars->fReorder, p->pPars->fVeryVerbose );
if ( bNext == NULL )
{
if ( !p->pPars->fSilent )
printf( "Reached timeout during image computation (%d seconds).\n", p->pPars->TimeLimit );
p->pPars->iFrame = nIters - 1;
Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
return -1;
}
Cudd_Ref( bNext );
Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
//Extra_bddPrintSupport( p->dd, bNext ); printf( "\n" );
// remap these states into the global manager
bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pLoc2Glo ); Cudd_Ref( bNext );
Cudd_RecursiveDeref( p->dd, bTemp );
nBddSize = Cudd_DagSize(bNext);
// check if there are any new states
if ( Cudd_bddLeq( p->ddG, bNext, bReached ) ) // implication = no new states
{
Cudd_RecursiveDeref( p->ddG, bNext ); bNext = NULL;
break;
}
// get the new states
bCurrent = Cudd_bddAnd( p->ddG, bNext, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
// remap these states into the current state vars
bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Loc ); Cudd_Ref( bCurrent );
Cudd_RecursiveDeref( p->ddG, bTemp );
// add to the reached states
bReached = Cudd_bddOr( p->ddG, bTemp = bReached, bNext ); Cudd_Ref( bReached );
Cudd_RecursiveDeref( p->ddG, bTemp );
Cudd_RecursiveDeref( p->ddG, bNext );
bNext = NULL;
if ( p->pPars->fVeryVerbose )
{
double nMints = Cudd_CountMinterm(p->ddG, bReached, Saig_ManRegNum(p->pAig) );
// Extra_bddPrint( p->ddG, bReached );printf( "\n" );
fprintf( stdout, " Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) );
fflush( stdout );
}
if ( p->pPars->fVerbose )
{
fprintf( stdout, "F =%3d : ", nIters );
fprintf( stdout, "Image =%6d ", nBddSize );
fprintf( stdout, "(%4d%4d) ",
Cudd_ReadReorderings(p->dd), Cudd_ReadGarbageCollections(p->dd) );
fprintf( stdout, "Reach =%6d ", Cudd_DagSize(bReached) );
fprintf( stdout, "(%4d%4d) ",
Cudd_ReadReorderings(p->ddG), Cudd_ReadGarbageCollections(p->ddG) );
Abc_PrintTime( 1, "Time", clock() - clk2 );
}
// check timeframe limit
if ( nIters == p->pPars->nIterMax - 1 )
{
if ( !p->pPars->fSilent )
printf( "Reached limit on the number of timeframes (%d).\n", p->pPars->nIterMax );
p->pPars->iFrame = nIters;
Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
return -1;
}
}
if ( bReached == NULL )
return 0; // reachable
if ( bCurrent )
Cudd_RecursiveDeref( p->dd, bCurrent );
// report the stats
if ( p->pPars->fVerbose )
{
double nMints = Cudd_CountMinterm(p->ddG, bReached, Saig_ManRegNum(p->pAig) );
if ( nIters >= p->pPars->nIterMax )
fprintf( stdout, "Reachability analysis is stopped after %d frames.\n", nIters );
else
fprintf( stdout, "Reachability analysis completed after %d frames.\n", nIters );
fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) );
fflush( stdout );
}
if ( p->pPars->fDumpReached )
{
Llb_ManDumpReached( p->ddG, bReached, p->pAig->pName, "reached.blif" );
printf( "Reached states with %d BDD nodes are dumpted into file \"reached.blif\".\n", Cudd_DagSize(bReached) );
}
Cudd_RecursiveDeref( p->ddG, bReached );
if ( nIters >= p->pPars->nIterMax )
{
if ( !p->pPars->fSilent )
{
printf( "Verified only for states reachable in %d frames. ", nIters );
Abc_PrintTime( 1, "Time", clock() - clk );
}
return -1; // undecided
}
if ( !p->pPars->fSilent )
{
printf( "The miter is proved unreachable after %d iterations. ", nIters );
Abc_PrintTime( 1, "Time", clock() - clk );
}
p->pPars->iFrame = nIters - 1;
return 1; // unreachable
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_CoreReachability( Llb_Img_t * p )
{
Vec_Ptr_t * vSupps, * vQuant0, * vQuant1;
int RetValue;
// get supports and quantified variables
if ( p->pPars->fBackward )
{
Vec_PtrReverseOrder( p->vDdMans );
vSupps = Llb_ImgSupports( p->pAig, p->vDdMans, p->vVarsNs, p->vVarsCs, 0, p->pPars->fVeryVerbose );
}
else
vSupps = Llb_ImgSupports( p->pAig, p->vDdMans, p->vVarsCs, p->vVarsNs, 0, p->pPars->fVeryVerbose );
Llb_ImgSchedule( vSupps, &vQuant0, &vQuant1, p->pPars->fVeryVerbose );
Vec_VecFree( (Vec_Vec_t *)vSupps );
// remove variables
Llb_ImgQuantifyFirst( p->pAig, p->vDdMans, vQuant0, p->pPars->fVeryVerbose );
// perform reachability
RetValue = Llb_CoreReachability_int( p, vQuant0, vQuant1 );
Vec_VecFree( (Vec_Vec_t *)vQuant0 );
Vec_VecFree( (Vec_Vec_t *)vQuant1 );
return RetValue;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Llb_CoreConstructAll( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Int_t * vVarsNs )
{
DdManager * dd;
Vec_Ptr_t * vDdMans;
Vec_Ptr_t * vLower, * vUpper;
int i;
vDdMans = Vec_PtrStart( Vec_PtrSize(vResult) );
Vec_PtrForEachEntryReverse( Vec_Ptr_t *, vResult, vLower, i )
{
if ( i < Vec_PtrSize(vResult) - 1 )
dd = Llb_ImgPartition( p, vLower, vUpper );
else
dd = Llb_DriverLastPartition( p, vVarsNs );
Vec_PtrWriteEntry( vDdMans, i, dd );
vUpper = vLower;
}
return vDdMans;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_CoreSetVarMaps( Llb_Img_t * p )
{
Aig_Obj_t * pObj;
int i, iVarCs, iVarNs;
assert( p->vVarsCs != NULL );
assert( p->vVarsNs != NULL );
assert( p->vCs2Glo == NULL );
assert( p->vNs2Glo == NULL );
assert( p->vGlo2Cs == NULL );
assert( p->vGlo2Ns == NULL );
p->vCs2Glo = Vec_IntStartFull( Aig_ManObjNumMax(p->pAig) );
p->vNs2Glo = Vec_IntStartFull( Aig_ManObjNumMax(p->pAig) );
p->vGlo2Cs = Vec_IntStartFull( Aig_ManRegNum(p->pAig) );
p->vGlo2Ns = Vec_IntStartFull( Aig_ManRegNum(p->pAig) );
for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
{
iVarCs = Vec_IntEntry( p->vVarsCs, i );
iVarNs = Vec_IntEntry( p->vVarsNs, i );
assert( iVarCs >= 0 && iVarCs < Aig_ManObjNumMax(p->pAig) );
assert( iVarNs >= 0 && iVarNs < Aig_ManObjNumMax(p->pAig) );
Vec_IntWriteEntry( p->vCs2Glo, iVarCs, i );
Vec_IntWriteEntry( p->vNs2Glo, iVarNs, i );
Vec_IntWriteEntry( p->vGlo2Cs, i, iVarCs );
Vec_IntWriteEntry( p->vGlo2Ns, i, iVarNs );
}
// add mapping of the PIs
Saig_ManForEachPi( p->pAig, pObj, i )
Vec_IntWriteEntry( p->vCs2Glo, Aig_ObjId(pObj), Aig_ManRegNum(p->pAig)+i );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Llb_Img_t * Llb_CoreStart( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
{
Llb_Img_t * p;
p = ABC_CALLOC( Llb_Img_t, 1 );
p->pInit = pInit;
p->pAig = pAig;
p->pPars = pPars;
p->dd = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
p->ddG = Cudd_Init( Aig_ManRegNum(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
p->ddR = Cudd_Init( Aig_ManPiNum(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT );
Cudd_AutodynEnable( p->ddG, CUDD_REORDER_SYMM_SIFT );
Cudd_AutodynEnable( p->ddR, CUDD_REORDER_SYMM_SIFT );
p->vRings = Vec_PtrAlloc( 100 );
p->vDriRefs = Llb_DriverCountRefs( pAig );
p->vVarsCs = Llb_DriverCollectCs( pAig );
p->vVarsNs = Llb_DriverCollectNs( pAig, p->vDriRefs );
Llb_CoreSetVarMaps( p );
return p;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_CoreStop( Llb_Img_t * p )
{
DdManager * dd;
DdNode * bTemp;
int i;
Vec_PtrForEachEntry( DdManager *, p->vDdMans, dd, i )
{
if ( dd->bFunc )
Cudd_RecursiveDeref( dd, dd->bFunc );
if ( dd->bFunc2 )
Cudd_RecursiveDeref( dd, dd->bFunc2 );
Extra_StopManager( dd );
}
Vec_PtrFree( p->vDdMans );
if ( p->ddR->bFunc )
Cudd_RecursiveDeref( p->ddR, p->ddR->bFunc );
Vec_PtrForEachEntry( DdNode *, p->vRings, bTemp, i )
Cudd_RecursiveDeref( p->ddR, bTemp );
Vec_PtrFree( p->vRings );
Extra_StopManager( p->dd );
Extra_StopManager( p->ddG );
Extra_StopManager( p->ddR );
Vec_IntFreeP( &p->vDriRefs );
Vec_IntFreeP( &p->vVarsCs );
Vec_IntFreeP( &p->vVarsNs );
Vec_IntFreeP( &p->vCs2Glo );
Vec_IntFreeP( &p->vNs2Glo );
Vec_IntFreeP( &p->vGlo2Cs );
Vec_IntFreeP( &p->vGlo2Ns );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_CoreExperiment( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars, Vec_Ptr_t * vResult )
{
int RetValue;
Llb_Img_t * p;
// printf( "\n" );
// pPars->fVerbose = 1;
p = Llb_CoreStart( pInit, pAig, pPars );
p->vDdMans = Llb_CoreConstructAll( pAig, vResult, p->vVarsNs );
RetValue = Llb_CoreReachability( p );
Llb_CoreStop( p );
return RetValue;
}
/**Function*************************************************************
Synopsis [Finds balanced cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_ManReachMinCut( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
{
extern Vec_Ptr_t * Llb_ManComputeCuts( Aig_Man_t * p, int Num, int fVerbose, int fVeryVerbose );
Vec_Ptr_t * vResult;
Aig_Man_t * p;
int RetValue = -1;
p = Aig_ManDupFlopsOnly( pAig );
//Aig_ManShow( p, 0, NULL );
if ( pPars->fVerbose )
Aig_ManPrintStats( pAig );
if ( pPars->fVerbose )
Aig_ManPrintStats( p );
Aig_ManFanoutStart( p );
vResult = Llb_ManComputeCuts( p, pPars->nPartValue, pPars->fVerbose, pPars->fVeryVerbose );
if ( !pPars->fSkipReach )
RetValue = Llb_CoreExperiment( pAig, p, pPars, vResult );
Vec_VecFree( (Vec_Vec_t *)vResult );
Aig_ManFanoutStop( p );
Aig_ManCleanMarkAB( p );
Aig_ManStop( p );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

208
src/aig/llb/llb2Driver.c Normal file
View File

@ -0,0 +1,208 @@
/**CFile****************************************************************
FileName [llb2Driver.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [BDD based reachability.]
Synopsis [Procedures working with flop drivers.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: llb2Driver.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "llbInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
// driver issue:arises when creating
// - driver ref-counter array
// - Ns2Glo maps
// - final partition
// - change-phase cube
// LI variable is used when
// - driver drives more than one LI
// - driver is a PI
// - driver is a constant
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Returns the array of times each flop driver is referenced.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Llb_DriverCountRefs( Aig_Man_t * p )
{
Vec_Int_t * vCounts;
Aig_Obj_t * pObj;
int i;
vCounts = Vec_IntStart( Aig_ManObjNumMax(p) );
Saig_ManForEachLi( p, pObj, i )
Vec_IntAddToEntry( vCounts, Aig_ObjFaninId0(pObj), 1 );
return vCounts;
}
/**Function*************************************************************
Synopsis [Returns array of NS variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Llb_DriverCollectNs( Aig_Man_t * pAig, Vec_Int_t * vDriRefs )
{
Vec_Int_t * vVars;
Aig_Obj_t * pObj, * pDri;
int i;
vVars = Vec_IntAlloc( Aig_ManRegNum(pAig) );
Saig_ManForEachLi( pAig, pObj, i )
{
pDri = Aig_ObjFanin0(pObj);
if ( Vec_IntEntry( vDriRefs, Aig_ObjId(pDri) ) != 1 || Saig_ObjIsPi(pAig, pDri) || Aig_ObjIsConst1(pDri) )
Vec_IntPush( vVars, Aig_ObjId(pObj) );
else
Vec_IntPush( vVars, Aig_ObjId(pDri) );
}
return vVars;
}
/**Function*************************************************************
Synopsis [Returns array of CS variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Llb_DriverCollectCs( Aig_Man_t * pAig )
{
Vec_Int_t * vVars;
Aig_Obj_t * pObj;
int i;
vVars = Vec_IntAlloc( Aig_ManRegNum(pAig) );
Saig_ManForEachLo( pAig, pObj, i )
Vec_IntPush( vVars, Aig_ObjId(pObj) );
return vVars;
}
/**Function*************************************************************
Synopsis [Create cube for phase swapping.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Llb_DriverPhaseCube( Aig_Man_t * pAig, Vec_Int_t * vDriRefs, DdManager * dd )
{
DdNode * bCube, * bVar, * bTemp;
Aig_Obj_t * pObj;
int i;
bCube = Cudd_ReadOne( dd ); Cudd_Ref( bCube );
Saig_ManForEachLi( pAig, pObj, i )
{
assert( Vec_IntEntry( vDriRefs, Aig_ObjFaninId0(pObj) ) >= 1 );
if ( Vec_IntEntry( vDriRefs, Aig_ObjFaninId0(pObj) ) != 1 )
continue;
if ( !Aig_ObjFaninC0(pObj) )
continue;
bVar = Cudd_bddIthVar( dd, Aig_ObjFaninId0(pObj) );
bCube = Cudd_bddAnd( dd, bTemp = bCube, bVar ); Cudd_Ref( bCube );
Cudd_RecursiveDeref( dd, bTemp );
}
Cudd_Deref( bCube );
return bCube;
}
/**Function*************************************************************
Synopsis [Compute the last partition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs )
{
int fVerbose = 1;
DdManager * dd;
DdNode * bVar1, * bVar2, * bProd, * bRes, * bTemp;
Aig_Obj_t * pObj;
int i;
dd = Cudd_Init( Aig_ManObjNumMax(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
bRes = Cudd_ReadOne(dd); Cudd_Ref( bRes );
// mark the duplicated flop inputs
Aig_ManForEachNodeVec( p, vVarsNs, pObj, i )
{
if ( !Saig_ObjIsLi(p, pObj) )
continue;
bVar1 = Cudd_bddIthVar( dd, Aig_ObjId(pObj) );
bVar2 = Cudd_bddIthVar( dd, Aig_ObjFaninId0(pObj) );
if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
bVar2 = Cudd_ReadOne(dd);
bVar2 = Cudd_NotCond( bVar2, Aig_ObjFaninC0(pObj) );
bProd = Cudd_bddXnor( dd, bVar1, bVar2 ); Cudd_Ref( bProd );
bRes = Cudd_bddAnd( dd, bTemp = bRes, bProd ); Cudd_Ref( bRes );
Cudd_RecursiveDeref( dd, bTemp );
Cudd_RecursiveDeref( dd, bProd );
}
/*
Saig_ManForEachLi( p, pObj, i )
printf( "%d ", Aig_ObjId(pObj) );
printf( "\n" );
Saig_ManForEachLi( p, pObj, i )
printf( "%c%d ", Aig_ObjFaninC0(pObj)? '-':'+', Aig_ObjFaninId0(pObj) );
printf( "\n" );
*/
Cudd_AutodynDisable( dd );
// Cudd_RecursiveDeref( dd, bRes );
// Extra_StopManager( dd );
dd->bFunc = bRes;
return dd;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

104
src/aig/llb/llb2Dump.c Normal file
View File

@ -0,0 +1,104 @@
/**CFile****************************************************************
FileName [llb2Dump.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [BDD based reachability.]
Synopsis [Dumps the BDD of reached states into a file.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: llb2Dump.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "llbInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Returns a dummy name.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Llb_ManGetDummyName( char * pPrefix, int Num, int nDigits )
{
static char Buffer[2000];
sprintf( Buffer, "%s%0*d", pPrefix, nDigits, Num );
return Buffer;
}
/**Function*************************************************************
Synopsis [Writes reached state BDD into a BLIF file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_ManDumpReached( DdManager * ddG, DdNode * bReached, char * pModel, char * pFileName )
{
FILE * pFile;
Vec_Ptr_t * vNamesIn, * vNamesOut;
char * pName;
int i, nDigits;
// reorder the BDD
Cudd_ReduceHeap( ddG, CUDD_REORDER_SYMM_SIFT, 1 );
// create input names
nDigits = Extra_Base10Log( Cudd_ReadSize(ddG) );
vNamesIn = Vec_PtrAlloc( Cudd_ReadSize(ddG) );
for ( i = 0; i < Cudd_ReadSize(ddG); i++ )
{
pName = Llb_ManGetDummyName( "ff", i, nDigits );
Vec_PtrPush( vNamesIn, Extra_UtilStrsav(pName) );
}
// create output names
vNamesOut = Vec_PtrAlloc( 1 );
Vec_PtrPush( vNamesOut, Extra_UtilStrsav("Reached") );
// write the file
pFile = fopen( pFileName, "wb" );
Cudd_DumpBlif( ddG, 1, &bReached, (char **)Vec_PtrArray(vNamesIn), (char **)Vec_PtrArray(vNamesOut), pModel, pFile );
fclose( pFile );
// cleanup
Vec_PtrForEachEntry( char *, vNamesIn, pName, i )
ABC_FREE( pName );
Vec_PtrForEachEntry( char *, vNamesOut, pName, i )
ABC_FREE( pName );
Vec_PtrFree( vNamesIn );
Vec_PtrFree( vNamesOut );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

1374
src/aig/llb/llb2Flow.c Normal file

File diff suppressed because it is too large Load Diff

440
src/aig/llb/llb2Image.c Normal file
View File

@ -0,0 +1,440 @@
/**CFile****************************************************************
FileName [llb2Image.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [BDD based reachability.]
Synopsis [Computes image using partitioned structure.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: llb2Image.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "llbInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
extern Vec_Ptr_t * Llb_ManCutNodes( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper );
extern Vec_Ptr_t * Llb_ManCutRange( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Computes supports of the partitions.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Llb_ImgSupports( Aig_Man_t * p, Vec_Ptr_t * vDdMans, Vec_Int_t * vStart, Vec_Int_t * vStop, int fAddPis, int fVerbose )
{
Vec_Ptr_t * vSupps;
Vec_Int_t * vOne;
Aig_Obj_t * pObj;
DdManager * dd;
DdNode * bSupp, * bTemp;
int i, Entry, nSize;
nSize = Cudd_ReadSize( (DdManager *)Vec_PtrEntry( vDdMans, 0 ) );
vSupps = Vec_PtrAlloc( 100 );
// create initial
vOne = Vec_IntStart( nSize );
Vec_IntForEachEntry( vStart, Entry, i )
Vec_IntWriteEntry( vOne, Entry, 1 );
Vec_PtrPush( vSupps, vOne );
// create intermediate
Vec_PtrForEachEntry( DdManager *, vDdMans, dd, i )
{
vOne = Vec_IntStart( nSize );
bSupp = Cudd_Support( dd, dd->bFunc ); Cudd_Ref( bSupp );
for ( bTemp = bSupp; bTemp != Cudd_ReadOne(dd); bTemp = cuddT(bTemp) )
Vec_IntWriteEntry( vOne, bTemp->index, 1 );
Cudd_RecursiveDeref( dd, bSupp );
Vec_PtrPush( vSupps, vOne );
}
// create final
vOne = Vec_IntStart( nSize );
Vec_IntForEachEntry( vStop, Entry, i )
Vec_IntWriteEntry( vOne, Entry, 1 );
if ( fAddPis )
Saig_ManForEachPi( p, pObj, i )
Vec_IntWriteEntry( vOne, Aig_ObjId(pObj), 1 );
Vec_PtrPush( vSupps, vOne );
// print supports
assert( nSize == Aig_ManObjNumMax(p) );
if ( fVerbose )
Aig_ManForEachObj( p, pObj, i )
{
int k, Counter = 0;
Vec_PtrForEachEntry( Vec_Int_t *, vSupps, vOne, k )
Counter += Vec_IntEntry(vOne, i);
if ( Counter == 0 )
continue;
printf( "Obj = %4d : ", i );
if ( Saig_ObjIsPi(p,pObj) )
printf( "pi " );
else if ( Saig_ObjIsLo(p,pObj) )
printf( "lo " );
else if ( Saig_ObjIsLi(p,pObj) )
printf( "li " );
else if ( Aig_ObjIsNode(pObj) )
printf( "and " );
Vec_PtrForEachEntry( Vec_Int_t *, vSupps, vOne, k )
printf( "%d", Vec_IntEntry(vOne, i) );
printf( "\n" );
}
return vSupps;
}
/**Function*************************************************************
Synopsis [Computes quantification schedule.]
Description [Input array contains supports: 0=starting, ... intermediate...
N-1=final. Output arrays contain immediately quantifiable vars (vQuant0)
and vars that should be quantified after conjunction (vQuant1).]
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_ImgSchedule( Vec_Ptr_t * vSupps, Vec_Ptr_t ** pvQuant0, Vec_Ptr_t ** pvQuant1, int fVerbose )
{
Vec_Int_t * vOne;
int nVarsAll, Counter, iSupp, Entry, i, k;
// start quantification arrays
*pvQuant0 = Vec_PtrAlloc( Vec_PtrSize(vSupps) );
*pvQuant1 = Vec_PtrAlloc( Vec_PtrSize(vSupps) );
Vec_PtrForEachEntry( Vec_Int_t *, vSupps, vOne, k )
{
Vec_PtrPush( *pvQuant0, Vec_IntAlloc(16) );
Vec_PtrPush( *pvQuant1, Vec_IntAlloc(16) );
}
// count how many times each var appears
nVarsAll = Vec_IntSize( (Vec_Int_t *)Vec_PtrEntry(vSupps, 0) );
for ( i = 0; i < nVarsAll; i++ )
{
Counter = 0;
Vec_PtrForEachEntry( Vec_Int_t *, vSupps, vOne, k )
if ( Vec_IntEntry(vOne, i) )
{
iSupp = k;
Counter++;
}
if ( Counter == 0 )
continue;
if ( Counter == 1 )
Vec_IntPush( (Vec_Int_t *)Vec_PtrEntry(*pvQuant0, iSupp), i );
else // if ( Counter > 1 )
Vec_IntPush( (Vec_Int_t *)Vec_PtrEntry(*pvQuant1, iSupp), i );
}
if ( fVerbose )
for ( i = 0; i < Vec_PtrSize(vSupps); i++ )
{
printf( "%2d : Quant0 = ", i );
Vec_IntForEachEntry( (Vec_Int_t *)Vec_PtrEntry(*pvQuant0, i), Entry, k )
printf( "%d ", Entry );
printf( "\n" );
}
if ( fVerbose )
for ( i = 0; i < Vec_PtrSize(vSupps); i++ )
{
printf( "%2d : Quant1 = ", i );
Vec_IntForEachEntry( (Vec_Int_t *)Vec_PtrEntry(*pvQuant1, i), Entry, k )
printf( "%d ", Entry );
printf( "\n" );
}
}
/**Function*************************************************************
Synopsis [Computes one partition in a separate BDD manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper )
{
Vec_Ptr_t * vNodes, * vRange;
Aig_Obj_t * pObj;
DdManager * dd;
DdNode * bBdd0, * bBdd1, * bProd, * bRes, * bTemp;
int i;
dd = Cudd_Init( Aig_ManObjNumMax(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
Vec_PtrForEachEntry( Aig_Obj_t *, vLower, pObj, i )
pObj->pData = Cudd_bddIthVar( dd, Aig_ObjId(pObj) );
vNodes = Llb_ManCutNodes( p, vLower, vUpper );
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
{
bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( (DdNode *)pObj->pData );
}
vRange = Llb_ManCutRange( p, vLower, vUpper );
bRes = Cudd_ReadOne(dd); Cudd_Ref( bRes );
Vec_PtrForEachEntry( Aig_Obj_t *, vRange, pObj, i )
{
assert( Aig_ObjIsNode(pObj) );
bProd = Cudd_bddXnor( dd, Cudd_bddIthVar(dd, Aig_ObjId(pObj)), (DdNode *)pObj->pData ); Cudd_Ref( bProd );
bRes = Cudd_bddAnd( dd, bTemp = bRes, bProd ); Cudd_Ref( bRes );
Cudd_RecursiveDeref( dd, bTemp );
Cudd_RecursiveDeref( dd, bProd );
}
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
Vec_PtrFree( vRange );
Vec_PtrFree( vNodes );
Cudd_AutodynDisable( dd );
// Cudd_RecursiveDeref( dd, bRes );
// Extra_StopManager( dd );
dd->bFunc = bRes;
return dd;
}
/**Function*************************************************************
Synopsis [Derives positive cube composed of nodes IDs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Llb_ImgComputeCube( Aig_Man_t * pAig, Vec_Int_t * vNodeIds, DdManager * dd )
{
DdNode * bProd, * bTemp;
Aig_Obj_t * pObj;
int i;
bProd = Cudd_ReadOne(dd); Cudd_Ref( bProd );
Aig_ManForEachNodeVec( pAig, vNodeIds, pObj, i )
{
bProd = Cudd_bddAnd( dd, bTemp = bProd, Cudd_bddIthVar(dd, Aig_ObjId(pObj)) ); Cudd_Ref( bProd );
Cudd_RecursiveDeref( dd, bTemp );
}
Cudd_Deref( bProd );
return bProd;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_ImgQuantifyFirst( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, Vec_Ptr_t * vQuant0, int fVerbose )
{
DdManager * dd;
DdNode * bProd, * bRes, * bTemp;
int i, clk = clock();
Vec_PtrForEachEntry( DdManager *, vDdMans, dd, i )
{
// remember unquantified ones
assert( dd->bFunc2 == NULL );
dd->bFunc2 = dd->bFunc; Cudd_Ref( dd->bFunc2 );
Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
bRes = dd->bFunc;
if ( fVerbose )
Abc_Print( 1, "Part %2d : Init =%5d. ", i, Cudd_DagSize(bRes) );
bProd = Llb_ImgComputeCube( pAig, (Vec_Int_t *)Vec_PtrEntry(vQuant0, i+1), dd ); Cudd_Ref( bProd );
bRes = Cudd_bddExistAbstract( dd, bTemp = bRes, bProd ); Cudd_Ref( bRes );
Cudd_RecursiveDeref( dd, bTemp );
Cudd_RecursiveDeref( dd, bProd );
dd->bFunc = bRes;
Cudd_AutodynDisable( dd );
if ( fVerbose )
Abc_Print( 1, "Quant =%5d. ", Cudd_DagSize(bRes) );
Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
if ( fVerbose )
Abc_Print( 1, "Reo = %5d. ", Cudd_DagSize(bRes) );
Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
if ( fVerbose )
Abc_Print( 1, "Reo = %5d. ", Cudd_DagSize(bRes) );
if ( fVerbose )
Abc_Print( 1, "Supp = %3d. ", Cudd_SupportSize(dd, bRes) );
if ( fVerbose )
Abc_PrintTime( 1, "Time", clock() - clk );
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_ImgQuantifyReset( Vec_Ptr_t * vDdMans )
{
DdManager * dd;
int i;
Vec_PtrForEachEntry( DdManager *, vDdMans, dd, i )
{
assert( dd->bFunc2 != NULL );
Cudd_RecursiveDeref( dd, dd->bFunc );
dd->bFunc = dd->bFunc2;
dd->bFunc2 = NULL;
}
}
/**Function*************************************************************
Synopsis [Computes image of the initial set of states.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Llb_ImgComputeImage( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, DdManager * dd, DdNode * bInit,
Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQuant1, Vec_Int_t * vDriRefs,
int TimeTarget, int fBackward, int fReorder, int fVerbose )
{
int fCheckSupport = 0;
DdManager * ddPart;
DdNode * bImage, * bGroup, * bCube, * bTemp;
int i, clk, clk0 = clock();
bImage = bInit; Cudd_Ref( bImage );
if ( fBackward )
{
// change polarity
bCube = Llb_DriverPhaseCube( pAig, vDriRefs, dd ); Cudd_Ref( bCube );
bImage = Extra_bddChangePolarity( dd, bTemp = bImage, bCube ); Cudd_Ref( bImage );
Cudd_RecursiveDeref( dd, bTemp );
Cudd_RecursiveDeref( dd, bCube );
}
else
{
// quantify unique vriables
bCube = Llb_ImgComputeCube( pAig, (Vec_Int_t *)Vec_PtrEntry(vQuant0, 0), dd ); Cudd_Ref( bCube );
bImage = Cudd_bddExistAbstract( dd, bTemp = bImage, bCube ); Cudd_Ref( bImage );
Cudd_RecursiveDeref( dd, bTemp );
Cudd_RecursiveDeref( dd, bCube );
}
// perform image computation
Vec_PtrForEachEntry( DdManager *, vDdMans, ddPart, i )
{
clk = clock();
if ( fVerbose )
printf( " %2d : ", i );
// transfer the BDD from the group manager to the main manager
bGroup = Cudd_bddTransfer( ddPart, dd, ddPart->bFunc ); Cudd_Ref( bGroup );
if ( fVerbose )
printf( "Pt0 =%6d. Pt1 =%6d. ", Cudd_DagSize(ddPart->bFunc), Cudd_DagSize(bGroup) );
// perform partial product
bCube = Llb_ImgComputeCube( pAig, (Vec_Int_t *)Vec_PtrEntry(vQuant1, i+1), dd ); Cudd_Ref( bCube );
bImage = Cudd_bddAndAbstract( dd, bTemp = bImage, bGroup, bCube ); Cudd_Ref( bImage );
if ( fVerbose )
printf( "Im0 =%6d. Im1 =%6d. ", Cudd_DagSize(bTemp), Cudd_DagSize(bImage) );
//printf("\n"); Extra_bddPrintSupport(dd, bImage); printf("\n");
Cudd_RecursiveDeref( dd, bTemp );
Cudd_RecursiveDeref( dd, bCube );
Cudd_RecursiveDeref( dd, bGroup );
// Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
// Abc_Print( 1, "Reo =%6d. ", Cudd_DagSize(bImage) );
// chech runtime
if ( TimeTarget && clock() >= TimeTarget )
{
Cudd_RecursiveDeref( dd, bImage );
return NULL;
}
if ( fVerbose )
printf( "Supp =%3d. ", Cudd_SupportSize(dd, bImage) );
if ( fVerbose )
Abc_PrintTime( 1, "T", clock() - clk );
}
if ( !fBackward )
{
// change polarity
bCube = Llb_DriverPhaseCube( pAig, vDriRefs, dd ); Cudd_Ref( bCube );
bImage = Extra_bddChangePolarity( dd, bTemp = bImage, bCube ); Cudd_Ref( bImage );
Cudd_RecursiveDeref( dd, bTemp );
Cudd_RecursiveDeref( dd, bCube );
}
else
{
// quantify unique vriables
bCube = Llb_ImgComputeCube( pAig, (Vec_Int_t *)Vec_PtrEntry(vQuant0, 0), dd ); Cudd_Ref( bCube );
bImage = Cudd_bddExistAbstract( dd, bTemp = bImage, bCube ); Cudd_Ref( bImage );
Cudd_RecursiveDeref( dd, bTemp );
Cudd_RecursiveDeref( dd, bCube );
}
if ( fReorder )
{
if ( fVerbose )
Abc_Print( 1, " Reordering... Before =%5d. ", Cudd_DagSize(bImage) );
Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
if ( fVerbose )
Abc_Print( 1, "After =%5d. ", Cudd_DagSize(bImage) );
// Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
// Abc_Print( 1, "After =%5d. ", Cudd_DagSize(bImage) );
if ( fVerbose )
Abc_PrintTime( 1, "Time", clock() - clk0 );
// Abc_Print( 1, "\n" );
}
Cudd_Deref( bImage );
return bImage;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

905
src/aig/llb/llb3Image.c Normal file
View File

@ -0,0 +1,905 @@
/**CFile****************************************************************
FileName [llb3Image.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [BDD based reachability.]
Synopsis [Computes image using partitioned structure.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: llb3Image.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "llbInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Llb_Var_t_ Llb_Var_t;
struct Llb_Var_t_
{
int iVar; // variable number
int nScore; // variable score
Vec_Int_t * vParts; // partitions
};
typedef struct Llb_Prt_t_ Llb_Prt_t;
struct Llb_Prt_t_
{
int iPart; // partition number
int nSize; // the number of BDD nodes
DdNode * bFunc; // the partition
Vec_Int_t * vVars; // support
};
typedef struct Llb_Mgr_t_ Llb_Mgr_t;
struct Llb_Mgr_t_
{
Aig_Man_t * pAig; // AIG manager
Vec_Ptr_t * vLeaves; // leaves in the AIG manager
Vec_Ptr_t * vRoots; // roots in the AIG manager
DdManager * dd; // working BDD manager
DdNode * bCurrent; // current state functions in terms of vLeaves
int * pVars2Q; // variables to quantify
// internal
Llb_Prt_t ** pParts; // partitions
Llb_Var_t ** pVars; // variables
int iPartFree; // next free partition
int nVars; // the number of BDD variables
int nSuppMax; // maximum support size
// temporary
int * pSupp; // temporary support storage
};
static inline Llb_Var_t * Llb_MgrVar( Llb_Mgr_t * p, int i ) { return p->pVars[i]; }
static inline Llb_Prt_t * Llb_MgrPart( Llb_Mgr_t * p, int i ) { return p->pParts[i]; }
// iterator over vars
#define Llb_MgrForEachVar( p, pVar, i ) \
for ( i = 0; (i < p->nVars) && (((pVar) = Llb_MgrVar(p, i)), 1); i++ ) if ( pVar == NULL ) {} else
// iterator over parts
#define Llb_MgrForEachPart( p, pPart, i ) \
for ( i = 0; (i < p->iPartFree) && (((pPart) = Llb_MgrPart(p, i)), 1); i++ ) if ( pPart == NULL ) {} else
// iterator over vars of one partition
#define Llb_PartForEachVar( p, pPart, pVar, i ) \
for ( i = 0; (i < Vec_IntSize(pPart->vVars)) && (((pVar) = Llb_MgrVar(p, Vec_IntEntry(pPart->vVars,i))), 1); i++ )
// iterator over parts of one variable
#define Llb_VarForEachPart( p, pVar, pPart, i ) \
for ( i = 0; (i < Vec_IntSize(pVar->vParts)) && (((pPart) = Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,i))), 1); i++ )
// statistics
int timeBuild, timeAndEx, timeOther;
int nSuppMax;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Removes one variable.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinRemoveVar( Llb_Mgr_t * p, Llb_Var_t * pVar )
{
assert( p->pVars[pVar->iVar] == pVar );
p->pVars[pVar->iVar] = NULL;
Vec_IntFree( pVar->vParts );
ABC_FREE( pVar );
}
/**Function*************************************************************
Synopsis [Removes one partition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinRemovePart( Llb_Mgr_t * p, Llb_Prt_t * pPart )
{
assert( p->pParts[pPart->iPart] == pPart );
p->pParts[pPart->iPart] = NULL;
Vec_IntFree( pPart->vVars );
Cudd_RecursiveDeref( p->dd, pPart->bFunc );
ABC_FREE( pPart );
}
/**Function*************************************************************
Synopsis [Create cube with singleton variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Llb_NonlinCreateCube1( Llb_Mgr_t * p, Llb_Prt_t * pPart )
{
DdNode * bCube, * bTemp;
Llb_Var_t * pVar;
int i;
bCube = Cudd_ReadOne(p->dd); Cudd_Ref( bCube );
Llb_PartForEachVar( p, pPart, pVar, i )
{
assert( Vec_IntSize(pVar->vParts) > 0 );
if ( Vec_IntSize(pVar->vParts) != 1 )
continue;
assert( Vec_IntEntry(pVar->vParts, 0) == pPart->iPart );
bCube = Cudd_bddAnd( p->dd, bTemp = bCube, Cudd_bddIthVar(p->dd, pVar->iVar) ); Cudd_Ref( bCube );
Cudd_RecursiveDeref( p->dd, bTemp );
}
Cudd_Deref( bCube );
return bCube;
}
/**Function*************************************************************
Synopsis [Create cube of variables appearing only in two partitions.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Llb_NonlinCreateCube2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2 )
{
DdNode * bCube, * bTemp;
Llb_Var_t * pVar;
int i;
bCube = Cudd_ReadOne(p->dd); Cudd_Ref( bCube );
Llb_PartForEachVar( p, pPart1, pVar, i )
{
assert( Vec_IntSize(pVar->vParts) > 0 );
if ( Vec_IntSize(pVar->vParts) != 2 )
continue;
if ( (Vec_IntEntry(pVar->vParts, 0) == pPart1->iPart && Vec_IntEntry(pVar->vParts, 1) == pPart2->iPart) ||
(Vec_IntEntry(pVar->vParts, 0) == pPart2->iPart && Vec_IntEntry(pVar->vParts, 1) == pPart1->iPart) )
{
bCube = Cudd_bddAnd( p->dd, bTemp = bCube, Cudd_bddIthVar(p->dd, pVar->iVar) ); Cudd_Ref( bCube );
Cudd_RecursiveDeref( p->dd, bTemp );
}
}
Cudd_Deref( bCube );
return bCube;
}
/**Function*************************************************************
Synopsis [Returns 1 if partition has singleton variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_NonlinHasSingletonVars( Llb_Mgr_t * p, Llb_Prt_t * pPart )
{
Llb_Var_t * pVar;
int i;
Llb_PartForEachVar( p, pPart, pVar, i )
if ( Vec_IntSize(pVar->vParts) == 1 )
return 1;
return 0;
}
/**Function*************************************************************
Synopsis [Returns 1 if partition has singleton variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinPrint( Llb_Mgr_t * p )
{
Llb_Prt_t * pPart;
Llb_Var_t * pVar;
int i, k;
printf( "\n" );
Llb_MgrForEachVar( p, pVar, i )
{
printf( "Var %3d : ", i );
Llb_VarForEachPart( p, pVar, pPart, k )
printf( "%d ", pPart->iPart );
printf( "\n" );
}
Llb_MgrForEachPart( p, pPart, i )
{
printf( "Part %3d : ", i );
Llb_PartForEachVar( p, pPart, pVar, k )
printf( "%d ", pVar->iVar );
printf( "\n" );
}
}
/**Function*************************************************************
Synopsis [Quantifies singles belonging to one partition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_NonlinQuantify1( Llb_Mgr_t * p, Llb_Prt_t * pPart, int fSubset )
{
Llb_Var_t * pVar;
Llb_Prt_t * pTemp;
Vec_Ptr_t * vSingles;
DdNode * bCube, * bTemp;
int i, RetValue, nSizeNew;
if ( fSubset )
{
int Length;
// int nSuppSize = Cudd_SupportSize( p->dd, pPart->bFunc );
// pPart->bFunc = Cudd_SubsetHeavyBranch( p->dd, bTemp = pPart->bFunc, nSuppSize, 3*pPart->nSize/4 ); Cudd_Ref( pPart->bFunc );
pPart->bFunc = Cudd_LargestCube( p->dd, bTemp = pPart->bFunc, &Length ); Cudd_Ref( pPart->bFunc );
printf( "Subsetting %3d : ", pPart->iPart );
printf( "(Supp =%3d Node =%5d) -> ", Cudd_SupportSize(p->dd, bTemp), Cudd_DagSize(bTemp) );
printf( "(Supp =%3d Node =%5d)\n", Cudd_SupportSize(p->dd, pPart->bFunc), Cudd_DagSize(pPart->bFunc) );
RetValue = (Cudd_DagSize(bTemp) == Cudd_DagSize(pPart->bFunc));
Cudd_RecursiveDeref( p->dd, bTemp );
if ( RetValue )
return 1;
}
else
{
// create cube to be quantified
bCube = Llb_NonlinCreateCube1( p, pPart ); Cudd_Ref( bCube );
// assert( !Cudd_IsConstant(bCube) );
// derive new function
pPart->bFunc = Cudd_bddExistAbstract( p->dd, bTemp = pPart->bFunc, bCube ); Cudd_Ref( pPart->bFunc );
Cudd_RecursiveDeref( p->dd, bTemp );
Cudd_RecursiveDeref( p->dd, bCube );
}
// get support
vSingles = Vec_PtrAlloc( 0 );
nSizeNew = Cudd_DagSize(pPart->bFunc);
Extra_SupportArray( p->dd, pPart->bFunc, p->pSupp );
Llb_PartForEachVar( p, pPart, pVar, i )
if ( p->pSupp[pVar->iVar] )
{
assert( Vec_IntSize(pVar->vParts) > 1 );
pVar->nScore -= pPart->nSize - nSizeNew;
}
else
{
RetValue = Vec_IntRemove( pVar->vParts, pPart->iPart );
assert( RetValue );
pVar->nScore -= pPart->nSize;
if ( Vec_IntSize(pVar->vParts) == 0 )
Llb_NonlinRemoveVar( p, pVar );
else if ( Vec_IntSize(pVar->vParts) == 1 )
Vec_PtrPushUnique( vSingles, Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0)) );
}
// update partition
pPart->nSize = nSizeNew;
Vec_IntClear( pPart->vVars );
for ( i = 0; i < p->nVars; i++ )
if ( p->pSupp[i] && p->pVars2Q[i] )
Vec_IntPush( pPart->vVars, i );
// remove other variables
Vec_PtrForEachEntry( Llb_Prt_t *, vSingles, pTemp, i )
Llb_NonlinQuantify1( p, pTemp, 0 );
Vec_PtrFree( vSingles );
return 0;
}
/**Function*************************************************************
Synopsis [Quantifies singles belonging to one partition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_NonlinQuantify2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2, int Limit )
{
int fVerbose = 0;
Llb_Var_t * pVar;
Llb_Prt_t * pTemp;
Vec_Ptr_t * vSingles;
DdNode * bCube, * bFunc;
int i, RetValue, nSuppSize;
int iPart1 = pPart1->iPart;
int iPart2 = pPart2->iPart;
// create cube to be quantified
bCube = Llb_NonlinCreateCube2( p, pPart1, pPart2 ); Cudd_Ref( bCube );
if ( fVerbose )
{
printf( "\n" );
printf( "\n" );
Llb_NonlinPrint( p );
printf( "Conjoining partitions %d and %d.\n", pPart1->iPart, pPart2->iPart );
Extra_bddPrintSupport( p->dd, bCube ); printf( "\n" );
}
// derive new function
// bFunc = Cudd_bddAndAbstract( p->dd, pPart1->bFunc, pPart2->bFunc, bCube ); Cudd_Ref( bFunc );
bFunc = Cudd_bddAndAbstractLimit( p->dd, pPart1->bFunc, pPart2->bFunc, bCube, Limit );
if ( bFunc == NULL )
{
/*
int RetValue;
Cudd_RecursiveDeref( p->dd, bCube );
if ( pPart1->nSize < pPart2->nSize )
RetValue = Llb_NonlinQuantify1( p, pPart1, 1 );
else
RetValue = Llb_NonlinQuantify1( p, pPart2, 1 );
if ( RetValue )
Limit = Limit + 1000;
Llb_NonlinQuantify2( p, pPart1, pPart2, Limit );
*/
return 1;
}
Cudd_Ref( bFunc );
Cudd_RecursiveDeref( p->dd, bCube );
// create new partition
pTemp = p->pParts[p->iPartFree] = ABC_CALLOC( Llb_Prt_t, 1 );
pTemp->iPart = p->iPartFree++;
pTemp->nSize = Cudd_DagSize(bFunc);
pTemp->bFunc = bFunc;
pTemp->vVars = Vec_IntAlloc( 8 );
// update variables
Llb_PartForEachVar( p, pPart1, pVar, i )
{
RetValue = Vec_IntRemove( pVar->vParts, pPart1->iPart );
assert( RetValue );
pVar->nScore -= pPart1->nSize;
}
// update variables
Llb_PartForEachVar( p, pPart2, pVar, i )
{
RetValue = Vec_IntRemove( pVar->vParts, pPart2->iPart );
assert( RetValue );
pVar->nScore -= pPart2->nSize;
}
// add variables to the new partition
nSuppSize = 0;
Extra_SupportArray( p->dd, bFunc, p->pSupp );
for ( i = 0; i < p->nVars; i++ )
{
nSuppSize += p->pSupp[i];
if ( p->pSupp[i] && p->pVars2Q[i] )
{
pVar = Llb_MgrVar( p, i );
pVar->nScore += pTemp->nSize;
Vec_IntPush( pVar->vParts, pTemp->iPart );
Vec_IntPush( pTemp->vVars, i );
}
}
p->nSuppMax = ABC_MAX( p->nSuppMax, nSuppSize );
// remove variables and collect partitions with singleton variables
vSingles = Vec_PtrAlloc( 0 );
Llb_PartForEachVar( p, pPart1, pVar, i )
{
if ( Vec_IntSize(pVar->vParts) == 0 )
Llb_NonlinRemoveVar( p, pVar );
else if ( Vec_IntSize(pVar->vParts) == 1 )
{
if ( fVerbose )
printf( "Adding partition %d because of var %d.\n",
Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0))->iPart, pVar->iVar );
Vec_PtrPushUnique( vSingles, Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0)) );
}
}
Llb_PartForEachVar( p, pPart2, pVar, i )
{
if ( pVar == NULL )
continue;
if ( Vec_IntSize(pVar->vParts) == 0 )
Llb_NonlinRemoveVar( p, pVar );
else if ( Vec_IntSize(pVar->vParts) == 1 )
{
if ( fVerbose )
printf( "Adding partition %d because of var %d.\n",
Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0))->iPart, pVar->iVar );
Vec_PtrPushUnique( vSingles, Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0)) );
}
}
// remove partitions
Llb_NonlinRemovePart( p, pPart1 );
Llb_NonlinRemovePart( p, pPart2 );
// remove other variables
if ( fVerbose )
Llb_NonlinPrint( p );
Vec_PtrForEachEntry( Llb_Prt_t *, vSingles, pTemp, i )
{
if ( fVerbose )
printf( "Updating partitiong %d with singlton vars.\n", pTemp->iPart );
Llb_NonlinQuantify1( p, pTemp, 0 );
}
if ( fVerbose )
Llb_NonlinPrint( p );
Vec_PtrFree( vSingles );
return 0;
}
/**Function*************************************************************
Synopsis [Computes volume of the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinCutNodes_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
{
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
return;
Aig_ObjSetTravIdCurrent(p, pObj);
if ( Saig_ObjIsLi(p, pObj) )
{
Llb_NonlinCutNodes_rec(p, Aig_ObjFanin0(pObj), vNodes);
return;
}
if ( Aig_ObjIsConst1(pObj) )
return;
assert( Aig_ObjIsNode(pObj) );
Llb_NonlinCutNodes_rec(p, Aig_ObjFanin0(pObj), vNodes);
Llb_NonlinCutNodes_rec(p, Aig_ObjFanin1(pObj), vNodes);
Vec_PtrPush( vNodes, pObj );
}
/**Function*************************************************************
Synopsis [Computes volume of the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Llb_NonlinCutNodes( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper )
{
Vec_Ptr_t * vNodes;
Aig_Obj_t * pObj;
int i;
// mark the lower cut with the traversal ID
Aig_ManIncrementTravId(p);
Vec_PtrForEachEntry( Aig_Obj_t *, vLower, pObj, i )
Aig_ObjSetTravIdCurrent( p, pObj );
// count the upper cut
vNodes = Vec_PtrAlloc( 100 );
Vec_PtrForEachEntry( Aig_Obj_t *, vUpper, pObj, i )
Llb_NonlinCutNodes_rec( p, pObj, vNodes );
return vNodes;
}
/**Function*************************************************************
Synopsis [Returns array of BDDs for the roots in terms of the leaves.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Llb_NonlinBuildBdds( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, DdManager * dd )
{
Vec_Ptr_t * vNodes, * vResult;
Aig_Obj_t * pObj;
DdNode * bBdd0, * bBdd1, * bProd;
int i;
Aig_ManConst1(p)->pData = Cudd_ReadOne( dd );
Vec_PtrForEachEntry( Aig_Obj_t *, vLower, pObj, i )
pObj->pData = Cudd_bddIthVar( dd, Aig_ObjId(pObj) );
vNodes = Llb_NonlinCutNodes( p, vLower, vUpper );
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
{
bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( (DdNode *)pObj->pData );
}
vResult = Vec_PtrAlloc( 100 );
Vec_PtrForEachEntry( Aig_Obj_t *, vUpper, pObj, i )
{
if ( Aig_ObjIsNode(pObj) )
{
bProd = Cudd_bddXnor( dd, Cudd_bddIthVar(dd, Aig_ObjId(pObj)), (DdNode *)pObj->pData ); Cudd_Ref( bProd );
}
else
{
assert( Saig_ObjIsLi(p, pObj) );
bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
bProd = Cudd_bddXnor( dd, Cudd_bddIthVar(dd, Aig_ObjId(pObj)), bBdd0 ); Cudd_Ref( bProd );
}
Vec_PtrPush( vResult, bProd );
}
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
Vec_PtrFree( vNodes );
return vResult;
}
/**Function*************************************************************
Synopsis [Starts non-linear quantification scheduling.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinAddPair( Llb_Mgr_t * p, DdNode * bFunc, int iPart, int iVar )
{
if ( p->pVars[iVar] == NULL )
{
p->pVars[iVar] = ABC_CALLOC( Llb_Var_t, 1 );
p->pVars[iVar]->iVar = iVar;
p->pVars[iVar]->nScore = 0;
p->pVars[iVar]->vParts = Vec_IntAlloc( 8 );
}
Vec_IntPush( p->pVars[iVar]->vParts, iPart );
Vec_IntPush( p->pParts[iPart]->vVars, iVar );
}
/**Function*************************************************************
Synopsis [Starts non-linear quantification scheduling.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinStart( Llb_Mgr_t * p )
{
Vec_Ptr_t * vRootBdds;
Llb_Prt_t * pPart;
DdNode * bFunc;
int i, k, nSuppSize;
// create and collect BDDs
vRootBdds = Llb_NonlinBuildBdds( p->pAig, p->vLeaves, p->vRoots, p->dd ); // come referenced
Vec_PtrPush( vRootBdds, p->bCurrent );
// add pairs (refs are consumed inside)
Vec_PtrForEachEntry( DdNode *, vRootBdds, bFunc, i )
{
assert( !Cudd_IsConstant(bFunc) );
// create partition
p->pParts[i] = ABC_CALLOC( Llb_Prt_t, 1 );
p->pParts[i]->iPart = i;
p->pParts[i]->bFunc = bFunc;
p->pParts[i]->vVars = Vec_IntAlloc( 8 );
// add support dependencies
nSuppSize = 0;
Extra_SupportArray( p->dd, bFunc, p->pSupp );
for ( k = 0; k < p->nVars; k++ )
{
nSuppSize += p->pSupp[k];
if ( p->pSupp[k] && p->pVars2Q[k] )
Llb_NonlinAddPair( p, bFunc, i, k );
}
p->nSuppMax = ABC_MAX( p->nSuppMax, nSuppSize );
}
Vec_PtrFree( vRootBdds );
// remove singles
Llb_MgrForEachPart( p, pPart, i )
if ( Llb_NonlinHasSingletonVars(p, pPart) )
Llb_NonlinQuantify1( p, pPart, 0 );
}
/**Function*************************************************************
Synopsis [Checks that each var appears in at least one partition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinCheckVars( Llb_Mgr_t * p )
{
Llb_Var_t * pVar;
int i;
Llb_MgrForEachVar( p, pVar, i )
assert( Vec_IntSize(pVar->vParts) > 1 );
}
/**Function*************************************************************
Synopsis [Find next partition to quantify]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_NonlinNextPartitions( Llb_Mgr_t * p, Llb_Prt_t ** ppPart1, Llb_Prt_t ** ppPart2 )
{
Llb_Var_t * pVar, * pVarBest = NULL;
Llb_Prt_t * pPart, * pPart1Best = NULL, * pPart2Best = NULL;
int i;
Llb_NonlinCheckVars( p );
// find variable with minimum score
Llb_MgrForEachVar( p, pVar, i )
if ( pVarBest == NULL || pVarBest->nScore > pVar->nScore )
pVarBest = pVar;
if ( pVarBest == NULL )
return 0;
// find two partitions with minimum size
Llb_VarForEachPart( p, pVarBest, pPart, i )
{
if ( pPart1Best == NULL )
pPart1Best = pPart;
else if ( pPart2Best == NULL )
pPart2Best = pPart;
else if ( pPart1Best->nSize > pPart->nSize || pPart2Best->nSize > pPart->nSize )
{
if ( pPart1Best->nSize > pPart2Best->nSize )
pPart1Best = pPart;
else
pPart2Best = pPart;
}
}
*ppPart1 = pPart1Best;
*ppPart2 = pPart2Best;
return 1;
}
/**Function*************************************************************
Synopsis [Reorders BDDs in the working manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinReorder( DdManager * dd, int fVerbose )
{
int clk = clock();
if ( fVerbose )
Abc_Print( 1, "Reordering... Before =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
if ( fVerbose )
Abc_Print( 1, "After =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
if ( fVerbose )
Abc_Print( 1, "After =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
if ( fVerbose )
Abc_PrintTime( 1, "Time", clock() - clk );
}
/**Function*************************************************************
Synopsis [Recomputes scores after variable reordering.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinRecomputeScores( Llb_Mgr_t * p )
{
Llb_Prt_t * pPart;
Llb_Var_t * pVar;
int i, k;
Llb_MgrForEachPart( p, pPart, i )
pPart->nSize = Cudd_DagSize(pPart->bFunc);
Llb_MgrForEachVar( p, pVar, i )
{
pVar->nScore = 0;
Llb_VarForEachPart( p, pVar, pPart, k )
pVar->nScore += pPart->nSize;
}
}
/**Function*************************************************************
Synopsis [Recomputes scores after variable reordering.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinVerifyScores( Llb_Mgr_t * p )
{
Llb_Prt_t * pPart;
Llb_Var_t * pVar;
int i, k, nScore;
Llb_MgrForEachPart( p, pPart, i )
assert( pPart->nSize == Cudd_DagSize(pPart->bFunc) );
Llb_MgrForEachVar( p, pVar, i )
{
nScore = 0;
Llb_VarForEachPart( p, pVar, pPart, k )
nScore += pPart->nSize;
assert( nScore == pVar->nScore );
}
}
/**Function*************************************************************
Synopsis [Starts non-linear quantification scheduling.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Llb_Mgr_t * Llb_NonlinAlloc( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, DdManager * dd, DdNode * bCurrent )
{
Llb_Mgr_t * p;
p = ABC_CALLOC( Llb_Mgr_t, 1 );
p->pAig = pAig;
p->vLeaves = vLeaves;
p->vRoots = vRoots;
p->dd = dd;
p->bCurrent = bCurrent;
p->pVars2Q = pVars2Q;
p->nVars = Cudd_ReadSize(dd);
p->iPartFree = Vec_PtrSize(vRoots) + 1;
p->pVars = ABC_CALLOC( Llb_Var_t *, p->nVars );
p->pParts = ABC_CALLOC( Llb_Prt_t *, 2 * p->iPartFree );
p->pSupp = ABC_ALLOC( int, Cudd_ReadSize(dd) );
return p;
}
/**Function*************************************************************
Synopsis [Stops non-linear quantification scheduling.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinFree( Llb_Mgr_t * p )
{
Llb_Prt_t * pPart;
Llb_Var_t * pVar;
int i;
Llb_MgrForEachVar( p, pVar, i )
Llb_NonlinRemoveVar( p, pVar );
Llb_MgrForEachPart( p, pPart, i )
Llb_NonlinRemovePart( p, pPart );
ABC_FREE( p->pVars );
ABC_FREE( p->pParts );
ABC_FREE( p->pSupp );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis [Performs image computation.]
Description [Computes image of BDDs (vFuncs).]
SideEffects [BDDs in vFuncs are derefed inside. The result is refed.]
SeeAlso []
***********************************************************************/
DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q,
DdManager * dd, DdNode * bCurrent, int fReorder, int fVerbose, int * pOrder, int Limit )
{
Llb_Prt_t * pPart, * pPart1, * pPart2;
Llb_Mgr_t * p;
DdNode * bFunc, * bTemp;
int i, nReorders, timeInside;
int clk = clock(), clk2;
// start the manager
clk2 = clock();
p = Llb_NonlinAlloc( pAig, vLeaves, vRoots, pVars2Q, dd, bCurrent );
Llb_NonlinStart( p );
timeBuild += clock() - clk2;
timeInside = clock() - clk2;
// compute scores
Llb_NonlinRecomputeScores( p );
// save permutation
memcpy( pOrder, dd->invperm, sizeof(int) * dd->size );
// iteratively quantify variables
while ( Llb_NonlinNextPartitions(p, &pPart1, &pPart2) )
{
clk2 = clock();
nReorders = Cudd_ReadReorderings(dd);
if ( Llb_NonlinQuantify2( p, pPart1, pPart2, Limit ) )
{
Llb_NonlinFree( p );
return NULL;
}
timeAndEx += clock() - clk2;
timeInside += clock() - clk2;
if ( nReorders < Cudd_ReadReorderings(dd) )
Llb_NonlinRecomputeScores( p );
// else
// Llb_NonlinVerifyScores( p );
}
// load partitions
bFunc = Cudd_ReadOne(p->dd); Cudd_Ref( bFunc );
Llb_MgrForEachPart( p, pPart, i )
{
bFunc = Cudd_bddAnd( p->dd, bTemp = bFunc, pPart->bFunc ); Cudd_Ref( bFunc );
Cudd_RecursiveDeref( p->dd, bTemp );
}
nSuppMax = p->nSuppMax;
Llb_NonlinFree( p );
// reorder variables
if ( fReorder )
Llb_NonlinReorder( dd, fVerbose );
timeOther += clock() - clk - timeInside;
// return
Cudd_Deref( bFunc );
return bFunc;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

711
src/aig/llb/llb3Nonlin.c Normal file
View File

@ -0,0 +1,711 @@
/**CFile****************************************************************
FileName [llb2Nonlin.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [BDD based reachability.]
Synopsis [Non-linear quantification scheduling.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: llb2Nonlin.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "llbInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Llb_Mnn_t_ Llb_Mnn_t;
struct Llb_Mnn_t_
{
Aig_Man_t * pInit; // AIG manager
Aig_Man_t * pAig; // AIG manager
Gia_ParLlb_t * pPars; // parameters
DdManager * dd; // BDD manager
DdManager * ddG; // BDD manager
DdManager * ddR; // BDD manager
Vec_Ptr_t * vRings; // onion rings in ddR
Vec_Ptr_t * vLeaves;
Vec_Ptr_t * vRoots;
int * pVars2Q;
int * pOrder;
Vec_Int_t * vCs2Glo; // cur state variables into global variables
Vec_Int_t * vNs2Glo; // next state variables into global variables
Vec_Int_t * vGlo2Cs; // global variables into cur state variables
Vec_Int_t * vGlo2Ns; // global variables into next state variables
int timeImage;
int timeTran1;
int timeTran2;
int timeGloba;
int timeOther;
int timeTotal;
int timeReo;
int timeReoG;
};
extern int timeBuild, timeAndEx, timeOther;
extern int nSuppMax;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Finds variable whose 0-cofactor is the smallest.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_NonlinFindBestVar( DdManager * dd, DdNode * bFunc, Aig_Man_t * pAig )
{
Aig_Obj_t * pObj;
// Vec_Int_t * vVars;
DdNode * bCof, * bVar, * bTemp;
int i, iVar, iVarBest = -1, iValue, iValueBest = ABC_INFINITY;
int Size, Size0, Size1;
int clk = clock();
// vVars = Vec_IntStartNatural( Cudd_ReadSize(dd) );
printf( "Original = %6d. SuppSize = %3d. Vars = %3d.\n",
Size = Cudd_DagSize(bFunc), Cudd_SupportSize(dd, bFunc), Aig_ManRegNum(pAig) );
// Vec_IntForEachEntry( vVars, iVar, i )
Saig_ManForEachLo( pAig, pObj, i )
{
iVar = Aig_ObjId(pObj);
/*
printf( "Var =%3d : ", iVar );
bVar = Cudd_bddIthVar(dd, iVar);
bCof = Cudd_Cofactor( dd, bFunc, Cudd_Not(bVar) ); Cudd_Ref( bCof );
// bCof = Cudd_bddAnd( dd, bTemp = bCof, Cudd_Not(bVar) ); Cudd_Ref( bCof );
// Cudd_RecursiveDeref( dd, bTemp );
printf( "Supp0 =%3d ", Cudd_SupportSize(dd, bCof) );
printf( "Size0 =%6d ", Size0 = Cudd_DagSize(bCof) );
Cudd_RecursiveDeref( dd, bCof );
bCof = Cudd_Cofactor( dd, bFunc, bVar ); Cudd_Ref( bCof );
// bCof = Cudd_bddAnd( dd, bTemp = bCof, bVar ); Cudd_Ref( bCof );
// Cudd_RecursiveDeref( dd, bTemp );
printf( "Supp1 =%3d ", Cudd_SupportSize(dd, bCof) );
printf( "Size1 =%6d ", Size1 = Cudd_DagSize(bCof) );
Cudd_RecursiveDeref( dd, bCof );
printf( "D =%6d ", Size0 + Size1 - Size );
printf( "B =%6d\n", ABC_MAX(Size0, Size1) - ABC_MIN(Size0, Size1) );
*/
// printf( "Var =%3d : ", iVar );
bVar = Cudd_bddIthVar(dd, iVar);
bCof = Cudd_Cofactor( dd, bFunc, Cudd_Not(bVar) ); Cudd_Ref( bCof );
bCof = Cudd_bddAnd( dd, bTemp = bCof, Cudd_Not(bVar) ); Cudd_Ref( bCof );
Cudd_RecursiveDeref( dd, bTemp );
Size0 = Cudd_DagSize(bCof);
// printf( "Supp0 =%3d ", Cudd_SupportSize(dd, bCof) );
// printf( "Size0 =%6d ", Size0 );
Cudd_RecursiveDeref( dd, bCof );
bCof = Cudd_Cofactor( dd, bFunc, bVar ); Cudd_Ref( bCof );
bCof = Cudd_bddAnd( dd, bTemp = bCof, bVar ); Cudd_Ref( bCof );
Cudd_RecursiveDeref( dd, bTemp );
Size1 = Cudd_DagSize(bCof);
// printf( "Supp1 =%3d ", Cudd_SupportSize(dd, bCof) );
// printf( "Size1 =%6d ", Size1 );
Cudd_RecursiveDeref( dd, bCof );
iValue = ABC_MAX(Size0, Size1) - ABC_MIN(Size0, Size1) + Size0 + Size1 - Size;
// printf( "D =%6d ", Size0 + Size1 - Size );
// printf( "B =%6d ", ABC_MAX(Size0, Size1) - ABC_MIN(Size0, Size1) );
// printf( "S =%6d\n", iValue );
if ( iValueBest > iValue )
{
iValueBest = iValue;
iVarBest = i;
}
}
// Vec_IntFree( vVars );
printf( "Best var = %d. Best value = %d. ", iVarBest, iValueBest );
Abc_PrintTime( 1, "Time", clock() - clk );
return iVarBest;
}
/**Function*************************************************************
Synopsis [Finds variable whose 0-cofactor is the smallest.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinTrySubsetting( DdManager * dd, DdNode * bFunc )
{
DdNode * bNew;
printf( "Original = %6d. SuppSize = %3d. ",
Cudd_DagSize(bFunc), Cudd_SupportSize(dd, bFunc) );
bNew = Cudd_SubsetHeavyBranch( dd, bFunc, Cudd_SupportSize(dd, bFunc), 1000 ); Cudd_Ref( bNew );
printf( "Result = %6d. SuppSize = %3d.\n",
Cudd_DagSize(bNew), Cudd_SupportSize(dd, bNew) );
Cudd_RecursiveDeref( dd, bNew );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinPrepareVarMap( Llb_Mnn_t * p )
{
Aig_Obj_t * pObjLi, * pObjLo, * pObj;
int i, iVarLi, iVarLo;
p->vCs2Glo = Vec_IntStartFull( Aig_ManObjNumMax(p->pAig) );
p->vNs2Glo = Vec_IntStartFull( Aig_ManObjNumMax(p->pAig) );
p->vGlo2Cs = Vec_IntStartFull( Aig_ManRegNum(p->pAig) );
p->vGlo2Ns = Vec_IntStartFull( Aig_ManRegNum(p->pAig) );
Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
{
iVarLi = Aig_ObjId(pObjLi);
iVarLo = Aig_ObjId(pObjLo);
assert( iVarLi >= 0 && iVarLi < Aig_ManObjNumMax(p->pAig) );
assert( iVarLo >= 0 && iVarLo < Aig_ManObjNumMax(p->pAig) );
Vec_IntWriteEntry( p->vCs2Glo, iVarLo, i );
Vec_IntWriteEntry( p->vNs2Glo, iVarLi, i );
Vec_IntWriteEntry( p->vGlo2Cs, i, iVarLo );
Vec_IntWriteEntry( p->vGlo2Ns, i, iVarLi );
}
// add mapping of the PIs
Saig_ManForEachPi( p->pAig, pObj, i )
{
Vec_IntWriteEntry( p->vCs2Glo, Aig_ObjId(pObj), Aig_ManRegNum(p->pAig)+i );
Vec_IntWriteEntry( p->vNs2Glo, Aig_ObjId(pObj), Aig_ManRegNum(p->pAig)+i );
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd )
{
Aig_Obj_t * pObj;
DdNode * bRes, * bVar, * bTemp;
int i, iVar;
bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes );
Saig_ManForEachLo( pAig, pObj, i )
{
iVar = (Cudd_ReadSize(dd) == Aig_ManRegNum(pAig)) ? i : Aig_ObjId(pObj);
bVar = Cudd_bddIthVar( dd, iVar );
bRes = Cudd_bddAnd( dd, bTemp = bRes, Cudd_Not(bVar) ); Cudd_Ref( bRes );
Cudd_RecursiveDeref( dd, bTemp );
}
Cudd_Deref( bRes );
return bRes;
}
/**Function*************************************************************
Synopsis [Derives counter-example by backward reachability.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Llb_NonlinDeriveCex( Llb_Mnn_t * p )
{
extern Abc_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames );
extern int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p );
Abc_Cex_t * pCex;
Aig_Obj_t * pObj;
Vec_Int_t * vVarsNs;
DdNode * bState, * bImage, * bOneCube, * bTemp, * bRing;
int i, v, RetValue, nPiOffset;
char * pValues = ABC_ALLOC( char, Cudd_ReadSize(p->ddR) );
assert( Vec_PtrSize(p->vRings) > 0 );
// update quantifiable vars
memset( p->pVars2Q, 0, sizeof(int) * Cudd_ReadSize(p->dd) );
vVarsNs = Vec_IntAlloc( Aig_ManRegNum(p->pAig) );
Saig_ManForEachLi( p->pAig, pObj, i )
{
p->pVars2Q[Aig_ObjId(pObj)] = 1;
Vec_IntPush( vVarsNs, Aig_ObjId(pObj) );
}
// allocate room for the counter-example
pCex = Ssw_SmlAllocCounterExample( Saig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Vec_PtrSize(p->vRings) );
pCex->iFrame = Vec_PtrSize(p->vRings) - 1;
pCex->iPo = -1;
// get the last cube
bOneCube = Cudd_bddIntersect( p->ddR, Vec_PtrEntryLast(p->vRings), p->ddR->bFunc ); Cudd_Ref( bOneCube );
RetValue = Cudd_bddPickOneCube( p->ddR, bOneCube, pValues );
Cudd_RecursiveDeref( p->ddR, bOneCube );
assert( RetValue );
// write PIs of counter-example
nPiOffset = Saig_ManRegNum(p->pAig) + Saig_ManPiNum(p->pAig) * (Vec_PtrSize(p->vRings) - 1);
Saig_ManForEachPi( p->pAig, pObj, i )
if ( pValues[Saig_ManRegNum(p->pAig)+i] == 1 )
Aig_InfoSetBit( pCex->pData, nPiOffset + i );
// write state in terms of NS variables
if ( Vec_PtrSize(p->vRings) > 1 )
{
bState = Llb_CoreComputeCube( p->dd, vVarsNs, 1, pValues ); Cudd_Ref( bState );
}
// perform backward analysis
Vec_PtrForEachEntryReverse( DdNode *, p->vRings, bRing, v )
{
if ( v == Vec_PtrSize(p->vRings) - 1 )
continue;
// compute the next states
bImage = Llb_NonlinImage( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->dd, bState,
p->pPars->fReorder, p->pPars->fVeryVerbose, p->pOrder, ABC_INFINITY ); // consumed reference
assert( bImage != NULL );
Cudd_Ref( bImage );
//Extra_bddPrintSupport( p->dd, bImage ); printf( "\n" );
// move reached states into ring manager
bImage = Extra_TransferPermute( p->dd, p->ddR, bTemp = bImage, Vec_IntArray(p->vCs2Glo) ); Cudd_Ref( bImage );
Cudd_RecursiveDeref( p->dd, bTemp );
// intersect with the previous set
bOneCube = Cudd_bddIntersect( p->ddR, bImage, bRing ); Cudd_Ref( bOneCube );
Cudd_RecursiveDeref( p->ddR, bImage );
// find any assignment of the BDD
RetValue = Cudd_bddPickOneCube( p->ddR, bOneCube, pValues );
Cudd_RecursiveDeref( p->ddR, bOneCube );
assert( RetValue );
// write PIs of counter-example
nPiOffset -= Saig_ManPiNum(p->pAig);
Saig_ManForEachPi( p->pAig, pObj, i )
if ( pValues[Saig_ManRegNum(p->pAig)+i] == 1 )
Aig_InfoSetBit( pCex->pData, nPiOffset + i );
// check that we get the init state
if ( v == 0 )
{
Saig_ManForEachLo( p->pAig, pObj, i )
assert( pValues[i] == 0 );
break;
}
// write state in terms of NS variables
bState = Llb_CoreComputeCube( p->dd, vVarsNs, 1, pValues ); Cudd_Ref( bState );
}
assert( nPiOffset == Saig_ManRegNum(p->pAig) );
// update the output number
RetValue = Ssw_SmlFindOutputCounterExample( p->pInit, pCex );
assert( RetValue >= 0 && RetValue < Saig_ManPoNum(p->pInit) ); // invalid CEX!!!
pCex->iPo = RetValue;
// cleanup
ABC_FREE( pValues );
Vec_IntFree( vVarsNs );
return pCex;
}
/**Function*************************************************************
Synopsis [Perform reachability with hints.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_NonlinReachability( Llb_Mnn_t * p )
{
DdNode * bCurrent, * bNext, * bTemp;
int nIters, nBddSize0, nBddSize;
int clk2, clk3, clk = clock();
assert( Aig_ManRegNum(p->pAig) > 0 );
// compute time to stop
if ( p->pPars->TimeLimit )
p->pPars->TimeTarget = clock() + p->pPars->TimeLimit * CLOCKS_PER_SEC;
else
p->pPars->TimeTarget = 0;
// create bad state in the ring manager
p->ddR->bFunc = Llb_BddComputeBad( p->pInit, p->ddR ); Cudd_Ref( p->ddR->bFunc );
// compute the starting set of states
bCurrent = Llb_NonlinComputeInitState( p->pAig, p->dd ); Cudd_Ref( bCurrent );
p->ddG->bFunc = Llb_NonlinComputeInitState( p->pAig, p->ddG ); Cudd_Ref( p->ddG->bFunc ); // reached
p->ddG->bFunc2 = Llb_NonlinComputeInitState( p->pAig, p->ddG ); Cudd_Ref( p->ddG->bFunc2 ); // frontier
for ( nIters = 0; nIters < p->pPars->nIterMax; nIters++ )
{
// check the runtime limit
clk2 = clock();
if ( p->pPars->TimeLimit && clock() >= p->pPars->TimeTarget )
{
if ( !p->pPars->fSilent )
printf( "Reached timeout during image computation (%d seconds).\n", p->pPars->TimeLimit );
p->pPars->iFrame = nIters - 1;
Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
return -1;
}
// save the onion ring
bTemp = Extra_TransferPermute( p->dd, p->ddR, bCurrent, Vec_IntArray(p->vCs2Glo) ); Cudd_Ref( bTemp );
Vec_PtrPush( p->vRings, bTemp );
// check it for bad states
if ( !p->pPars->fSkipOutCheck && !Cudd_bddLeq( p->ddR, bTemp, Cudd_Not(p->ddR->bFunc) ) )
{
assert( p->pInit->pSeqModel == NULL );
if ( !p->pPars->fBackward )
p->pInit->pSeqModel = Llb_NonlinDeriveCex( p );
Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
if ( !p->pPars->fSilent )
{
if ( !p->pPars->fBackward )
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", p->pInit->pSeqModel->iPo, nIters );
else
printf( "Output ??? was asserted in frame %d (counter-example is not produced). ", nIters );
Abc_PrintTime( 1, "Time", clock() - clk );
}
return 0;
}
// compute the next states
clk3 = clock();
nBddSize0 = Cudd_DagSize( bCurrent );
bNext = Llb_NonlinImage( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->dd, bCurrent,
p->pPars->fReorder, p->pPars->fVeryVerbose, p->pOrder, p->pPars->nBddMax );
if ( bNext == NULL ) // Llb_NonlimImage() consumes reference of bCurrent!!!
{
int iVar;
DdNode * bVar;
// if ( !p->pPars->fSilent )
// printf( "Reached timeout during image computation (%d seconds).\n", p->pPars->TimeLimit );
// p->pPars->iFrame = nIters - 1;
// return -1;
bCurrent = Extra_TransferPermute( p->ddG, p->dd, p->ddG->bFunc2, Vec_IntArray(p->vGlo2Cs) ); Cudd_Ref( bCurrent );
iVar = Llb_NonlinFindBestVar( p->dd, bCurrent, p->pAig );
bVar = Cudd_bddIthVar(p->dd, iVar);
bCurrent = Cudd_Cofactor( p->dd, bTemp = bCurrent, Cudd_Not(bVar) ); Cudd_Ref( bCurrent );
Cudd_RecursiveDeref( p->dd, bTemp );
bCurrent = Cudd_bddAnd( p->dd, bTemp = bCurrent, Cudd_Not(bVar) ); Cudd_Ref( bCurrent );
Cudd_RecursiveDeref( p->dd, bTemp );
continue;
}
Cudd_Ref( bNext );
nBddSize = Cudd_DagSize( bNext );
p->timeImage += clock() - clk3;
// transfer to the state manager
clk3 = clock();
Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc2 );
p->ddG->bFunc2 = Extra_TransferPermute( p->dd, p->ddG, bNext, Vec_IntArray(p->vNs2Glo) ); Cudd_Ref( p->ddG->bFunc2 );
Cudd_RecursiveDeref( p->dd, bNext );
p->timeTran1 += clock() - clk3;
// derive new states
clk3 = clock();
p->ddG->bFunc2 = Cudd_bddAnd( p->ddG, bTemp = p->ddG->bFunc2, Cudd_Not(p->ddG->bFunc) ); Cudd_Ref( p->ddG->bFunc2 );
Cudd_RecursiveDeref( p->ddG, bTemp );
if ( Cudd_IsConstant(p->ddG->bFunc2) )
break;
// add to the reached set
p->ddG->bFunc = Cudd_bddOr( p->ddG, bTemp = p->ddG->bFunc, p->ddG->bFunc2 ); Cudd_Ref( p->ddG->bFunc );
Cudd_RecursiveDeref( p->ddG, bTemp );
p->timeGloba += clock() - clk3;
// reset permutation
// RetValue = Cudd_CheckZeroRef( dd );
// assert( RetValue == 0 );
// Cudd_ShuffleHeap( dd, pOrder );
// move new states to the working manager
clk3 = clock();
bCurrent = Extra_TransferPermute( p->ddG, p->dd, p->ddG->bFunc2, Vec_IntArray(p->vGlo2Cs) ); Cudd_Ref( bCurrent );
p->timeTran2 += clock() - clk3;
// report the results
if ( p->pPars->fVerbose )
{
printf( "I =%3d : ", nIters );
printf( "Fr =%7d ", nBddSize0 );
printf( "Im =%7d ", nBddSize );
printf( "(%4d %4d) ", Cudd_ReadReorderings(p->dd), Cudd_ReadGarbageCollections(p->dd) );
printf( "Rea =%6d ", Cudd_DagSize(p->ddG->bFunc) );
printf( "(%4d %4d) ", Cudd_ReadReorderings(p->ddG), Cudd_ReadGarbageCollections(p->ddG) );
printf( "S =%4d ", nSuppMax );
Abc_PrintTime( 1, "T", clock() - clk2 );
}
/*
if ( pPars->fVerbose )
{
double nMints = Cudd_CountMinterm(ddG, bReached, Saig_ManRegNum(pAig) );
// Extra_bddPrint( ddG, bReached );printf( "\n" );
printf( "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(pAig)) );
fflush( stdout );
}
*/
if ( nIters == p->pPars->nIterMax - 1 )
{
if ( !p->pPars->fSilent )
printf( "Reached limit on the number of timeframes (%d).\n", p->pPars->nIterMax );
p->pPars->iFrame = nIters;
Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
return -1;
}
// Llb_NonlinReorder( p->ddG, 1 );
// Llb_NonlinFindBestVar( p->ddG, bReached, NULL );
}
// report the stats
if ( p->pPars->fVerbose )
{
double nMints = Cudd_CountMinterm(p->ddG, p->ddG->bFunc, Saig_ManRegNum(p->pAig) );
if ( nIters >= p->pPars->nIterMax || nBddSize > p->pPars->nBddMax )
printf( "Reachability analysis is stopped after %d frames.\n", nIters );
else
printf( "Reachability analysis completed after %d frames.\n", nIters );
printf( "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) );
fflush( stdout );
}
if ( nIters >= p->pPars->nIterMax || nBddSize > p->pPars->nBddMax )
{
if ( !p->pPars->fSilent )
printf( "Verified only for states reachable in %d frames. ", nIters );
return -1; // undecided
}
// report
if ( !p->pPars->fSilent )
printf( "The miter is proved unreachable after %d iterations. ", nIters );
p->pPars->iFrame = nIters - 1;
Abc_PrintTime( 1, "Time", clock() - clk );
return 1; // unreachable
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Llb_Mnn_t * Llb_MnnStart( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
{
Llb_Mnn_t * p;
Aig_Obj_t * pObj;
int i;
p = ABC_CALLOC( Llb_Mnn_t, 1 );
p->pInit = pInit;
p->pAig = pAig;
p->pPars = pPars;
p->dd = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
p->ddG = Cudd_Init( Aig_ManRegNum(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
p->ddR = Cudd_Init( Aig_ManPiNum(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT );
Cudd_AutodynEnable( p->ddG, CUDD_REORDER_SYMM_SIFT );
Cudd_AutodynEnable( p->ddR, CUDD_REORDER_SYMM_SIFT );
p->vRings = Vec_PtrAlloc( 100 );
// create leaves
p->vLeaves = Vec_PtrAlloc( Aig_ManPiNum(pAig) );
Aig_ManForEachPi( pAig, pObj, i )
Vec_PtrPush( p->vLeaves, pObj );
// create roots
p->vRoots = Vec_PtrAlloc( Aig_ManPoNum(pAig) );
Saig_ManForEachLi( pAig, pObj, i )
Vec_PtrPush( p->vRoots, pObj );
// variables to quantify
p->pOrder = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
p->pVars2Q = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
Aig_ManForEachPi( pAig, pObj, i )
p->pVars2Q[Aig_ObjId(pObj)] = 1;
Llb_NonlinPrepareVarMap( p );
return p;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_MnnStop( Llb_Mnn_t * p )
{
DdNode * bTemp;
int i;
if ( p->pPars->fVerbose )
{
p->timeOther = p->timeTotal - p->timeImage - p->timeTran1 - p->timeTran2 - p->timeGloba;
p->timeReo = Cudd_ReadReorderingTime(p->dd);
p->timeReoG = Cudd_ReadReorderingTime(p->ddG);
ABC_PRTP( "Image ", p->timeImage, p->timeTotal );
ABC_PRTP( " build ", timeBuild, p->timeTotal );
ABC_PRTP( " and-ex ", timeAndEx, p->timeTotal );
ABC_PRTP( " other ", timeOther, p->timeTotal );
ABC_PRTP( "Transfer1", p->timeTran1, p->timeTotal );
ABC_PRTP( "Transfer2", p->timeTran2, p->timeTotal );
ABC_PRTP( "Global ", p->timeGloba, p->timeTotal );
ABC_PRTP( "Other ", p->timeOther, p->timeTotal );
ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
ABC_PRTP( " reo ", p->timeReo, p->timeTotal );
ABC_PRTP( " reoG ", p->timeReoG, p->timeTotal );
}
if ( p->ddR->bFunc )
Cudd_RecursiveDeref( p->ddR, p->ddR->bFunc );
Vec_PtrForEachEntry( DdNode *, p->vRings, bTemp, i )
Cudd_RecursiveDeref( p->ddR, bTemp );
Vec_PtrFree( p->vRings );
if ( p->ddR->bFunc )
Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc );
if ( p->ddR->bFunc2 )
Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc2 );
Extra_StopManager( p->dd );
Extra_StopManager( p->ddG );
Extra_StopManager( p->ddR );
Vec_IntFreeP( &p->vCs2Glo );
Vec_IntFreeP( &p->vNs2Glo );
Vec_IntFreeP( &p->vGlo2Cs );
Vec_IntFreeP( &p->vGlo2Ns );
Vec_PtrFree( p->vLeaves );
Vec_PtrFree( p->vRoots );
ABC_FREE( p->pVars2Q );
ABC_FREE( p->pOrder );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis [Finds balanced cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinExperiment( Aig_Man_t * pAig, int Num )
{
Llb_Mnn_t * pMnn;
Gia_ParLlb_t Pars, * pPars = &Pars;
Aig_Man_t * p;
int clk = clock();
Llb_ManSetDefaultParams( pPars );
pPars->fVerbose = 1;
p = Aig_ManDupFlopsOnly( pAig );
//Aig_ManShow( p, 0, NULL );
Aig_ManPrintStats( pAig );
Aig_ManPrintStats( p );
pMnn = Llb_MnnStart( pAig, p, pPars );
Llb_NonlinReachability( pMnn );
pMnn->timeTotal = clock() - clk;
Llb_MnnStop( pMnn );
Aig_ManStop( p );
}
/**Function*************************************************************
Synopsis [Finds balanced cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_NonlinCoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
{
Llb_Mnn_t * pMnn;
Aig_Man_t * p;
int RetValue = -1;
p = Aig_ManDupFlopsOnly( pAig );
//Aig_ManShow( p, 0, NULL );
if ( pPars->fVerbose )
Aig_ManPrintStats( pAig );
if ( pPars->fVerbose )
Aig_ManPrintStats( p );
if ( !pPars->fSkipReach )
{
int clk = clock();
pMnn = Llb_MnnStart( pAig, p, pPars );
RetValue = Llb_NonlinReachability( pMnn );
pMnn->timeTotal = clock() - clk;
Llb_MnnStop( pMnn );
}
Aig_ManStop( p );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

File diff suppressed because it is too large Load Diff

View File

@ -1,56 +0,0 @@
/**CFile****************************************************************
FileName [llbCex.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [BDD based reachability.]
Synopsis [Deriving counter-example.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: llbCex.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "llbInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Llb_ManDeriveCex( Llb_Man_t * p, DdNode * bInter, int iOutFail, int iIter )
{
return NULL;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

View File

@ -1,639 +0,0 @@
/**CFile****************************************************************
FileName [llbFlow.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [BDD based reachability.]
Synopsis [Flow computation.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: llbFlow.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "llbInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Llb_Flw_t_ Llb_Flw_t;
struct Llb_Flw_t_
{
unsigned Source : 1; // source of the graph
unsigned Sink : 1; // sink of the graph
unsigned Flow : 1; // node has flow
unsigned Mark : 1; // visited node
unsigned Id : 14; // ID of the corresponding node
unsigned nFanins : 14; // number of fanins
Llb_Flw_t * Fanins[0]; // fanins
};
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Llb_Flw_t * Llb_FlwAlloc( Vec_Int_t * vMem, Vec_Ptr_t * vStore, int Id, int nFanins )
{
Llb_Flw_t * p;
int nWords = (sizeof(Llb_Flw_t) + nFanins * sizeof(void *)) / sizeof(int);
p = (Llb_Flw_t *)Vec_IntFetch( vMem, nWords );
memset( p, 1, nWords * sizeof(int) );
p->Id = Id;
p->nFanins = 0;//nFanins;
Vec_PtrWriteEntry( vStore, Id, p );
return p;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_FlwAddFanin( Llb_Flw_t * pFrom, Llb_Flw_t * pTo )
{
pFrom->Fanins[pFrom->nFanins++] = pTo;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_AigCreateFlw( Aig_Man_t * p, Vec_Int_t ** pvMem, Vec_Ptr_t ** pvTops, Vec_Ptr_t ** pvBots )
{
Llb_Flw_t * pFlwTop, * pFlwBot;
Vec_Ptr_t * vTops, * vBots;
Vec_Int_t * vMem;
Aig_Obj_t * pObj;
int i;
vMem = Vec_IntAlloc( Aig_ManObjNumMax(p) * (sizeof(Llb_Flw_t) + sizeof(void *) * 8) );
vBots = Vec_PtrStart( Aig_ManObjNumMax(p) );
vTops = Vec_PtrStart( Aig_ManObjNumMax(p) );
Aig_ManForEachObj( p, pObj, i )
{
pFlwBot = Llb_FlwAlloc( vMem, vBots, i, Aig_ObjIsPo(pObj) + 2 * Aig_ObjIsNode(pObj) );
pFlwTop = Llb_FlwAlloc( vMem, vTops, i, Aig_ObjRefs(pObj) + 1 );
Llb_FlwAddFanin( pFlwBot, pFlwTop );
Llb_FlwAddFanin( pFlwTop, pFlwBot );
Llb_FlwAddFanin( pFlwBot, (Llb_Flw_t *)Vec_PtrEntry(vTops, Aig_ObjFaninId0(pObj)) );
Llb_FlwAddFanin( pFlwBot, (Llb_Flw_t *)Vec_PtrEntry(vTops, Aig_ObjFaninId1(pObj)) );
Llb_FlwAddFanin( (Llb_Flw_t *)Vec_PtrEntry(vTops, Aig_ObjFaninId0(pObj)), pFlwBot );
Llb_FlwAddFanin( (Llb_Flw_t *)Vec_PtrEntry(vTops, Aig_ObjFaninId1(pObj)), pFlwBot );
}
Aig_ManForEachObj( p, pObj, i )
{
pFlwBot = (Llb_Flw_t *)Vec_PtrEntry( vBots, i );
pFlwTop = (Llb_Flw_t *)Vec_PtrEntry( vTops, i );
assert( pFlwBot->nFanins == (unsigned)Aig_ObjIsPo(pObj) + 2 * Aig_ObjIsNode(pObj) );
assert( pFlwTop->nFanins == (unsigned)Aig_ObjRefs(pObj) + 1 );
}
*pvMem = vMem;
*pvTops = vTops;
*pvBots = vBots;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_AigCleanMarks( Vec_Ptr_t * vFlw )
{
Llb_Flw_t * pFlw;
int i;
Vec_PtrForEachEntry( Llb_Flw_t *, vFlw, pFlw, i )
pFlw->Mark = 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_AigCleanFlow( Vec_Ptr_t * vFlw )
{
Llb_Flw_t * pFlw;
int i;
Vec_PtrForEachEntry( Llb_Flw_t *, vFlw, pFlw, i )
pFlw->Flow = 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Llb_AigCollectCut( Vec_Ptr_t * vNodes, Vec_Ptr_t * vBots, Vec_Ptr_t * vTops )
{
Vec_Int_t * vCut;
Llb_Flw_t * pFlwBot, * pFlwTop;
Aig_Obj_t * pObj;
int i;
vCut = Vec_IntAlloc( 100 );
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
{
pFlwBot = (Llb_Flw_t *)Vec_PtrEntry( vBots, i );
pFlwTop = (Llb_Flw_t *)Vec_PtrEntry( vTops, i );
if ( pFlwBot->Mark && !pFlwTop->Mark )
Vec_IntPush( vCut, i );
}
return vCut;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_AigPushFlow_rec( Llb_Flw_t * pFlw, Llb_Flw_t * pFlwPrev, Vec_Ptr_t * vMarked, Vec_Ptr_t * vFlowed )
{
int i;
if ( pFlw->Mark )
return 0;
pFlw->Mark = 1;
Vec_PtrPush( vMarked, pFlw );
if ( pFlw->Source )
return 0;
if ( pFlw->Sink )
{
pFlw->Flow = 1;
Vec_PtrPush( vFlowed, pFlw );
return 1;
}
// assert( Aig_ObjIsNode(pObj) );
for ( i = 0; i < (int)pFlw->nFanins; i++ )
{
if ( pFlw->Fanins[i] == pFlwPrev )
continue;
if ( Llb_AigPushFlow_rec( pFlw->Fanins[i], pFlw, vMarked, vFlowed ) )
break;
}
if ( i == (int)pFlw->nFanins )
return 0;
if ( i == 0 )
{
pFlw->Flow = 1;
Vec_PtrPush( vFlowed, pFlw );
}
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_AigPushFlow( Vec_Ptr_t * vFlwBots, Vec_Ptr_t * vMarked, Vec_Ptr_t * vFlowed )
{
Llb_Flw_t * pFlw;
int i, Counter = 0;
Vec_PtrForEachEntry( Llb_Flw_t *, vFlwBots, pFlw, i )
{
pFlw->Mark = 1;
if ( Llb_AigPushFlow_rec( pFlw->Fanins[0], pFlw, vMarked, vFlowed ) )
{
Counter++;
pFlw->Flow = 1;
Vec_PtrPush( vFlowed, pFlw );
}
}
return Counter;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Llb_AigFindMinCut( Vec_Ptr_t * vNodes, Vec_Ptr_t * vFlwBots, Vec_Ptr_t * vFlwTop, Vec_Ptr_t * vFlwBots2, Vec_Ptr_t * vFlwTop2 )
{
Vec_Int_t * vCut;
Vec_Ptr_t * vMarked, * vFlowed;
int Value;
vMarked = Vec_PtrAlloc( 100 );
vFlowed = Vec_PtrAlloc( 100 );
Value = Llb_AigPushFlow( vFlwBots2, vMarked, vFlowed );
Llb_AigCleanMarks( vMarked );
Value = Llb_AigPushFlow( vFlwBots2, vMarked, vFlowed );
assert( Value == 0 );
vCut = Llb_AigCollectCut( vNodes, vFlwBots, vFlwTop );
Llb_AigCleanMarks( vMarked );
Llb_AigCleanFlow( vFlowed );
return vCut;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Llb_AigCollectFlowTerminals( Aig_Man_t * p, Vec_Ptr_t * vFlws, Vec_Int_t * vCut )
{
Vec_Ptr_t * pFlwRes;
Aig_Obj_t * pObj;
int i;
pFlwRes = Vec_PtrAlloc( Vec_IntSize(vCut) );
Aig_ManForEachNodeVec( p, vCut, pObj, i )
Vec_PtrPush( pFlwRes, Vec_PtrEntry( vFlws, Aig_ObjId(pObj) ) );
return pFlwRes;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_AigMarkFlowTerminals( Vec_Ptr_t * vFlws, int fSource, int fSink )
{
Llb_Flw_t * pFlw;
int i;
Vec_PtrForEachEntry( Llb_Flw_t *, vFlws, pFlw, i )
{
pFlw->Source = fSource;
pFlw->Sink = fSink;
}
}
/**Function*************************************************************
Synopsis [Collects internal nodes in the DFS order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_ManCollectNodes_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
{
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
return;
Aig_ObjSetTravIdCurrent(p, pObj);
assert( Aig_ObjIsNode(pObj) );
Llb_ManCollectNodes_rec( p, Aig_ObjFanin0(pObj), vNodes );
Llb_ManCollectNodes_rec( p, Aig_ObjFanin1(pObj), vNodes );
Vec_PtrPush( vNodes, pObj );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Llb_ManCollectNodes( Aig_Man_t * p, Vec_Int_t * vCut1, Vec_Int_t * vCut2 )
{
Vec_Ptr_t * vNodes;
Aig_Obj_t * pObj;
int i;
Aig_ManIncrementTravId( p );
Aig_ManForEachNodeVec( p, vCut1, pObj, i )
Aig_ObjSetTravIdCurrent( p, pObj );
vNodes = Vec_PtrAlloc( Aig_ManObjNumMax(p) );
Aig_ManForEachNodeVec( p, vCut2, pObj, i )
Llb_ManCollectNodes_rec( p, pObj, vNodes );
return vNodes;
}
/**Function*************************************************************
Synopsis [Collects internal nodes in the DFS order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_ManCountNodes_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
{
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
return 0;
Aig_ObjSetTravIdCurrent(p, pObj);
assert( Aig_ObjIsNode(pObj) );
return 1 + Llb_ManCountNodes_rec( p, Aig_ObjFanin0(pObj) ) +
Llb_ManCountNodes_rec( p, Aig_ObjFanin1(pObj) );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_ManCountNodes( Aig_Man_t * p, Vec_Int_t * vCut1, Vec_Int_t * vCut2 )
{
Aig_Obj_t * pObj;
int i, Counter = 0;
Aig_ManIncrementTravId( p );
Aig_ManForEachNodeVec( p, vCut1, pObj, i )
Aig_ObjSetTravIdCurrent( p, pObj );
Aig_ManForEachNodeVec( p, vCut2, pObj, i )
Counter += Llb_ManCountNodes_rec( p, pObj );
return Counter;
}
/**Function*************************************************************
Synopsis [Computes starting cuts.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Llb_ManComputeCioCut( Aig_Man_t * pAig, int fCollectCos )
{
Vec_Int_t * vCut;
Aig_Obj_t * pObj;
int i;
vCut = Vec_IntAlloc( 500 );
if ( fCollectCos )
Aig_ManForEachPo( pAig, pObj, i )
Vec_IntPush( vCut, Aig_ObjId(pObj) );
else
Aig_ManForEachPi( pAig, pObj, i )
Vec_IntPush( vCut, Aig_ObjId(pObj) );
return vCut;
}
/**Function*************************************************************
Synopsis [Inserts the new cut into the array.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_ManCutInsert( Aig_Man_t * p, Vec_Ptr_t * vCuts, Vec_Int_t * vVols, int iEntry, Vec_Int_t * vCutNew )
{
Vec_Int_t * vCut1, * vCut2;
int Vol1, Vol2;
Vec_PtrInsert( vCuts, iEntry, vCutNew );
Vec_IntInsert( vVols, iEntry, -1 );
vCut1 = (Vec_Int_t *)Vec_PtrEntry( vCuts, iEntry );
vCut2 = (Vec_Int_t *)Vec_PtrEntry( vCuts, iEntry+1 );
Vol1 = Llb_ManCountNodes( p, vCut1, vCutNew );
Vol2 = Llb_ManCountNodes( p, vCutNew, vCut2 );
Vec_IntWriteEntry( vVols, iEntry-1, Vol1 );
Vec_IntWriteEntry( vVols, iEntry, Vol2 );
}
/**Function*************************************************************
Synopsis [Returns the set of cuts resulting from the flow computation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Llb_ManComputePartitioning( Aig_Man_t * p, int nVolumeMin, int nVolumeMax )
{
Vec_Ptr_t * vCuts, * vFlwTops, * vFlwBots;
Vec_Int_t * vVols, * vCut1, * vCut2, * vCut, * vMem;
int nMaxValue, iEntry;
vCuts = Vec_PtrAlloc( 1000 );
vVols = Vec_IntAlloc( 1000 );
// prepare flow computation
Llb_AigCreateFlw( p, &vMem, &vFlwTops, &vFlwBots );
// start with regular cuts
Vec_PtrPush( vCuts, Llb_ManComputeCioCut(p, 0) );
Vec_PtrPush( vCuts, Llb_ManComputeCioCut(p, 1) );
Vec_IntPush( vVols, Aig_ManNodeNum(p) );
// split cuts with the largest volume
while ( (nMaxValue = Vec_IntFindMax(vVols)) > nVolumeMax )
{
Vec_Ptr_t * vNodes, * vFlwBots2, * vFlwTops2;
iEntry = Vec_IntFind( vVols, nMaxValue ); assert( iEntry >= 0 );
vCut1 = (Vec_Int_t *)Vec_PtrEntry( vCuts, iEntry );
vCut2 = (Vec_Int_t *)Vec_PtrEntry( vCuts, iEntry+1 );
// collect nodes
vNodes = Llb_ManCollectNodes( p, vCut1, vCut1 );
assert( Vec_PtrSize(vNodes) == nMaxValue );
assert( Llb_ManCountNodes(p, vCut1, vCut2) == nMaxValue );
// collect sources and sinks
vFlwBots2 = Llb_AigCollectFlowTerminals( p, vFlwBots, vCut1 );
vFlwTops2 = Llb_AigCollectFlowTerminals( p, vFlwTops, vCut2 );
// mark sources and sinks
Llb_AigMarkFlowTerminals( vFlwBots2, 1, 0 );
Llb_AigMarkFlowTerminals( vFlwTops2, 0, 1 );
vCut = Llb_AigFindMinCut( vNodes, vFlwBots, vFlwTops, vFlwBots2, vFlwTops2 );
Llb_AigMarkFlowTerminals( vFlwBots2, 0, 0 );
Llb_AigMarkFlowTerminals( vFlwTops2, 0, 0 );
// insert new cut
Llb_ManCutInsert( p, vCuts, vVols, iEntry+1, vCut );
// deallocate
Vec_PtrFree( vNodes );
Vec_PtrFree( vFlwBots2 );
Vec_PtrFree( vFlwTops2 );
}
Vec_IntFree( vMem );
Vec_PtrFree( vFlwTops );
Vec_PtrFree( vFlwBots );
return vCuts;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Llb_ManMarkPivotNodesFlow( Aig_Man_t * p, Vec_Ptr_t * vCuts )
{
Vec_Int_t * vVar2Obj, * vCut;
Aig_Obj_t * pObj;
int i, k;
// mark inputs/outputs
Aig_ManForEachPi( p, pObj, i )
pObj->fMarkA = 1;
Saig_ManForEachLi( p, pObj, i )
pObj->fMarkA = 1;
// mark internal pivot nodes
Vec_PtrForEachEntry( Vec_Int_t *, vCuts, vCut, i )
Aig_ManForEachNodeVec( p, vCut, pObj, k )
pObj->fMarkA = 1;
// assign variable numbers
Aig_ManConst1(p)->fMarkA = 0;
vVar2Obj = Vec_IntAlloc( 100 );
Aig_ManForEachPi( p, pObj, i )
Vec_IntPush( vVar2Obj, Aig_ObjId(pObj) );
Aig_ManForEachNode( p, pObj, i )
if ( pObj->fMarkA )
Vec_IntPush( vVar2Obj, Aig_ObjId(pObj) );
Saig_ManForEachLi( p, pObj, i )
Vec_IntPush( vVar2Obj, Aig_ObjId(pObj) );
return vVar2Obj;
}
/**Function*************************************************************
Synopsis [Returns the set of cuts resulting from the flow computation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_ManPartitionUsingFlow( Llb_Man_t * p, Vec_Ptr_t * vCuts )
{
Vec_Int_t * vCut1, * vCut2;
int i;
vCut1 = (Vec_Int_t *)Vec_PtrEntry( vCuts, 0 );
Vec_PtrForEachEntryStart( Vec_Int_t *, vCuts, vCut1, i, 1 )
{
vCut2 = (Vec_Int_t *)Vec_PtrEntry( vCuts, i );
Llb_ManGroupCreateFromCuts( p, vCut1, vCut2 );
vCut1 = vCut2;
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Llb_Man_t * Llb_ManStartFlow( Aig_Man_t * pAigGlo, Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
{
Vec_Ptr_t * vCuts;
Llb_Man_t * p;
vCuts = Llb_ManComputePartitioning( pAig, pPars->nVolumeMin, pPars->nVolumeMax );
Aig_ManCleanMarkA( pAig );
p = ABC_CALLOC( Llb_Man_t, 1 );
p->pAigGlo = pAigGlo;
p->pPars = pPars;
p->pAig = pAig;
p->vVar2Obj = Llb_ManMarkPivotNodesFlow( p->pAig, vCuts );
p->vObj2Var = Vec_IntInvert( p->vVar2Obj, -1 );
Llb_ManPrepareVarMap( p );
Aig_ManCleanMarkA( pAig );
Llb_ManPartitionUsingFlow( p, vCuts );
Vec_VecFreeP( (Vec_Vec_t **)&vCuts );
return p;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

View File

@ -37,11 +37,8 @@
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
@ -109,8 +106,6 @@ struct Llb_Grp_t_
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== llbCex.c =======================================================*/
extern Abc_Cex_t * Llb_ManDeriveCex( Llb_Man_t * p, DdNode * bInter, int iOutFail, int iIter );
/*=== llbConstr.c ======================================================*/
extern Vec_Int_t * Llb_ManDeriveConstraints( Aig_Man_t * p );
extern void Llb_ManPrintEntries( Aig_Man_t * p, Vec_Int_t * vCands );
@ -118,8 +113,10 @@ extern void Llb_ManPrintEntries( Aig_Man_t * p, Vec_Int_t * vCands );
extern int Llb_ManModelCheckAig( Aig_Man_t * pAigGlo, Gia_ParLlb_t * pPars, Vec_Int_t * vHints, DdManager ** pddGlo );
/*=== llbCluster.c ======================================================*/
extern void Llb_ManCluster( Llb_Mtr_t * p );
/*=== llbDump.c ======================================================*/
extern void Llb_ManDumpReached( DdManager * ddG, DdNode * bReached, char * pModel, char * pFileName );
/*=== llbFlow.c ======================================================*/
extern Llb_Man_t * Llb_ManStartFlow( Aig_Man_t * pAigGlo, Aig_Man_t * pAig, Gia_ParLlb_t * pPars );
extern Vec_Ptr_t * Llb_ManFlow( Aig_Man_t * p, Vec_Ptr_t * vSources, int * pnFlow );
/*=== llbHint.c ======================================================*/
extern int Llb_ManReachabilityWithHints( Llb_Man_t * p );
extern int Llb_ManModelCheckAigWithHints( Aig_Man_t * pAigGlo, Gia_ParLlb_t * pPars );
@ -148,7 +145,30 @@ extern int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, D
/*=== llbSched.c =====================================================*/
extern void Llb_MtrSchedule( Llb_Mtr_t * p );
/*=== llb2Bad.c ======================================================*/
extern DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd );
extern DdNode * Llb_BddQuantifyPis( Aig_Man_t * pInit, DdManager * dd, DdNode * bFunc );
/*=== llb2Core.c ======================================================*/
extern DdNode * Llb_CoreComputeCube( DdManager * dd, Vec_Int_t * vVars, int fUseVarIndex, char * pValues );
/*=== llb2Driver.c ======================================================*/
extern Vec_Int_t * Llb_DriverCountRefs( Aig_Man_t * p );
extern Vec_Int_t * Llb_DriverCollectNs( Aig_Man_t * pAig, Vec_Int_t * vDriRefs );
extern Vec_Int_t * Llb_DriverCollectCs( Aig_Man_t * pAig );
extern DdNode * Llb_DriverPhaseCube( Aig_Man_t * pAig, Vec_Int_t * vDriRefs, DdManager * dd );
extern DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs );
/*=== llb2Image.c ======================================================*/
extern Vec_Ptr_t * Llb_ImgSupports( Aig_Man_t * p, Vec_Ptr_t * vDdMans, Vec_Int_t * vStart, Vec_Int_t * vStop, int fAddPis, int fVerbose );
extern void Llb_ImgSchedule( Vec_Ptr_t * vSupps, Vec_Ptr_t ** pvQuant0, Vec_Ptr_t ** pvQuant1, int fVerbose );
extern DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper );
extern void Llb_ImgQuantifyFirst( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, Vec_Ptr_t * vQuant0, int fVerbose );
extern void Llb_ImgQuantifyReset( Vec_Ptr_t * vDdMans );
extern DdNode * Llb_ImgComputeImage( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, DdManager * dd, DdNode * bInit,
Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQuant1, Vec_Int_t * vDriRefs,
int TimeTarget, int fBackward, int fReorder, int fVerbose );
/*=== llb3Image.c ======================================================*/
extern DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q,
DdManager * dd, DdNode * bCurrent, int fReorder, int fVerbose, int * pOrder, int Limit );
ABC_NAMESPACE_HEADER_END

View File

@ -1,11 +1,19 @@
SRC += src/aig/llb/llbCex.c \
src/aig/llb/llbCluster.c \
src/aig/llb/llbConstr.c \
src/aig/llb/llbCore.c \
src/aig/llb/llbHint.c \
src/aig/llb/llbMan.c \
src/aig/llb/llbMatrix.c \
src/aig/llb/llbPart.c \
src/aig/llb/llbPivot.c \
src/aig/llb/llbReach.c \
src/aig/llb/llbSched.c
SRC += src/aig/llb/llb.c \
src/aig/llb/llb1Cluster.c \
src/aig/llb/llb1Constr.c \
src/aig/llb/llb1Core.c \
src/aig/llb/llb1Group.c \
src/aig/llb/llb1Hint.c \
src/aig/llb/llb1Man.c \
src/aig/llb/llb1Matrix.c \
src/aig/llb/llb1Pivot.c \
src/aig/llb/llb1Reach.c \
src/aig/llb/llb1Sched.c \
src/aig/llb/llb2Bad.c \
src/aig/llb/llb2Core.c \
src/aig/llb/llb2Driver.c \
src/aig/llb/llb2Dump.c \
src/aig/llb/llb2Flow.c \
src/aig/llb/llb2Image.c \
src/aig/llb/llb3Image.c \
src/aig/llb/llb3Nonlin.c

View File

@ -83,7 +83,7 @@ Nwk_Man_t * Nwk_ManDeriveFromAig( Aig_Man_t * p )
***********************************************************************/
Vec_Ptr_t * Nwk_ManDeriveRetimingCut( Aig_Man_t * p, int fForward, int fVerbose )
{
{
Vec_Ptr_t * vNodes;
Nwk_Man_t * pNtk;
Nwk_Obj_t * pNode;
@ -99,7 +99,7 @@ Vec_Ptr_t * Nwk_ManDeriveRetimingCut( Aig_Man_t * p, int fForward, int fVerbose
Vec_PtrForEachEntry( Nwk_Obj_t *, vNodes, pNode, i )
Vec_PtrWriteEntry( vNodes, i, pNode->pCopy );
Nwk_ManFree( pNtk );
assert( Vec_PtrSize(vNodes) <= Aig_ManRegNum(p) );
// assert( Vec_PtrSize(vNodes) <= Aig_ManRegNum(p) );
return vNodes;
}

View File

@ -22,6 +22,7 @@
#include "ssw.h"
#include "fra.h"
#include "bbr.h"
#include "pdr.h"
ABC_NAMESPACE_IMPL_START
@ -173,15 +174,32 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo
{
extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames );
Vec_Int_t * vFlopsNew;
int i, Entry;
int i, Entry, RetValue;
*piRetValue = -1;
if ( fUseDprove && Aig_ManRegNum(pAbs) > 0 )
{
/*
Fra_Sec_t SecPar, * pSecPar = &SecPar;
int RetValue;
Fra_SecSetDefaultParams( pSecPar );
pSecPar->fVerbose = fVerbose;
RetValue = Fra_FraigSec( pAbs, pSecPar, NULL );
*/
Abc_Cex_t * pCex = NULL;
Aig_Man_t * pAbsOrpos = Saig_ManDupOrpos( pAbs );
Pdr_Par_t Pars, * pPars = &Pars;
Pdr_ManSetDefaultParams( pPars );
pPars->nTimeOut = 10;
pPars->fVerbose = fVerbose;
if ( pPars->fVerbose )
printf( "Running property directed reachability...\n" );
RetValue = Pdr_ManSolve( pAbsOrpos, pPars, &pCex );
if ( pCex )
pCex->iPo = Ssw_SmlFindOutputCounterExample( pAbs, pCex );
Aig_ManStop( pAbsOrpos );
pAbs->pSeqModel = pCex;
if ( RetValue )
*piRetValue = 1;
}
else if ( fUseBdds && (Aig_ManRegNum(pAbs) > 0 && Aig_ManRegNum(pAbs) <= 80) )
{
@ -195,7 +213,9 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo
pPars->fReorderImage = 1;
pPars->fVerbose = fVerbose;
pPars->fSilent = 0;
Aig_ManVerifyUsingBdds( pAbs, pPars );
RetValue = Aig_ManVerifyUsingBdds( pAbs, pPars );
if ( RetValue )
*piRetValue = 1;
}
else
{

View File

@ -222,7 +222,7 @@ int Saig_TsiStateHash( unsigned * pState, int nWords, int nTableSize )
SeeAlso []
***********************************************************************/
int Saig_TsiCountNonXValuedRegisters( Saig_Tsim_t * p, int nWords, int nPref )
int Saig_TsiCountNonXValuedRegisters( Saig_Tsim_t * p, int nPref )
{
unsigned * pState;
int nRegs = p->pAig->nRegs;
@ -242,6 +242,53 @@ int Saig_TsiCountNonXValuedRegisters( Saig_Tsim_t * p, int nWords, int nPref )
Vec_IntPush( p->vNonXRegs, i );
}
return Vec_IntSize(p->vNonXRegs);
}
/**Function*************************************************************
Synopsis [Computes flops that are stuck-at constant.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_TsiComputeTransient( Saig_Tsim_t * p, int nPref )
{
Vec_Int_t * vCounters;
unsigned * pState;
int ValueThis, ValuePrev = -1, StepPrev = -1;
int i, k, nRegs = p->pAig->nRegs;
vCounters = Vec_IntStart( nPref );
for ( i = 0; i < nRegs; i++ )
{
Vec_PtrForEachEntry( unsigned *, p->vStates, pState, k )
{
ValueThis = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
//printf( "%s", (ValueThis == 1)? "0" : ((ValueThis == 2)? "1" : "x") );
assert( ValueThis != 0 );
if ( ValuePrev != ValueThis )
{
ValuePrev = ValueThis;
StepPrev = k;
}
}
//printf( "\n" );
if ( ValueThis == SAIG_XVSX )
continue;
if ( StepPrev >= nPref )
continue;
Vec_IntAddToEntry( vCounters, StepPrev, 1 );
}
Vec_IntForEachEntry( vCounters, ValueThis, i )
{
if ( ValueThis == 0 )
continue;
// printf( "%3d : %3d\n", i, ValueThis );
}
return vCounters;
}
/**Function*************************************************************
@ -821,7 +868,7 @@ int Saig_ManPhaseFrameNum( Aig_Man_t * p, Vec_Int_t * vInits )
SeeAlso []
***********************************************************************/
int Saig_ManPhasePrefixLength( Aig_Man_t * p, int fVerbose, int fVeryVerbose )
int Saig_ManPhasePrefixLength( Aig_Man_t * p, int fVerbose, int fVeryVerbose, Vec_Int_t ** pvTrans )
{
Saig_Tsim_t * pTsi;
int nFrames, nPrefix, nNonXRegs;
@ -835,7 +882,11 @@ int Saig_ManPhasePrefixLength( Aig_Man_t * p, int fVerbose, int fVeryVerbose )
// derive information
nPrefix = Saig_TsiComputePrefix( pTsi, (unsigned *)Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords );
nFrames = Vec_PtrSize(pTsi->vStates) - 1 - nPrefix;
nNonXRegs = Saig_TsiCountNonXValuedRegisters( pTsi, pTsi->nWords, nPrefix );
nNonXRegs = Saig_TsiCountNonXValuedRegisters( pTsi, nPrefix );
if ( pvTrans )
*pvTrans = Saig_TsiComputeTransient( pTsi, nPrefix );
// print statistics
if ( fVerbose )
printf( "Lead = %5d. Loop = %5d. Total flops = %5d. Binary flops = %5d.\n", nPrefix, nFrames, p->nRegs, nNonXRegs );
@ -871,7 +922,7 @@ Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrame
// derive information
pTsi->nPrefix = Saig_TsiComputePrefix( pTsi, (unsigned *)Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords );
pTsi->nCycle = Vec_PtrSize(pTsi->vStates) - 1 - pTsi->nPrefix;
pTsi->nNonXRegs = Saig_TsiCountNonXValuedRegisters(pTsi, pTsi->nWords, ABC_MIN(pTsi->nPrefix,nPref));
pTsi->nNonXRegs = Saig_TsiCountNonXValuedRegisters(pTsi, ABC_MIN(pTsi->nPrefix,nPref));
// print statistics
if ( fVerbose )
{
@ -927,7 +978,7 @@ Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose )
// derive information
pTsi->nPrefix = Saig_TsiComputePrefix( pTsi, (unsigned *)Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords );
pTsi->nCycle = Vec_PtrSize(pTsi->vStates) - 1 - pTsi->nPrefix;
pTsi->nNonXRegs = Saig_TsiCountNonXValuedRegisters(pTsi, pTsi->nWords, 0);
pTsi->nNonXRegs = Saig_TsiCountNonXValuedRegisters(pTsi, 0);
// print statistics
if ( fVerbose )
{

View File

@ -145,6 +145,32 @@ Aig_Man_t * Saig_ManTemporDecompose( Aig_Man_t * pAig, int nFrames )
return pAigNew;
}
/**Function*************************************************************
Synopsis [Find index of first non-zero entry.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Vec_IntLastNonZeroBeforeLimit( Vec_Int_t * vTemp, int Limit )
{
int Entry, i;
if ( vTemp == NULL )
return -1;
Vec_IntForEachEntryReverse( vTemp, Entry, i )
{
if ( i >= Limit )
continue;
if ( Entry )
return i;
}
return -1;
}
/**Function*************************************************************
Synopsis []
@ -156,19 +182,33 @@ Aig_Man_t * Saig_ManTemporDecompose( Aig_Man_t * pAig, int nFrames )
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fVerbose, int fVeryVerbose )
Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fUseTransSigs, int fVerbose, int fVeryVerbose )
{
extern int Saig_ManPhasePrefixLength( Aig_Man_t * p, int fVerbose, int fVeryVerbose );
extern int Saig_ManPhasePrefixLength( Aig_Man_t * p, int fVerbose, int fVeryVerbose, Vec_Int_t ** pvTrans );
Vec_Int_t * vTransSigs = NULL;
int RetValue, nFramesFinished = -1;
assert( nFrames >= 0 );
if ( nFrames == 0 )
{
nFrames = Saig_ManPhasePrefixLength( pAig, fVerbose, fVeryVerbose );
nFrames = Saig_ManPhasePrefixLength( pAig, fVerbose, fVeryVerbose, &vTransSigs );
if ( nFrames == 1 )
{
Vec_IntFreeP( &vTransSigs );
printf( "The leading sequence has length 1. Temporal decomposition is not performed.\n" );
return NULL;
}
if ( fUseTransSigs )
{
int Entry, i, iLast = -1;
Vec_IntForEachEntry( vTransSigs, Entry, i )
iLast = Entry ? i :iLast;
if ( iLast > 0 && iLast < nFrames )
{
Abc_Print( 1, "Reducing frame count from %d to %d to fit the last transient.\n", nFrames, iLast );
nFrames = iLast;
}
}
Abc_Print( 1, "Using computed frame number (%d).\n", nFrames );
}
else
@ -176,18 +216,27 @@ Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nCon
// run BMC2
if ( fUseBmc )
{
RetValue = Saig_BmcPerform( pAig, 0, nFrames, 5000, TimeOut, nConfLimit, 0, fVerbose, 0, &nFramesFinished );
RetValue = Saig_BmcPerform( pAig, 0, nFrames, 2000, TimeOut, nConfLimit, 0, fVerbose, 0, &nFramesFinished );
if ( RetValue == 0 )
{
Vec_IntFreeP( &vTransSigs );
printf( "A cex found in the first %d frames.\n", nFrames );
return NULL;
}
if ( nFramesFinished < nFrames )
{
printf( "BMC for %d frames could not be completed. A cex may exist!\n", nFrames );
return NULL;
int iLastBefore = Vec_IntLastNonZeroBeforeLimit( vTransSigs, nFramesFinished );
if ( iLastBefore < 1 || !fUseTransSigs )
{
Vec_IntFreeP( &vTransSigs );
printf( "BMC for %d frames could not be completed. A cex may exist!\n", nFrames );
return NULL;
}
assert( iLastBefore < nFramesFinished );
printf( "BMC succeeded to frame %d. Adjusting frame count to be (%d) based on the last transient signal.\n", nFramesFinished, iLastBefore );
}
}
Vec_IntFreeP( &vTransSigs );
return Saig_ManTemporDecompose( pAig, nFrames );
}

View File

@ -370,6 +370,8 @@ static int Abc_CommandAbc9PbaStart ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Reparam ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Posplit ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Reach ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Reach2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Reach3 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Undo ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -766,6 +768,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&reparam", Abc_CommandAbc9Reparam, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&posplit", Abc_CommandAbc9Posplit, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&reach", Abc_CommandAbc9Reach, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&reach2", Abc_CommandAbc9Reach2, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&reach3", Abc_CommandAbc9Reach3, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&undo", Abc_CommandAbc9Undo, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 );
@ -8414,9 +8418,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// extern Abc_Ntk_t * Abc_NtkTestExor( Abc_Ntk_t * pNtk, int fVerbose );
// extern Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk, If_Lib_t * pLutLib );
extern Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose );
extern void Abc_NtkDarTest( Abc_Ntk_t * pNtk );
extern void Abc_NtkDarTest( Abc_Ntk_t * pNtk, int Num );
// extern void Aig_ProcedureTest();
extern void Abc_NtkDarTest( Abc_Ntk_t * pNtk );
extern Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk );
extern void Amap_LibertyTest( char * pFileName );
extern void Bbl_ManTest( Abc_Ntk_t * pNtk );
@ -8435,7 +8438,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
fVerbose = 1;
fBmc = 0;
nFrames = 1;
nLevels = 200;
nLevels = 10;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FNbvwh" ) ) != EOF )
{
@ -8489,11 +8492,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Only works for sequential networks.\n" );
return 1;
}
{
extern void Abc_NtkDarTest( Abc_Ntk_t * pNtk );
Abc_NtkDarTest( pNtk );
}
Abc_NtkDarTest( pNtk, nLevels );
// Abc_NtkTestEsop( pNtk );
// Abc_NtkTestSop( pNtk );
@ -18975,17 +18975,18 @@ usage:
***********************************************************************/
int Abc_CommandTempor( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Abc_Ntk_t * Abc_NtkDarTempor( Abc_Ntk_t * pNtk, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fVerbose, int fVeryVerbose );
extern Abc_Ntk_t * Abc_NtkDarTempor( Abc_Ntk_t * pNtk, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fUseTransSigs, int fVerbose, int fVeryVerbose );
Abc_Ntk_t * pNtkRes, * pNtk = Abc_FrameReadNtk(pAbc);
int nFrames = 0;
int TimeOut = 300;
int nConfMax = 100000;
int fUseBmc = 1;
int fVerbose = 0;
int fVeryVerbose = 0;
int nFrames = 0;
int TimeOut = 300;
int nConfMax = 100000;
int fUseBmc = 1;
int fUseTransSigs = 0;
int fVerbose = 0;
int fVeryVerbose = 0;
int c;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FTCbvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "FTCbsvwh" ) ) != EOF )
{
switch ( c )
{
@ -19025,6 +19026,9 @@ int Abc_CommandTempor( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'b':
fUseBmc ^= 1;
break;
case 's':
fUseTransSigs ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -19052,7 +19056,7 @@ int Abc_CommandTempor( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
// modify the current network
pNtkRes = Abc_NtkDarTempor( pNtk, nFrames, TimeOut, nConfMax, fUseBmc, fVerbose, fVeryVerbose );
pNtkRes = Abc_NtkDarTempor( pNtk, nFrames, TimeOut, nConfMax, fUseBmc, fUseTransSigs, fVerbose, fVeryVerbose );
if ( pNtkRes == NULL )
{
Abc_Print( -1, "Temporal decomposition has failed.\n" );
@ -19063,12 +19067,13 @@ int Abc_CommandTempor( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: tempor [-FTC <num>] [-bvwh]\n" );
Abc_Print( -2, "usage: tempor [-FTC <num>] [-bsvwh]\n" );
Abc_Print( -2, "\t performs temporal decomposition\n" );
Abc_Print( -2, "\t-F <num> : init logic timeframe count (0 = use leading length) [default = %d]\n", nFrames );
Abc_Print( -2, "\t-T <num> : runtime limit in seconds for BMC (0=unused) [default = %d]\n", TimeOut );
Abc_Print( -2, "\t-C <num> : max number of SAT conflicts in BMC (0=unused) [default = %d]\n", nConfMax );
Abc_Print( -2, "\t-b : toggle running BMC2 on the init frames [default = %s]\n", fUseBmc? "yes": "no" );
Abc_Print( -2, "\t-s : toggle using transient signals [default = %s]\n", fUseTransSigs? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing ternary state space [default = %s]\n", fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
@ -19311,7 +19316,8 @@ usage:
Abc_Print( -2, "\t-R num : the %% of abstracted flops when refinement stops (0<=num<=100) [default = %d]\n", pPars->nRatio );
Abc_Print( -2, "\t-c : toggle dynamic addition of constraints [default = %s]\n", pPars->fConstr? "yes": "no" );
Abc_Print( -2, "\t-r : toggle using BDD-based reachability for filtering [default = %s]\n", pPars->fUseBdds? "yes": "no" );
Abc_Print( -2, "\t-p : toggle using \"dprove\" for filtering [default = %s]\n", pPars->fUseDprove? "yes": "no" );
// Abc_Print( -2, "\t-p : toggle using \"dprove\" for filtering [default = %s]\n", pPars->fUseDprove? "yes": "no" );
Abc_Print( -2, "\t-p : toggle using \"pdr\" for filtering [default = %s]\n", pPars->fUseDprove? "yes": "no" );
Abc_Print( -2, "\t-f : toggle starting BMC from a later frame [default = %s]\n", pPars->fUseStart? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
@ -26943,7 +26949,8 @@ usage:
Abc_Print( -2, "\t-C num : the max number of conflicts by SAT solver for BMC [default = %d]\n", pPars->nConfMaxBmc );
Abc_Print( -2, "\t-R num : the %% of abstracted flops when refinement stops (0<=num<=100) [default = %d]\n", pPars->nRatio );
Abc_Print( -2, "\t-r : toggle using BDD-based reachability for filtering [default = %s]\n", pPars->fUseBdds? "yes": "no" );
Abc_Print( -2, "\t-p : toggle using \"dprove\" for filtering [default = %s]\n", pPars->fUseDprove? "yes": "no" );
// Abc_Print( -2, "\t-p : toggle using \"dprove\" for filtering [default = %s]\n", pPars->fUseDprove? "yes": "no" );
Abc_Print( -2, "\t-p : toggle using \"pdr\" for filtering [default = %s]\n", pPars->fUseDprove? "yes": "no" );
Abc_Print( -2, "\t-f : toggle starting BMC from a later frame [default = %s]\n", pPars->fUseStart? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
@ -27592,7 +27599,7 @@ int Abc_CommandAbc9Reach( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
Abc_Print( -2, "usage: &reach [-TBFCHS num] [-L file] [-ripcsyzvwh]\n" );
Abc_Print( -2, "\t verifies sequential miter using BDD-based reachability\n" );
Abc_Print( -2, "\t model checking via BDD-based reachability (similar to IWLS'95)\n" );
Abc_Print( -2, "\t-T num : approximate time limit in seconds (0=infinite) [default = %d]\n", pPars->TimeLimit );
Abc_Print( -2, "\t-B num : max number of nodes in the intermediate BDDs [default = %d]\n", pPars->nBddMax );
Abc_Print( -2, "\t-F num : max number of reachability iterations [default = %d]\n", pPars->nIterMax );
@ -27613,6 +27620,276 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9Reach2( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_ParLlb_t Pars, * pPars = &Pars;
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
Aig_Man_t * pMan;
char * pLogFileName = NULL;
int c;
extern int Llb_ManReachMinCut( Aig_Man_t * pAig, Gia_ParLlb_t * pPars );
// set defaults
Llb_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "NBFTLrbyzdvwh" ) ) != EOF )
{
switch ( c )
{
case 'N':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
pPars->nPartValue = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nPartValue < 0 )
goto usage;
break;
case 'B':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" );
goto usage;
}
pPars->nBddMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nBddMax < 0 )
goto usage;
break;
case 'F':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
pPars->nIterMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nIterMax < 0 )
goto usage;
break;
case 'T':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage;
}
pPars->TimeLimit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->TimeLimit < 0 )
goto usage;
break;
case 'L':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-L\" should be followed by a file name.\n" );
goto usage;
}
pLogFileName = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'r':
pPars->fReorder ^= 1;
break;
case 'b':
pPars->fBackward ^= 1;
break;
case 'y':
pPars->fSkipOutCheck ^= 1;
break;
case 'z':
pPars->fSkipReach ^= 1;
break;
case 'd':
pPars->fDumpReached ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
case 'w':
pPars->fVeryVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Reach(): There is no AIG.\n" );
return 1;
}
if ( Gia_ManRegNum(pAbc->pGia) == 0 )
{
Abc_Print( -1, "Abc_CommandAbc9Reach(): The current AIG has no latches.\n" );
return 0;
}
pMan = Gia_ManToAigSimple( pAbc->pGia );
pAbc->Status = Llb_ManReachMinCut( pMan, pPars );
pAbc->nFrames = pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pMan->pSeqModel );
if ( pLogFileName )
Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "&reach2" );
Aig_ManStop( pMan );
return 0;
usage:
Abc_Print( -2, "usage: &reach2 [-NFT num] [-L file] [-rbyzdvwh]\n" );
Abc_Print( -2, "\t model checking via BDD-based reachability (min-cut-based)\n" );
Abc_Print( -2, "\t-N num : partitioning value (MinVol=nANDs/N/2; MaxVol=nANDs/N) [default = %d]\n", pPars->nPartValue );
// Abc_Print( -2, "\t-B num : the BDD node increase when hints kick in [default = %d]\n", pPars->nBddMax );
Abc_Print( -2, "\t-F num : max number of reachability iterations [default = %d]\n", pPars->nIterMax );
Abc_Print( -2, "\t-T num : approximate time limit in seconds (0=infinite) [default = %d]\n", pPars->TimeLimit );
Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
Abc_Print( -2, "\t-r : enable dynamic BDD variable reordering [default = %s]\n", pPars->fReorder? "yes": "no" );
Abc_Print( -2, "\t-b : perform backward reachability analysis [default = %s]\n", pPars->fBackward? "yes": "no" );
Abc_Print( -2, "\t-y : skip checking property outputs [default = %s]\n", pPars->fSkipOutCheck? "yes": "no" );
Abc_Print( -2, "\t-z : skip reachability (run preparation phase only) [default = %s]\n", pPars->fSkipReach? "yes": "no" );
Abc_Print( -2, "\t-d : dump BDD of reached states into file \"reached.blif\" [default = %s]\n", pPars->fDumpReached? "yes": "no" );
Abc_Print( -2, "\t-v : prints verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : prints additional information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9Reach3( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_ParLlb_t Pars, * pPars = &Pars;
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
Aig_Man_t * pMan;
char * pLogFileName = NULL;
int c;
extern int Llb_NonlinCoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars );
// set defaults
Llb_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "BFTLryzvwh" ) ) != EOF )
{
switch ( c )
{
case 'B':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" );
goto usage;
}
pPars->nBddMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nBddMax < 0 )
goto usage;
break;
case 'F':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
pPars->nIterMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nIterMax < 0 )
goto usage;
break;
case 'T':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage;
}
pPars->TimeLimit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->TimeLimit < 0 )
goto usage;
break;
case 'L':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-L\" should be followed by a file name.\n" );
goto usage;
}
pLogFileName = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'r':
pPars->fReorder ^= 1;
break;
case 'y':
pPars->fSkipOutCheck ^= 1;
break;
case 'z':
pPars->fSkipReach ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
case 'w':
pPars->fVeryVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Reach(): There is no AIG.\n" );
return 1;
}
if ( Gia_ManRegNum(pAbc->pGia) == 0 )
{
Abc_Print( -1, "Abc_CommandAbc9Reach(): The current AIG has no latches.\n" );
return 0;
}
pMan = Gia_ManToAigSimple( pAbc->pGia );
pAbc->Status = Llb_NonlinCoreReach( pMan, pPars );
pAbc->nFrames = pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pMan->pSeqModel );
if ( pLogFileName )
Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "&reach2" );
Aig_ManStop( pMan );
return 0;
usage:
Abc_Print( -2, "usage: &reach3 [-BFT num] [-L file] [-ryzvh]\n" );
Abc_Print( -2, "\t model checking via BDD-based reachability (non-linear QS)\n" );
Abc_Print( -2, "\t-B num : the BDD node increase when hints kick in [default = %d]\n", pPars->nBddMax );
Abc_Print( -2, "\t-F num : max number of reachability iterations [default = %d]\n", pPars->nIterMax );
Abc_Print( -2, "\t-T num : approximate time limit in seconds (0=infinite) [default = %d]\n", pPars->TimeLimit );
Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
Abc_Print( -2, "\t-r : enable dynamic BDD variable reordering [default = %s]\n", pPars->fReorder? "yes": "no" );
Abc_Print( -2, "\t-y : skip checking property outputs [default = %s]\n", pPars->fSkipOutCheck? "yes": "no" );
Abc_Print( -2, "\t-z : skip reachability (run preparation phase only) [default = %s]\n", pPars->fSkipReach? "yes": "no" );
Abc_Print( -2, "\t-v : prints verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
// Abc_Print( -2, "\t-w : prints additional information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []

View File

@ -2940,15 +2940,15 @@ Abc_Ntk_t * Abc_NtkDarEnlarge( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarTempor( Abc_Ntk_t * pNtk, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fVerbose, int fVeryVerbose )
Abc_Ntk_t * Abc_NtkDarTempor( Abc_Ntk_t * pNtk, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fUseTransSigs, int fVerbose, int fVeryVerbose )
{
extern Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fVerbose, int fVeryVerbose );
extern Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fUseTransSigs, int fVerbose, int fVeryVerbose );
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
return NULL;
pTemp = Saig_ManTempor( pMan, nFrames, TimeOut, nConfLimit, fUseBmc, fVerbose, fVeryVerbose );
pTemp = Saig_ManTempor( pMan, nFrames, TimeOut, nConfLimit, fUseBmc, fUseTransSigs, fVerbose, fVeryVerbose );
Aig_ManStop( pMan );
if ( pTemp == NULL )
return Abc_NtkDup( pNtk );
@ -3937,11 +3937,13 @@ void Abc_NtkDarConstrProfile( Abc_Ntk_t * pNtk, int fVerbose )
SeeAlso []
***********************************************************************/
void Abc_NtkDarTest( Abc_Ntk_t * pNtk )
void Abc_NtkDarTest( Abc_Ntk_t * pNtk, int Num )
{
// extern void Saig_ManDetectConstr( Aig_Man_t * p );
// extern void Saig_ManDetectConstrFuncTest( Aig_Man_t * p );
extern void Saig_ManFoldConstrTest( Aig_Man_t * pAig );
// extern void Saig_ManFoldConstrTest( Aig_Man_t * pAig );
extern void Llb_ManComputeDomsTest( Aig_Man_t * pAig, int Num );
// extern void Fsim_ManTest( Aig_Man_t * pAig );
@ -3992,6 +3994,15 @@ Aig_ManPrintStats( pMan );
// Pdr_ManEquivClasses( pMan );
}
// Llb_ManComputeDomsTest( pMan, Num );
{
extern void Llb_ManMinCutTest( Aig_Man_t * pMan, int Num );
extern void Llb_BddStructAnalysis( Aig_Man_t * pMan );
extern void Llb_NonlinExperiment( Aig_Man_t * pAig, int Num );
// Llb_BddStructAnalysis( pMan );
Llb_ManMinCutTest( pMan, Num );
// Llb_NonlinExperiment( pMan, Num );
}
// Saig_MvManSimulate( pMan, 1 );
// Saig_ManDetectConstr( pMan );

View File

@ -720,6 +720,7 @@ EXTERN DdNode * Cudd_addRoundOff ARGS((DdManager *dd, DdNode *f, int N));
EXTERN DdNode * Cudd_addWalsh ARGS((DdManager *dd, DdNode **x, DdNode **y, int n));
EXTERN DdNode * Cudd_addResidue ARGS((DdManager *dd, int n, int m, int options, int top));
EXTERN DdNode * Cudd_bddAndAbstract ARGS((DdManager *manager, DdNode *f, DdNode *g, DdNode *cube));
EXTERN DdNode * Cudd_bddAndAbstractLimit ARGS((DdManager *manager, DdNode *f, DdNode *g, DdNode *cube, unsigned int limit));
EXTERN int Cudd_ApaNumberOfDigits ARGS((int binaryDigits));
EXTERN DdApaNumber Cudd_NewApaNumber ARGS((int digits));
EXTERN void Cudd_ApaCopy ARGS((int digits, DdApaNumber source, DdApaNumber dest));

View File

@ -109,6 +109,46 @@ Cudd_bddAndAbstract(
} /* end of Cudd_bddAndAbstract */
/**Function********************************************************************
Synopsis [Takes the AND of two BDDs and simultaneously abstracts the
variables in cube. Returns NULL if too many nodes are required.]
Description [Takes the AND of two BDDs and simultaneously abstracts
the variables in cube. The variables are existentially abstracted.
Returns a pointer to the result is successful; NULL otherwise.
In particular, if the number of new nodes created exceeds
<code>limit</code>, this function returns NULL.]
SideEffects [None]
SeeAlso [Cudd_bddAndAbstract]
******************************************************************************/
DdNode *
Cudd_bddAndAbstractLimit(
DdManager * manager,
DdNode * f,
DdNode * g,
DdNode * cube,
unsigned int limit)
{
DdNode *res;
unsigned int saveLimit = manager->maxLive;
manager->maxLive = (manager->keys - manager->dead) +
(manager->keysZ - manager->deadZ) + limit;
do {
manager->reordered = 0;
res = cuddBddAndAbstractRecur(manager, f, g, cube);
} while (manager->reordered == 1);
manager->maxLive = saveLimit;
return(res);
} /* end of Cudd_bddAndAbstractLimit */
/*---------------------------------------------------------------------------*/
/* Definition of internal functions */
/*---------------------------------------------------------------------------*/

View File

@ -174,7 +174,8 @@ Cudd_Init(
unique->memused += sizeof(DdNode *) * unique->maxSize;
unique->bReached = NULL;
unique->bFunc = NULL;
unique->bFunc2 = NULL;
return(unique);
} /* end of Cudd_Init */

View File

@ -439,7 +439,8 @@ struct DdManager { /* specialized DD symbol table */
int nvars; /* variables used so far */
int threshold; /* for pseudo var threshold value*/
#endif
DdNode * bReached;
DdNode * bFunc;
DdNode * bFunc2;
};
typedef struct Move {

View File

@ -196,6 +196,8 @@ extern DdNode * Extra_bddCreateExor( DdManager * dd, int nVars );
extern DdNode * Extra_zddPrimes( DdManager * dd, DdNode * F );
extern void Extra_bddPermuteArray( DdManager * dd, DdNode ** bNodesIn, DdNode ** bNodesOut, int nNodes, int *permut );
extern DdNode * Extra_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars );
extern DdNode * Extra_bddChangePolarity( DdManager * dd, DdNode * bFunc, DdNode * bVars );
extern DdNode * extraBddChangePolarity( DdManager * dd, DdNode * bFunc, DdNode * bVars );
#ifndef ABC_PRB
#define ABC_PRB(dd,f) printf("%s = ", #f); Extra_bddPrint(dd,f); printf("\n")

View File

@ -1013,6 +1013,32 @@ DdNode * Extra_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars )
return bRes;
}
/**Function********************************************************************
Synopsis [Changes the polarity of vars listed in the cube.]
Description []
SideEffects []
SeeAlso []
******************************************************************************/
DdNode * Extra_bddChangePolarity(
DdManager * dd, /* the DD manager */
DdNode * bFunc,
DdNode * bVars)
{
DdNode *res;
do {
dd->reordered = 0;
res = extraBddChangePolarity( dd, bFunc, bVars );
} while (dd->reordered == 1);
return(res);
} /* end of Extra_bddChangePolarity */
/*---------------------------------------------------------------------------*/
/* Definition of internal functions */
/*---------------------------------------------------------------------------*/
@ -1659,6 +1685,121 @@ cuddBddPermuteRecur( DdManager * manager /* DD manager */ ,
} /* end of cuddBddPermuteRecur */
/**Function********************************************************************
Synopsis [Performs the reordering-sensitive step of Extra_bddChangePolarity().]
Description []
SideEffects []
SeeAlso []
******************************************************************************/
DdNode * extraBddChangePolarity(
DdManager * dd, /* the DD manager */
DdNode * bFunc,
DdNode * bVars)
{
DdNode * bRes;
if ( bVars == b1 )
return bFunc;
if ( Cudd_IsConstant(bFunc) )
return bFunc;
if ( bRes = cuddCacheLookup2(dd, extraBddChangePolarity, bFunc, bVars) )
return bRes;
else
{
DdNode * bFR = Cudd_Regular(bFunc);
int LevelF = dd->perm[bFR->index];
int LevelV = dd->perm[bVars->index];
if ( LevelV < LevelF )
bRes = extraBddChangePolarity( dd, bFunc, cuddT(bVars) );
else // if ( LevelF <= LevelV )
{
DdNode * bRes0, * bRes1;
DdNode * bF0, * bF1;
DdNode * bVarsNext;
// cofactor the functions
if ( bFR != bFunc ) // bFunc is complemented
{
bF0 = Cudd_Not( cuddE(bFR) );
bF1 = Cudd_Not( cuddT(bFR) );
}
else
{
bF0 = cuddE(bFR);
bF1 = cuddT(bFR);
}
if ( LevelF == LevelV )
bVarsNext = cuddT(bVars);
else
bVarsNext = bVars;
bRes0 = extraBddChangePolarity( dd, bF0, bVarsNext );
if ( bRes0 == NULL )
return NULL;
cuddRef( bRes0 );
bRes1 = extraBddChangePolarity( dd, bF1, bVarsNext );
if ( bRes1 == NULL )
{
Cudd_RecursiveDeref( dd, bRes0 );
return NULL;
}
cuddRef( bRes1 );
if ( LevelF == LevelV )
{ // swap the cofactors
DdNode * bTemp;
bTemp = bRes0;
bRes0 = bRes1;
bRes1 = bTemp;
}
/* only aRes0 and aRes1 are referenced at this point */
/* consider the case when Res0 and Res1 are the same node */
if ( bRes0 == bRes1 )
bRes = bRes1;
/* consider the case when Res1 is complemented */
else if ( Cudd_IsComplement(bRes1) )
{
bRes = cuddUniqueInter(dd, bFR->index, Cudd_Not(bRes1), Cudd_Not(bRes0));
if ( bRes == NULL )
{
Cudd_RecursiveDeref(dd,bRes0);
Cudd_RecursiveDeref(dd,bRes1);
return NULL;
}
bRes = Cudd_Not(bRes);
}
else
{
bRes = cuddUniqueInter( dd, bFR->index, bRes1, bRes0 );
if ( bRes == NULL )
{
Cudd_RecursiveDeref(dd,bRes0);
Cudd_RecursiveDeref(dd,bRes1);
return NULL;
}
}
cuddDeref( bRes0 );
cuddDeref( bRes1 );
}
/* insert the result into cache */
cuddCacheInsert2(dd, extraBddChangePolarity, bFunc, bVars, bRes);
return bRes;
}
} /* end of extraBddChangePolarity */
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

View File

@ -311,14 +311,15 @@ static inline void Hash_FltRemove( Hash_Flt_t *p, int key )
***********************************************************************/
static inline void Hash_FltFree( Hash_Flt_t *p ) {
int bin;
Hash_Flt_Entry_t *pEntry;
Hash_Flt_Entry_t *pEntry, *pTemp;
// free bins
for(bin = 0; bin < p->nBins; bin++) {
pEntry = p->pArray[bin];
while(pEntry) {
pTemp = pEntry;
pEntry = pEntry->pNext;
ABC_FREE( pEntry );
ABC_FREE( pTemp );
}
}

View File

@ -115,19 +115,17 @@ static inline Hash_Ptr_t * Hash_PtrAlloc( int nBins )
static inline int Hash_PtrExists( Hash_Ptr_t *p, int key )
{
int bin;
Hash_Ptr_Entry_t *pEntry, **pLast;
Hash_Ptr_Entry_t *pEntry;
// find the bin where this key would live
bin = (*(p->fHash))(key, p->nBins);
// search for key
pLast = &(p->pArray[bin]);
pEntry = p->pArray[bin];
while(pEntry) {
if (pEntry->key == key) {
return 1;
}
pLast = &(pEntry->pNext);
pEntry = pEntry->pNext;
}
@ -310,16 +308,18 @@ static inline void* Hash_PtrRemove( Hash_Ptr_t *p, int key )
SeeAlso []
***********************************************************************/
static inline void Hash_PtrFree( Hash_Ptr_t *p ) {
static inline void Hash_PtrFree( Hash_Ptr_t *p )
{
int bin;
Hash_Ptr_Entry_t *pEntry;
Hash_Ptr_Entry_t *pEntry, *pTemp;
// free bins
for(bin = 0; bin < p->nBins; bin++) {
pEntry = p->pArray[bin];
while(pEntry) {
pTemp = pEntry;
pEntry = pEntry->pNext;
ABC_FREE( pEntry );
ABC_FREE( pTemp );
}
}