diff --git a/.gitignore b/.gitignore index cbb424152..f0c5201c6 100644 --- a/.gitignore +++ b/.gitignore @@ -8,6 +8,12 @@ ReleaseExt/ _/ _TEST/ +_sandwich/ +_scripts/ +*.aig +*.vcproj +*.sh +*.v lib/abc* lib/m114* lib/bip* diff --git a/Makefile b/Makefile index 0cc979b75..9a9f7abd5 100644 --- a/Makefile +++ b/Makefile @@ -33,7 +33,8 @@ MODULES := \ src/proof/pdr src/proof/abs src/proof/live src/proof/ssc src/proof/int \ src/proof/cec src/proof/acec src/proof/dch src/proof/fraig src/proof/fra src/proof/ssw \ src/aig/aig src/aig/saig src/aig/gia src/aig/ioa src/aig/ivy src/aig/hop \ - src/aig/miniaig + src/aig/miniaig \ + src/sat/bsat2 all: $(PROG) default: $(PROG) diff --git a/abc.rc b/abc.rc deleted file mode 100644 index a3efc0b09..000000000 --- a/abc.rc +++ /dev/null @@ -1,148 +0,0 @@ -# global parameters -set check # checks intermediate networks -#set checkfio # prints warnings when fanins/fanouts are duplicated -#unset checkread # does not check new networks after reading from file -#set backup # saves backup networks retrived by "undo" and "recall" -#set savesteps 1 # sets the maximum number of backup networks to save -#set progressbar # display the progress bar - -# program names for internal calls -set dotwin dot.exe -set dotunix dot -set gsviewwin gsview32.exe -set gsviewunix gv -set siswin sis.exe -set sisunix sis -set mvsiswin mvsis.exe -set mvsisunix mvsis -set capowin MetaPl-Capo10.1-Win32.exe -set capounix MetaPl-Capo10.1 -set gnuplotwin wgnuplot.exe -set gnuplotunix gnuplot - -# Niklas Een's commands -#load_plugin C:\_projects\abc\lib\bip_win.exe "BIP" - -# standard aliases -alias hi history -alias b balance -alias cg clockgate -alias cl cleanup -alias clp collapse -alias cs care_set -alias el eliminate -alias esd ext_seq_dcs -alias f fraig -alias fs fraig_sweep -alias fsto fraig_store -alias fres fraig_restore -alias fr fretime -alias ft fraig_trust -alias ic indcut -alias lp lutpack -alias pcon print_cone -alias pd print_dsd -alias pex print_exdc -d -alias pf print_factor -alias pfan print_fanio -alias pg print_gates -alias pl print_level -alias plat print_latch -alias pio print_io -alias pk print_kmap -alias pm print_miter -alias ps print_stats -alias psb print_stats -b -alias psu print_supp -alias psy print_symm -alias pun print_unate -alias q quit -alias r read -alias ra read_aiger -alias r3 retime -M 3 -alias r3f retime -M 3 -f -alias r3b retime -M 3 -b -alias ren renode -alias rh read_hie -alias ri read_init -alias rl read_blif -alias rb read_bench -alias ret retime -alias dret dretime -alias rp read_pla -alias rt read_truth -alias rv read_verilog -alias rvl read_verlib -alias rsup read_super mcnc5_old.super -alias rlib read_library -alias rlibc read_library cadence.genlib -alias rty read_liberty -alias rlut read_lut -alias rw rewrite -alias rwz rewrite -z -alias rf refactor -alias rfz refactor -z -alias re restructure -alias rez restructure -z -alias rs resub -alias rsz resub -z -alias sa set autoexec ps -alias scl scleanup -alias sif if -s -alias so source -x -alias st strash -alias sw sweep -alias ssw ssweep -alias tr0 trace_start -alias tr1 trace_check -alias trt "r c.blif; st; tr0; b; tr1" -alias u undo -alias w write -alias wa write_aiger -alias wb write_bench -alias wc write_cnf -alias wh write_hie -alias wl write_blif -alias wp write_pla -alias wv write_verilog - -# standard scripts -alias resyn "b; rw; rwz; b; rwz; b" -alias resyn2 "b; rw; rf; b; rw; rwz; b; rfz; rwz; b" -alias resyn2a "b; rw; b; rw; rwz; b; rwz; b" -alias resyn3 "b; rs; rs -K 6; b; rsz; rsz -K 6; b; rsz -K 5; b" -alias compress "b -l; rw -l; rwz -l; b -l; rwz -l; b -l" -alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l" -alias choice "fraig_store; resyn; fraig_store; resyn2; fraig_store; fraig_restore" -alias choice2 "fraig_store; balance; fraig_store; resyn; fraig_store; resyn2; fraig_store; resyn2; fraig_store; fraig_restore" -alias rwsat "st; rw -l; b -l; rw -l; rf -l" -alias drwsat2 "st; drw; b -l; drw; drf; ifraig -C 20; drw; b -l; drw; drf" -alias share "st; multi -m; sop; fx; resyn2" -alias addinit "read_init; undc; strash; zero" -alias blif2aig "undc; strash; zero" -alias v2p "&vta_gla; &ps; &gla_derive; &put; w 1.aig; pdr -v" -alias g2p "&ps; &gla_derive; &put; w 2.aig; pdr -v" -alias &sw_ "&put; sweep; st; &get" -alias &fx_ "&put; sweep; sop; fx; st; &get" -alias &dc3 "&b; &jf -K 6; &b; &jf -K 4; &b" -alias &dc4 "&b; &jf -K 7; &fx; &b; &jf -K 5; &fx; &b" - -# resubstitution scripts for the IWLS paper -alias src_rw "st; rw -l; rwz -l; rwz -l" -alias src_rs "st; rs -K 6 -N 2 -l; rs -K 9 -N 2 -l; rs -K 12 -N 2 -l" -alias src_rws "st; rw -l; rs -K 6 -N 2 -l; rwz -l; rs -K 9 -N 2 -l; rwz -l; rs -K 12 -N 2 -l" -alias resyn2rs "b; rs -K 6; rw; rs -K 6 -N 2; rf; rs -K 8; b; rs -K 8 -N 2; rw; rs -K 10; rwz; rs -K 10 -N 2; b; rs -K 12; rfz; rs -K 12 -N 2; rwz; b" -alias r2rs "b; rs -K 6; rw; rs -K 6 -N 2; rf; rs -K 8; b; rs -K 8 -N 2; rw; rs -K 10; rwz; rs -K 10 -N 2; b; rs -K 12; rfz; rs -K 12 -N 2; rwz; b" -alias compress2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; rw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l" -alias c2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; rw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l" - -# use this script to convert 1-valued and DC-valued flops for an AIG -alias fix_aig "logic; undc; strash; zero" - -# use this script to convert 1-valued and DC-valued flops for a logic network coming from BLIF -alias fix_blif "undc; strash; zero" - -# lazy man's synthesis -alias recadd3 "st; rec_add3; b; rec_add3; dc2; rec_add3; if -K 8; bidec; st; rec_add3; dc2; rec_add3; if -g -K 6; st; rec_add3" - - diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 25a3758eb..e0654afda 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1790,6 +1790,29 @@ extern void Tas_ManSatPrintStats( Tas_Man_t * p ); extern int Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 ); extern int Tas_ManSolveArray( Tas_Man_t * p, Vec_Ptr_t * vObjs ); +/*=== giaBound.c ===========================================================*/ +typedef struct Bnd_Man_t_ Bnd_Man_t; + +extern Bnd_Man_t* Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl ); +extern void Bnd_ManStop(); +//for fraig +extern void Bnd_ManMap( int iLit, int id, int spec ); +extern void Bnd_ManMerge( int id1, int id2, int phaseDiff ); +extern void Bnd_ManFinalizeMappings(); +extern void Bnd_ManPrintMappings(); +// for eco +extern int Bnd_ManCheckBound( Gia_Man_t *p ); +extern void Bnd_ManFindBound( Gia_Man_t *p ); +extern Gia_Man_t* Bnd_ManGenSpecOut( Gia_Man_t *p ); +extern Gia_Man_t* Bnd_ManGenImplOut( Gia_Man_t *p ); +extern Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPatch ); +extern void Bnd_ManSetEqOut( int eq ); +extern void Bnd_ManSetEqRes( int eq ); +extern void Bnd_ManPrintStats(); + +// util +extern Gia_Man_t* Bnd_ManCutBoundary( Gia_Man_t *p, Vec_Int_t* vEI, Vec_Int_t* vEO, Vec_Bit_t* vEI_phase, Vec_Bit_t* vEO_phase ); + ABC_NAMESPACE_HEADER_END diff --git a/src/aig/gia/giaBound.c b/src/aig/gia/giaBound.c new file mode 100644 index 000000000..7988d8655 --- /dev/null +++ b/src/aig/gia/giaBound.c @@ -0,0 +1,1048 @@ +#include "gia.h" +#include "misc/tim/tim.h" +#include "misc/vec/vecWec.h" +#include "proof/cec/cec.h" + + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Bnd_Man_t_ Bnd_Man_t; + +struct Bnd_Man_t_ +{ + int nBI; + int nBO; + int nBI_miss; + int nBO_miss; + int nInternal; + int nExtra; + int nMerged_spec; + int nMerged_impl; + + int nNode_spec; + int nNode_impl; + int nNode_patch; + int nNode_patched; + + int status; // 0: init 1: boundary found 2: out generated 3: patched generated + + int combLoop_spec; + int combLoop_impl; + int eq_out; + int eq_res; + int nChoice_spec; + int nChoice_impl; + int feedthrough; + + Vec_Ptr_t* vBmiter2Spec; + Vec_Ptr_t* vBmiter2Impl; + Vec_Int_t* vSpec2Impl; + Vec_Bit_t* vSpec2Impl_phase; + + Vec_Int_t* vBI; + Vec_Int_t* vBO; + Vec_Int_t* vEI_spec; + Vec_Int_t* vEO_spec; + Vec_Int_t* vEI_impl; + Vec_Int_t* vEO_impl; + Vec_Bit_t* vEI_phase; + Vec_Bit_t* vEO_phase; + + Vec_Int_t* vSpec2Impl_diff; + Vec_Int_t* vImpl2Spec_diff; // note that this include bufs, which should merge into their fanins + +}; + +Bnd_Man_t* pBnd; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +void Bnd_ManSetEqOut( int eq ) { pBnd -> eq_out = eq;} +void Bnd_ManSetEqRes( int eq ) { pBnd -> eq_res = eq;} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +Bnd_Man_t* Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl ) +{ + int i; + Bnd_Man_t* p = ABC_CALLOC( Bnd_Man_t, 1 ); + + p -> vBmiter2Spec = Vec_PtrAlloc( Gia_ManObjNum(pSpec) + Gia_ManObjNum(pImpl) ); + p -> vBmiter2Impl = Vec_PtrAlloc( Gia_ManObjNum(pSpec) + Gia_ManObjNum(pImpl) ); + Vec_PtrFill( p -> vBmiter2Spec, (Gia_ManObjNum(pSpec) + Gia_ManObjNum(pImpl)), 0 ); + Vec_PtrFill( p -> vBmiter2Impl, (Gia_ManObjNum(pSpec) + Gia_ManObjNum(pImpl)), 0 ); + for( i = 0; i < Vec_PtrSize( p -> vBmiter2Impl ); i ++ ) + { + Vec_PtrSetEntry( p -> vBmiter2Spec, i, Vec_IntAlloc(1) ); + Vec_PtrSetEntry( p -> vBmiter2Impl, i, Vec_IntAlloc(1) ); + } + + p -> vSpec2Impl = Vec_IntAlloc( Gia_ManObjNum(pSpec) ); + p -> vSpec2Impl_phase = Vec_BitAlloc( Gia_ManObjNum(pSpec) ); + Vec_IntFill( p -> vSpec2Impl, Gia_ManObjNum(pSpec), -1 ); + Vec_BitFill( p -> vSpec2Impl_phase, Gia_ManObjNum(pSpec), 0 ); + + p -> vBI = Vec_IntAlloc(16); + p -> vBO = Vec_IntAlloc(16); + p -> vEI_spec = Vec_IntAlloc(16); + p -> vEO_spec = Vec_IntAlloc(16); + p -> vEI_impl = Vec_IntAlloc(16); + p -> vEO_impl = Vec_IntAlloc(16); + p -> vEI_phase = Vec_BitAlloc(16); + p -> vEO_phase = Vec_BitAlloc(16); + + p -> nNode_spec = Gia_ManAndNum(pSpec) - Gia_ManBufNum(pSpec); + p -> nNode_impl = Gia_ManAndNum(pImpl); + p -> nNode_patch = 0; + p -> nNode_patched = 0; + + p -> status = 0; + p -> combLoop_spec = 0; + p -> combLoop_impl = 0; + p -> eq_out = 0; + p -> eq_res = 0; + + p -> nChoice_spec = 0; + p -> nChoice_impl = 0; + p -> feedthrough = 0; + + p -> vSpec2Impl_diff = Vec_IntAlloc( Gia_ManObjNum(pSpec) ); + Vec_IntFill( p -> vSpec2Impl_diff, Gia_ManObjNum(pSpec), 0 ); + + p -> vImpl2Spec_diff = Vec_IntAlloc( Gia_ManObjNum(pImpl) ); + Vec_IntFill( p -> vImpl2Spec_diff, Gia_ManObjNum(pImpl), 0 ); + + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bnd_ManStop() +{ + assert(pBnd); + + Vec_PtrFree( pBnd-> vBmiter2Spec ); + Vec_PtrFree( pBnd-> vBmiter2Impl ); + Vec_IntFree( pBnd-> vSpec2Impl ); + Vec_BitFree( pBnd-> vSpec2Impl_phase ); + + Vec_IntFree( pBnd->vBI ); + Vec_IntFree( pBnd->vBO ); + Vec_IntFree( pBnd->vEI_spec ); + Vec_IntFree( pBnd->vEO_spec ); + Vec_IntFree( pBnd->vEI_impl ); + Vec_IntFree( pBnd->vEO_impl ); + Vec_BitFree( pBnd->vEI_phase ); + Vec_BitFree( pBnd->vEO_phase ); + + Vec_IntFree( pBnd-> vSpec2Impl_diff ); + Vec_IntFree( pBnd-> vImpl2Spec_diff ); + + ABC_FREE( pBnd ); +} + + +void Bnd_ManMap( int iLit, int id, int spec ) +{ + + if ( spec ) + { + Vec_IntPush( Vec_PtrEntry( pBnd -> vBmiter2Spec, iLit >> 1), id ); + Vec_BitSetEntry( pBnd -> vSpec2Impl_phase, id, iLit & 1 ); + } + else + { + assert( (iLit & 1) == 0 ); + Vec_IntPush( Vec_PtrEntry( pBnd -> vBmiter2Impl, iLit >> 1), id ); + } +} + +void Bnd_ManMerge( int id_repr, int id_obj, int phaseDiff ) +{ + + + Vec_Ptr_t* vBmiter2Spec = pBnd -> vBmiter2Spec; + Vec_Ptr_t* vBmiter2Impl = pBnd -> vBmiter2Impl; + Vec_Bit_t* vSpec2Impl_phase = pBnd -> vSpec2Impl_phase; + int id, i; + + Vec_Int_t *vIds_spec_repr, *vIds_impl_repr, *vIds_spec_obj, *vIds_impl_obj; + + vIds_spec_repr = Vec_PtrEntry( vBmiter2Spec, id_repr ); + vIds_impl_repr = Vec_PtrEntry( vBmiter2Impl, id_repr ); + vIds_spec_obj = Vec_PtrEntry( vBmiter2Spec, id_obj ); + vIds_impl_obj = Vec_PtrEntry( vBmiter2Impl, id_obj ); + + Vec_IntForEachEntry( vIds_spec_obj, id, i ) + { + Vec_IntPush(vIds_spec_repr, id); + } + Vec_IntForEachEntry( vIds_impl_obj, id, i ) + { + Vec_IntPush(vIds_impl_repr, id); + } + + // handle spec2impl phase + if ( phaseDiff ) + { + Vec_IntForEachEntry( vIds_spec_obj, id, i ) + { + Vec_BitSetEntry( vSpec2Impl_phase, id, !Vec_BitEntry(vSpec2Impl_phase, id) ); + // printf( "spec id %d's phase set to %d\n", id, Vec_BitEntry(vSpec2Impl_phase, id) ); + } + } + + Vec_IntClear(vIds_spec_obj); + Vec_IntClear(vIds_impl_obj); + +} +void Bnd_ManFinalizeMappings() +{ + + Vec_Ptr_t* vBmiter2Spec = pBnd -> vBmiter2Spec; + Vec_Ptr_t* vBmiter2Impl = pBnd -> vBmiter2Impl; + Vec_Int_t* vSpec2Impl = pBnd -> vSpec2Impl; + + Vec_Int_t *vSpec, *vImpl; + int i, j, id; + + pBnd -> nMerged_impl = 0; + pBnd -> nMerged_spec = 0; + + + for( i = 0; i < Vec_PtrSize(vBmiter2Spec); i++ ) + { + vSpec = Vec_PtrEntry( vBmiter2Spec, i ); + vImpl = Vec_PtrEntry( vBmiter2Impl, i ); + + // create spec2impl + if ( Vec_IntSize(vSpec) != 0 && Vec_IntSize(vImpl) != 0 ) + { + Vec_IntForEachEntry( vSpec, id, j ) + { + Vec_IntSetEntry( vSpec2Impl, id, Vec_IntEntry(vImpl, 0) ); + + // record the number of different choice of vEI_impl, vEO_impl + Vec_IntSetEntry( pBnd->vSpec2Impl_diff, id, Vec_IntSize(vImpl)-1 ); + } + + Vec_IntForEachEntry( vImpl, id, j ) + { + // record the number of different choice of vEI_impl, vEO_impl + Vec_IntSetEntry( pBnd->vImpl2Spec_diff, id, Vec_IntSize(vSpec)-1 ); + } + + + } + + // count number of nodes merged into the same circuit + if ( Vec_IntSize(vSpec) != 0 ) + { + pBnd->nMerged_spec += Vec_IntSize(vSpec) - 1; + } + if ( Vec_IntSize(vImpl) != 0 ) + { + pBnd->nMerged_impl += Vec_IntSize(vImpl) - 1; + } + } + + +} +void Bnd_ManPrintMappings() +{ + Vec_Ptr_t* vBmiter2Spec = pBnd -> vBmiter2Spec; + Vec_Ptr_t* vBmiter2Impl = pBnd -> vBmiter2Impl; + Vec_Int_t* vIds_spec, *vIds_impl; + int k, id; + for( int j=0; j < Vec_PtrSize(vBmiter2Spec); j++ ) + { + printf("node %d: ", j); + vIds_spec = Vec_PtrEntry( vBmiter2Spec, j); + vIds_impl = Vec_PtrEntry( vBmiter2Impl, j); + Vec_IntForEachEntry(vIds_spec, id, k) + printf("%d ", id); + printf("| "); + Vec_IntForEachEntry(vIds_impl, id, k) + printf("%d ", id); + printf("\n"); + } + +} + +void Bnd_ManPrintBound() +{ + + // printf("%d nodes merged in spec\n", pBnd ->nMerged_spec - Vec_IntSize(pBnd->vBI) - Vec_IntSize(pBnd->vBO) ); + // printf("%d nodes merged in impl\n", pBnd ->nMerged_impl ); + printf("BI spec:\t"); Vec_IntPrint(pBnd -> vBI); + printf("BO spec:\t"); Vec_IntPrint(pBnd -> vBO); + printf("EI spec:\t"); Vec_IntPrint(pBnd -> vEI_spec); + printf("EI impl:\t"); Vec_IntPrint(pBnd -> vEI_impl); + printf("EI phase:\t"); Vec_BitPrint(pBnd -> vEI_phase); + printf("EO spec:\t"); Vec_IntPrint(pBnd -> vEO_spec); + printf("EO impl:\t"); Vec_IntPrint(pBnd -> vEO_impl); + printf("EO phase:\t"); Vec_BitPrint(pBnd -> vEO_phase); +} + +void Bnd_ManPrintStats() +{ + Bnd_Man_t* p = pBnd; + + + printf("\nSTATS\n"); + + int warning = 0; + if ( p->nChoice_spec > 0 ) + { + warning = 1; + printf("WARNING: multiple equiv nodes on the boundary of spec\n"); + } + if ( p->nChoice_impl > 0 ) + { + warning = 1; + printf("WARNING: multiple equiv nodes on the boundary of impl\n"); + } + if ( p->feedthrough ) + { + warning = 1; + printf("WARNING: feedthrough inside patch\n"); + } + + printf("The outsides of spec and impl are %sEQ.\n", p->eq_out ? "" : "NOT " ); + printf("The patched impl and patch are %sEQ.\n", p->eq_res ? "" : "NOT " ); + + // #internal + // nBI, nBO + // nBI_miss, nBO_miss + // nAI, nAO, nExtra + // #spec, #impl, #patched + // combLoop_spec, combLoop_impl + // status + // #different choice of impl on boundary + // warning (may be neq) + // eq_out, eq_res + + // printf("\nRESULT\n"); + // printf("%d,%d,%d,%d,%d,%d,%d,%d,%d,%d,%d,%d,%d,%d,%d,%d,%d,%d,%d,%d\n", + // p->nInternal, + // p->nBI, p->nBO, + // p->nBI_miss, p->nBO_miss, + // Vec_IntSize(p->vEI_spec), Vec_IntSize(p->vEO_spec), p->nExtra, + // p->nNode_spec, p->nNode_impl, p->nNode_patched, + // p->combLoop_spec, p->combLoop_impl, + // p->status, + // p->nChoice_impl, + // p->nChoice_spec, + // p->feedthrough, + // warning, + // p->eq_out, p->eq_res + // ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [check if the given boundary is valid. Return 0 if + the boundary is invalid. Return k if the boundary is valid and + there're k boundary inputs. ] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Bnd_ManCheckBound( Gia_Man_t * p ) +{ + int i; + Gia_Obj_t *pObj; + int valid = 1; + pBnd -> nBI = 0; + pBnd -> nBO = 0; + pBnd -> nInternal = 0; + + printf( "Checking boundary... \n"); + + Vec_Int_t *vPath; + vPath = Vec_IntAlloc( Gia_ManObjNum(p) ); + Vec_IntFill( vPath, Gia_ManObjNum(p), 0 ); + int path; + + Gia_ManForEachObjReverse1( p , pObj, i ) + { + if ( Gia_ObjIsCo( pObj ) ) + { + Vec_IntSetEntry( vPath, Gia_ObjId( p, pObj ), 1 ); + } + + path = Vec_IntEntry( vPath, Gia_ObjId(p, pObj) ); + // printf("path = %d\n", path); + + if ( path >= 8 ) + { + valid = 0; + printf("there're more than 2 bufs in a path\n"); + break; + } + + + if( Gia_ObjIsBuf( pObj ) ) + { + Vec_IntSetEntry( vPath, Gia_ObjId( p, Gia_ObjFanin0( pObj ) ), Vec_IntEntry( vPath, Gia_ObjId(p, Gia_ObjFanin0( pObj ) ) ) | path << 1 ); + if ( path == 1 ) // boundary input + { + // TODO: record BIs here since they may not be in the first n buffers + pBnd -> nBO ++; + } + } + else if ( Gia_ObjFaninNum( p, pObj ) >= 1 ) + { + Vec_IntSetEntry( vPath, Gia_ObjId( p, Gia_ObjFanin0( pObj ) ), Vec_IntEntry( vPath, Gia_ObjId(p, Gia_ObjFanin0( pObj ) ) ) | path ); + if ( Gia_ObjFaninNum( p, pObj ) >= 2 ) + { + assert( Gia_ObjFaninNum( p, pObj ) <= 2 ); + Vec_IntSetEntry( vPath, Gia_ObjId( p, Gia_ObjFanin1( pObj ) ), Vec_IntEntry( vPath, Gia_ObjId(p, Gia_ObjFanin1( pObj ) ) ) | path ); + } + if ( path == 2 ) // inside boundary + { + // TODO: record BIs here since they may not be in the first n buffers + pBnd -> nInternal ++; + } + } + else // PI or const, check validity + { + if ( (Vec_IntEntry( vPath, Gia_ObjId(p, pObj) ) | 5) != 5 ) + { + valid = 0; + printf("incorrect buf number at pi %d\n", Vec_IntEntry(vPath, Gia_ObjId(p, pObj)) ); + break; + } + } + } + + pBnd -> nBI = Gia_ManBufNum(p) - pBnd -> nBO; + + if ( !valid ) + { + printf("invalid boundary\n"); + return 0; + } + else + { + printf("valid boundary ("); + printf("#BI = %d\t#BO = %d\t", pBnd -> nBI, Gia_ManBufNum(p)- pBnd -> nBI); + printf("#Internal = %d)\n", pBnd -> nInternal ); + assert( pBnd -> nBI > 0 ); + return pBnd -> nBI; + } +} + + +int Bnd_CheckFlagRec( Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t* vFlag ) +{ + int id = Gia_ObjId(p, pObj); + if ( Vec_IntEntry(vFlag, id) == 1 ) return 1; + if ( Vec_IntEntry(vFlag, id) == 2 ) return 0; + + Vec_IntSetEntry(vFlag, id, 1); + + int ret = 1; + for( int i = 0; i < Gia_ObjFaninNum(p, pObj); i++ ) + { + if ( !Bnd_CheckFlagRec( p, Gia_ObjFanin(pObj, i), vFlag ) ) + { + ret = 0; + break; + } + } + return ret; + +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Bnd_ManCheckExtBound( Gia_Man_t * p, Vec_Int_t *vEI, Vec_Int_t *vEO ) +{ + Vec_Int_t *vFlag = Vec_IntAlloc( Gia_ManObjNum(p) ); + Vec_IntFill( vFlag, Gia_ManObjNum(p), 0 ); + int success = 1; + int i, id; + + Vec_IntForEachEntry( vEO, id, i ) + { + Vec_IntSetEntry( vFlag, id, 2 ); + } + + Vec_IntForEachEntry( vEI, id, i ) + { + if ( Vec_IntEntry(vFlag, id) == 2 ) continue; // BI connected to BO directly + + if ( !Bnd_CheckFlagRec( p, Gia_ManObj(p, id), vFlag ) ) + { + success = 0; + break; + } + } + + + Vec_IntFree(vFlag); + return success; +} + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +void Bnd_ManFindBound( Gia_Man_t * p ) +{ + Vec_Int_t *vFlag; + Vec_Ptr_t *vQ; + Gia_Obj_t *pObj; + int i, j, id, cnt; + + Vec_Int_t *vAI = Vec_IntAlloc(16); + Vec_Int_t *vAO = Vec_IntAlloc(16); + + Vec_Int_t *vSpec2Impl = pBnd -> vSpec2Impl; + Vec_Bit_t *vSpec2Impl_phase = pBnd -> vSpec2Impl_phase; + Vec_Int_t *vBI = pBnd -> vBI; + Vec_Int_t *vBO = pBnd -> vBO; + Vec_Int_t *vEI_spec = pBnd -> vEI_spec; + Vec_Int_t *vEO_spec = pBnd -> vEO_spec; + Vec_Int_t *vEI_impl = pBnd -> vEI_impl; + Vec_Int_t *vEO_impl = pBnd -> vEO_impl; + Vec_Bit_t *vEI_phase = pBnd -> vEI_phase; + Vec_Bit_t *vEO_phase = pBnd -> vEO_phase; + + + // prepare to compute extended boundary + vQ = Vec_PtrAlloc(16); + vFlag = Vec_IntAlloc( Gia_ManObjNum(p) ); + Vec_IntFill( vFlag, Gia_ManObjNum(p), 0 ); + + Gia_ManStaticFanoutStart(p); + + // save bo, bi + cnt = 0; + Gia_ManForEachBuf(p, pObj, i) + { + if ( cnt < pBnd -> nBI ) + { + Vec_IntPush( vBI, Gia_ObjId(p, pObj) ); + } + else + { + Vec_IntPush( vBO, Gia_ObjId(p, pObj) ); + } + cnt++; + } + + // compute EO, travse with flag 1 + Vec_IntForEachEntry( vBO, id, i ) + { + if ( Vec_IntEntry( vSpec2Impl, id ) == -1 ) // BO not matched + { + Vec_PtrPush( vQ, Gia_ManObj(p, id) ); + } + else + { + Vec_IntPush(vEO_spec, id); + } + } + printf("%d BO doesn't match. ", Vec_PtrSize(vQ) ); + pBnd -> nBO_miss = Vec_PtrSize(vQ); + + int cnt_extra = - Vec_PtrSize(vQ); + while( Vec_PtrSize(vQ) > 0 ) + { + pObj = Vec_PtrPop(vQ); + id = Gia_ObjId( p, pObj ); + + if ( Vec_IntEntry( vFlag, id ) == 1 ) continue; + Vec_IntSetEntry( vFlag, id, 1 ); + + // printf("%d\n", id); + + if ( Vec_IntEntry( vSpec2Impl, id ) != -1 ) // matched + { + Vec_IntPush( vEO_spec, id ); + Vec_IntPush( vAO, id ); + } + else + { + for( j = 0; j < Gia_ObjFanoutNum(p, pObj); j++ ) + { + Vec_PtrPush( vQ, Gia_ObjFanout(p, pObj, j) ); + // printf("\t%d\n", Gia_ObjId( p1, Gia_ObjFanout(p1, pObj, j) ) ); + } + } + } + // printf("%d AO found with %d extra nodes\n", Vec_IntSize(vAO) , cnt_extra ); + printf("%d AO found\n", Vec_IntSize(vAO) ); + + + // mark TFOC of BO with flag 1 to prevent them from being selected into EI + // stop at CO + Vec_IntForEachEntry( pBnd -> vBO, id, i ) + { + Vec_PtrPush( vQ, Gia_ManObj(p, id) ); + } + Vec_IntForEachEntry( vFlag, id, i ) + { + Vec_IntSetEntry( vFlag, id, 0 ); + } + while( Vec_PtrSize(vQ) > 0 ) + { + pObj = Vec_PtrPop(vQ); + id = Gia_ObjId( p, pObj ); + + if ( Vec_IntEntry( vFlag, id ) == 1 ) continue; + Vec_IntSetEntry( vFlag, id, 1 ); + + for( j = 0; j < Gia_ObjFanoutNum(p, pObj); j++ ) + { + Vec_PtrPush( vQ, Gia_ObjFanout(p, pObj, j) ); + } + } + + + + // compute EI, traverse with flag 2 + + // add unmatched BI to queue + Vec_IntForEachEntry( vBI, id, i ) + { + if ( Vec_IntEntry( vSpec2Impl, id ) == -1 ) // BO not matched + { + Vec_PtrPush( vQ, Gia_ManObj(p, id) ); + } + else + { + Vec_IntPush(vEI_spec, id); + } + } + printf("%d BI doesn't match. ", Vec_PtrSize(vQ) ); + pBnd -> nBI_miss = Vec_PtrSize(vQ); + cnt_extra -= Vec_PtrSize(vQ); + + // add AO to queue + Vec_IntForEachEntry( vAO, id, i ) + { + Vec_PtrPush( vQ, Gia_ManObj(p, id) ); + } + + // set flag 2 for BO + Vec_IntForEachEntry( vBO, id, i ) + { + Vec_IntSetEntry( vFlag, id, 2 ); + } + + // traverse down from AI and unmatched BI + while( Vec_PtrSize(vQ) > 0 ) + { + pObj = Vec_PtrPop(vQ); + id = Gia_ObjId( p, pObj ); + + if ( Vec_IntEntry( vFlag, id ) == 2 ) continue; + cnt_extra ++; + + // printf("%d\n", id); + + if ( Vec_IntEntry(vFlag, id) != 1 && Vec_IntEntry( vSpec2Impl, id ) != -1 ) // matched + { + Vec_IntPush( vEI_spec, id ); + Vec_IntPush( vAI, id ); + } + else + { + for( j = 0; j < Gia_ObjFaninNum(p, pObj); j++ ) + { + Vec_PtrPush( vQ, Gia_ObjFanin(pObj, j) ); + // printf("\t%d\n", Gia_ObjId( p1, Gia_ObjFanout(p1, pObj, j) ) ); + } + } + + Vec_IntSetEntry( vFlag, id, 2 ); + } + printf("%d AI found with %d extra nodes in total\n", Vec_IntSize(vAI) , cnt_extra ); + pBnd -> nExtra = cnt_extra; + + + // gen vEI_impl, vEO_impl, vEI_phase, vEO_phase + Vec_IntForEachEntry( vEI_spec, id, i ) + { + Vec_IntPush( vEI_impl, Vec_IntEntry( vSpec2Impl, id ) ); + Vec_BitPush( vEI_phase, Vec_BitEntry( vSpec2Impl_phase, id ) ); + } + Vec_IntForEachEntry( vEO_spec, id, i ) + { + Vec_IntPush( vEO_impl, Vec_IntEntry( vSpec2Impl, id ) ); + Vec_BitPush( vEO_phase, Vec_BitEntry( vSpec2Impl_phase, id ) ); + } + + + // count number of choice of boundary + Vec_IntForEachEntry( vEI_spec, id, i ) + pBnd -> nChoice_impl += Vec_IntEntry( pBnd -> vSpec2Impl_diff, id ); + Vec_IntForEachEntry( vEO_spec, id, i ) + pBnd -> nChoice_impl += Vec_IntEntry( pBnd -> vSpec2Impl_diff, id ); + Vec_IntForEachEntry( vEI_impl, id, i ) + pBnd -> nChoice_spec += Vec_IntEntry( pBnd -> vImpl2Spec_diff, id ); + Vec_IntForEachEntry( vEO_impl, id, i ) + pBnd -> nChoice_spec += Vec_IntEntry( pBnd -> vImpl2Spec_diff, id ); + pBnd -> nChoice_spec -= ( pBnd->nBI + pBnd ->nBO - pBnd->nBI_miss - pBnd->nBO_miss); + + // print + pBnd -> status = 1; + printf("#EI = %d\t#EO = %d\t#Extra Node = %d\n", Vec_IntSize(vEI_spec) , Vec_IntSize(vEO_spec), cnt_extra ); + Bnd_ManPrintBound(); + + // check boundary has comb loop + if ( !Bnd_ManCheckExtBound( p, vEI_spec, vEO_spec ) ) + { + printf("Combinational loop exist\n"); + pBnd -> combLoop_spec = 1; + } + + + // clean up + Vec_IntFree(vAI); + Vec_IntFree(vAO); +} + + + + +/**Function************************************************************* + + Synopsis [] + + Description [create circuit with the boundary changed to CI/CO] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +Gia_Man_t* Bnd_ManCutBoundary( Gia_Man_t *p, Vec_Int_t* vEI, Vec_Int_t* vEO, Vec_Bit_t* vEI_phase, Vec_Bit_t* vEO_phase ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + Vec_Int_t * vValue; + int i, id, lit; + + // check if the boundary has loop (EO cannot be in the TFC of EI ) + if ( !Bnd_ManCheckExtBound( p, vEI, vEO ) ) + { + printf("Combinational loop exist\n"); + pBnd -> combLoop_impl = 1; + return 0; + } + + // detect feedthrough + Gia_ManFillValue(p); + Vec_IntForEachEntry(vEO, id, i) + { + Gia_ManObj(p, id) -> Value = 1; + } + Vec_IntForEachEntry(vEI, id, i) + { + if ( Gia_ManObj(p, id) -> Value == 1 ) + pBnd -> feedthrough = 1; + } + + // initialize + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew -> pName = ABC_ALLOC( char, strlen(p->pName)+10); + sprintf( pNew -> pName, "%s_out", p -> pName ); + Gia_ManHashStart( pNew ); + Gia_ManFillValue(p); + Gia_ManConst0(p) -> Value = 0; + + + // record the original value for eo + vValue = Vec_IntAlloc( Gia_ManObjNum(p) ); + Vec_IntFill( vValue, Gia_ManObjNum(p), -1 ); + + // create ci for ci and eo + Gia_ManForEachCi( p, pObj, i ) + { + pObj -> Value = Gia_ManAppendCi( pNew ); + } + Vec_IntForEachEntry( vEO, id, i ) + { + if( Gia_ManObj(p, id) -> Value != ~0 ) + { + Vec_IntSetEntry( vValue, id, Gia_ManObj(p, id) -> Value ); + } + Gia_ManObj( p, id ) -> Value = Gia_ManAppendCi(pNew); + if ( vEO_phase && Vec_BitEntry( vEO_phase, i ) ) + { + Gia_ManObj( p, id ) -> Value ^= 1; + } + } + + + // add aig nodes + Gia_ManForEachAnd(p, pObj, i) + { + if ( pObj -> Value != ~0 ) continue; + pObj -> Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + } + + // create co for co and ei + Gia_ManForEachCo(p, pObj, i) + { + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } + Vec_IntForEachEntry( vEI, id, i ) + { + pObj = Gia_ManObj(p, id); + // lit = Gia_ManObj(p, id)->Value; + if ( Gia_ObjIsAnd(pObj) ) lit = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + else + { + assert(Gia_ObjIsCi(pObj) || Gia_ObjIsConst0(pObj)); + if ( Vec_IntEntry(vValue, id) != -1 ) + { + lit = Vec_IntEntry( vValue, id ); // EI at PI and EI merged with EO + } + else { + lit = pObj -> Value; // EI at PI + } + } + if ( vEI_phase && Vec_BitEntry( vEI_phase, i ) ) lit ^= 1; + Gia_ManAppendCo( pNew, lit ); + } + + // clean up + Vec_IntFree( vValue ); + Gia_ManHashStop( pNew ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; + +} + +Gia_Man_t* Bnd_ManGenSpecOut( Gia_Man_t* p ) +{ + printf("Generating spec_out with given boundary.\n"); + Gia_Man_t *pNew = Bnd_ManCutBoundary( p, pBnd->vEI_spec, pBnd->vEO_spec, 0, 0 ); + return pNew; +} +Gia_Man_t* Bnd_ManGenImplOut( Gia_Man_t* p ) +{ + printf("Generating impl_out with given boundary.\n"); + Gia_Man_t *pNew = Bnd_ManCutBoundary( p, pBnd->vEI_impl, pBnd->vEO_impl, pBnd->vEI_phase, pBnd->vEO_phase ); + if ( pNew ) pBnd -> status = 2; + else pBnd -> combLoop_impl = 1; + return pNew; +} + +void Bnd_AddNodeRec( Gia_Man_t *p, Gia_Man_t *pNew, Gia_Obj_t *pObj ) +{ + // TODO does this mean constant zero node? + if ( pObj -> Value != ~0 ) return; + + for( int i = 0; i < Gia_ObjFaninNum(p, pObj); i++ ) + { + Bnd_AddNodeRec( p, pNew, Gia_ObjFanin(pObj, i) ); + } + + if ( Gia_ObjIsAnd(pObj) ) + { + pObj -> Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + } + else + { + if ( Gia_ObjIsCi(pObj) ) + { + printf("Ci with value 0 encountered (id = %d)\n", Gia_ObjId(p, pObj) ); + } + assert( Gia_ObjIsCo(pObj) ); + pObj -> Value = Gia_ObjFanin0Copy(pObj); + } +} + +Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPatch ) +{ + + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i, id, cnt; + Vec_Int_t *vBI_patch, *vBO_patch; + + pBnd -> nNode_patch = Gia_ManAndNotBufNum( pPatch ); + + pNew = Gia_ManStart( Gia_ManObjNum(pOut) + Gia_ManObjNum( pSpec ) + Gia_ManObjNum(pPatch) ); + pNew -> pName = ABC_ALLOC( char, strlen(pOut->pName)+3); + sprintf( pNew -> pName, "%s_p", pOut -> pName ); + Gia_ManHashStart( pNew ); + Gia_ManFillValue(pOut); + Gia_ManFillValue(pSpec); + Gia_ManFillValue(pPatch); + Gia_ManConst0(pOut)->Value = 0; + Gia_ManConst0(pSpec)->Value = 0; + Gia_ManConst0(pPatch)->Value = 0; + + // get bi and bo in patch + cnt = 0; + vBI_patch = Vec_IntAlloc(16); + vBO_patch = Vec_IntAlloc(16); + Gia_ManForEachBuf( pPatch, pObj, i ) + { + if ( cnt < pBnd -> nBI ) + { + Vec_IntPush( vBI_patch, Gia_ObjId( pPatch, pObj ) ); + } + else + { + + Vec_IntPush( vBO_patch, Gia_ObjId( pPatch, pObj ) ); + } + cnt ++; + } + assert( Vec_IntSize( vBI_patch ) == Vec_IntSize(pBnd->vBI) ); + assert( Vec_IntSize( vBO_patch ) == Vec_IntSize(pBnd->vBO) ); + + + // add Impl (real) PI + for ( i = 0; i < Gia_ManCiNum(pSpec); i++ ) + { + pObj = Gia_ManCi(pOut, i); + pObj -> Value = Gia_ManAppendCi( pNew ); + } + + // add Impl EI to CI + // printf("adding EI to CI in Impl\n"); + for ( i = 0; i < Vec_IntSize( pBnd -> vEI_spec ); i++ ) + { + pObj = Gia_ManCo(pOut, i + Gia_ManCoNum(pSpec) ); + Bnd_AddNodeRec( pOut, pNew, pObj ); + + // set Spec EI + Gia_ManObj( pSpec, Vec_IntEntry(pBnd -> vEI_spec, i) ) -> Value = pObj -> Value; + // printf(" %d",pObj -> Value); + } + // printf("\n"); + + // add Spec BI to EI + // printf("adding BI to EI in Spec\n"); + Vec_IntForEachEntry( pBnd -> vBI, id, i ) + { + pObj = Gia_ManObj( pSpec, id ); + Bnd_AddNodeRec( pSpec, pNew, pObj ); + + // set patch bi + Gia_ManObj( pPatch, Vec_IntEntry( vBI_patch, i) ) -> Value = pObj -> Value; + // printf(" %d",pObj -> Value); + } + // printf("\n"); + + // add Patch BO to BI + // printf("adding BO to BI in Patch\n"); + Vec_IntForEachEntry( vBO_patch, id, i ) + { + pObj = Gia_ManObj( pPatch, id ); + Bnd_AddNodeRec( pPatch, pNew, pObj ); + + // set spec bo + Gia_ManObj( pSpec, Vec_IntEntry( pBnd -> vBO, i) ) -> Value = pObj -> Value; + // printf(" %d",pObj -> Value); + } + // printf("\n"); + + // add Spec EO to BO + // printf("adding EO to BO in Spec\n"); + Vec_IntForEachEntry( pBnd -> vEO_spec, id, i ) + { + pObj = Gia_ManObj( pSpec, id ); + Bnd_AddNodeRec( pSpec, pNew, pObj ); + + // set impl EO (PI) + Gia_ManCi( pOut, i + Gia_ManCiNum(pSpec) ) -> Value = pObj -> Value; + // printf(" %d",pObj -> Value); + } + // printf("\n"); + + // add Impl (real) PO to EO + // printf("adding CO to EO in Impl\n"); + for ( i = 0; i < Gia_ManCoNum(pSpec); i++ ) + { + pObj = Gia_ManCo( pOut, i ); + Bnd_AddNodeRec( pOut, pNew, pObj ); + Gia_ManAppendCo( pNew, pObj->Value ); + // printf(" %d",pObj -> Value); + } + // printf("\n"); + + + // clean up + Vec_IntFree( vBI_patch ); + Vec_IntFree( vBO_patch ); + Gia_ManHashStop( pNew ); + + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + + pBnd -> nNode_patched = Gia_ManAndNum( pNew ); + pBnd -> status = 3; + + return pNew; +} + + + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END \ No newline at end of file diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index dbedca099..46c6f4da0 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -30,6 +30,9 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// + +extern Bnd_Man_t* pBnd; + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -5674,7 +5677,7 @@ Gia_Man_t * Gia_ManDupAddFlop( Gia_Man_t * p ) ***********************************************************************/ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose ) { - Vec_Int_t * vLits; + // Vec_Int_t * vLits; Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj; int i, iLit; @@ -5692,7 +5695,7 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose ) assert( Gia_ManRegNum(p2) == 0 ); assert( Gia_ManCiNum(p1) == Gia_ManCiNum(p2) ); assert( Gia_ManCoNum(p1) == Gia_ManCoNum(p2) ); - vLits = Vec_IntAlloc( Gia_ManBufNum(p1) ); + // vLits = Vec_IntAlloc( Gia_ManBufNum(p1) ); if ( fVerbose ) printf( "Creating a boundary miter with %d inputs, %d outputs, and %d buffers.\n", Gia_ManCiNum(p1), Gia_ManCoNum(p1), Gia_ManBufNum(p1) ); @@ -5702,28 +5705,123 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose ) Gia_ManHashStart( pNew ); Gia_ManConst0(p1)->Value = 0; Gia_ManConst0(p2)->Value = 0; - Gia_ManForEachCi( p1, pObj, i ) - pObj->Value = Gia_ManCi(p2, i)->Value = Gia_ManAppendCi( pNew ); - Gia_ManForEachAnd( p2, pObj, i ) - pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - Gia_ManForEachAnd( p1, pObj, i ) { - pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - if ( Gia_ObjIsBuf(pObj) ) - Vec_IntPush( vLits, pObj->Value ); + + + for( int i = 0; i < Gia_ManCiNum(p1); i++ ) + { + int iLit = Gia_ManCi(p1, i)->Value = Gia_ManCi(p2, i) -> Value = Gia_ManAppendCi(pNew); + + pObj = Gia_ManCi(p1, i); + Bnd_ManMap( iLit, Gia_ObjId( p1, pObj ), 1 ); + + pObj = Gia_ManCi(p2, i); + Bnd_ManMap( iLit, Gia_ObjId( p2, pObj) , 0 ); + } + + // record the corresponding impl node of each lit + Gia_ManForEachAnd( p2, pObj, i ) + { + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Bnd_ManMap( pObj -> Value, Gia_ObjId(p2, pObj), 0 ); + } + + // record hashed equivalent nodes + Gia_ManForEachAnd( p1, pObj, i ) + { + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Bnd_ManMap( pObj -> Value, Gia_ObjId(p1, pObj), 1 ); + } + Gia_ManForEachCo( p2, pObj, i ) - Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); - //Gia_ManForEachCo( p1, pObj, i ) - // Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); - Vec_IntForEachEntry( vLits, iLit, i ) - Gia_ManAppendCo( pNew, iLit ); - Vec_IntFree( vLits ); + { + iLit = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } + Gia_ManForEachCo( p1, pObj, i ) + { + iLit = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } + // Vec_IntForEachEntry( vLits, iLit, i ) + // Gia_ManAppendCo( pNew, iLit ); + // Vec_IntFree( vLits ); Gia_ManHashStop( pNew ); pNew = Gia_ManCleanup( pTemp = pNew ); Gia_ManStop( pTemp ); return pNew; } +/**Function************************************************************* + Synopsis [Duplicates AIG while putting objects in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManImplFromBMiter( Gia_Man_t * p, int nPo, int nBInput ) +{ + Gia_Man_t * pNew, *pTemp; + Gia_Obj_t * pObj, *pObj2; + int i; + int nBoundI = 0, nBoundO = 0; + int nExtra; + Gia_ManFillValue( p ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + // pNew->pName = Abc_UtilStrsav( p->pName ); + // pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + + // add po of impl + Gia_ManForEachCo( p, pObj, i ) + { + if ( i < nPo ) + { + Gia_ManDupOrderDfs_rec( pNew, p, pObj ); + } + } + nExtra = Gia_ManAndNum( pNew ); + + // add boundary as buf + Gia_ManForEachCo( p, pObj, i ) + { + if ( i >= 2 * nPo ) + { + pObj2 = Gia_ObjFanin0(pObj); + if (~pObj2->Value) // visited boundary + { + if ( i >= 2 * nPo + nBInput ) + { + nBoundO ++; + } + else nBoundI ++; + } + + Gia_ManDupOrderDfs_rec( pNew, p, pObj2 ); + Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) ); + } + } + nExtra = Gia_ManAndNum( pNew ) - nExtra - Gia_ManBufNum( pNew ); + + Gia_ManForEachCi( p, pObj, i ) + if ( !~pObj->Value ) + pObj->Value = Gia_ManAppendCi(pNew); + assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(p) ); + + Gia_ManDupRemapCis( pNew, p ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + + + printf( "synthesized implementation:\n" ); + printf( "\t%d / %d input boundary recovered.\n", nBoundI, nBInput ); + printf( "\t%d / %d output boundary recovered.\n", nBoundO, Gia_ManCoNum(p)-2*nPo-nBInput ); + printf( "\t%d / %d unused nodes in the box.\n", nExtra, Gia_ManAndNum(pNew) - Gia_ManBufNum( pNew ) ); + + return pNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index 236d43b32..9e5ae3a57 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -109,4 +109,5 @@ SRC += src/aig/gia/giaAig.c \ src/aig/gia/giaTsim.c \ src/aig/gia/giaTtopt.cpp \ src/aig/gia/giaUnate.c \ - src/aig/gia/giaUtil.c + src/aig/gia/giaUtil.c \ + src/aig/gia/giaBound.c \ No newline at end of file diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 89683acf7..9a558c2da 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -599,6 +599,7 @@ static int Abc_CommandAbc9ProdAdd ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9AddFlop ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9BMiter ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9GenHie ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9StrEco ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1380,6 +1381,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&addflop", Abc_CommandAbc9AddFlop, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&bmiter", Abc_CommandAbc9BMiter, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&gen_hie", Abc_CommandAbc9GenHie, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&str_eco", Abc_CommandAbc9StrEco, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 ); { @@ -38065,7 +38067,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) int fCbs = 1, approxLim = 600, subBatchSz = 1, adaRecycle = 500, nMaxNodes = 0; Cec4_ManSetParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPMrmdckngxysopwvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPMrmdckngxysopwqvh" ) ) != EOF ) { switch ( c ) { @@ -38218,6 +38220,9 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'w': pPars->fVeryVerbose ^= 1; break; + case 'q': + pPars->fBMiterInfo ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -38282,6 +38287,7 @@ usage: Abc_Print( -2, "\t-o : toggle using the old SAT sweeper [default = %s]\n", fUseIvy? "yes": "no" ); Abc_Print( -2, "\t-p : toggle trying to prove when running the old SAT sweeper [default = %s]\n", fUseProve? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing even more verbose information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); + Abc_Print( -2, "\t-q : toggle printing additional information for boundary miters [default = %s]\n", pPars->fVeryVerbose? "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"); return 1; @@ -51945,11 +51951,21 @@ int Abc_CommandAbc9BMiter( Abc_Frame_t * pAbc, int argc, char ** argv ) char * FileName = NULL; FILE * pFile = NULL; int c, fVerbose = 0; + int bi = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + // TODO: use a flag to block Bnd_Man + while ( ( c = Extra_UtilGetopt( argc, argv, "Ivh" ) ) != EOF ) { switch ( c ) { + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + bi = atoi(argv[globalUtilOptind++]); + break; case 'v': fVerbose ^= 1; break; @@ -51994,8 +52010,9 @@ int Abc_CommandAbc9BMiter( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &bmiter [-vh] \n" ); + Abc_Print( -2, "usage: &bmiter -I [-vh] \n" ); Abc_Print( -2, "\t creates the boundary miter\n" ); + Abc_Print( -2, "\t-I : number of boundary inputs\n" ); Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\t : the implementation file\n"); @@ -52062,6 +52079,207 @@ usage: Abc_Print( -2, "\t (the PO count of should not be less than the PI count of )\n"); return 1;} +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +extern Bnd_Man_t* pBnd; +int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ); + extern void Cec4_ManSetParams( Cec_ParFra_t * pPars ); + extern Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose ); + Gia_Man_t *pImpl, *pImpl_out = 0, *pSpec_out = 0, *pMiter, *pPatch, *pPatched, *pTemp, *pBmiter;; + char * FileName = NULL; + FILE * pFile = NULL; + int c, fVerbose = 0, success = 1; + + // params + Gps_Par_t Pars, * pPars = &Pars; + memset( pPars, 0, sizeof(Gps_Par_t) ); + Cec_ParCec_t ParsCec, *pParsCec = &ParsCec; + Cec_ManCecSetDefaultParams( pParsCec ); + Cec_ParFra_t ParsFra, *pParsFra = &ParsFra; + Cec4_ManSetParams( pParsFra ); + pParsFra -> fBMiterInfo = 1; + + // TODO: save return value and return at the end of the function + + // parse options + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9StrEco(): There is no AIG.\n" ); + return 0; + } + if ( argc != globalUtilOptind + 2 ) + { + printf("%d\n", argc-globalUtilOptind); + Abc_Print( -1, "Abc_CommandAbc9StrEco(): AIG should be given on the command line.\n" ); + return 0; + } + + // read impl + FileName = argv[globalUtilOptind]; + if ( (pFile = fopen( FileName, "r" )) == NULL ) + { + Abc_Print( -1, "Cannot open input file \"%s\". ", FileName ); + if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", ".blif", ".pla", ".eqn", ".bench" )) ) + Abc_Print( 1, "Did you mean \"%s\"?", FileName ); + Abc_Print( 1, "\n" ); + return 1; + } + fclose( pFile ); + pImpl = Gia_AigerRead( FileName, 0, 0, 0 ); + if ( pImpl == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9StrEco(): Cannot read the file name on the command line.\n" ); + return 0; + } + + // read patch + FileName = argv[globalUtilOptind+1]; + if ( (pFile = fopen( FileName, "r" )) == NULL ) + { + Abc_Print( -1, "Cannot open input file \"%s\". ", FileName ); + if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", ".blif", ".pla", ".eqn", ".bench" )) ) + Abc_Print( 1, "Did you mean \"%s\"?", FileName ); + Abc_Print( 1, "\n" ); + return 1; + } + fclose( pFile ); + pPatch = Gia_AigerRead( FileName, 0, 1, 0 ); + if ( pPatch == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9StrEco(): Cannot read the file name on the command line.\n" ); + return 0; + } + + // start boundary manager + pBnd = Bnd_ManStart( pAbc->pGia, pImpl ); + + // verify if spec eq impl + pMiter = Gia_ManMiter( pAbc->pGia, pImpl, 0, 1, 0, 0, 0 ); + if ( !Cec_ManVerify( pMiter, pParsCec ) ) + { + Abc_Print( -1, "Abc_CommandAbc9StrEco(): The given impl is not equivalent to spec.\n" ); + success = 0; + } + Gia_ManStop(pMiter); + + // check boundary + if ( success ) + { + if ( 0 == Bnd_ManCheckBound( pPatch ) || 0 == Bnd_ManCheckBound( pAbc -> pGia ) ) + { + Abc_Print( -1, "Abc_CommandAbc9StrEco(): The given boundary is invalid.\n" ); + success = 0; + } + } + + if ( success ) + { + // create bmiter, run fraig + pBmiter = Gia_ManBoundaryMiter( pAbc -> pGia, pImpl, 0 ); + pTemp = Cec4_ManSimulateTest( pBmiter, pParsFra ); + Gia_ManStop(pBmiter); + Gia_ManStop(pTemp); + + // find + Bnd_ManFindBound( pAbc -> pGia ); + + // create spec_out and + pSpec_out = Bnd_ManGenSpecOut( pAbc -> pGia ); + if ( !pSpec_out ) success = 0; + pImpl_out = Bnd_ManGenImplOut( pImpl ); + if ( !pImpl_out ) success = 0; + + // Gia_AigerWrite( pSpec_out, "spec_out.aig", 0, 0, 0 ); + // Gia_AigerWrite( pImpl_out, "impl_out.aig", 0, 0, 0 ); + // Gia_ManPrintStats( pSpec_out, pPars ); + // Gia_ManPrintStats( pImpl_out, pPars ); + + } + + if ( success ) + { + + // check if spec_out and imnpl_out are equivalent + printf("Checking the equivalence of spec_out and impl_out\n"); + pMiter = Gia_ManMiter( pSpec_out, pImpl_out, 0, 1, 0, 0, 0 ); + Bnd_ManSetEqOut( Cec_ManVerify( pMiter, pParsCec ) ); + Gia_ManStop( pMiter ); + + // generate patched impl + printf("Generating patched impl\n"); + pPatched = Bnd_ManGenPatched( pImpl_out, pAbc->pGia, pPatch ); + + // generate patched spec just for debugging + printf("Generating patched spec\n"); + pTemp = Bnd_ManGenPatched( pSpec_out, pAbc->pGia, pPatch ); + printf("Checking the equivalence of patched spec and patched impl\n"); + pMiter = Gia_ManMiter( pTemp, pPatched, 0, 1, 0, 0, 0 ); + Cec_ManVerify( pMiter, pParsCec ); + Gia_ManStop( pMiter ); + printf("Checking the equivalence of patched spec and patch\n"); + pMiter = Gia_ManMiter( pTemp, pPatch, 0, 1, 0, 0, 0 ); + Cec_ManVerify( pMiter, pParsCec ); + Gia_ManStop( pMiter ); + + Gia_ManStop( pTemp ); + + // check if patched is equiv to patch + printf("Checking the equivalence of patched impl and patch\n"); + pMiter = Gia_ManMiter( pPatch, pPatched, 0, 1, 0, 0, 0 ); + Bnd_ManSetEqRes( Cec_ManVerify( pMiter, pParsCec ) ); + Gia_ManStop( pMiter ); + + } + + Bnd_ManPrintStats(); + + Gia_ManStop( pImpl ); + Gia_ManStop( pPatch ); + if ( pSpec_out ) Gia_ManStop( pSpec_out ); + if ( pImpl_out ) Gia_ManStop( pImpl_out ); + if ( success ) + { + Abc_FrameUpdateGia( pAbc, pPatched ); + } + Bnd_ManStop(); + + return 0; + +usage: + Abc_Print( -2, "usage: &str_eco -I [-vh] \n" ); + Abc_Print( -2, "\t SAT-sweeping-based ECO\n" ); + Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "\t : the implementation aig. (should be equivalent to spec)\n"); + Abc_Print( -2, "\t : the modified spec. (should be a hierarchical AIG)\n"); + return 1; +} /**Function************************************************************* diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c index 6086fc616..6077a20c2 100644 --- a/src/base/abci/abcMiter.c +++ b/src/base/abci/abcMiter.c @@ -789,6 +789,7 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial, int fVer pNtkFrames->pName = Extra_UtilStrsav(Buffer); // map the constant nodes Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkFrames); + // create new latches (or their initial values) and remember them in the new latches if ( !fInitial ) { diff --git a/src/misc/vec/vecBit.h b/src/misc/vec/vecBit.h index e41d95aa9..9b0af9d94 100644 --- a/src/misc/vec/vecBit.h +++ b/src/misc/vec/vecBit.h @@ -626,6 +626,27 @@ static inline void Vec_BitReset( Vec_Bit_t * p ) p->pArray[i] = 0; } + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_BitPrint( Vec_Bit_t * p ) +{ + int i, Entry; + printf( "Vector has %d entries: {", Vec_BitSize(p) ); + Vec_BitForEachEntry( p, Entry, i ) + printf( " %d", Entry ); + printf( " }\n" ); +} + ABC_NAMESPACE_HEADER_END #endif diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h index d11bca3c3..c9aa96658 100644 --- a/src/proof/cec/cec.h +++ b/src/proof/cec/cec.h @@ -120,6 +120,8 @@ struct Cec_ParFra_t_ int fVeryVerbose; // verbose stats int fVerbose; // verbose stats int iOutFail; // the failed output + int fBMiterInfo; // printing BMiter information + int nPO; // number of po in original design given a bmiter }; // combinational equivalence checking parameters diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index 281deb0e9..b198c7ffe 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -219,6 +219,7 @@ void Cec4_ManSetParams( Cec_ParFra_t * pPars ) pPars->nSatVarMax = 1000; // the max number of SAT variables before recycling SAT solver pPars->nCallsRecycle = 500; // calls to perform before recycling SAT solver pPars->nGenIters = 100; // pattern generation iterations + pPars->fBMiterInfo = 0; // printing BMiter information } /**Function************************************************************* @@ -1781,8 +1782,10 @@ void Gia_ManRemoveWrongChoices( Gia_Man_t * p ) } //Abc_Print( 1, "Removed %d wrong choices.\n", Counter ); } + int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** ppNew, int fSimOnly ) { + Cec4_Man_t * pMan = Cec4_ManCreate( p, pPars ); Gia_Obj_t * pObj, * pRepr; int i, fSimulate = 1; @@ -1878,8 +1881,16 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p if ( pRepr == NULL ) continue; } + int id_obj = Gia_ObjId( p, pObj ); + int id_repr = Gia_ObjId( p, pRepr ); + if ( Abc_Lit2Var(pObj->Value) == Abc_Lit2Var(pRepr->Value) ) { + if ( pPars->fBMiterInfo ) + { + Bnd_ManMerge( id_repr, id_obj, pObj->fPhase ^ pRepr->fPhase ); + } + assert( (pObj->Value ^ pRepr->Value) == (pObj->fPhase ^ pRepr->fPhase) ); Gia_ObjSetProved( p, i ); if ( Gia_ObjId(p, pRepr) == 0 ) @@ -1887,8 +1898,26 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p continue; } if ( Cec4_ManSweepNode(pMan, i, Gia_ObjId(p, pRepr)) && Gia_ObjProved(p, i) ) + { + if (pPars->fBMiterInfo){ + + Bnd_ManMerge( id_repr, id_obj, pObj->fPhase ^ pRepr->fPhase ); + // printf( "proven %d merged into %d (phase : %d)\n", Gia_ObjId(p, pObj), Gia_ObjId(p,pRepr), pObj->fPhase ^ pRepr -> fPhase ); + + } pObj->Value = Abc_LitNotCond( pRepr->Value, pObj->fPhase ^ pRepr->fPhase ); + + + } } + + if ( pPars->fBMiterInfo ) + { + // print + Bnd_ManFinalizeMappings(); + // Bnd_ManPrintMappings(); + } + if ( p->iPatsPi > 0 ) { abctime clk2 = Abc_Clock(); @@ -1937,6 +1966,7 @@ Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ) { Gia_Man_t * pNew = NULL; Cec4_ManPerformSweeping( p, pPars, &pNew, 0 ); + return pNew; } void Cec4_ManSimulateTest2( Gia_Man_t * p, int nConfs, int fVerbose )