diff --git a/.gitignore b/.gitignore index cdf34f18d..9bd049424 100644 --- a/.gitignore +++ b/.gitignore @@ -31,6 +31,7 @@ src/aig/ddb/ *.plg *.zip +*.DS_Store abcspaceext.dsw abcext.dsp diff --git a/Makefile b/Makefile index dc909bb63..a546f65fd 100644 --- a/Makefile +++ b/Makefile @@ -26,9 +26,9 @@ MODULES := \ src/misc/vec src/misc/hash src/misc/tim src/misc/bzlib src/misc/zlib \ src/misc/mem src/misc/bar src/misc/bbl src/misc/parse \ src/opt/cut src/opt/fxu src/opt/fxch src/opt/rwr src/opt/mfs src/opt/sim \ - src/opt/ret src/opt/fret src/opt/res src/opt/lpk src/opt/nwk src/opt/rwt \ + src/opt/ret src/opt/fret src/opt/res src/opt/lpk src/opt/nwk src/opt/rwt src/opt/rar \ src/opt/cgt src/opt/csw src/opt/dar src/opt/dau src/opt/dsc src/opt/sfm src/opt/sbd \ - src/sat/bsat src/sat/xsat src/sat/satoko src/sat/csat src/sat/msat src/sat/psat src/sat/cnf src/sat/bmc src/sat/glucose src/sat/glucose2 \ + src/sat/bsat src/sat/xsat src/sat/satoko src/sat/csat src/sat/msat src/sat/psat src/sat/cnf src/sat/bmc src/sat/glucose src/sat/glucose2 src/sat/kissat src/sat/cadical \ src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky \ src/bool/rsb src/bool/rpo \ src/proof/pdr src/proof/abs src/proof/live src/proof/ssc src/proof/int \ diff --git a/abclib.dsp b/abclib.dsp index 559d59d2a..921030b34 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -691,6 +691,10 @@ SOURCE=.\src\base\io\ioWriteGml.c # End Source File # Begin Source File +SOURCE=.\src\base\io\ioWriteHMetis.c +# End Source File +# Begin Source File + SOURCE=.\src\base\io\ioWriteList.c # End Source File # Begin Source File @@ -2514,6 +2518,742 @@ SOURCE=.\src\sat\glucose2\Vec.h SOURCE=.\src\sat\glucose2\XAlloc.h # End Source File # End Group +# Begin Group "kissat" + +# PROP Default_Filter "" +# Begin Source File + +SOURCE=.\src\sat\kissat\allocate.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\analyze.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\ands.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\arena.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\assign.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\averages.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\backbone.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\backtrack.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\build.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\bump.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\check.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\classify.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\clause.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\collect.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\colors.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\compact.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\config.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\congruence.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\decide.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\deduce.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\definition.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\dense.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\dump.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\eliminate.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\equivalences.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\error.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\extend.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\factor.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\fastel.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\file.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\flags.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\format.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\forward.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\gates.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\heap.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\ifthenelse.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\import.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\internal.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\kimits.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\kissatSolver.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\kissatTest.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\kitten.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\kptions.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\krite.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\kucky.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\learn.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\logging.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\minimize.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\mode.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\phases.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\preprocess.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\print.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\probe.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\profile.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\promote.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\proof.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\propbeyond.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\propdense.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\propinitially.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\proprobe.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\propsearch.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\queue.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\reduce.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\reluctant.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\reorder.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\rephase.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\report.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\resize.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\resolve.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\resources.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\restart.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\search.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\shrink.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\smooth.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\sort.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\stack.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\statistics.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\strengthen.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\substitute.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\sweep.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\terminate.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\tiers.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\trail.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\transitive.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\utilities.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\vector.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\vivify.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\walk.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\warmup.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\watch.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\kissat\weaken.c +# End Source File +# End Group +# Begin Group "cadical" + +# PROP Default_Filter "" +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_kitten.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_analyze.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_arena.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_assume.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_averages.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_backtrack.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_backward.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_bins.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_block.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_ccadical.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_checker.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_clause.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_collect.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_compact.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_condition.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_config.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_congruence.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_constrain.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_contract.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_cover.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_decide.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_decompose.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_deduplicate.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_definition.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_drattracer.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_elim.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_elimfast.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_ema.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_extend.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_external.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_external_propagate.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_factor.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_file.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_flags.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_flip.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_format.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_frattracer.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_gates.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_idruptracer.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_instantiate.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_internal.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_ipasir.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_lidruptracer.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_limit.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_logging.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_lookahead.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_lratchecker.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_lrattracer.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_lucky.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_message.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_minimize.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_occs.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_options.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_parse.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_phases.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_probe.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_profile.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_proof.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_propagate.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_queue.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_random.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_reap.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_reduce.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_rephase.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_report.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_resources.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_restart.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_restore.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_score.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_shrink.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_signal.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_solution.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_solver.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_stable.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_stats.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_subsume.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_sweep.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_terminal.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_ternary.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_tier.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_transred.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_unstable.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_util.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_var.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_veripbtracer.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_version.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_vivify.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_walk.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadical_watch.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadicalSolver.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\cadical\cadicalTest.c +# End Source File +# End Group # End Group # Begin Group "opt" @@ -2578,6 +3318,54 @@ SOURCE=.\src\opt\fxu\fxuSingle.c SOURCE=.\src\opt\fxu\fxuUpdate.c # End Source File # End Group +# Begin Group "rar" + +# PROP Default_Filter "" +# Begin Source File + +SOURCE=.\src\opt\rar\rewire_map.h +# End Source File +# Begin Source File + +SOURCE=.\src\opt\rar\rewire_miaig.h +# End Source File +# Begin Source File + +SOURCE=.\src\opt\rar\rewire_rar.h +# End Source File +# Begin Source File + +SOURCE=.\src\opt\rar\rewire_rng.h +# End Source File +# Begin Source File + +SOURCE=.\src\opt\rar\rewire_time.h +# End Source File +# Begin Source File + +SOURCE=.\src\opt\rar\rewire_tt.h +# End Source File +# Begin Source File + +SOURCE=.\src\opt\rar\rewire_vec.h +# End Source File +# Begin Source File + +SOURCE=.\src\opt\rar\rewire_map.c +# End Source File +# Begin Source File + +SOURCE=.\src\opt\rar\rewire_miaig.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\opt\rar\rewire_rar.c +# End Source File +# Begin Source File + +SOURCE=.\src\opt\rar\rewire_rng.c +# End Source File +# End Group # Begin Group "rwr" # PROP Default_Filter "" @@ -4111,6 +4899,10 @@ SOURCE=.\src\misc\util\utilBridge.c # End Source File # Begin Source File +SOURCE=.\src\misc\util\utilBSet.c +# End Source File +# Begin Source File + SOURCE=.\src\misc\util\utilCex.c # End Source File # Begin Source File @@ -5207,6 +5999,10 @@ SOURCE=.\src\aig\gia\giaRex.c # End Source File # Begin Source File +SOURCE=.\src\aig\gia\giaRrr.cpp +# End Source File +# Begin Source File + SOURCE=.\src\aig\gia\giaSat3.c # End Source File # Begin Source File diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index bb9e7ad7a..b950da4be 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -249,6 +249,11 @@ struct Gia_Man_t_ int iFirstPoId; int iFirstAndObj; int iFirstPoObj; + Vec_Str_t * vTTISOPs; // truth tables from ISOP computation + Vec_Int_t * vTTLut; // truth tables from ISOP computation + Vec_Int_t * vMFFCsInfo; // MFFC information + Vec_Int_t * vMFFCsLuts; // MFFCs for each lut + Vec_Ptr_t * vLutsRankings; // LUTs rankings of inputs }; @@ -1431,6 +1436,7 @@ extern void Gia_ManEquivFixOutputPairs( Gia_Man_t * p ); extern int Gia_ManCheckTopoOrder( Gia_Man_t * p ); extern int * Gia_ManDeriveNexts( Gia_Man_t * p ); extern void Gia_ManDeriveReprs( Gia_Man_t * p ); +extern void Gia_ManDeriveReprsFromSibls( Gia_Man_t *p ); extern int Gia_ManEquivCountLits( Gia_Man_t * p ); extern int Gia_ManEquivCountLitsAll( Gia_Man_t * p ); extern int Gia_ManEquivCountClasses( Gia_Man_t * p ); @@ -1801,6 +1807,9 @@ extern Gia_Man_t * Gia_ManTtoptCare( Gia_Man_t * p, int nIns, int nOuts, extern Gia_Man_t * Gia_ManTransductionBdd( Gia_Man_t * pGia, int nType, int fMspf, int nRandom, int nSortType, int nPiShuffle, int nParameter, int fLevel, Gia_Man_t * pExdc, int fNewLine, int nVerbose ); extern Gia_Man_t * Gia_ManTransductionTt( Gia_Man_t * pGia, int nType, int fMspf, int nRandom, int nSortType, int nPiShuffle, int nParameter, int fLevel, Gia_Man_t * pExdc, int fNewLine, int nVerbose ); +/*=== giaRrr.cpp ===========================================================*/ +extern Gia_Man_t * Gia_ManRrr( Gia_Man_t *pGia, int iSeed, int nWords, int nTimeout, int nSchedulerVerbose, int nPartitionerVerbose, int nOptimizerVerbose, int nAnalyzerVerbose, int nSimulatorVerbose, int nSatSolverVerbose, int fUseBddCspf, int fUseBddMspf, int nConflictLimit, int nSortType, int nOptimizerFlow, int nSchedulerFlow, int nDistance, int nRestarts, int nThreads, int nWindowSize, int fDeterministic ); + /*=== giaCTas.c ===========================================================*/ typedef struct Tas_Man_t_ Tas_Man_t; extern Tas_Man_t * Tas_ManAlloc( Gia_Man_t * pAig, int nBTLimit ); @@ -1843,6 +1852,8 @@ 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 ); +extern int Gia_ObjCheckMffc( Gia_Man_t * p, Gia_Obj_t * pRoot, int Limit, Vec_Int_t * vNodes, Vec_Int_t * vLeaves, Vec_Int_t * vInners ); + ABC_NAMESPACE_HEADER_END diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c index c764a0993..07bab5fec 100644 --- a/src/aig/gia/giaAig.c +++ b/src/aig/gia/giaAig.c @@ -19,10 +19,12 @@ ***********************************************************************/ #include "giaAig.h" +#include "aig/gia/gia.h" #include "proof/fra/fra.h" #include "proof/dch/dch.h" #include "opt/dar/dar.h" #include "opt/dau/dau.h" +#include ABC_NAMESPACE_IMPL_START @@ -191,6 +193,8 @@ Gia_Man_t * Gia_ManFromAigChoices( Aig_Man_t * p ) Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) ); //assert( Gia_ManObjNum(pNew) == Aig_ManObjNum(p) ); //Gia_ManCheckChoices( pNew ); + if ( pNew->pSibls ) + Gia_ManDeriveReprsFromSibls( pNew ); return pNew; } diff --git a/src/aig/gia/giaAigerExt.c b/src/aig/gia/giaAigerExt.c index d149b0a5e..d9f86f294 100644 --- a/src/aig/gia/giaAigerExt.c +++ b/src/aig/gia/giaAigerExt.c @@ -314,7 +314,7 @@ int Gia_AigerWriteCellMappingInstance( Gia_Man_t * p, unsigned char * pBuffer, i Vec_Str_t * Gia_AigerWriteCellMappingDoc( Gia_Man_t * p ) { unsigned char * pBuffer; - int i, iFan, nCells = 0, nInstances = 0, nSize = 8, nSize2 = 0; + int i, nCells = 0, nInstances = 0, nSize = 8, nSize2 = 0; Mio_Cell2_t * pCells = Mio_CollectRootsNewDefault2( 6, &nCells, 0 ); assert( pCells ); diff --git a/src/aig/gia/giaDeep.c b/src/aig/gia/giaDeep.c index 8d563726f..3698c2cd7 100644 --- a/src/aig/gia/giaDeep.c +++ b/src/aig/gia/giaDeep.c @@ -162,6 +162,65 @@ Gia_Man_t * Gia_ManDeepSyn( Gia_Man_t * pGia, int nIters, int nNoImpr, int TimeO return pBest; } +/**Function************************************************************* + + Synopsis [Generating one AIG by applying a randomized script.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManRandSyn( Gia_Man_t * p, unsigned random_seed ) +{ + char * pCompress2rs = "balance -l; resub -K 6 -l; rewrite -l; resub -K 6 -N 2 -l; refactor -l; resub -K 8 -l; balance -l; resub -K 8 -N 2 -l; rewrite -l; resub -K 10 -l; rewrite -z -l; resub -K 10 -N 2 -l; balance -l; resub -K 12 -l; refactor -z -l; resub -K 12 -N 2 -l; rewrite -z -l; balance -l"; + unsigned Rand = random_seed; + int fDch = Rand & 1; + //int fCom = (Rand >> 1) & 3; + int fCom = (Rand >> 1) & 1; + int fFx = (Rand >> 2) & 1; + int fUseTwo = 0; + int KLut = fUseTwo ? 2 + (Rand % 5) : 3 + (Rand % 4); + //int fChange = 0; + char Command[2000]; + char pComp[1000]; + if ( fCom == 3 ) + sprintf( pComp, "; &put; %s; %s; %s; &get", pCompress2rs, pCompress2rs, pCompress2rs ); + else if ( fCom == 2 ) + sprintf( pComp, "; &put; %s; %s; &get", pCompress2rs, pCompress2rs ); + else if ( fCom == 1 ) + sprintf( pComp, "; &put; %s; &get", pCompress2rs ); + else if ( fCom == 0 ) + sprintf( pComp, "; &dc2" ); + sprintf( Command, "&dch%s; &if -a -K %d; &mfs -e -W 20 -L 20%s%s", + fDch ? " -f" : "", KLut, fFx ? "; &fx; &st" : "", pComp ); + Gia_Man_t * pOld = Abc_FrameGetGia(Abc_FrameGetGlobalFrame()); + Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), Gia_ManDup(p) ); + if ( Abc_FrameIsBatchMode() ) + { + if ( Cmd_CommandExecute(Abc_FrameGetGlobalFrame(), Command) ) + { + Abc_Print( 1, "Something did not work out with the command \"%s\".\n", Command ); + return NULL; + } + } + else + { + Abc_FrameSetBatchMode( 1 ); + if ( Cmd_CommandExecute(Abc_FrameGetGlobalFrame(), Command) ) + { + Abc_Print( 1, "Something did not work out with the command \"%s\".\n", Command ); + return NULL; + } + Abc_FrameSetBatchMode( 0 ); + } + Gia_Man_t * pRes = Abc_FrameGetGia(Abc_FrameGetGlobalFrame()); + Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), pOld ); + return pRes; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index 09def827d..36e604153 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -310,6 +310,39 @@ void Gia_ManDeriveReprs( Gia_Man_t * p ) } } +/**Function************************************************************* + + Synopsis [Given pSibls, derives original representitives and nexts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +void Gia_ManDeriveReprsFromSibls( Gia_Man_t *p ) +{ + + int i, iObj; + assert( !p->pReprs && p->pSibls ); + p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) ); + for ( i = 0; i < Gia_ManObjNum(p); i++ ) + Gia_ObjSetRepr( p, i, GIA_VOID ); + for ( i = 0; i < Gia_ManObjNum(p); i++ ) + { + if ( p->pSibls[i] == 0 ) + continue; + if ( p->pReprs[i].iRepr != GIA_VOID ) + continue; + for ( iObj = p->pSibls[i]; iObj; iObj = p->pSibls[iObj] ) + p->pReprs[iObj].iRepr = i; + } + ABC_FREE( p->pNexts ); + p->pNexts = Gia_ManDeriveNexts( p ); +} + /**Function************************************************************* Synopsis [] @@ -2770,7 +2803,10 @@ void Gia_ManTransferEquivs2( Gia_Man_t * p, Gia_Man_t * pOld ) { Vec_IntClear( vClass ); Gia_ClassForEachObj( p, i, k ) - Vec_IntPushUnique( vClass, Abc_Lit2Var(Gia_ManObj(p, k)->Value) ); + if ( (int)Gia_ManObj(p, k)->Value >= 0 ) + Vec_IntPushUnique( vClass, Abc_Lit2Var(Gia_ManObj(p, k)->Value) ); + if ( Vec_IntSize( vClass ) <= 1 ) + continue; assert( Vec_IntSize( vClass ) > 1 ); Vec_IntSort( vClass, 0 ); iRepr = Vec_IntEntry( vClass, 0 ); diff --git a/src/aig/gia/giaFx.c b/src/aig/gia/giaFx.c index c20241ed1..7517072e7 100644 --- a/src/aig/gia/giaFx.c +++ b/src/aig/gia/giaFx.c @@ -217,7 +217,9 @@ Vec_Wec_t * Gia_ManFxRetrieve( Gia_Man_t * p, Vec_Str_t ** pvCompl, int fReverse int nVars = Gia_ObjLutSize( p, i ); int * pVars = Gia_ObjLutFanins( p, i ); word * pTruth = Vec_WrdEntryP( vTruths, Counter++ * nWords ); + Abc_TtFlipVar5( pTruth, nVars ); int Status = Kit_TruthIsop( (unsigned *)pTruth, nVars, vCover, 1 ); + Abc_TtFlipVar5( pTruth, nVars ); if ( Vec_IntSize(vCover) == 0 || (Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover,0) == 0) ) { Vec_StrWriteEntry( *pvCompl, pObj->Value, (char)(Vec_IntSize(vCover) == 0) ); diff --git a/src/aig/gia/giaGen.c b/src/aig/gia/giaGen.c index 03b194e7c..a807fe60f 100644 --- a/src/aig/gia/giaGen.c +++ b/src/aig/gia/giaGen.c @@ -1302,6 +1302,65 @@ Gia_Man_t * Gia_ManGenMux( int nIns, char * pNums ) return p; } + +/**Function************************************************************* + + Synopsis [Generates N-bit sorter using pair-wise sorting algorithm.] + + Description [https://en.wikipedia.org/wiki/Pairwise_sorting_network] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Gia_ManGenSorterOne( Gia_Man_t * p, int * pLits, int i, int k ) +{ + int Lit1 = Gia_ManAppendAnd( p, pLits[i], pLits[k] ); + int Lit2 = Gia_ManAppendOr ( p, pLits[i], pLits[k] ); + pLits[i] = Lit1; + pLits[k] = Lit2; +} +static inline void Gia_ManGenSorterConstrMerge( Gia_Man_t * p, int * pLits, int lo, int hi, int r ) +{ + int i, step = r * 2; + if ( step < hi - lo ) + { + Gia_ManGenSorterConstrMerge( p, pLits, lo, hi-r, step ); + Gia_ManGenSorterConstrMerge( p, pLits, lo+r, hi, step ); + for ( i = lo+r; i < hi-r; i += step ) + Gia_ManGenSorterOne( p, pLits, i, i+r ); + } +} +static inline void Gia_ManGenSorterConstrRange( Gia_Man_t * p, int * pLits, int lo, int hi ) +{ + if ( hi - lo >= 1 ) + { + int i, mid = lo + (hi - lo) / 2; + for ( i = lo; i <= mid; i++ ) + Gia_ManGenSorterOne( p, pLits, i, i + (hi - lo + 1) / 2 ); + Gia_ManGenSorterConstrRange( p, pLits, lo, mid ); + Gia_ManGenSorterConstrRange( p, pLits, mid+1, hi ); + Gia_ManGenSorterConstrMerge( p, pLits, lo, hi, 1 ); + } +} +Gia_Man_t * Gia_ManGenSorter( int LogN ) +{ + int i, nVars = 1 << LogN; + int nVarsAlloc = nVars + 2 * (nVars * LogN * (LogN-1) / 4 + nVars - 1); + Vec_Int_t * vLits = Vec_IntAlloc( nVars ); + Gia_Man_t * p = Gia_ManStart( 1 + 2*nVars + nVarsAlloc ); + p->pName = Abc_UtilStrsav( "sorter" ); + for ( i = 0; i < nVars; i++ ) + Vec_IntPush( vLits, Gia_ManAppendCi(p) ); + Gia_ManGenSorterConstrRange( p, Vec_IntArray(vLits), 0, nVars - 1 ); + for ( i = 0; i < nVars; i++ ) + Gia_ManAppendCo( p, Vec_IntEntry(vLits, i) ); + Vec_IntFree( vLits ); + return p; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 8ce1db834..d0af551b0 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -807,7 +807,7 @@ void Gia_ManPrintNpnClasses( Gia_Man_t * p ) int i, k, iFan, Class, OtherClasses, OtherClasses2, nTotal, Counter, Counter2; unsigned * pTruth; int nLutSize = 0; assert( Gia_ManHasMapping(p) ); - assert( Gia_ManLutSizeMax( p ) <= 4 ); + //assert( Gia_ManLutSizeMax( p ) <= 4 ); vLeaves = Vec_IntAlloc( 100 ); vVisited = Vec_IntAlloc( 100 ); vTruth = Vec_IntAlloc( (1<<16) ); diff --git a/src/aig/gia/giaMfs.c b/src/aig/gia/giaMfs.c index f4a841510..81eb298d3 100644 --- a/src/aig/gia/giaMfs.c +++ b/src/aig/gia/giaMfs.c @@ -422,7 +422,9 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes ) int nVarsNew; Abc_TtSimplify( pTruth, Vec_IntArray(vLeaves), Vec_IntSize(vLeaves), &nVarsNew ); Vec_IntShrink( vLeaves, nVarsNew ); + Abc_TtFlipVar5( pTruth, Vec_IntSize(vLeaves) ); iLitNew = Gia_ManFromIfLogicCreateLut( pNew, pTruth, vLeaves, vCover, vMapping, vMapping2 ); + Abc_TtFlipVar5( pTruth, Vec_IntSize(vLeaves) ); if ( MapSize < Vec_IntSize(vMapping2) ) { assert( Vec_IntEntryLast(vMapping2) == Abc_Lit2Var(iLitNew) ); @@ -430,7 +432,11 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes ) } } else + { + Abc_TtFlipVar5( pTruth, Vec_IntSize(vLeaves) ); iLitNew = Gia_ManFromIfLogicCreateLut( pNew, pTruth, vLeaves, vCover, vMapping, vMapping2 ); + Abc_TtFlipVar5( pTruth, Vec_IntSize(vLeaves) ); + } } else // internal CO { diff --git a/src/aig/gia/giaMini.c b/src/aig/gia/giaMini.c index 5f7ca0d57..5ebedfb78 100644 --- a/src/aig/gia/giaMini.c +++ b/src/aig/gia/giaMini.c @@ -555,6 +555,23 @@ char * Abc_FrameGiaOutputMiniLutAttr( Abc_Frame_t * pAbc, void * pMiniLut ) printf( "Current network in ABC framework is not defined.\n" ); return Gia_ManToMiniLutAttr( pGia, pMiniLut ); } +int * Abc_FrameGiaOutputMiniLutObj( Abc_Frame_t * pAbc ) +{ + int * pRes = NULL; + if ( pAbc == NULL ) + printf( "ABC framework is not initialized by calling Abc_Start()\n" ); + if ( pAbc->vMiniLutObjs == NULL ) + printf( "MiniLut objects are not defined.\n" ); + pRes = Vec_IntReleaseArray( pAbc->vMiniLutObjs ); + Vec_IntFreeP( &pAbc->vMiniLutObjs ); + return pRes; +} +void Abc_FrameSetObjDelays( Abc_Frame_t * pAbc, int * pDelays, int nDelays ) +{ + Vec_IntFreeP( &pAbc->vObjDelays ); + pAbc->vObjDelays = Vec_IntAllocArrayCopy( pDelays, nDelays ); +} + /**Function************************************************************* diff --git a/src/aig/gia/giaNf.c b/src/aig/gia/giaNf.c index f41d8dd49..f70a63135 100644 --- a/src/aig/gia/giaNf.c +++ b/src/aig/gia/giaNf.c @@ -1172,7 +1172,10 @@ void Nf_ManCutMatchOne( Nf_Man_t * p, int iObj, int * pCut, int * pCutSet ) if ( ArrivalA + pC->iDelays[k] <= Required && Required != SCL_INFINITY ) { Delay = Abc_MaxInt( Delay, ArrivalA + pC->iDelays[k] ); - AreaF += pBestF[iFanin]->M[fComplF][1].F; + if ( AreaF >= (float)1e32 || pBestF[iFanin]->M[fComplF][1].F >= (float)1e32 ) + AreaF = (float)1e32; + else + AreaF += pBestF[iFanin]->M[fComplF][1].F; } else { @@ -1617,8 +1620,7 @@ int Nf_ManSetMapRefs( Nf_Man_t * p ) p->pPars->Area++; p->nInvs++; } - reqTime = Abc_MinInt( Nf_ObjRequired(p, i, 0), Nf_ObjRequired(p, i, 1) ); - Tim_ManSetCiRequired( p->pManTim, Gia_ObjCioId(pObj), reqTime ); + Tim_ManSetCiRequired( p->pManTim, Gia_ObjCioId(pObj), Nf_ObjRequired(p, i, 0) ); continue; } if ( Gia_ObjIsCo(pObj) ) @@ -1930,7 +1932,9 @@ void Nf_ManResetMatches( Nf_Man_t * p, int Round ) Nf_Mat_t * pDc, * pAc, * pMfan, * pM[2]; int i, c, Arrival; // go through matches in the topo order - Gia_ManForEachAnd( p->pGia, pObj, i ) + if ( p->pManTim ) + Tim_ManIncrementTravId( p->pManTim ); + Gia_ManForEachObjWithBoxes( p->pGia, pObj, i ) { if ( Gia_ObjIsBuf(pObj) ) { @@ -1947,6 +1951,18 @@ void Nf_ManResetMatches( Nf_Man_t * p, int Round ) } continue; } + if ( Gia_ObjIsCi(pObj) ) + { + Arrival = Tim_ManGetCiArrival( p->pManTim, Gia_ObjCioId(pObj) ); + Nf_ObjPrepareCi( p, i, Arrival ); + continue; + } + if ( Gia_ObjIsCo(pObj) ) + { + Arrival = Nf_ObjMatchD( p, Gia_ObjFaninId0(pObj, i), Gia_ObjFaninC0(pObj) )->D; + Tim_ManSetCoArrival( p->pManTim, Gia_ObjCioId(pObj), Arrival ); + continue; + } // select the best match for each phase for ( c = 0; c < 2; c++ ) { @@ -2019,29 +2035,38 @@ void Nf_ManComputeMappingEla( Nf_Man_t * p ) Mio_Cell2_t * pCell; Nf_Mat_t Mb, * pMb = &Mb, * pM; word AreaBef, AreaAft, Gain = 0; - int i, c, iVar, Id, fCompl, k, * pCut, reqTime; - int Required; - Nf_ManSetOutputRequireds( p, 1 ); + int i, c, iVar, Id, fCompl, k, * pCut, Required; Nf_ManResetMatches( p, p->Iter - p->pPars->nRounds ); + Nf_ManSetOutputRequireds( p, 1 ); Gia_ManForEachObjReverseWithBoxes( p->pGia, pObj, i ) { if ( Gia_ObjIsBuf(pObj) ) { if ( Nf_ObjMapRefNum(p, i, 1) ) Nf_ObjUpdateRequired( p, i, 0, Nf_ObjRequired(p, i, 1) - p->InvDelayI ); - Nf_ObjUpdateRequired( p, Gia_ObjFaninId0(pObj, i), Gia_ObjFaninC0(pObj), Nf_ObjRequired(p, i, 0) ); + int reqTime = Nf_ObjRequired(p, i, 0); + int iObj = Gia_ObjFaninId0p(p->pGia, pObj); + int fCompl = Gia_ObjFaninC0(pObj); + Nf_ObjUpdateRequired( p, iObj, fCompl, reqTime ); + if ( iObj > 0 && Nf_ObjMatchBest(p, iObj, fCompl)->fCompl ) + Nf_ObjUpdateRequired( p, iObj, !fCompl, reqTime - p->InvDelayI ); continue; } if ( Gia_ObjIsCi(pObj) ) { - reqTime = Abc_MinInt( Nf_ObjRequired(p, i, 0), Nf_ObjRequired(p, i, 1) ); - Tim_ManSetCiRequired( p->pManTim, Gia_ObjCioId(pObj), reqTime ); + if ( Nf_ObjMapRefNum(p, i, 1) ) + Nf_ObjUpdateRequired( p, i, 0, Nf_ObjRequired(p, i, 1) - p->InvDelayI ); + Tim_ManSetCiRequired( p->pManTim, Gia_ObjCioId(pObj), Nf_ObjRequired(p, i, 0) ); continue; } if ( Gia_ObjIsCo(pObj) ) { - reqTime = Tim_ManGetCoRequired( p->pManTim, Gia_ObjCioId(pObj) ); - Nf_ObjUpdateRequired( p, Gia_ObjFaninId0(pObj, i), Gia_ObjFaninC0(pObj), reqTime ); + int reqTime = Tim_ManGetCoRequired( p->pManTim, Gia_ObjCioId(pObj) ); + int iObj = Gia_ObjFaninId0p(p->pGia, pObj); + int fCompl = Gia_ObjFaninC0(pObj); + Nf_ObjUpdateRequired( p, iObj, fCompl, reqTime ); + if ( iObj > 0 && Nf_ObjMatchBest(p, iObj, fCompl)->fCompl ) + Nf_ObjUpdateRequired( p, iObj, !fCompl, reqTime - p->InvDelayI ); continue; } for ( c = 0; c < 2; c++ ) diff --git a/src/aig/gia/giaPat2.c b/src/aig/gia/giaPat2.c index 93c4b1da9..b0839f5d4 100644 --- a/src/aig/gia/giaPat2.c +++ b/src/aig/gia/giaPat2.c @@ -965,6 +965,12 @@ Vec_Wec_t * Min_ManComputeCexes( Gia_Man_t * p, Vec_Int_t * vOuts0, int nMaxTrie if ( Vec_IntEntry(vStats[2], i) >= nMinCexes || Vec_IntEntry(vStats[1], i) > 10*Vec_IntEntry(vStats[2], i) ) continue; { + assert( Gia_ObjIsCo(pObj) ); + if ( Gia_ObjFaninId0p(p, pObj) == 0 ) { + if ( fVerbose ) + printf( "Output %d is driven by constant %d.\n", Gia_ObjCioId(pObj), Gia_ObjFaninC0(pObj) ); + continue; + } abctime clk = Abc_Clock(); int iObj = Min_ManCo(pNew, i); int Index = Gia_ObjCioId(pObj); diff --git a/src/aig/gia/giaResub.c b/src/aig/gia/giaResub.c index fc6fd7bf0..a4141a050 100644 --- a/src/aig/gia/giaResub.c +++ b/src/aig/gia/giaResub.c @@ -68,7 +68,7 @@ int Gia_ObjCheckMffc_rec( Gia_Man_t * p,Gia_Obj_t * pObj, int Limit, Vec_Int_t * return 0; return 1; } -static inline int Gia_ObjCheckMffc( Gia_Man_t * p, Gia_Obj_t * pRoot, int Limit, Vec_Int_t * vNodes, Vec_Int_t * vLeaves, Vec_Int_t * vInners ) +int Gia_ObjCheckMffc( Gia_Man_t * p, Gia_Obj_t * pRoot, int Limit, Vec_Int_t * vNodes, Vec_Int_t * vLeaves, Vec_Int_t * vInners ) { int RetValue, iObj, i; Vec_IntClear( vNodes ); diff --git a/src/aig/gia/giaRrr.cpp b/src/aig/gia/giaRrr.cpp new file mode 100644 index 000000000..df3b91e60 --- /dev/null +++ b/src/aig/gia/giaRrr.cpp @@ -0,0 +1,37 @@ +#include "aig/gia/gia.h" + +#include "opt/rrr/rrr.h" +#include "opt/rrr/rrrAbc.h" + +ABC_NAMESPACE_IMPL_START + +Gia_Man_t *Gia_ManRrr(Gia_Man_t *pGia, int iSeed, int nWords, int nTimeout, int nSchedulerVerbose, int nPartitionerVerbose, int nOptimizerVerbose, int nAnalyzerVerbose, int nSimulatorVerbose, int nSatSolverVerbose, int fUseBddCspf, int fUseBddMspf, int nConflictLimit, int nSortType, int nOptimizerFlow, int nSchedulerFlow, int nDistance, int nRestarts, int nThreads, int nWindowSize, int fDeterministic) { + rrr::AndNetwork ntk; + ntk.Read(pGia, rrr::GiaReader); + rrr::Parameter Par; + Par.iSeed = iSeed; + Par.nWords = nWords; + Par.nTimeout = nTimeout; + Par.nSchedulerVerbose = nSchedulerVerbose; + Par.nPartitionerVerbose = nPartitionerVerbose; + Par.nOptimizerVerbose = nOptimizerVerbose; + Par.nAnalyzerVerbose = nAnalyzerVerbose; + Par.nSimulatorVerbose = nSimulatorVerbose; + Par.nSatSolverVerbose = nSatSolverVerbose; + Par.fUseBddCspf = fUseBddCspf; + Par.fUseBddMspf = fUseBddMspf; + Par.nConflictLimit = nConflictLimit; + Par.nSortType = nSortType; + Par.nOptimizerFlow = nOptimizerFlow; + Par.nSchedulerFlow = nSchedulerFlow; + Par.nDistance = nDistance; + Par.nRestarts = nRestarts; + Par.nThreads = nThreads; + Par.nWindowSize = nWindowSize; + Par.fDeterministic = fDeterministic; + rrr::Perform(&ntk, &Par); + Gia_Man_t *pNew = rrr::CreateGia(&ntk); + return pNew; +} + +ABC_NAMESPACE_IMPL_END diff --git a/src/aig/gia/giaSatLut.c b/src/aig/gia/giaSatLut.c index 20074b46d..ba25ec90e 100644 --- a/src/aig/gia/giaSatLut.c +++ b/src/aig/gia/giaSatLut.c @@ -25,6 +25,12 @@ #include "map/scl/sclCon.h" #include "misc/vec/vecHsh.h" +#ifdef _MSC_VER +#define unlink _unlink +#else +#include +#endif + ABC_NAMESPACE_IMPL_START @@ -1216,6 +1222,351 @@ void Gia_ManLutSat( Gia_Man_t * pGia, int LutSize, int nNumber, int nImproves, i Vec_IntFreeP( &pGia->vPacking ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_RunKadical( char * pFileNameIn, char * pFileNameOut, int nBTLimit, int TimeOut, int fVerbose ) +{ + extern Vec_Int_t * Exa4_ManParse( char *pFileName ); + int fVerboseSolver = 0; + abctime clkTotal = Abc_Clock(); + Vec_Int_t * vRes = NULL; +#ifdef _WIN32 + char * pKadical = "kadical.exe"; +#else + char * pKadical = "kadical"; +#endif + char Command[1000], * pCommand = (char *)&Command; + if ( nBTLimit ) { + if ( TimeOut ) + sprintf( pCommand, "%s -c %d -t %d %s %s > %s", pKadical, nBTLimit, TimeOut, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut ); + else + sprintf( pCommand, "%s -c %d %s %s > %s", pKadical, nBTLimit, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut ); + } + else { + if ( TimeOut ) + sprintf( pCommand, "%s -t %d %s %s > %s", pKadical, TimeOut, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut ); + else + sprintf( pCommand, "%s %s %s > %s", pKadical, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut ); + } +#ifdef __wasm + if ( 1 ) +#else + if ( system( pCommand ) == -1 ) +#endif + { + fprintf( stdout, "Command \"%s\" did not succeed.\n", pCommand ); + return 0; + } + vRes = Exa4_ManParse( pFileNameOut ); + if ( fVerbose ) + { + if ( vRes ) + printf( "The problem has a solution. " ); + else if ( vRes == NULL && TimeOut == 0 ) + printf( "The problem has no solution. " ); + else if ( vRes == NULL ) + printf( "The problem has no solution or reached a resource limit after %d sec. ", TimeOut ); + Abc_PrintTime( 1, "SAT solver time", Abc_Clock() - clkTotal ); + } + return vRes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_SatVarReqPos( int i ) { return i*7+0; } // p +int Gia_SatVarReqNeg( int i ) { return i*7+1; } // n +int Gia_SatVarAckPos( int i ) { return i*7+2; } // P +int Gia_SatVarAckNeg( int i ) { return i*7+3; } // N +int Gia_SatVarInv ( int i ) { return i*7+4; } // i +int Gia_SatVarFan0 ( int i ) { return i*7+5; } // 0 +int Gia_SatVarFan1 ( int i ) { return i*7+6; } // 1 + +int Gia_SatValReqPos( Vec_Int_t * p, int i ) { return Vec_IntEntry(p, i*7+0); } // p +int Gia_SatValReqNeg( Vec_Int_t * p, int i ) { return Vec_IntEntry(p, i*7+1); } // n +int Gia_SatValAckPos( Vec_Int_t * p, int i ) { return Vec_IntEntry(p, i*7+2); } // P +int Gia_SatValAckNeg( Vec_Int_t * p, int i ) { return Vec_IntEntry(p, i*7+3); } // N +int Gia_SatValInv ( Vec_Int_t * p, int i ) { return Vec_IntEntry(p, i*7+4); } // i +int Gia_SatValFan0 ( Vec_Int_t * p, int i ) { return Vec_IntEntry(p, i*7+5); } // 0 +int Gia_SatValFan1 ( Vec_Int_t * p, int i ) { return Vec_IntEntry(p, i*7+6); } // 1 + +void Gia_SatDumpClause( Vec_Str_t * vStr, int * pLits, int nLits ) +{ + for ( int i = 0; i < nLits; i++ ) + Vec_StrPrintF( vStr, "%d ", Abc_LitIsCompl(pLits[i]) ? -Abc_Lit2Var(pLits[i])-1 : Abc_Lit2Var(pLits[i])+1 ); + Vec_StrPrintF( vStr, "0\n" ); +} +void Gia_SatDumpLiteral( Vec_Str_t * vStr, int Lit ) +{ + Gia_SatDumpClause( vStr, &Lit, 1 ); +} +void Gia_SatDumpKlause( Vec_Str_t * vStr, int nIns, int nAnds, int nBound ) +{ + int i, nVars = nIns + 7*nAnds; + Vec_StrPrintF( vStr, "k %d ", nVars - nBound ); + // counting primary inputs: n + for ( i = 0; i < nIns; i++ ) + Vec_StrPrintF( vStr, "-%d ", Gia_SatVarReqNeg(1+i)+1 ); + // counting internal nodes: p, n, P, N, i, 0, 1 + for ( i = 0; i < 7*nAnds; i++ ) + Vec_StrPrintF( vStr, "-%d ", (1+nIns)*7+i+1 ); + Vec_StrPrintF( vStr, "0\n" ); +} + +Vec_Str_t * Gia_ManSimpleCnf( Gia_Man_t * p, int nBound ) +{ + Vec_Str_t * vStr = Vec_StrAlloc( 10000 ); + Gia_SatDumpKlause( vStr, Gia_ManCiNum(p), Gia_ManAndNum(p), nBound ); + int i, n, m, Id, pLits[4]; Gia_Obj_t * pObj; + for ( n = 0; n < 7; n++ ) + Gia_SatDumpLiteral( vStr, Abc_Var2Lit(n, 1) ); + // acknowledge positive PI literals + Gia_ManForEachCiId( p, Id, i ) + for ( n = 0; n < 7; n++ ) if ( n != 1 ) + Gia_SatDumpLiteral( vStr, Abc_Var2Lit(Gia_SatVarReqPos(Id)+n, n>0) ); + // require driving PO literals + Gia_ManForEachCo( p, pObj, i ) + Gia_SatDumpLiteral( vStr, Abc_Var2Lit( Gia_SatVarReqPos(Gia_ObjFaninId0p(p, pObj)) + Gia_ObjFaninC0(pObj), 0 ) ); + // internal nodes + Gia_ManForEachAnd( p, pObj, i ) { + int fCompl[2] = { Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj) }; + int iFans[2] = { Gia_ObjFaninId0(pObj, i), Gia_ObjFaninId1(pObj, i) }; + Gia_Obj_t * pFans[2] = { Gia_ObjFanin0(pObj), Gia_ObjFanin1(pObj) }; + // require inverter: p & !n & N -> i, n & !p & P -> i + for ( n = 0; n < 2; n++ ) { + pLits[0] = Abc_Var2Lit( Gia_SatVarReqPos(i)+n, 1 ); + pLits[1] = Abc_Var2Lit( Gia_SatVarReqNeg(i)-n, 0 ); + pLits[2] = Abc_Var2Lit( Gia_SatVarAckNeg(i)-n, 1 ); + pLits[3] = Abc_Var2Lit( Gia_SatVarInv (i), 0 ); + Gia_SatDumpClause( vStr, pLits, 4 ); + } + // exclusive acknowledge: !P + !N + pLits[0] = Abc_Var2Lit( Gia_SatVarAckPos(i), 1 ); + pLits[1] = Abc_Var2Lit( Gia_SatVarAckNeg(i), 1 ); + Gia_SatDumpClause( vStr, pLits, 2 ); + // required acknowledge: p -> P + N, n -> P + N + pLits[1] = Abc_Var2Lit( Gia_SatVarAckPos(i), 0 ); + pLits[2] = Abc_Var2Lit( Gia_SatVarAckNeg(i), 0 ); + pLits[0] = Abc_Var2Lit( Gia_SatVarReqPos(i), 1 ); + Gia_SatDumpClause( vStr, pLits, 3 ); + pLits[0] = Abc_Var2Lit( Gia_SatVarReqNeg(i), 1 ); + Gia_SatDumpClause( vStr, pLits, 3 ); + // forbid acknowledge: !p & !n -> !P, !p & !n -> !N + pLits[0] = Abc_Var2Lit( Gia_SatVarReqPos(i), 0 ); + pLits[1] = Abc_Var2Lit( Gia_SatVarReqNeg(i), 0 ); + pLits[2] = Abc_Var2Lit( Gia_SatVarAckPos(i), 1 ); + Gia_SatDumpClause( vStr, pLits, 3 ); + pLits[2] = Abc_Var2Lit( Gia_SatVarAckNeg(i), 1 ); + Gia_SatDumpClause( vStr, pLits, 3 ); + // when fanins can be used: !N & !P -> !0, !N & !P -> !1 + pLits[0] = Abc_Var2Lit( Gia_SatVarAckPos(i), 0 ); + pLits[1] = Abc_Var2Lit( Gia_SatVarAckNeg(i), 0 ); + pLits[2] = Abc_Var2Lit( Gia_SatVarFan0(i), 1 ); + Gia_SatDumpClause( vStr, pLits, 3 ); + pLits[2] = Abc_Var2Lit( Gia_SatVarFan1(i), 1 ); + Gia_SatDumpClause( vStr, pLits, 3 ); + // when fanins are not used: 0 -> !N, 0 -> !P, 1 -> !N, 1 -> !P + for ( m = 0; m < 2; m++ ) + for ( n = 0; n < 2; n++ ) { + pLits[0] = Abc_Var2Lit( Gia_SatVarFan0(i)+n, 1 ); + pLits[1] = Abc_Var2Lit( Gia_SatVarReqPos(iFans[n])+m, 1 ); + Gia_SatDumpClause( vStr, pLits, 2 ); + } + // can only extend both when both complemented: !(C0 & C1) -> !0 + !1 + pLits[0] = Abc_Var2Lit( Gia_SatVarFan0(i), 1 ); + pLits[1] = Abc_Var2Lit( Gia_SatVarFan1(i), 1 ); + if ( !fCompl[0] || !fCompl[1] ) + Gia_SatDumpClause( vStr, pLits, 2 ); + // if fanin is a primary input, cannot extend it (pi -> !0 or pi -> !1) + for ( n = 0; n < 2; n++ ) + if ( Gia_ObjIsCi(pFans[n]) ) + Gia_SatDumpLiteral( vStr, Abc_Var2Lit( Gia_SatVarFan0(i)+n, 1 ) ); + // propagating assignments when fanin is not used + // P & !0 -> C0 ? P0 : N0 + // N & !0 -> C0 ? N0 : P0 + // P & !1 -> C1 ? P1 : N1 + // N & !1 -> C1 ? N1 : P1 + for ( m = 0; m < 2; m++ ) + for ( n = 0; n < 2; n++ ) { + pLits[0] = Abc_Var2Lit( Gia_SatVarAckPos(i)+m, 1 ); + pLits[1] = Abc_Var2Lit( Gia_SatVarFan0(i)+n, 0 ); + pLits[2] = Abc_Var2Lit( Gia_SatVarReqPos(iFans[n]) + !(m ^ fCompl[n]), 0 ); + Gia_SatDumpClause( vStr, pLits, 3 ); + } + // propagating assignments when fanins are used + // P & 0 -> (C0 ^ C00) ? P00 : N00 + // P & 0 -> (C0 ^ C01) ? P01 : N01 + // N & 0 -> (C0 ^ C00) ? N00 : P00 + // N & 0 -> (C0 ^ C01) ? N01 : P01 + // P & 1 -> (C1 ^ C10) ? P10 : N10 + // P & 1 -> (C1 ^ C11) ? P11 : N11 + // N & 1 -> (C1 ^ C10) ? N10 : P10 + // N & 1 -> (C1 ^ C11) ? N11 : P11 + for ( m = 0; m < 2; m++ ) + for ( n = 0; n < 2; n++ ) + if ( Gia_ObjIsAnd(pFans[n]) ) { + pLits[0] = Abc_Var2Lit( Gia_SatVarAckPos(i)+m, 1 ); + pLits[1] = Abc_Var2Lit( Gia_SatVarFan0(i)+n, 1 ); + pLits[2] = Abc_Var2Lit( Gia_SatVarReqPos(Gia_ObjFaninId0p(p, pFans[n])) + !(m ^ fCompl[n] ^ Gia_ObjFaninC0(pFans[n])), 0 ); + Gia_SatDumpClause( vStr, pLits, 3 ); + pLits[2] = Abc_Var2Lit( Gia_SatVarReqPos(Gia_ObjFaninId1p(p, pFans[n])) + !(m ^ fCompl[n] ^ Gia_ObjFaninC1(pFans[n])), 0 ); + Gia_SatDumpClause( vStr, pLits, 3 ); + } + } + Vec_StrPush( vStr, '\0' ); + return vStr; +} + +typedef enum { + GIA_GATE_ZERO, // 0: + GIA_GATE_ONE, // 1: + GIA_GATE_BUF, // 2: + GIA_GATE_INV, // 3: + GIA_GATE_NAN2, // 4: + GIA_GATE_NOR2, // 5: + GIA_GATE_AOI21, // 6: + GIA_GATE_NAN3, // 7: + GIA_GATE_NOR3, // 8: + GIA_GATE_OAI21, // 9: + GIA_GATE_AOI22, // 10: + GIA_GATE_OAI22, // 11: + RTM_VAL_VOID // 12: unused value +} Gia_ManGate_t; + +Vec_Int_t * Gia_ManDeriveSimpleMapping( Gia_Man_t * p, Vec_Int_t * vRes ) +{ + Vec_Int_t * vMapping = Vec_IntStart( 2*Gia_ManObjNum(p) ); + int i, Id; Gia_Obj_t * pObj; + Gia_ManForEachCiId( p, Id, i ) + if ( Gia_SatValReqNeg(vRes, Id) ) + Vec_IntWriteEntry( vMapping, Abc_Var2Lit(Id, 1), -1 ); + Gia_ManForEachAnd( p, pObj, i ) + { + if ( Gia_SatValAckPos(vRes, i) + Gia_SatValAckNeg(vRes, i) == 0 ) + continue; + assert( Gia_SatValAckPos(vRes, i) != Gia_SatValAckNeg(vRes, i) ); + if ( (Gia_SatValReqPos(vRes, i) && Gia_SatValReqNeg(vRes, i)) || Gia_SatValInv(vRes, i) ) + Vec_IntWriteEntry( vMapping, Abc_Var2Lit(i, Gia_SatValAckPos(vRes, i)), -1 ); + int fComp = Gia_SatValAckNeg(vRes, i); + int fFan0 = Gia_SatValFan0(vRes, i); + int fFan1 = Gia_SatValFan1(vRes, i); + Gia_Obj_t * pFans[2] = { Gia_ObjFanin0(pObj), Gia_ObjFanin1(pObj) }; + Vec_IntWriteEntry( vMapping, Abc_Var2Lit(i, fComp), Vec_IntSize(vMapping) ); + if ( fFan0 && fFan1 ) { + assert( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) ); + Vec_IntPush( vMapping, 4 ); + Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pFans[0]), !(fComp ^ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC0(pFans[0]))) ); + Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pFans[0]), !(fComp ^ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pFans[0]))) ); + Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pFans[1]), !(fComp ^ Gia_ObjFaninC1(pObj) ^ Gia_ObjFaninC0(pFans[1]))) ); + Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pFans[1]), !(fComp ^ Gia_ObjFaninC1(pObj) ^ Gia_ObjFaninC1(pFans[1]))) ); + Vec_IntPush( vMapping, fComp ? GIA_GATE_OAI22 : GIA_GATE_AOI22 ); + } else if ( fFan0 ) { + Vec_IntPush( vMapping, 3 ); + Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pFans[0]), !(fComp ^ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC0(pFans[0]))) ); + Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pFans[0]), !(fComp ^ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pFans[0]))) ); + Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pObj), !(fComp ^ Gia_ObjFaninC1(pObj))) ); + if ( Gia_ObjFaninC0(pObj) ) + Vec_IntPush( vMapping, fComp ? GIA_GATE_OAI21 : GIA_GATE_AOI21 ); + else + Vec_IntPush( vMapping, fComp ? GIA_GATE_NAN3 : GIA_GATE_NOR3 ); + } else if ( fFan1 ) { + Vec_IntPush( vMapping, 3 ); + Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pFans[1]), !(fComp ^ Gia_ObjFaninC1(pObj) ^ Gia_ObjFaninC0(pFans[1]))) ); + Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pFans[1]), !(fComp ^ Gia_ObjFaninC1(pObj) ^ Gia_ObjFaninC1(pFans[1]))) ); + Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pObj), !(fComp ^ Gia_ObjFaninC0(pObj))) ); + if ( Gia_ObjFaninC1(pObj) ) + Vec_IntPush( vMapping, fComp ? GIA_GATE_OAI21 : GIA_GATE_AOI21 ); + else + Vec_IntPush( vMapping, fComp ? GIA_GATE_NAN3 : GIA_GATE_NOR3 ); + } else { + Vec_IntPush( vMapping, 2 ); + Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pObj), !(fComp ^ Gia_ObjFaninC0(pObj))) ); + Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pObj), !(fComp ^ Gia_ObjFaninC1(pObj))) ); + Vec_IntPush( vMapping, fComp ? GIA_GATE_NAN2 : GIA_GATE_NOR2 ); + } + } + return vMapping; +} +void Gia_ManSimplePrintMapping( Vec_Int_t * vRes, int nIns ) +{ + int i, k, nObjs = Vec_IntSize(vRes)/7, nSteps = Abc_Base10Log(nObjs); + int nCard = Vec_IntSum(vRes) - nIns; char NumStr[10]; + printf( "Solution with cardinality %d:\n", nCard ); + for ( k = 0; k < nSteps; k++ ) { + printf( " " ); + for ( i = 0; i < nObjs; i++ ) { + sprintf( NumStr, "%02d", i ); + printf( "%c", NumStr[k] ); + } + printf( "\n" ); + } + for ( k = 0; k < 7; k++ ) { + printf( "%c ", "pnPNi01"[k] ); + for ( i = 0; i < nObjs; i++ ) + if ( Vec_IntEntry( vRes, i*7+k ) == 0 ) + printf( " " ); + else + printf( "1" ); + printf( "\n" ); + } +} +int Gia_ManDumpCnf( char * pFileName, Vec_Str_t * vStr, int nVars ) +{ + FILE * pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) { printf( "Cannot open input file \"%s\".\n", pFileName ); return 0; } + fprintf( pFile, "p knf %d %d\n%s\n", nVars, Vec_StrCountEntry(vStr, '\n'), Vec_StrArray(vStr) ); + fclose( pFile ); + return 1; +} +int Gia_ManSimpleMapping( Gia_Man_t * p, int nBound, int nBTLimit, int nTimeout, int fVerbose ) +{ + char * pFileNameI = (char *)"__temp__.cnf"; + char * pFileNameO = (char *)"__temp__.out"; + if ( nBound == 0 ) + nBound = 5 * Gia_ManAndNum(p); + Vec_Str_t * vStr = Gia_ManSimpleCnf( p, nBound/2 ); + int nVars = 7*(Gia_ManObjNum(p)-Gia_ManCoNum(p)); + if ( !Gia_ManDumpCnf(pFileNameI, vStr, nVars) ) { + Vec_StrFree( vStr ); + return 0; + } + if ( fVerbose ) + printf( "SAT variables = %d. SAT clauses = %d. Cardinality bound = %d. Conflict limit = %d. Timeout = %d.\n", + nVars, Vec_StrCountEntry(vStr, '\n'), nBound, nBTLimit, nTimeout ); + //char pFileName[100]; sprintf( pFileName, "temp%02d.cnf", nBound/2 ); + //Gia_ManDumpCnf( pFileName, vStr, nVars ); + Vec_StrFree( vStr ); + Vec_Int_t * vRes = Gia_RunKadical( pFileNameI, pFileNameO, nBTLimit, nTimeout, 1 ); + unlink( pFileNameI ); + //unlink( pFileNameO ); + if ( vRes == NULL ) + return 0; + Vec_IntFreeP( &p->vCellMapping ); + assert( p->vCellMapping == NULL ); + Vec_IntDrop( vRes, 0 ); + if ( fVerbose ) Gia_ManSimplePrintMapping( vRes, Gia_ManCiNum(p) ); + p->vCellMapping = Gia_ManDeriveSimpleMapping( p, vRes ); + Vec_IntFree( vRes ); + return 1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaSif.c b/src/aig/gia/giaSif.c index c52ab4dd9..4df5c47f7 100644 --- a/src/aig/gia/giaSif.c +++ b/src/aig/gia/giaSif.c @@ -645,6 +645,25 @@ Gia_Man_t * Gia_ManSifPerform( Gia_Man_t * p, int nLutSize, int fEvalOnly, int f pNew = Gia_ManSifTransform( p, vCuts, vTimes, nLutSize, Upper, fVerbose ); Vec_IntFree( vCuts ); Vec_IntFree( vTimes ); + //Gia_ManTransferTiming( pNew, p ); + if ( p->vNamesIn ) { + char * pName; int i; + pNew->vNamesIn = p->vNamesIn; p->vNamesIn = NULL; + Vec_PtrForEachEntryStart( char *, pNew->vNamesIn, pName, i, Gia_ManPiNum(pNew) ) + ABC_FREE( pName ); + Vec_PtrShrink( pNew->vNamesIn, Gia_ManPiNum(pNew) ); + for ( i = 0; i < Gia_ManRegNum(pNew); i++ ) + Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsavNum("_fo", i) ); + } + if ( p->vNamesOut ) { + char * pName; int i; + pNew->vNamesOut = p->vNamesOut; p->vNamesOut = NULL; + Vec_PtrForEachEntryStart( char *, pNew->vNamesOut, pName, i, Gia_ManPoNum(pNew) ) + ABC_FREE( pName ); + Vec_PtrShrink( pNew->vNamesOut, Gia_ManPoNum(pNew) ); + for ( i = 0; i < Gia_ManRegNum(pNew); i++ ) + Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsavNum("_fi", i) ); + } return pNew; } diff --git a/src/aig/gia/giaSwitch.c b/src/aig/gia/giaSwitch.c index bf94ad72d..26e29591c 100644 --- a/src/aig/gia/giaSwitch.c +++ b/src/aig/gia/giaSwitch.c @@ -612,7 +612,7 @@ Vec_Int_t * Gia_ManSwiSimulate( Gia_Man_t * pAig, Gia_ParSwi_t * pPars ) else if ( pPars->fProbTrans ) { Gia_ManForEachObj( pAig, pObj, i ) - pSwitching[i] = Gia_ManSwiComputeProbOne( p->pData1[i], pPars->nWords*(pPars->nIters-pPars->nPref) ); + pSwitching[i] = Gia_ManSwiComputeSwitching( p->pData1[i], pPars->nWords*(pPars->nIters-pPars->nPref) ); } else { diff --git a/src/aig/gia/giaTruth.c b/src/aig/gia/giaTruth.c index c24748ede..0845eae96 100644 --- a/src/aig/gia/giaTruth.c +++ b/src/aig/gia/giaTruth.c @@ -559,6 +559,11 @@ void Gia_ObjComputeTruthTableStart( Gia_Man_t * p, int nVarsMax ) p->vTtMemory = Vec_WrdStart( p->nTtWords * 64 ); p->vTtNums = Vec_IntAlloc( Gia_ManObjNum(p) + 1000 ); Vec_IntFill( p->vTtNums, Vec_IntCap(p->vTtNums), -ABC_INFINITY ); + if ( nVarsMax >= 6 ) { + word * pTruth; int i; + Vec_PtrForEachEntry( word *, p->vTtInputs, pTruth, i ) + Abc_TtFlipVar5( pTruth, nVarsMax ); + } } void Gia_ObjComputeTruthTableStop( Gia_Man_t * p ) { diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index 41c56c1fa..de7149935 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -3453,6 +3453,117 @@ Gia_Man_t * Gia_ManDupInsertWindows( Gia_Man_t * p, Vec_Ptr_t * vvIns, Vec_Ptr_t return pNew; } +/**Function************************************************************* + + Synopsis [Computing equivalent nodes across the two AIGs.] + + Description [Assumes that both AIGs are structurally hashed without dandling nodes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManCreateDualOutputMiter( Gia_Man_t * p0, Gia_Man_t * p1 ) +{ + Gia_Man_t * pNew; Gia_Obj_t * pObj; int i; + assert( Gia_ManCiNum(p0) == Gia_ManCiNum(p1) ); + assert( Gia_ManCoNum(p0) == Gia_ManCoNum(p1) ); + // start the manager + pNew = Gia_ManStart( Gia_ManObjNum(p0) + Gia_ManObjNum(p1) ); + pNew->pName = Abc_UtilStrsav( "miter" ); + Gia_ManFillValue( p0 ); + Gia_ManFillValue( p1 ); + // map combinational inputs + Gia_ManConst0(p0)->Value = 0; + Gia_ManConst0(p1)->Value = 0; + Gia_ManForEachCi( p0, pObj, i ) + Gia_ManCi(p1, i)->Value = pObj->Value = Gia_ManAppendCi( pNew ); + // map internal nodes and outputs + Gia_ManHashAlloc( pNew ); + Gia_ManForEachAnd( p0, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + assert( Gia_ManAndNum(pNew) == Gia_ManAndNum(p0) ); // the input AIG p0 is structurally hashed + Gia_ManForEachAnd( p1, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + // add the outputs + Gia_ManForEachCo( p0, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManForEachCo( p1, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + printf( "The two AIGs have %d structurally equivalent nodes.\n", Gia_ManAndNum(p0) + Gia_ManAndNum(p1) - Gia_ManAndNum(pNew) ); + // there should be no dangling nodes (otherwise, the second AIG may not be structurally hashed) + int nDangling = Gia_ManMarkDangling(pNew); + assert( nDangling == 0 ); + Gia_ManCleanMark01(pNew); + return pNew; +} +Vec_Int_t * Gia_ManFindMutualEquivs( Gia_Man_t * p0, Gia_Man_t * p1, int nConflictLimit, int fVerbose ) +{ + Vec_Int_t * vPairs = Vec_IntAlloc( 100 ); + // derive the miter + Gia_Man_t * pMiter = Gia_ManCreateDualOutputMiter( p0, p1 ); + //Gia_ManPrintStats( pMiter, NULL ); + //Gia_AigerWrite( pMiter, "out.aig", 0, 0, 0 ); + // perform SAT sweeping + extern Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose ); + Gia_Man_t * pNew = Cec4_ManSimulateTest3( pMiter, nConflictLimit, fVerbose ); + Gia_ManStop( pNew ); + // now, pMiter is annotated with the equiv class info + + // here we collect AIG node pairs with the following properties: + // - the first node belongs to p0; the second node belongs to p1 + // - both nodes are internal nodes of p0 and p1 (not primary inputs/outputs) + // - these nodes are combinationally equivalent (possibly up to the complement) + // - these nodes are "singleton" equivalences (no other nodes in p0 and p1 are equivalent to them) + // - these nodes are not structurally equivalent (that is, they have structurally different TFI logic cones) + + // count the number of nodes in each equivalence class + Vec_Int_t * vCounts = Vec_IntStart( Gia_ManObjNum(pMiter) ); + Gia_Obj_t * pObj; int i, k; + Gia_ManForEachClass( pMiter, i ) + Gia_ClassForEachObj( pMiter, i, k ) + Vec_IntAddToEntry( vCounts, i, 1 ); + + // map each miter node coming from p1 into the corresponding node in p1 + Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(pMiter) ); + int iStartP1 = 1 + Gia_ManPiNum(p0) + Gia_ManAndNum(p0); + Gia_ManForEachAnd( p1, pObj, i ) + if ( Abc_Lit2Var(pObj->Value) >= iStartP1 ) // node from p1 (not from p0) + Vec_IntWriteEntry( vMap, Abc_Lit2Var(pObj->Value), i ); + + // go through functionally (not structurally!) equivalent nodes in the second AIG + // and collect those node pairs from p0 and p1 whose equivalence class contains exactly two nodes + for ( i = iStartP1; i < Gia_ManObjNum(pMiter) - Gia_ManCoNum(pMiter); i++ ) { + assert( Gia_ObjIsAnd(Gia_ManObj(pMiter, i)) ); + int Repr = Gia_ObjRepr(pMiter, i); + if ( Repr == GIA_VOID || Repr >= iStartP1 || Vec_IntEntry(vCounts, Repr) != 2 ) + continue; + assert( Repr < iStartP1 ); // node in p0 + assert( Vec_IntEntry(vMap, i) > 0 ); // node in p1 + Vec_IntPushTwo( vPairs, Repr, Vec_IntEntry(vMap, i) ); + } + // cleanup + Vec_IntFree( vMap ); + Vec_IntFree( vCounts ); + Gia_ManStop( pMiter ); + return vPairs; +} +void Gia_ManFindMutualEquivsTest() +{ + Gia_Man_t * p0 = Gia_AigerRead( "p0.aig", 0, 0, 0 ); + Gia_Man_t * p1 = Gia_AigerRead( "p1.aig", 0, 0, 0 ); + Vec_Int_t * vPairs = Gia_ManFindMutualEquivs( p0, p1, 0, 0 ); + printf( "Pair Aig0 node Aig1 node\n" ); + int i, Obj0, Obj1; + Vec_IntForEachEntryDouble( vPairs, Obj0, Obj1, i ) + printf( "%3d %6d %6d\n", i/2, Obj0, Obj1 ); + Gia_ManStop( p0 ); + Gia_ManStop( p1 ); + Vec_IntFree( vPairs ); +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index 27240f443..2e64d1d1b 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -73,6 +73,7 @@ SRC += src/aig/gia/giaAig.c \ src/aig/gia/giaResub6.c \ src/aig/gia/giaRetime.c \ src/aig/gia/giaRex.c \ + src/aig/gia/giaRrr.cpp \ src/aig/gia/giaSatEdge.c \ src/aig/gia/giaSatLE.c \ src/aig/gia/giaSatLut.c \ @@ -111,4 +112,4 @@ SRC += src/aig/gia/giaAig.c \ src/aig/gia/giaTtopt.cpp \ src/aig/gia/giaUnate.c \ src/aig/gia/giaUtil.c \ - src/aig/gia/giaBound.c \ No newline at end of file + src/aig/gia/giaBound.c diff --git a/src/aig/miniaig/ndr.h b/src/aig/miniaig/ndr.h index 193730636..1d2211f96 100644 --- a/src/aig/miniaig/ndr.h +++ b/src/aig/miniaig/ndr.h @@ -219,7 +219,8 @@ static inline void Ndr_DataPushString( Ndr_Data_t * p, int ObjType, int Type, ch { //word Truth = (word)pFunc; //Ndr_DataPushArray( p, Type, 2, (int *)&Truth ); - Ndr_DataPushArray( p, Type, 2, (int *)&pFunc ); + int nInts = (strlen(pFunc) + 1 + sizeof(int) - 1) / sizeof(int); + Ndr_DataPushArray( p, Type, nInts, (int *)&pFunc ); } else { diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 73d218438..ada1f499f 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -640,6 +640,7 @@ extern ABC_DLL Vec_Ptr_t * Abc_AigDfsMap( Abc_Ntk_t * pNtk ); extern ABC_DLL Vec_Vec_t * Abc_DfsLevelized( Abc_Obj_t * pNode, int fTfi ); extern ABC_DLL Vec_Vec_t * Abc_NtkLevelize( Abc_Ntk_t * pNtk ); extern ABC_DLL int Abc_NtkLevel( Abc_Ntk_t * pNtk ); +extern ABC_DLL int Abc_NtkLevelR( Abc_Ntk_t * pNtk ); extern ABC_DLL int Abc_NtkLevelReverse( Abc_Ntk_t * pNtk ); extern ABC_DLL int Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk ); extern ABC_DLL int Abc_NtkIsAcyclicWithBoxes( Abc_Ntk_t * pNtk ); diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c index a1345db8c..68c005a5e 100644 --- a/src/base/abc/abcDfs.c +++ b/src/base/abc/abcDfs.c @@ -1514,6 +1514,14 @@ int Abc_NtkLevelReverse( Abc_Ntk_t * pNtk ) } return LevelsMax; } +int Abc_NtkLevelR( Abc_Ntk_t * pNtk ) +{ + int i, LevelMax = Abc_NtkLevelReverse( pNtk ); + Abc_Obj_t * pNode; + Abc_NtkForEachObj( pNtk, pNode, i ) + pNode->Level = (int)(LevelMax - pNode->Level + 1); + return LevelMax; +} /**Function************************************************************* diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index 3c8fd383e..c9eeb79c6 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -1344,10 +1344,11 @@ Abc_Ntk_t * Abc_NtkCreateWithNodes( Vec_Ptr_t * vSop ) Abc_NodeFreeNames( vNames ); // create the node, add PIs as fanins, set the function Vec_PtrForEachEntry( char *, vSop, pSop, i ) - { + { pNode = Abc_NtkCreateNode( pNtkNew ); - Abc_NtkForEachPi( pNtkNew, pFanin, k ) - Abc_ObjAddFanin( pNode, pFanin ); + if ( Abc_SopGetVarNum(pSop) > 0 ) + Abc_NtkForEachPi( pNtkNew, pFanin, k ) + Abc_ObjAddFanin( pNode, pFanin ); pNode->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, pSop ); // create the only PO pNodePo = Abc_NtkCreatePo(pNtkNew); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index ed4a88f6d..c126df352 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -60,6 +60,7 @@ #include "opt/sbd/sbd.h" #include "bool/rpo/rpo.h" #include "map/mpm/mpm.h" +#include "map/mio/mio.h" #include "opt/fret/fretime.h" #include "opt/nwk/nwkMerge.h" #include "base/acb/acbPar.h" @@ -153,7 +154,9 @@ static int Abc_CommandResubCore ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandResubCheck ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRr ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandCascade ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandLutCasDec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandLutCas ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandBsEval ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandExtract ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandVarMin ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFaultClasses ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -286,11 +289,13 @@ static int Abc_CommandRecMerge3 ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandMap ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAmap ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPhaseMap ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandStochMap ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandUnmap ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAttach ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSuperChoice ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSuperChoiceLut ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTimeScale ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandRewire ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandFpga ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandFpgaFast ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -476,6 +481,7 @@ static int Abc_CommandAbc9Scorr ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Choice ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Sat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SatEnum ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9AdvGenSim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Fraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9CFraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Srm ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -506,6 +512,7 @@ static int Abc_CommandAbc9Lf ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Mf ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Nf ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Of ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Simap ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Pack ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Edge ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SatLut ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -517,6 +524,8 @@ static int Abc_CommandAbc9LNetOpt ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Ttopt ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Transduction ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9TranStoch ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Rrr ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Rewire ( Abc_Frame_t * pAbc, int argc, char ** argv ); //#endif static int Abc_CommandAbc9LNetMap ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Unmap ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -582,6 +591,7 @@ static int Abc_CommandAbc9Exorcism ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Mfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Mfsd ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9DeepSyn ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9RandSyn ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SatSyn ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9StochSyn ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9PoPart2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -616,6 +626,7 @@ static int Abc_CommandAbc9Odc ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9GenRel ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9GenMux ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9GenComp ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9GenSorter ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9GenNeuron ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Window ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9FunAbs ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -952,7 +963,9 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Synthesis", "resub_check", Abc_CommandResubCheck, 0 ); // Cmd_CommandAdd( pAbc, "Synthesis", "rr", Abc_CommandRr, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "cascade", Abc_CommandCascade, 1 ); + Cmd_CommandAdd( pAbc, "Synthesis", "lutcasdec", Abc_CommandLutCasDec, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "lutcas", Abc_CommandLutCas, 1 ); + Cmd_CommandAdd( pAbc, "Synthesis", "bseval", Abc_CommandBsEval, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "extract", Abc_CommandExtract, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "varmin", Abc_CommandVarMin, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "faultclasses", Abc_CommandFaultClasses, 0 ); @@ -1083,11 +1096,13 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "SC mapping", "map", Abc_CommandMap, 1 ); Cmd_CommandAdd( pAbc, "SC mapping", "amap", Abc_CommandAmap, 1 ); Cmd_CommandAdd( pAbc, "SC mapping", "phase_map", Abc_CommandPhaseMap, 1 ); + Cmd_CommandAdd( pAbc, "SC mapping", "stochmap", Abc_CommandStochMap, 1 ); Cmd_CommandAdd( pAbc, "SC mapping", "unmap", Abc_CommandUnmap, 1 ); Cmd_CommandAdd( pAbc, "SC mapping", "attach", Abc_CommandAttach, 1 ); Cmd_CommandAdd( pAbc, "SC mapping", "superc", Abc_CommandSuperChoice, 1 ); Cmd_CommandAdd( pAbc, "SC mapping", "supercl", Abc_CommandSuperChoiceLut, 1 ); Cmd_CommandAdd( pAbc, "SC mapping", "timescale", Abc_CommandTimeScale, 0 ); + Cmd_CommandAdd( pAbc, "SC mapping", "rewire", Abc_CommandRewire, 1 ); // Cmd_CommandAdd( pAbc, "FPGA mapping", "fpga", Abc_CommandFpga, 1 ); // Cmd_CommandAdd( pAbc, "FPGA mapping", "ffpga", Abc_CommandFpgaFast, 1 ); @@ -1274,6 +1289,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&choice", Abc_CommandAbc9Choice, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&sat", Abc_CommandAbc9Sat, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&satenum", Abc_CommandAbc9SatEnum, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&adv_sim_gen", Abc_CommandAbc9AdvGenSim, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&fraig", Abc_CommandAbc9Fraig, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&cfraig", Abc_CommandAbc9CFraig, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&srm", Abc_CommandAbc9Srm, 0 ); @@ -1304,6 +1320,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&mf", Abc_CommandAbc9Mf, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&nf", Abc_CommandAbc9Nf, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&of", Abc_CommandAbc9Of, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&simap", Abc_CommandAbc9Simap, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&pack", Abc_CommandAbc9Pack, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&edge", Abc_CommandAbc9Edge, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&satlut", Abc_CommandAbc9SatLut, 0 ); @@ -1315,6 +1332,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&ttopt", Abc_CommandAbc9Ttopt, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&transduction", Abc_CommandAbc9Transduction, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&transtoch" , Abc_CommandAbc9TranStoch, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&rrr", Abc_CommandAbc9Rrr, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&rewire" , Abc_CommandAbc9Rewire, 0 ); //#endif Cmd_CommandAdd( pAbc, "ABC9", "&lnetmap", Abc_CommandAbc9LNetMap, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&unmap", Abc_CommandAbc9Unmap, 0 ); @@ -1380,6 +1399,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&mfs", Abc_CommandAbc9Mfs, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&mfsd", Abc_CommandAbc9Mfsd, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&deepsyn", Abc_CommandAbc9DeepSyn, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&randsyn", Abc_CommandAbc9RandSyn, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&satsyn", Abc_CommandAbc9SatSyn, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&stochsyn", Abc_CommandAbc9StochSyn, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&popart2", Abc_CommandAbc9PoPart2, 0 ); @@ -1420,6 +1440,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&genrel", Abc_CommandAbc9GenRel, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&genmux", Abc_CommandAbc9GenMux, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&gencomp", Abc_CommandAbc9GenComp, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&gensorter", Abc_CommandAbc9GenSorter, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&genneuron", Abc_CommandAbc9GenNeuron, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&window", Abc_CommandAbc9Window, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&funabs", Abc_CommandAbc9FunAbs, 0 ); @@ -1605,7 +1626,7 @@ usage: Abc_Print( -2, "\t-f : toggles printing the literal count in the factored forms [default = %s]\n", fFactor? "yes": "no" ); Abc_Print( -2, "\t-b : toggles saving the best logic network in \"best.blif\" [default = %s]\n", fSaveBest? "yes": "no" ); Abc_Print( -2, "\t-d : toggles dumping statistics about the network into file [default = %s]\n", fDumpResult? "yes": "no" ); - Abc_Print( -2, "\t-l : toggles printing delay of LUT mapping using LUT library [default = %s]\n", fSaveBest? "yes": "no" ); + Abc_Print( -2, "\t-l : toggles printing delay of LUT mapping using LUT library [default = %s]\n", fUseLutLib? "yes": "no" ); Abc_Print( -2, "\t-t : toggles printing runtime statistics [default = %s]\n", fPrintTime? "yes": "no" ); Abc_Print( -2, "\t-m : toggles printing MUX statistics [default = %s]\n", fPrintMuxes? "yes": "no" ); Abc_Print( -2, "\t-p : toggles printing power dissipation due to switching [default = %s]\n", fPower? "yes": "no" ); @@ -3852,7 +3873,7 @@ usage: Abc_Print( -2, "usage: strash [-acrih]\n" ); Abc_Print( -2, "\t transforms combinational logic into an AIG\n" ); Abc_Print( -2, "\t-a : toggles between using all nodes and DFS nodes [default = %s]\n", fAllNodes? "all": "DFS" ); - Abc_Print( -2, "\t-c : toggles cleanup to remove the dagling AIG nodes [default = %s]\n", fCleanup? "all": "DFS" ); + Abc_Print( -2, "\t-c : toggles cleanup to remove the dangling AIG nodes [default = %s]\n", fCleanup? "all": "DFS" ); Abc_Print( -2, "\t-r : toggles using the record of AIG subgraphs [default = %s]\n", fRecord? "yes": "no" ); Abc_Print( -2, "\t-i : toggles complementing the POs of the AIG [default = %s]\n", fComplOuts? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); @@ -7439,14 +7460,58 @@ usage: ***********************************************************************/ int Abc_CommandRunGen( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Acb_NtkRunGen( char * pFileNames[2], int fVerbose ); - char * pFileNames[4] = {NULL}; - int c, fVerbose = 0; + extern void Acb_NtkRunGen( int nInputs, int nMints, int nFuncs, int Seed, int fVerbose, char * pScript ); + int c, nInputs = 10, nMints = 10, nFuncs = 10, Seed = 0, fVerbose = 0; char * pScript = NULL; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "IMRSCvh" ) ) != EOF ) { switch ( c ) { + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + nInputs = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + nMints = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'R': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" ); + goto usage; + } + nFuncs = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + Seed = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by a script.\n" ); + goto usage; + } + pScript = argv[globalUtilOptind]; + globalUtilOptind++; + break; case 'v': fVerbose ^= 1; break; @@ -7456,21 +7521,24 @@ int Abc_CommandRunGen( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } - if ( argc - globalUtilOptind != 2 ) + if ( pScript == NULL ) { - Abc_Print( 1, "Expecting two file names on the command line.\n" ); - goto usage; + Abc_Print( -1, "Command line switch \"-C\" should be specified and followed by a string.\n" ); + goto usage; } - for ( c = 0; c < 2; c++ ) - pFileNames[c] = argv[globalUtilOptind+c]; - Acb_NtkRunGen( pFileNames, fVerbose ); + Acb_NtkRunGen( nInputs, nMints, nFuncs, Seed, fVerbose, pScript ); return 0; usage: - Abc_Print( -2, "usage: rungen [-vh] \n" ); - Abc_Print( -2, "\t experimental command\n" ); - Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); - Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "usage: rungen [-IMRS num] [-C script] [-vh]\n" ); + Abc_Print( -2, "\t running the script on a set of randomly generated functions\n" ); + Abc_Print( -2, "\t-I : the number of input variables [default = %d]\n", nInputs ); + Abc_Print( -2, "\t-M : the number of positive minterms in the random function [default = %d]\n", nMints ); + Abc_Print( -2, "\t-R : the number of random functions to try [default = %d]\n", nFuncs ); + Abc_Print( -2, "\t-S : the random seed [default = %d]\n", Seed ); + Abc_Print( -2, "\t-C : the script to apply [default = provided by the user]\n" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -8791,7 +8859,7 @@ int Abc_CommandCascade( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pNtk == NULL ) { - Abc_Print( -1, "Empty network.\n" ); + Abc_Print( -1, "Empty neAtwork.\n" ); return 1; } @@ -8834,6 +8902,7 @@ usage: return 1; } + /**Function************************************************************* Synopsis [] @@ -8845,13 +8914,14 @@ usage: SeeAlso [] ***********************************************************************/ -int Abc_CommandLutCas( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandLutCasDec( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Abc_Ntk_t * Abc_NtkLutCascade( Abc_Ntk_t * pNtk, int nLutSize, int fVerbose ); - Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc), * pNtkRes; - int c, nLutSize = 6, fVerbose = 0; + extern Abc_Ntk_t * Abc_NtkLutCascadeGen( int nLutSize, int nStages, int nRails, int nShared, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkLutCascade2( Abc_Ntk_t * pNtk, int nLutSize, int nLuts, int nRails, int nIters, int fVerbose, char * pGuide ); + Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc), * pNtkRes; char * pGuide = NULL; + int c, nLutSize = 6, nStages = 8, nRails = 1, nShared = 2, nIters = 1, fGen = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Kvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "KMRSIgvh" ) ) != EOF ) { switch ( c ) { @@ -8866,6 +8936,53 @@ int Abc_CommandLutCas( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nLutSize < 0 ) goto usage; break; + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + nStages = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nStages < 0 ) + goto usage; + break; + case 'R': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" ); + goto usage; + } + nRails = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nRails < 0 ) + goto usage; + break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + nShared = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nShared < 0 ) + goto usage; + break; + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + nIters = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nIters < 0 ) + goto usage; + break; + case 'g': + fGen ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -8875,6 +8992,17 @@ int Abc_CommandLutCas( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } + if ( fGen ) + { + pNtkRes = Abc_NtkLutCascadeGen( nLutSize, nStages, nRails, nShared, fVerbose ); + if ( pNtkRes == NULL ) + { + Abc_Print( -1, "LUT cascade generation failed.\n" ); + return 1; + } + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + } if ( pNtk == NULL ) { @@ -8891,7 +9019,15 @@ int Abc_CommandLutCas( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Run command \"strash\" to convert the network into an AIG.\n" ); return 1; } - pNtkRes = Abc_NtkLutCascade( pNtk, nLutSize, fVerbose ); + if ( Abc_NtkCiNum(pNtk) > nLutSize + (nLutSize - nRails) * (nStages - 1) ) + { + Abc_Print( -1, "Cannot decompose %d-input function into a %d-rail cascade of %d %d-LUTs (max suppose size = %d).\n", + Abc_NtkCiNum(pNtk), nRails, nStages, nLutSize, nLutSize + (nLutSize - nRails) * (nStages - 1) ); + return 1; + } + if ( argc == globalUtilOptind + 1 ) + pGuide = argv[globalUtilOptind]; + pNtkRes = Abc_NtkLutCascade2( pNtk, nLutSize, nStages, nRails, nIters, fVerbose, pGuide ); if ( pNtkRes == NULL ) { Abc_Print( -1, "LUT cascade mapping failed.\n" ); @@ -8901,14 +9037,304 @@ int Abc_CommandLutCas( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: lutcas [-K ] [-vh]\n" ); - Abc_Print( -2, "\t derives single-rail LUT cascade for the primary output function\n" ); + Abc_Print( -2, "usage: lutcasdec [-KMRSI ] [-vh]\n" ); + Abc_Print( -2, "\t decomposes the primary output functions into LUT cascades\n" ); Abc_Print( -2, "\t-K : the number of LUT inputs [default = %d]\n", nLutSize ); + Abc_Print( -2, "\t-M : the maximum delay (the number of stages) [default = %d]\n", nStages ); + Abc_Print( -2, "\t-R : the number of direct connections (rails) [default = %d]\n", nRails ); + Abc_Print( -2, "\t-S : the number of shared variables in each stage [default = %d]\n", nShared ); + Abc_Print( -2, "\t-I : the number of iterations when looking for a solution [default = %d]\n", nIters ); + Abc_Print( -2, "\t-g : toggle generating random cascade with these parameters [default = %s]\n", fGen? "yes": "no" ); Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandLutCas( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Abc_Ntk_t * Abc_NtkLutCascadeMap( Abc_Ntk_t * pNtk, int nLutsMax, int nIters, int fDelayLut, int fDelayRoute, int fDelayDirect, int fVerbose ); + Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc), * pNtkRes; + int c, nLutSize = 6, nLutsMax = 8, nIters = 1000, Seed = 0, fVerbose = 0; + int fDelayLut = 10, fDelayRoute = 30, fDelayDirect = 3; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "KMISLWDfvh" ) ) != EOF ) + { + switch ( c ) + { + case 'K': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" ); + goto usage; + } + nLutSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nLutSize < 0 ) + goto usage; + break; + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + nLutsMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nLutsMax < 0 ) + goto usage; + break; + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + nIters = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nIters < 0 ) + goto usage; + break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + Seed = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( Seed < 0 ) + goto usage; + break; + case 'L': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" ); + goto usage; + } + fDelayLut = atof(argv[globalUtilOptind]); + globalUtilOptind++; + if ( fDelayLut < 0 ) + goto usage; + break; + case 'W': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" ); + goto usage; + } + fDelayRoute = atof(argv[globalUtilOptind]); + globalUtilOptind++; + if ( fDelayRoute < 0 ) + goto usage; + break; + case 'D': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" ); + goto usage; + } + fDelayDirect = atof(argv[globalUtilOptind]); + globalUtilOptind++; + if ( fDelayDirect < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + Abc_Print( -1, "Empty network.\n" ); + return 1; + } + if ( !Abc_NtkIsLogic(pNtk) ) + { + Abc_Print( -1, "Run command \"if\" or any other LUT mapper to map the current network into LUTs.\n" ); + return 1; + } + if ( Abc_NtkGetFaninMax(pNtk) > nLutSize ) + { + Abc_Print( -1, "The current network contains nodes with fanin count (%d) exceeding the LUT size (%d).\n", Abc_NtkGetFaninMax(pNtk), nLutSize ); + return 1; + } + srand( Seed ); + pNtkRes = Abc_NtkLutCascadeMap( pNtk, nLutsMax, nIters, fDelayLut, fDelayRoute, fDelayDirect, fVerbose ); + if ( pNtkRes == NULL ) + { + Abc_Print( -1, "LUT cascade mapping failed.\n" ); + return 1; + } + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + Abc_Print( -2, "usage: lutcas [-KMISLWD ] [-vh]\n" ); + Abc_Print( -2, "\t decomposes the current network into LUT cascades\n" ); + Abc_Print( -2, "\t-K : the number of LUT inputs [default = %d]\n", nLutSize ); + Abc_Print( -2, "\t-M : the maximum number of LUTs in the cascade [default = %d]\n", nLutsMax ); + Abc_Print( -2, "\t-I : the number of iterations when looking for a solution [default = %d]\n", nIters ); + Abc_Print( -2, "\t-S : the random seed used to randimize solutions [default = %d]\n", Seed ); + Abc_Print( -2, "\t-L : the intrinsic LUT delay [default = %d]\n", fDelayLut ); + Abc_Print( -2, "\t-W : the routable wire delay [default = %d]\n", fDelayRoute ); + Abc_Print( -2, "\t-D : the non-routable wire delay [default = %d]\n", fDelayDirect ); + Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandBsEval( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern void Abc_BSEvalOneTest( word * pT, int nVars, int nBVars, int fVerbose ); + extern void Abc_BSEvalBestTest( word * pIn, int nVars, int nBVars, int fShared, int fVerbose ); + extern void Abc_BSEvalBestGen( int nVars, int nBVars, int nFuncs, int nMints, int fTryAll, int fShared, int fVerbose ); + int c, nVars = 0, nBVars = 0, nSVars = 0, nFuncs = 0, nMints = 0, fTryAll = 0, fVerbose = 0; char * pTtStr = NULL; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "IBSRMavh" ) ) != EOF ) + { + switch ( c ) + { + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + nVars = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nVars < 2 || nVars > 16 ) + goto usage; + break; + case 'B': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" ); + goto usage; + } + nBVars = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nBVars < 1 || nBVars > 16 ) + goto usage; + break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + nSVars = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nSVars < 0 || nSVars > 16 ) + goto usage; + break; + case 'R': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" ); + goto usage; + } + nFuncs = atoi(argv[globalUtilOptind]); + if ( nFuncs < 1 ) + goto usage; + globalUtilOptind++; + break; + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + nMints = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'a': + fTryAll ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( argc == globalUtilOptind + 1 ) + pTtStr = argv[globalUtilOptind]; + if ( pTtStr ) + { + nVars = Abc_Base2Log((int)strlen(pTtStr)) + 2; + if ( (1 << (nVars-2)) != (int)strlen(pTtStr) ) + { + Abc_Print( -1, "Truth table is expected to have %d hex digits (instead of %d).\n", (1 << (nVars-2)), strlen(pTtStr) ); + return 1; + } + } + if ( nVars == 0 ) + { + Abc_Print( -1, "The number of variables should be specified on the command line.\n" ); + return 1; + } + if ( nBVars == 0 ) + { + Abc_Print( -1, "The bound set size should be specified on the command line.\n" ); + return 1; + } + if ( nFuncs ) + Abc_BSEvalBestGen( nVars, nBVars, nFuncs, nMints, fTryAll, nSVars == 1, fVerbose ); + else if ( pTtStr ) + { + word pTruth[1024] = {0}; + Abc_TtReadHex( pTruth, pTtStr ); + if ( fTryAll ) + Abc_BSEvalBestTest( pTruth, nVars, nBVars, nSVars == 1, fVerbose ); + else + Abc_BSEvalOneTest( pTruth, nVars, nBVars, fVerbose ); + } + return 0; + +usage: + Abc_Print( -2, "usage: bseval [-IBSRM ] [-avh] \n" ); + Abc_Print( -2, "\t bound set evaluation\n" ); + Abc_Print( -2, "\t-I : the number of input variables [default = %d]\n", nVars ); + Abc_Print( -2, "\t-B : the number of bound set variables [default = %d]\n", nBVars ); + Abc_Print( -2, "\t-S : the number of shared variables [default = %d]\n", nSVars ); + Abc_Print( -2, "\t-R : the number of random functions to try [default = unused]\n" ); + Abc_Print( -2, "\t-M : the number of positive minterms in the random function [default = unused]\n" ); + Abc_Print( -2, "\t-a : toggle trying all bound sets of this size [default = %s]\n", fTryAll ? "yes" : "no" ); + Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose ? "yes" : "no" ); + Abc_Print( -2, "\t-h : print the command usage\n" ); + Abc_Print( -2, "\t : truth table in hex notation\n" ); + return 1; +} + /**Function************************************************************* Synopsis [] @@ -9786,8 +10212,7 @@ usage: Abc_Print( -2, "\t synthesizes the smallest circuit composed of two-input gates\n" ); Abc_Print( -2, "\t for the only NPN class of 5-input functions that requires 12 gates;\n" ); Abc_Print( -2, "\t all other functions can be realized with 11 two-input gates or less\n" ); - Abc_Print( -2, "\t (see Section 7.1.2 \"Boolean evaluation\" in the book by Donald Knuth\n" ); - Abc_Print( -2, "\t http://www.cs.utsa.edu/~wagner/knuth/fasc0c.pdf)\n" ); + Abc_Print( -2, "\t (see Section 7.1.2 \"Boolean evaluation\" in the book The Art of Computer Programming by Donald Knuth)\n" ); return 1; } @@ -9804,13 +10229,14 @@ usage: ***********************************************************************/ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars ); + extern int Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars ); extern void Exa3_ManExactSynthesis2( Bmc_EsPar_t * pPars ); + extern void Exa3_ManExactSynthesisRand( Bmc_EsPar_t * pPars ); int c; Bmc_EsPar_t Pars, * pPars = &Pars; Bmc_EsParSetDefault( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "INKTiaocgvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "INKTSRMiaocgvh" ) ) != EOF ) { switch ( c ) { @@ -9858,6 +10284,33 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->RuntimeLim < 0 ) goto usage; break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + pPars->pSymStr = argv[globalUtilOptind]; + globalUtilOptind++; + break; + case 'R': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nRandFuncs = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nMintNum = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; case 'i': pPars->fUseIncr ^= 1; break; @@ -9884,16 +10337,21 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( argc == globalUtilOptind + 1 ) pPars->pTtStr = argv[globalUtilOptind]; - if ( pPars->pTtStr == NULL ) + if ( pPars->pTtStr == NULL && pPars->pSymStr == NULL && pPars->nRandFuncs == 0 ) { Abc_Print( -1, "Truth table should be given on the command line.\n" ); return 1; } - if ( (1 << (pPars->nVars-2)) != (int)strlen(pPars->pTtStr) ) + if ( pPars->pTtStr && (1 << (pPars->nVars-2)) != (int)strlen(pPars->pTtStr) ) { Abc_Print( -1, "Truth table is expected to have %d hex digits (instead of %d).\n", (1 << (pPars->nVars-2)), strlen(pPars->pTtStr) ); return 1; } + if ( pPars->pSymStr && pPars->nVars+1 != strlen(pPars->pSymStr) ) + { + Abc_Print( -1, "The char string of the %d-variable symmetric function should have %d zeros and ones (instead of %d).\n", pPars->nVars, pPars->nVars+1, strlen(pPars->pSymStr) ); + return 1; + } if ( pPars->nVars > pPars->nNodes * (pPars->nLutSize - 1) + 1 ) { Abc_Print( -1, "Function with %d variales cannot be implemented with %d %d-input LUTs.\n", pPars->nVars, pPars->nNodes, pPars->nLutSize ); @@ -9909,19 +10367,26 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Node size should not be more than 6 inputs.\n" ); return 1; } - if ( pPars->fGlucose ) + if ( pPars->nRandFuncs ) { + pPars->fGlucose = 1; + Exa3_ManExactSynthesisRand( pPars ); + } + else if ( pPars->fGlucose ) Exa3_ManExactSynthesis( pPars ); else Exa3_ManExactSynthesis2( pPars ); return 0; usage: - Abc_Print( -2, "usage: lutexact [-INKT ] [-iaocgvh] \n" ); + Abc_Print( -2, "usage: lutexact [-INKTRM ] [-S string] [-iaocgvh] \n" ); Abc_Print( -2, "\t exact synthesis of I-input function using N K-input gates\n" ); Abc_Print( -2, "\t-I : the number of input variables [default = %d]\n", pPars->nVars ); Abc_Print( -2, "\t-N : the number of K-input nodes [default = %d]\n", pPars->nNodes ); Abc_Print( -2, "\t-K : the number of node fanins [default = %d]\n", pPars->nLutSize ); Abc_Print( -2, "\t-T : the runtime limit in seconds [default = %d]\n", pPars->RuntimeLim ); + Abc_Print( -2, "\t-R : the number of random functions to try [default = unused]\n" ); + Abc_Print( -2, "\t-M : the number of positive minterms in the random function [default = unused]\n" ); + Abc_Print( -2, "\t-S : charasteristic string of a symmetric function [default = %d]\n", pPars->pSymStr ); Abc_Print( -2, "\t-i : toggle using incremental solving [default = %s]\n", pPars->fUseIncr ? "yes" : "no" ); Abc_Print( -2, "\t-a : toggle using only AND-gates when K = 2 [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" ); Abc_Print( -2, "\t-o : toggle using additional optimizations [default = %s]\n", pPars->fFewerVars ? "yes" : "no" ); @@ -19038,7 +19503,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv ) int fUseBuffs; int fVerbose; int c; - extern Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, double AreaMulti, double DelayMulti, float LogFan, float Slew, float Gain, int nGatesMin, int fRecovery, int fSwitching, int fSkipFanout, int fUseProfile, int fUseBuffs, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, Mio_Library_t* userLib, double DelayTarget, double AreaMulti, double DelayMulti, float LogFan, float Slew, float Gain, int nGatesMin, int fRecovery, int fSwitching, int fSkipFanout, int fUseProfile, int fUseBuffs, int fVerbose ); extern int Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose, int fVeryVerbose ); pNtk = Abc_FrameReadNtk(pAbc); @@ -19189,7 +19654,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv ) } Abc_Print( 0, "The network was strashed and balanced before mapping.\n" ); // get the new network - pNtkRes = Abc_NtkMap( pNtk, DelayTarget, AreaMulti, DelayMulti, LogFan, Slew, Gain, nGatesMin, fRecovery, fSwitching, fSkipFanout, fUseProfile, fUseBuffs, fVerbose ); + pNtkRes = Abc_NtkMap( pNtk, /*userLib=*/NULL, DelayTarget, AreaMulti, DelayMulti, LogFan, Slew, Gain, nGatesMin, fRecovery, fSwitching, fSkipFanout, fUseProfile, fUseBuffs, fVerbose ); if ( pNtkRes == NULL ) { Abc_NtkDelete( pNtk ); @@ -19201,7 +19666,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv ) else { // get the new network - pNtkRes = Abc_NtkMap( pNtk, DelayTarget, AreaMulti, DelayMulti, LogFan, Slew, Gain, nGatesMin, fRecovery, fSwitching, fSkipFanout, fUseProfile, fUseBuffs, fVerbose ); + pNtkRes = Abc_NtkMap( pNtk, /*userLib=*/NULL, DelayTarget, AreaMulti, DelayMulti, LogFan, Slew, Gain, nGatesMin, fRecovery, fSwitching, fSkipFanout, fUseProfile, fUseBuffs, fVerbose ); if ( pNtkRes == NULL ) { Abc_Print( -1, "Mapping has failed.\n" ); @@ -19481,6 +19946,124 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandStochMap( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); + extern void Abc_NtkStochMap( int nSuppMax, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript, int nProcs ); + int c, nMaxSize = 14, nIters = 1, TimeOut = 0, Seed = 0, nProcs = 1, fVerbose = 0; char * pScript; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "NITSPvh" ) ) != EOF ) + { + switch ( c ) + { + case 'N': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + nMaxSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nMaxSize < 0 ) + goto usage; + break; + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + nIters = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nIters < 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; + } + TimeOut = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( TimeOut < 0 ) + goto usage; + break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + Seed = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( Seed < 0 ) + goto usage; + break; + case 'P': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" ); + goto usage; + } + nProcs = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nProcs < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + Abc_Print( -1, "Abc_CommandStochMap(): There is no AIG.\n" ); + return 0; + } + if ( !Abc_NtkIsMappedLogic(pNtk) ) + { + Abc_Print( -1, "Abc_CommandStochMap(): Expecting a mapped current newtork as input.\n" ); + return 0; + } + if ( argc != globalUtilOptind + 1 ) + { + printf( "Expecting a synthesis script in quotes on the command line (for example: \"&st; &dch; &if\").\n" ); + goto usage; + } + pScript = Abc_UtilStrsav( argv[globalUtilOptind] ); + Abc_NtkStochMap( nMaxSize, nIters, TimeOut, Seed, fVerbose, pScript, nProcs ); + ABC_FREE( pScript ); + return 0; + +usage: + Abc_Print( -2, "usage: stochmap [-NITSP ] [-tvh]