diff options
-rw-r--r-- | src/expr/datatype.cpp | 2 | ||||
-rw-r--r-- | src/smt/term_formula_removal.cpp | 16 | ||||
-rw-r--r-- | src/smt/term_formula_removal.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/ceg_instantiator.cpp | 29 | ||||
-rw-r--r-- | src/theory/quantifiers/ceg_instantiator.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 98 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 9 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 9 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 2 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_rewriter.cpp | 1 | ||||
-rw-r--r-- | test/Makefile.am | 1 | ||||
-rw-r--r-- | test/regress/regress0/rels/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/rels/card_transpose.cvc | 6 | ||||
-rw-r--r-- | test/regress/regress1/Makefile.am | 2 | ||||
-rw-r--r-- | test/regress/regress1/quantifiers/Makefile | 8 | ||||
-rw-r--r-- | test/regress/regress1/quantifiers/Makefile.am | 30 | ||||
-rw-r--r-- | test/regress/regress1/quantifiers/bug802.smt2 | 12 | ||||
-rw-r--r-- | test/unit/util/stats_black.h | 1 |
20 files changed, 164 insertions, 72 deletions
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 8a6d5d4a3..f80961cf8 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -601,7 +601,7 @@ bool Datatype::getSygusAllowConst() const { } bool Datatype::getSygusAllowAll() const { - return d_sygus_allow_const; + return d_sygus_allow_all; } Expr Datatype::getSygusEvaluationFunc() const { diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index 87db183e2..bd133b0af 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -153,10 +153,7 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output, if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) { // Remember if we're inside a quantifier inQuant = true; - }else if( theory::kindToTheoryId(node.getKind())!=theory::THEORY_BOOL && - node.getKind()!=kind::EQUAL && node.getKind()!=kind::SEP_STAR && - node.getKind()!=kind::SEP_WAND && node.getKind()!=kind::SEP_LABEL && - node.getKind()!=kind::BITVECTOR_EAGER_ATOM ){ + }else if( !inTerm && hasNestedTermChildren( node ) ){ // Remember if we're inside a term Debug("ite") << "In term because of " << node << " " << node.getKind() << std::endl; inTerm = true; @@ -208,7 +205,7 @@ Node RemoveTermFormulas::replace(TNode node, bool inQuant, bool inTerm) const { if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) { // Remember if we're inside a quantifier inQuant = true; - }else if( theory::kindToTheoryId(node.getKind())!=theory::THEORY_BOOL && node.getKind()!=kind::EQUAL ){ + }else if( !inTerm && hasNestedTermChildren( node ) ){ // Remember if we're inside a term inTerm = true; } @@ -233,4 +230,13 @@ Node RemoveTermFormulas::replace(TNode node, bool inQuant, bool inTerm) const { } } +// returns true if the children of node should be considered nested terms +bool RemoveTermFormulas::hasNestedTermChildren( TNode node ) { + return theory::kindToTheoryId(node.getKind())!=theory::THEORY_BOOL && + node.getKind()!=kind::EQUAL && node.getKind()!=kind::SEP_STAR && + node.getKind()!=kind::SEP_WAND && node.getKind()!=kind::SEP_LABEL && + node.getKind()!=kind::BITVECTOR_EAGER_ATOM; + // dont' worry about FORALL or EXISTS (handled separately) +} + }/* CVC4 namespace */ diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index 09991c571..9c96bbf15 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -40,6 +40,8 @@ class RemoveTermFormulas { ITECache d_iteCache; static inline int cacheVal( bool inQuant, bool inTerm ) { return (inQuant ? 1 : 0) + 2*(inTerm ? 1 : 0); } + + static bool hasNestedTermChildren( TNode node ); public: RemoveTermFormulas(context::UserContext* u); diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 84743fc1d..33dfa19bc 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -817,6 +817,7 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& reconstructed, bool rconsSygus ) { d_solution = s; const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype(); + Trace("csi-sol") << "Reconstruct to syntax " << s << ", allow all = " << dt.getSygusAllowAll() << " " << stn << ", reconstruct = " << rconsSygus << std::endl; //reconstruct the solution into sygus if necessary reconstructed = 0; diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 7ce299864..1543b2ebd 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -717,14 +717,10 @@ void CegInstantiator::processAssertions() { std::map< Node, Node > aux_subs; //for each variable - std::vector< TheoryId > tids; - tids.push_back(THEORY_UF); for( unsigned i=0; i<d_vars.size(); i++ ){ Node pv = d_vars[i]; TypeNode pvtn = pv.getType(); - //collect relevant theories - std::map< TypeNode, bool > visited; - collectTheoryIds( pvtn, visited, tids ); + Trace("cbqi-proc-debug") << "Collect theory ids from type " << pvtn << " of " << pv << std::endl; //collect information about eqc if( ee->hasTerm( pv ) ){ Node pvr = ee->getRepresentative( pv ); @@ -739,8 +735,8 @@ void CegInstantiator::processAssertions() { } } //collect assertions for relevant theories - for( unsigned i=0; i<tids.size(); i++ ){ - TheoryId tid = tids[i]; + for( unsigned i=0; i<d_tids.size(); i++ ){ + TheoryId tid = d_tids[i]; Theory* theory = d_qe->getTheoryEngine()->theoryOf( tid ); if( theory && d_qe->getTheoryEngine()->isTheoryEnabled(tid) ){ Trace("cbqi-proc") << "Collect assertions from theory " << tid << std::endl; @@ -781,7 +777,7 @@ void CegInstantiator::processAssertions() { TypeNode rtn = r.getType(); TheoryId tid = Theory::theoryOf( rtn ); //if we care about the theory of this eqc - if( std::find( tids.begin(), tids.end(), tid )!=tids.end() ){ + if( std::find( d_tids.begin(), d_tids.end(), tid )!=d_tids.end() ){ if( rtn.isInteger() || rtn.isReal() ){ rtn = rtn.getBaseType(); } @@ -810,7 +806,7 @@ void CegInstantiator::processAssertions() { if( it!=aux_subs.end() ){ addToAuxVarSubstitution( subs_lhs, subs_rhs, r, it->second ); }else{ - Trace("cbqi-proc") << "....no substitution found for auxiliary variable " << r << "!!!" << std::endl; + Trace("cbqi-proc") << "....no substitution found for auxiliary variable " << r << "!!! type is " << r.getType() << std::endl; Assert( false ); } } @@ -997,6 +993,21 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st for( unsigned i=0; i<lems.size(); i++ ){ collectCeAtoms( lems[i], visited ); } + + //compute the theory ids + d_tids.clear(); + d_tids.push_back(THEORY_UF); + for( unsigned r=0; r<2; r++ ){ + unsigned sz = r==0 ? d_vars.size() : d_aux_vars.size(); + for( unsigned i=0; i<sz; i++ ){ + Node pv = r==0 ? d_vars[i] : d_aux_vars[i]; + TypeNode pvtn = pv.getType(); + Trace("cbqi-proc-debug") << "Collect theory ids from type " << pvtn << " of " << pv << std::endl; + //collect relevant theories + std::map< TypeNode, bool > visited; + collectTheoryIds( pvtn, visited, d_tids ); + } + } } diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index 94d02de9b..f9a711704 100644 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -93,6 +93,8 @@ private: std::map< TypeNode, std::vector< Node > > d_curr_type_eqc; //auxiliary variables std::vector< Node > d_aux_vars; + // relevant theory ids + std::vector< TheoryId > d_tids; //literals to equalities for aux vars std::map< Node, std::map< Node, Node > > d_aux_eq; //the CE variables diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 420a3d2f7..008514dcc 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -2079,70 +2079,76 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { //try to make a matches making the body false Trace("qcf-check-debug") << "Get next match..." << std::endl; while( qi->getNextMatch( this ) ){ - Trace("qcf-inst") << "*** Produced match at effort " << e << " : " << std::endl; - qi->debugPrintMatch("qcf-inst"); - Trace("qcf-inst") << std::endl; - if( !qi->isMatchSpurious( this ) ){ - std::vector< int > assigned; - if( qi->completeMatch( this, assigned ) ){ - std::vector< Node > terms; - qi->getMatch( terms ); - bool tcs = qi->isTConstraintSpurious( this, terms ); - if( !tcs ){ - //for debugging - if( Debug.isOn("qcf-check-inst") ){ - Node inst = d_quantEngine->getInstantiation( q, terms ); - Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl; - Assert( !getTermDatabase()->isEntailed( inst, true ) ); - Assert( getTermDatabase()->isEntailed( inst, false ) || e>effort_conflict ); - } - if( d_quantEngine->addInstantiation( q, terms ) ){ - Trace("qcf-check") << " ... Added instantiation" << std::endl; - Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl; - qi->debugPrintMatch("qcf-inst"); - Trace("qcf-inst") << std::endl; - ++addedLemmas; - if( e==effort_conflict ){ - d_quantEngine->markRelevant( q ); - ++(d_quantEngine->d_statistics.d_instantiations_qcf); - if( options::qcfAllConflict() ){ - isConflict = true; - }else{ - d_conflict.set( true ); + if( d_quantEngine->inConflict() ){ + Trace("qcf-check") << " ... Quantifiers engine discovered conflict, "; + Trace("qcf-check") << "probably related to disequal congruent terms in master equality engine" << std::endl; + break; + }else{ + Trace("qcf-inst") << "*** Produced match at effort " << e << " : " << std::endl; + qi->debugPrintMatch("qcf-inst"); + Trace("qcf-inst") << std::endl; + if( !qi->isMatchSpurious( this ) ){ + std::vector< int > assigned; + if( qi->completeMatch( this, assigned ) ){ + std::vector< Node > terms; + qi->getMatch( terms ); + bool tcs = qi->isTConstraintSpurious( this, terms ); + if( !tcs ){ + //for debugging + if( Debug.isOn("qcf-check-inst") ){ + Node inst = d_quantEngine->getInstantiation( q, terms ); + Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl; + Assert( !getTermDatabase()->isEntailed( inst, true ) ); + Assert( getTermDatabase()->isEntailed( inst, false ) || e>effort_conflict ); + } + if( d_quantEngine->addInstantiation( q, terms ) ){ + Trace("qcf-check") << " ... Added instantiation" << std::endl; + Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl; + qi->debugPrintMatch("qcf-inst"); + Trace("qcf-inst") << std::endl; + ++addedLemmas; + if( e==effort_conflict ){ + d_quantEngine->markRelevant( q ); + ++(d_quantEngine->d_statistics.d_instantiations_qcf); + if( options::qcfAllConflict() ){ + isConflict = true; + }else{ + d_conflict.set( true ); + } + break; + }else if( e==effort_prop_eq ){ + d_quantEngine->markRelevant( q ); + ++(d_quantEngine->d_statistics.d_instantiations_qcf); } + }else{ + Trace("qcf-inst") << " ... Failed to add instantiation" << std::endl; + //this should only happen if the algorithm generates the same propagating instance twice this round + //in this case, break to avoid exponential behavior break; - }else if( e==effort_prop_eq ){ - d_quantEngine->markRelevant( q ); - ++(d_quantEngine->d_statistics.d_instantiations_qcf); } }else{ - Trace("qcf-inst") << " ... Failed to add instantiation" << std::endl; - //this should only happen if the algorithm generates the same propagating instance twice this round - //in this case, break to avoid exponential behavior - break; + Trace("qcf-inst") << " ... Spurious instantiation (match is T-inconsistent)" << std::endl; } + //clean up assigned + qi->revertMatch( this, assigned ); + d_tempCache.clear(); }else{ - Trace("qcf-inst") << " ... Spurious instantiation (match is T-inconsistent)" << std::endl; + Trace("qcf-inst") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl; } - //clean up assigned - qi->revertMatch( this, assigned ); - d_tempCache.clear(); }else{ - Trace("qcf-inst") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl; + Trace("qcf-inst") << " ... Spurious instantiation (match is inconsistent)" << std::endl; } - }else{ - Trace("qcf-inst") << " ... Spurious instantiation (match is inconsistent)" << std::endl; } } Trace("qcf-check") << "Done, conflict = " << d_conflict << std::endl; - if( d_conflict ){ + if( d_conflict || d_quantEngine->inConflict() ){ break; } } } } } - if( addedLemmas>0 ){ + if( addedLemmas>0 || d_quantEngine->inConflict() ){ break; } } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 5ac5ae0cc..30b17d42c 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -278,10 +278,12 @@ void TermDb::computeUfTerms( TNode f ) { Trace("term-db-lemma") << "Disequal congruent terms : " << at << " " << n << "!!!!" << std::endl; if( !d_quantEngine->getTheoryEngine()->needCheck() ){ Trace("term-db-lemma") << " all theories passed with no lemmas." << std::endl; + // we should be a full effort check, prior to theory combination } Trace("term-db-lemma") << " add lemma : " << lem << std::endl; } d_quantEngine->addLemma( lem ); + d_quantEngine->setConflict(); d_consistent_ee = false; return; } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index db0efd988..55b1af83c 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -80,6 +80,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* d_util.push_back( d_term_db ); if( options::instPropagate() ){ + // notice that this option is incompatible with options::qcfAllConflict() d_inst_prop = new quantifiers::InstPropagator( this ); d_util.push_back( d_inst_prop ); d_inst_notify.push_back( d_inst_prop->getInstantiationNotify() ); @@ -1250,8 +1251,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo for( unsigned j=0; j<d_inst_notify.size(); j++ ){ if( !d_inst_notify[j]->notifyInstantiation( d_curr_effort_level, q, lem, terms, body ) ){ Trace("inst-add-debug") << "...we are in conflict." << std::endl; - d_conflict = true; - d_conflict_c = true; + setConflict(); Assert( !d_lemmas_waiting.empty() ); break; } @@ -1319,6 +1319,11 @@ void QuantifiersEngine::markRelevant( Node q ) { d_model->markRelevant( q ); } +void QuantifiersEngine::setConflict() { + d_conflict = true; + d_conflict_c = true; +} + bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) { Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter << ", " << d_ierCounter_lc << std::endl; //determine if we should perform check, based on instWhenMode diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index bb38e5e4a..7405241b7 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -39,11 +39,6 @@ namespace theory { class QuantifiersEngine; -namespace quantifiers { - class TermDb; - class TermDbSygus; -} - class InstantiationNotify { public: InstantiationNotify(){} @@ -53,6 +48,8 @@ public: }; namespace quantifiers { + class TermDb; + class TermDbSygus; class FirstOrderModel; //modules class InstantiationEngine; @@ -343,6 +340,8 @@ public: bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; } /** is in conflict */ bool inConflict() { return d_conflict; } + /** set conflict */ + void setConflict(); /** get number of waiting lemmas */ unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); } /** get needs check */ diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 0338eb1b3..a0748f2b9 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -856,7 +856,7 @@ void TheorySetsPrivate::checkUpwardsClosure( std::vector< Node >& lemmas ) { valid = true; }else{ // if not, check whether it is definitely not a member, if unknown, split - bool not_in_r2 = itm2n!=d_pol_mems[1].end() && itm2n->second.find( xr )!=itm2->second.end(); + bool not_in_r2 = itm2n!=d_pol_mems[1].end() && itm2n->second.find( xr )!=itm2n->second.end(); if( !not_in_r2 ){ exp.push_back( NodeManager::currentNM()->mkNode( kind::MEMBER, x, it2->second[1] ) ); valid = true; diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 3590fc62d..e42a3347d 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -328,6 +328,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { NodeManager::currentNM()->mkNode( kind::CARD, NodeManager::currentNM()->mkNode( kind::INTERSECTION, node[0][0], node[0][1] ) ) ); return RewriteResponse(REWRITE_DONE, ret ); } + break; } case kind::TRANSPOSE: { if(node[0].getKind() == kind::TRANSPOSE) { diff --git a/test/Makefile.am b/test/Makefile.am index 31f23e500..b61ac2381 100644 --- a/test/Makefile.am +++ b/test/Makefile.am @@ -74,6 +74,7 @@ subdirs_to_check = \ regress/regress1/sets \ regress/regress1/strings \ regress/regress1/sygus \ + regress/regress1/quantifiers \ regress/regress2 \ regress/regress2/arith \ regress/regress3 \ diff --git a/test/regress/regress0/rels/Makefile.am b/test/regress/regress0/rels/Makefile.am index d1c035371..7f772a8e1 100644 --- a/test/regress/regress0/rels/Makefile.am +++ b/test/regress/regress0/rels/Makefile.am @@ -112,7 +112,8 @@ TESTS = \ joinImg_1_1.cvc \ joinImg_1.cvc \ joinImg_2_1.cvc \ - joinImg_2.cvc + joinImg_2.cvc \ + card_transpose.cvc # unsolved : garbage_collect.cvc diff --git a/test/regress/regress0/rels/card_transpose.cvc b/test/regress/regress0/rels/card_transpose.cvc new file mode 100644 index 000000000..bde7fe53e --- /dev/null +++ b/test/regress/regress0/rels/card_transpose.cvc @@ -0,0 +1,6 @@ +% EXPECT: unknown (INCOMPLETE) +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +ASSERT (CARD(TRANSPOSE(x)) > 0); +CHECKSAT; diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am index c399a797f..aebf0de3b 100644 --- a/test/regress/regress1/Makefile.am +++ b/test/regress/regress1/Makefile.am @@ -1,4 +1,4 @@ -SUBDIRS = . bv aufbv auflia datatypes rewriterules lemmas decision fmf strings sets sygus sep +SUBDIRS = . bv aufbv auflia datatypes rewriterules lemmas decision fmf strings sets sygus sep quantifiers # don't override a BINARY imported from a personal.mk @mk_if@eq ($(BINARY),) diff --git a/test/regress/regress1/quantifiers/Makefile b/test/regress/regress1/quantifiers/Makefile new file mode 100644 index 000000000..fcd888f99 --- /dev/null +++ b/test/regress/regress1/quantifiers/Makefile @@ -0,0 +1,8 @@ +topdir = ../../../.. +srcdir = test/regress/regress1/quantifiers + +include $(topdir)/Makefile.subdir + +# synonyms for "check" +.PHONY: test +test: check diff --git a/test/regress/regress1/quantifiers/Makefile.am b/test/regress/regress1/quantifiers/Makefile.am new file mode 100644 index 000000000..cc5834a31 --- /dev/null +++ b/test/regress/regress1/quantifiers/Makefile.am @@ -0,0 +1,30 @@ +# don't override a BINARY imported from a personal.mk +@mk_if@eq ($(BINARY),) +@mk_empty@BINARY = cvc4 +end@mk_if@ + +LOG_COMPILER = @srcdir@/../../run_regression +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) + +if AUTOMAKE_1_11 +# old-style (pre-automake 1.12) test harness +TESTS_ENVIRONMENT = \ + $(LOG_COMPILER) \ + $(AM_LOG_FLAGS) $(LOG_FLAGS) +endif + +# These are run for all build profiles. +# If a test shouldn't be run in e.g. competition mode, +# put it below in "TESTS +=" +TESTS = \ + bug802.smt2 + +EXTRA_DIST = $(TESTS) + +# synonyms for "check" in this directory +.PHONY: regress regress1 test +regress regress1 test: check + +# do nothing in this subdir +.PHONY: regress0 regress2 regress3 regress4 +regress0 regress2 regress3 regress4: diff --git a/test/regress/regress1/quantifiers/bug802.smt2 b/test/regress/regress1/quantifiers/bug802.smt2 new file mode 100644 index 000000000..57da8510e --- /dev/null +++ b/test/regress/regress1/quantifiers/bug802.smt2 @@ -0,0 +1,12 @@ +(set-logic BV) +(set-info :source | +Hardware fixpoint check problems. +These benchmarks stem from an evaluation described in Wintersteiger, Hamadi, de Moura: Efficiently solving quantified bit-vector formulas, FMSD 42(1), 2013. +The hardware models that were used are from the VCEGAR benchmark suite (see www.cprover.org/hardware/). + |) +(set-info :smt-lib-version 2.0) +(set-info :category "industrial") +(set-info :status unsat) +(assert (forall ((Verilog__main.reset_64_0 Bool)) (forall ((Verilog__main.rst_64_0 Bool)) (forall ((Verilog__main.usb_rst_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.hold_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.stuff_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.sft_done_e_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.sft_done_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.sft_done_r_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.one_cnt_64_0 (_ BitVec 3))) (forall ((Verilog__main.i_tx_phy.eop_done_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.append_eop_sync3_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.clk_64_0 Bool)) (forall ((Verilog__main.clk_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.rst_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.fs_ce_64_0 Bool)) (forall ((Verilog__main.fs_ce_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.phy_mode_64_0 Bool)) (forall ((Verilog__main.phy_tx_mode_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.txdp_64_0 Bool)) (forall ((Verilog__main.txdp_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.txdn_64_0 Bool)) (forall ((Verilog__main.txdn_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.txoe_64_0 Bool)) (forall ((Verilog__main.txoe_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.DataOut_i_64_0 (_ BitVec 8))) (forall ((Verilog__main.DataOut_i_64_0 (_ BitVec 8))) (forall ((Verilog__main.i_tx_phy.TxValid_i_64_0 Bool)) (forall ((Verilog__main.TxValid_i_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.TxReady_o_64_0 Bool)) (forall ((Verilog__main.TxReady_o_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.RxActive_o_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.rx_active_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.RxValid_o_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.rx_valid_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.RxError_o_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.DataIn_o_64_0 (_ BitVec 8))) (forall ((Verilog__main.i_rx_phy.hold_reg_64_0 (_ BitVec 8))) (forall ((Verilog__main.i_rx_phy.LineState_64_0 (_ BitVec 2))) (forall ((Verilog__main.i_rx_phy.rxdp_s1_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.rxdn_s1_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.k_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.rxdp_s_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.rxdn_s_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.j_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.se0_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.lock_en_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.rx_en_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.change_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.rxdp_s1r_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.rxdn_s1r_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.drop_bit_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.one_cnt_64_0 (_ BitVec 3))) (forall ((Verilog__main.i_rx_phy.clk_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.rst_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.fs_ce_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.rxd_64_0 Bool)) (forall ((Verilog__main.rxd_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.rxdp_64_0 Bool)) (forall ((Verilog__main.rxdp_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.rxdn_64_0 Bool)) (forall ((Verilog__main.rxdn_64_0 Bool)) (forall ((Verilog__main.DataIn_o_64_0 (_ BitVec 8))) (forall ((Verilog__main.RxValid_o_64_0 Bool)) (forall ((Verilog__main.RxActive_o_64_0 Bool)) (forall ((Verilog__main.RxError_o_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.RxEn_i_64_0 Bool)) (forall ((Verilog__main.LineState_o_64_0 (_ BitVec 2))) (forall ((Verilog__main.reset_64_1 Bool)) (forall ((Verilog__main.rst_64_1 Bool)) (forall ((Verilog__main.usb_rst_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.hold_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.stuff_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.sft_done_e_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.sft_done_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.sft_done_r_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.one_cnt_64_1 (_ BitVec 3))) (forall ((Verilog__main.i_tx_phy.eop_done_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.append_eop_sync3_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.clk_64_1 Bool)) (forall ((Verilog__main.clk_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.rst_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.fs_ce_64_1 Bool)) (forall ((Verilog__main.fs_ce_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.phy_mode_64_1 Bool)) (forall ((Verilog__main.phy_tx_mode_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.txdp_64_1 Bool)) (forall ((Verilog__main.txdp_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.txdn_64_1 Bool)) (forall ((Verilog__main.txdn_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.txoe_64_1 Bool)) (forall ((Verilog__main.txoe_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.DataOut_i_64_1 (_ BitVec 8))) (forall ((Verilog__main.DataOut_i_64_1 (_ BitVec 8))) (forall ((Verilog__main.i_tx_phy.TxValid_i_64_1 Bool)) (forall ((Verilog__main.TxValid_i_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.TxReady_o_64_1 Bool)) (forall ((Verilog__main.TxReady_o_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.RxActive_o_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.rx_active_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.RxValid_o_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.rx_valid_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.RxError_o_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.DataIn_o_64_1 (_ BitVec 8))) (forall ((Verilog__main.i_rx_phy.hold_reg_64_1 (_ BitVec 8))) (forall ((Verilog__main.i_rx_phy.LineState_64_1 (_ BitVec 2))) (forall ((Verilog__main.i_rx_phy.rxdp_s1_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.rxdn_s1_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.k_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.rxdp_s_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.rxdn_s_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.j_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.se0_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.lock_en_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.rx_en_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.change_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.rxdp_s1r_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.rxdn_s1r_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.drop_bit_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.one_cnt_64_1 (_ BitVec 3))) (forall ((Verilog__main.i_rx_phy.clk_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.rst_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.fs_ce_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.rxd_64_1 Bool)) (forall ((Verilog__main.rxd_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.rxdp_64_1 Bool)) (forall ((Verilog__main.rxdp_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.rxdn_64_1 Bool)) (forall ((Verilog__main.rxdn_64_1 Bool)) (forall ((Verilog__main.DataIn_o_64_1 (_ BitVec 8))) (forall ((Verilog__main.RxValid_o_64_1 Bool)) (forall ((Verilog__main.RxActive_o_64_1 Bool)) (forall ((Verilog__main.RxError_o_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.RxEn_i_64_1 Bool)) (forall ((Verilog__main.LineState_o_64_1 (_ BitVec 2))) (forall ((Verilog__main.reset_64_2 Bool)) (forall ((Verilog__main.rst_64_2 Bool)) (forall ((Verilog__main.usb_rst_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.hold_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.stuff_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.sft_done_e_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.sft_done_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.sft_done_r_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.one_cnt_64_2 (_ BitVec 3))) (forall ((Verilog__main.i_tx_phy.eop_done_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.append_eop_sync3_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.clk_64_2 Bool)) (forall ((Verilog__main.clk_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.rst_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.fs_ce_64_2 Bool)) (forall ((Verilog__main.fs_ce_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.phy_mode_64_2 Bool)) (forall ((Verilog__main.phy_tx_mode_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.txdp_64_2 Bool)) (forall ((Verilog__main.txdp_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.txdn_64_2 Bool)) (forall ((Verilog__main.txdn_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.txoe_64_2 Bool)) (forall ((Verilog__main.txoe_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.DataOut_i_64_2 (_ BitVec 8))) (forall ((Verilog__main.DataOut_i_64_2 (_ BitVec 8))) (forall ((Verilog__main.i_tx_phy.TxValid_i_64_2 Bool)) (forall ((Verilog__main.TxValid_i_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.TxReady_o_64_2 Bool)) (forall ((Verilog__main.TxReady_o_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.RxActive_o_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.rx_active_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.RxValid_o_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.rx_valid_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.RxError_o_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.DataIn_o_64_2 (_ BitVec 8))) (forall ((Verilog__main.i_rx_phy.hold_reg_64_2 (_ BitVec 8))) (forall ((Verilog__main.i_rx_phy.LineState_64_2 (_ BitVec 2))) (forall ((Verilog__main.i_rx_phy.rxdp_s1_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.rxdn_s1_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.k_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.rxdp_s_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.rxdn_s_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.j_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.se0_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.lock_en_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.rx_en_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.change_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.rxdp_s1r_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.rxdn_s1r_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.drop_bit_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.one_cnt_64_2 (_ BitVec 3))) (forall ((Verilog__main.i_rx_phy.clk_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.rst_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.fs_ce_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.rxd_64_2 Bool)) (forall ((Verilog__main.rxd_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.rxdp_64_2 Bool)) (forall ((Verilog__main.rxdp_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.rxdn_64_2 Bool)) (forall ((Verilog__main.rxdn_64_2 Bool)) (forall ((Verilog__main.DataIn_o_64_2 (_ BitVec 8))) (forall ((Verilog__main.RxValid_o_64_2 Bool)) (forall ((Verilog__main.RxActive_o_64_2 Bool)) (forall ((Verilog__main.RxError_o_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.RxEn_i_64_2 Bool)) (forall ((Verilog__main.LineState_o_64_2 (_ BitVec 2))) (forall ((Verilog__main.i_tx_phy.sd_bs_o_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.sd_nrzi_o_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.append_eop_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.append_eop_sync1_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.append_eop_sync2_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.txoe_r1_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.txoe_r2_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.state_64_0 (_ BitVec 3))) (forall ((Verilog__main.i_tx_phy.tx_ready_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.tx_ready_d_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.ld_sop_d_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.ld_data_d_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.ld_eop_d_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.tx_ip_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.tx_ip_sync_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.bit_cnt_64_0 (_ BitVec 3))) (forall ((Verilog__main.i_tx_phy.hold_reg_64_0 (_ BitVec 8))) (forall ((Verilog__main.i_tx_phy.sd_raw_o_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.data_done_64_0 Bool)) (forall ((Verilog__main.i_tx_phy.ld_data_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.rxd_t1_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.rxd_s1_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.rxd_s_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.rxdp_t1_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.rxdn_t1_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.synced_d_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.bit_cnt_64_0 (_ BitVec 3))) (forall ((Verilog__main.i_rx_phy.rx_valid1_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.shift_en_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.sd_r_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.sd_nrzi_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.dpll_state_64_0 (_ BitVec 2))) (forall ((Verilog__main.i_rx_phy.fs_ce_d_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.fs_ce_r1_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.fs_ce_r2_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.fs_ce_r3_64_0 Bool)) (forall ((Verilog__main.i_rx_phy.fs_state_64_0 (_ BitVec 3))) (forall ((Verilog__main.i_rx_phy.rx_valid_r_64_0 Bool)) (forall ((Verilog__main.rst_cnt_64_0 (_ BitVec 5))) (forall ((Verilog__main.i_tx_phy.sd_bs_o_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.sd_nrzi_o_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.append_eop_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.append_eop_sync1_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.append_eop_sync2_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.txoe_r1_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.txoe_r2_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.state_64_1 (_ BitVec 3))) (forall ((Verilog__main.i_tx_phy.tx_ready_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.tx_ready_d_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.ld_sop_d_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.ld_data_d_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.ld_eop_d_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.tx_ip_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.tx_ip_sync_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.bit_cnt_64_1 (_ BitVec 3))) (forall ((Verilog__main.i_tx_phy.hold_reg_64_1 (_ BitVec 8))) (forall ((Verilog__main.i_tx_phy.sd_raw_o_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.data_done_64_1 Bool)) (forall ((Verilog__main.i_tx_phy.ld_data_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.rxd_t1_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.rxd_s1_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.rxd_s_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.rxdp_t1_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.rxdn_t1_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.synced_d_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.bit_cnt_64_1 (_ BitVec 3))) (forall ((Verilog__main.i_rx_phy.rx_valid1_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.shift_en_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.sd_r_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.sd_nrzi_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.dpll_state_64_1 (_ BitVec 2))) (forall ((Verilog__main.i_rx_phy.fs_ce_d_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.fs_ce_r1_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.fs_ce_r2_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.fs_ce_r3_64_1 Bool)) (forall ((Verilog__main.i_rx_phy.fs_state_64_1 (_ BitVec 3))) (forall ((Verilog__main.i_rx_phy.rx_valid_r_64_1 Bool)) (forall ((Verilog__main.rst_cnt_64_1 (_ BitVec 5))) (forall ((Verilog__main.i_tx_phy.sd_bs_o_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.sd_nrzi_o_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.append_eop_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.append_eop_sync1_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.append_eop_sync2_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.txoe_r1_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.txoe_r2_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.state_64_2 (_ BitVec 3))) (forall ((Verilog__main.i_tx_phy.tx_ready_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.tx_ready_d_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.ld_sop_d_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.ld_data_d_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.ld_eop_d_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.tx_ip_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.tx_ip_sync_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.bit_cnt_64_2 (_ BitVec 3))) (forall ((Verilog__main.i_tx_phy.hold_reg_64_2 (_ BitVec 8))) (forall ((Verilog__main.i_tx_phy.sd_raw_o_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.data_done_64_2 Bool)) (forall ((Verilog__main.i_tx_phy.ld_data_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.rxd_t1_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.rxd_s1_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.rxd_s_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.rxdp_t1_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.rxdn_t1_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.synced_d_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.bit_cnt_64_2 (_ BitVec 3))) (forall ((Verilog__main.i_rx_phy.rx_valid1_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.shift_en_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.sd_r_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.sd_nrzi_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.dpll_state_64_2 (_ BitVec 2))) (forall ((Verilog__main.i_rx_phy.fs_ce_d_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.fs_ce_r1_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.fs_ce_r2_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.fs_ce_r3_64_2 Bool)) (forall ((Verilog__main.i_rx_phy.fs_state_64_2 (_ BitVec 3))) (forall ((Verilog__main.i_rx_phy.rx_valid_r_64_2 Bool)) (forall ((Verilog__main.rst_cnt_64_2 (_ BitVec 5))) (exists ((Verilog__main.reset_64_0_39_ Bool)) (exists ((Verilog__main.rst_64_0_39_ Bool)) (exists ((Verilog__main.usb_rst_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.hold_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.stuff_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.sft_done_e_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.sft_done_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.sft_done_r_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.one_cnt_64_0_39_ (_ BitVec 3))) (exists ((Verilog__main.i_tx_phy.eop_done_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.append_eop_sync3_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.clk_64_0_39_ Bool)) (exists ((Verilog__main.clk_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.rst_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.fs_ce_64_0_39_ Bool)) (exists ((Verilog__main.fs_ce_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.phy_mode_64_0_39_ Bool)) (exists ((Verilog__main.phy_tx_mode_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.txdp_64_0_39_ Bool)) (exists ((Verilog__main.txdp_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.txdn_64_0_39_ Bool)) (exists ((Verilog__main.txdn_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.txoe_64_0_39_ Bool)) (exists ((Verilog__main.txoe_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.DataOut_i_64_0_39_ (_ BitVec 8))) (exists ((Verilog__main.DataOut_i_64_0_39_ (_ BitVec 8))) (exists ((Verilog__main.i_tx_phy.TxValid_i_64_0_39_ Bool)) (exists ((Verilog__main.TxValid_i_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.TxReady_o_64_0_39_ Bool)) (exists ((Verilog__main.TxReady_o_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.RxActive_o_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rx_active_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.RxValid_o_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rx_valid_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.RxError_o_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.DataIn_o_64_0_39_ (_ BitVec 8))) (exists ((Verilog__main.i_rx_phy.hold_reg_64_0_39_ (_ BitVec 8))) (exists ((Verilog__main.i_rx_phy.LineState_64_0_39_ (_ BitVec 2))) (exists ((Verilog__main.i_rx_phy.rxdp_s1_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rxdn_s1_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.k_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rxdp_s_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rxdn_s_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.j_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.se0_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.lock_en_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rx_en_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.change_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rxdp_s1r_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rxdn_s1r_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.drop_bit_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.one_cnt_64_0_39_ (_ BitVec 3))) (exists ((Verilog__main.i_rx_phy.clk_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rst_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.fs_ce_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rxd_64_0_39_ Bool)) (exists ((Verilog__main.rxd_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rxdp_64_0_39_ Bool)) (exists ((Verilog__main.rxdp_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rxdn_64_0_39_ Bool)) (exists ((Verilog__main.rxdn_64_0_39_ Bool)) (exists ((Verilog__main.DataIn_o_64_0_39_ (_ BitVec 8))) (exists ((Verilog__main.RxValid_o_64_0_39_ Bool)) (exists ((Verilog__main.RxActive_o_64_0_39_ Bool)) (exists ((Verilog__main.RxError_o_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.RxEn_i_64_0_39_ Bool)) (exists ((Verilog__main.LineState_o_64_0_39_ (_ BitVec 2))) (exists ((Verilog__main.reset_64_1_39_ Bool)) (exists ((Verilog__main.rst_64_1_39_ Bool)) (exists ((Verilog__main.usb_rst_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.hold_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.stuff_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.sft_done_e_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.sft_done_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.sft_done_r_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.one_cnt_64_1_39_ (_ BitVec 3))) (exists ((Verilog__main.i_tx_phy.eop_done_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.append_eop_sync3_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.clk_64_1_39_ Bool)) (exists ((Verilog__main.clk_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.rst_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.fs_ce_64_1_39_ Bool)) (exists ((Verilog__main.fs_ce_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.phy_mode_64_1_39_ Bool)) (exists ((Verilog__main.phy_tx_mode_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.txdp_64_1_39_ Bool)) (exists ((Verilog__main.txdp_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.txdn_64_1_39_ Bool)) (exists ((Verilog__main.txdn_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.txoe_64_1_39_ Bool)) (exists ((Verilog__main.txoe_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.DataOut_i_64_1_39_ (_ BitVec 8))) (exists ((Verilog__main.DataOut_i_64_1_39_ (_ BitVec 8))) (exists ((Verilog__main.i_tx_phy.TxValid_i_64_1_39_ Bool)) (exists ((Verilog__main.TxValid_i_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.TxReady_o_64_1_39_ Bool)) (exists ((Verilog__main.TxReady_o_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.RxActive_o_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rx_active_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.RxValid_o_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rx_valid_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.RxError_o_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.DataIn_o_64_1_39_ (_ BitVec 8))) (exists ((Verilog__main.i_rx_phy.hold_reg_64_1_39_ (_ BitVec 8))) (exists ((Verilog__main.i_rx_phy.LineState_64_1_39_ (_ BitVec 2))) (exists ((Verilog__main.i_rx_phy.rxdp_s1_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rxdn_s1_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.k_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rxdp_s_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rxdn_s_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.j_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.se0_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.lock_en_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rx_en_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.change_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rxdp_s1r_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rxdn_s1r_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.drop_bit_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.one_cnt_64_1_39_ (_ BitVec 3))) (exists ((Verilog__main.i_rx_phy.clk_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rst_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.fs_ce_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rxd_64_1_39_ Bool)) (exists ((Verilog__main.rxd_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rxdp_64_1_39_ Bool)) (exists ((Verilog__main.rxdp_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rxdn_64_1_39_ Bool)) (exists ((Verilog__main.rxdn_64_1_39_ Bool)) (exists ((Verilog__main.DataIn_o_64_1_39_ (_ BitVec 8))) (exists ((Verilog__main.RxValid_o_64_1_39_ Bool)) (exists ((Verilog__main.RxActive_o_64_1_39_ Bool)) (exists ((Verilog__main.RxError_o_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.RxEn_i_64_1_39_ Bool)) (exists ((Verilog__main.LineState_o_64_1_39_ (_ BitVec 2))) (exists ((Verilog__main.i_tx_phy.sd_bs_o_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.sd_nrzi_o_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.append_eop_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.append_eop_sync1_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.append_eop_sync2_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.txoe_r1_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.txoe_r2_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.state_64_0_39_ (_ BitVec 3))) (exists ((Verilog__main.i_tx_phy.tx_ready_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.tx_ready_d_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.ld_sop_d_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.ld_data_d_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.ld_eop_d_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.tx_ip_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.tx_ip_sync_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.bit_cnt_64_0_39_ (_ BitVec 3))) (exists ((Verilog__main.i_tx_phy.hold_reg_64_0_39_ (_ BitVec 8))) (exists ((Verilog__main.i_tx_phy.sd_raw_o_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.data_done_64_0_39_ Bool)) (exists ((Verilog__main.i_tx_phy.ld_data_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rxd_t1_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rxd_s1_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rxd_s_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rxdp_t1_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rxdn_t1_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.synced_d_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.bit_cnt_64_0_39_ (_ BitVec 3))) (exists ((Verilog__main.i_rx_phy.rx_valid1_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.shift_en_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.sd_r_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.sd_nrzi_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.dpll_state_64_0_39_ (_ BitVec 2))) (exists ((Verilog__main.i_rx_phy.fs_ce_d_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.fs_ce_r1_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.fs_ce_r2_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.fs_ce_r3_64_0_39_ Bool)) (exists ((Verilog__main.i_rx_phy.fs_state_64_0_39_ (_ BitVec 3))) (exists ((Verilog__main.i_rx_phy.rx_valid_r_64_0_39_ Bool)) (exists ((Verilog__main.rst_cnt_64_0_39_ (_ BitVec 5))) (exists ((Verilog__main.i_tx_phy.sd_bs_o_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.sd_nrzi_o_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.append_eop_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.append_eop_sync1_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.append_eop_sync2_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.txoe_r1_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.txoe_r2_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.state_64_1_39_ (_ BitVec 3))) (exists ((Verilog__main.i_tx_phy.tx_ready_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.tx_ready_d_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.ld_sop_d_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.ld_data_d_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.ld_eop_d_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.tx_ip_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.tx_ip_sync_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.bit_cnt_64_1_39_ (_ BitVec 3))) (exists ((Verilog__main.i_tx_phy.hold_reg_64_1_39_ (_ BitVec 8))) (exists ((Verilog__main.i_tx_phy.sd_raw_o_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.data_done_64_1_39_ Bool)) (exists ((Verilog__main.i_tx_phy.ld_data_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rxd_t1_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rxd_s1_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rxd_s_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rxdp_t1_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.rxdn_t1_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.synced_d_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.bit_cnt_64_1_39_ (_ BitVec 3))) (exists ((Verilog__main.i_rx_phy.rx_valid1_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.shift_en_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.sd_r_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.sd_nrzi_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.dpll_state_64_1_39_ (_ BitVec 2))) (exists ((Verilog__main.i_rx_phy.fs_ce_d_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.fs_ce_r1_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.fs_ce_r2_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.fs_ce_r3_64_1_39_ Bool)) (exists ((Verilog__main.i_rx_phy.fs_state_64_1_39_ (_ BitVec 3))) (exists ((Verilog__main.i_rx_phy.rx_valid_r_64_1_39_ Bool)) (exists ((Verilog__main.rst_cnt_64_1_39_ (_ BitVec 5))) (=> (and (and (= Verilog__main.reset_64_0 (and Verilog__main.rst_64_0 (not Verilog__main.usb_rst_64_0))) (and (= Verilog__main.i_tx_phy.hold_64_0 Verilog__main.i_tx_phy.stuff_64_0) (= Verilog__main.i_tx_phy.sft_done_e_64_0 (and Verilog__main.i_tx_phy.sft_done_64_0 (not Verilog__main.i_tx_phy.sft_done_r_64_0))) (= Verilog__main.i_tx_phy.stuff_64_0 (= Verilog__main.i_tx_phy.one_cnt_64_0 (_ bv6 3))) (= Verilog__main.i_tx_phy.eop_done_64_0 Verilog__main.i_tx_phy.append_eop_sync3_64_0)) (= Verilog__main.i_tx_phy.clk_64_0 Verilog__main.clk_64_0) (= Verilog__main.i_tx_phy.rst_64_0 Verilog__main.reset_64_0) (= Verilog__main.i_tx_phy.fs_ce_64_0 Verilog__main.fs_ce_64_0) (= Verilog__main.i_tx_phy.phy_mode_64_0 Verilog__main.phy_tx_mode_64_0) (= Verilog__main.i_tx_phy.txdp_64_0 Verilog__main.txdp_64_0) (= Verilog__main.i_tx_phy.txdn_64_0 Verilog__main.txdn_64_0) (= Verilog__main.i_tx_phy.txoe_64_0 Verilog__main.txoe_64_0) (= Verilog__main.i_tx_phy.DataOut_i_64_0 Verilog__main.DataOut_i_64_0) (= Verilog__main.i_tx_phy.TxValid_i_64_0 Verilog__main.TxValid_i_64_0) (= Verilog__main.i_tx_phy.TxReady_o_64_0 Verilog__main.TxReady_o_64_0) (and (= Verilog__main.i_rx_phy.RxActive_o_64_0 Verilog__main.i_rx_phy.rx_active_64_0) (= Verilog__main.i_rx_phy.RxValid_o_64_0 Verilog__main.i_rx_phy.rx_valid_64_0) (= Verilog__main.i_rx_phy.RxError_o_64_0 false) (= Verilog__main.i_rx_phy.DataIn_o_64_0 Verilog__main.i_rx_phy.hold_reg_64_0) (= Verilog__main.i_rx_phy.LineState_64_0 (concat (ite Verilog__main.i_rx_phy.rxdp_s1_64_0 (_ bv1 1) (_ bv0 1)) (ite Verilog__main.i_rx_phy.rxdn_s1_64_0 (_ bv1 1) (_ bv0 1)))) (= Verilog__main.i_rx_phy.k_64_0 (and (not Verilog__main.i_rx_phy.rxdp_s_64_0) Verilog__main.i_rx_phy.rxdn_s_64_0)) (= Verilog__main.i_rx_phy.j_64_0 (and Verilog__main.i_rx_phy.rxdp_s_64_0 (not Verilog__main.i_rx_phy.rxdn_s_64_0))) (= Verilog__main.i_rx_phy.se0_64_0 (and (not Verilog__main.i_rx_phy.rxdp_s_64_0) (not Verilog__main.i_rx_phy.rxdn_s_64_0))) (= Verilog__main.i_rx_phy.lock_en_64_0 Verilog__main.i_rx_phy.rx_en_64_0) (= Verilog__main.i_rx_phy.change_64_0 (or (xor Verilog__main.i_rx_phy.rxdp_s1r_64_0 Verilog__main.i_rx_phy.rxdp_s1_64_0) (xor Verilog__main.i_rx_phy.rxdn_s1r_64_0 Verilog__main.i_rx_phy.rxdn_s1_64_0))) (= Verilog__main.i_rx_phy.drop_bit_64_0 (= Verilog__main.i_rx_phy.one_cnt_64_0 (_ bv6 3)))) (= Verilog__main.i_rx_phy.clk_64_0 Verilog__main.clk_64_0) (= Verilog__main.i_rx_phy.rst_64_0 Verilog__main.reset_64_0) (= Verilog__main.i_rx_phy.fs_ce_64_0 Verilog__main.fs_ce_64_0) (= Verilog__main.i_rx_phy.rxd_64_0 Verilog__main.rxd_64_0) (= Verilog__main.i_rx_phy.rxdp_64_0 Verilog__main.rxdp_64_0) (= Verilog__main.i_rx_phy.rxdn_64_0 Verilog__main.rxdn_64_0) (= Verilog__main.i_rx_phy.DataIn_o_64_0 Verilog__main.DataIn_o_64_0) (= Verilog__main.i_rx_phy.RxValid_o_64_0 Verilog__main.RxValid_o_64_0) (= Verilog__main.i_rx_phy.RxActive_o_64_0 Verilog__main.RxActive_o_64_0) (= Verilog__main.i_rx_phy.RxError_o_64_0 Verilog__main.RxError_o_64_0) (= Verilog__main.i_rx_phy.RxEn_i_64_0 Verilog__main.txoe_64_0) (= Verilog__main.i_rx_phy.LineState_64_0 Verilog__main.LineState_o_64_0)) (and (= Verilog__main.reset_64_1 (and Verilog__main.rst_64_1 (not Verilog__main.usb_rst_64_1))) (and (= Verilog__main.i_tx_phy.hold_64_1 Verilog__main.i_tx_phy.stuff_64_1) (= Verilog__main.i_tx_phy.sft_done_e_64_1 (and Verilog__main.i_tx_phy.sft_done_64_1 (not Verilog__main.i_tx_phy.sft_done_r_64_1))) (= Verilog__main.i_tx_phy.stuff_64_1 (= Verilog__main.i_tx_phy.one_cnt_64_1 (_ bv6 3))) (= Verilog__main.i_tx_phy.eop_done_64_1 Verilog__main.i_tx_phy.append_eop_sync3_64_1)) (= Verilog__main.i_tx_phy.clk_64_1 Verilog__main.clk_64_1) (= Verilog__main.i_tx_phy.rst_64_1 Verilog__main.reset_64_1) (= Verilog__main.i_tx_phy.fs_ce_64_1 Verilog__main.fs_ce_64_1) (= Verilog__main.i_tx_phy.phy_mode_64_1 Verilog__main.phy_tx_mode_64_1) (= Verilog__main.i_tx_phy.txdp_64_1 Verilog__main.txdp_64_1) (= Verilog__main.i_tx_phy.txdn_64_1 Verilog__main.txdn_64_1) (= Verilog__main.i_tx_phy.txoe_64_1 Verilog__main.txoe_64_1) (= Verilog__main.i_tx_phy.DataOut_i_64_1 Verilog__main.DataOut_i_64_1) (= Verilog__main.i_tx_phy.TxValid_i_64_1 Verilog__main.TxValid_i_64_1) (= Verilog__main.i_tx_phy.TxReady_o_64_1 Verilog__main.TxReady_o_64_1) (and (= Verilog__main.i_rx_phy.RxActive_o_64_1 Verilog__main.i_rx_phy.rx_active_64_1) (= Verilog__main.i_rx_phy.RxValid_o_64_1 Verilog__main.i_rx_phy.rx_valid_64_1) (= Verilog__main.i_rx_phy.RxError_o_64_1 false) (= Verilog__main.i_rx_phy.DataIn_o_64_1 Verilog__main.i_rx_phy.hold_reg_64_1) (= Verilog__main.i_rx_phy.LineState_64_1 (concat (ite Verilog__main.i_rx_phy.rxdp_s1_64_1 (_ bv1 1) (_ bv0 1)) (ite Verilog__main.i_rx_phy.rxdn_s1_64_1 (_ bv1 1) (_ bv0 1)))) (= Verilog__main.i_rx_phy.k_64_1 (and (not Verilog__main.i_rx_phy.rxdp_s_64_1) Verilog__main.i_rx_phy.rxdn_s_64_1)) (= Verilog__main.i_rx_phy.j_64_1 (and Verilog__main.i_rx_phy.rxdp_s_64_1 (not Verilog__main.i_rx_phy.rxdn_s_64_1))) (= Verilog__main.i_rx_phy.se0_64_1 (and (not Verilog__main.i_rx_phy.rxdp_s_64_1) (not Verilog__main.i_rx_phy.rxdn_s_64_1))) (= Verilog__main.i_rx_phy.lock_en_64_1 Verilog__main.i_rx_phy.rx_en_64_1) (= Verilog__main.i_rx_phy.change_64_1 (or (xor Verilog__main.i_rx_phy.rxdp_s1r_64_1 Verilog__main.i_rx_phy.rxdp_s1_64_1) (xor Verilog__main.i_rx_phy.rxdn_s1r_64_1 Verilog__main.i_rx_phy.rxdn_s1_64_1))) (= Verilog__main.i_rx_phy.drop_bit_64_1 (= Verilog__main.i_rx_phy.one_cnt_64_1 (_ bv6 3)))) (= Verilog__main.i_rx_phy.clk_64_1 Verilog__main.clk_64_1) (= Verilog__main.i_rx_phy.rst_64_1 Verilog__main.reset_64_1) (= Verilog__main.i_rx_phy.fs_ce_64_1 Verilog__main.fs_ce_64_1) (= Verilog__main.i_rx_phy.rxd_64_1 Verilog__main.rxd_64_1) (= Verilog__main.i_rx_phy.rxdp_64_1 Verilog__main.rxdp_64_1) (= Verilog__main.i_rx_phy.rxdn_64_1 Verilog__main.rxdn_64_1) (= Verilog__main.i_rx_phy.DataIn_o_64_1 Verilog__main.DataIn_o_64_1) (= Verilog__main.i_rx_phy.RxValid_o_64_1 Verilog__main.RxValid_o_64_1) (= Verilog__main.i_rx_phy.RxActive_o_64_1 Verilog__main.RxActive_o_64_1) (= Verilog__main.i_rx_phy.RxError_o_64_1 Verilog__main.RxError_o_64_1) (= Verilog__main.i_rx_phy.RxEn_i_64_1 Verilog__main.txoe_64_1) (= Verilog__main.i_rx_phy.LineState_64_1 Verilog__main.LineState_o_64_1)) (and (= Verilog__main.reset_64_2 (and Verilog__main.rst_64_2 (not Verilog__main.usb_rst_64_2))) (and (= Verilog__main.i_tx_phy.hold_64_2 Verilog__main.i_tx_phy.stuff_64_2) (= Verilog__main.i_tx_phy.sft_done_e_64_2 (and Verilog__main.i_tx_phy.sft_done_64_2 (not Verilog__main.i_tx_phy.sft_done_r_64_2))) (= Verilog__main.i_tx_phy.stuff_64_2 (= Verilog__main.i_tx_phy.one_cnt_64_2 (_ bv6 3))) (= Verilog__main.i_tx_phy.eop_done_64_2 Verilog__main.i_tx_phy.append_eop_sync3_64_2)) (= Verilog__main.i_tx_phy.clk_64_2 Verilog__main.clk_64_2) (= Verilog__main.i_tx_phy.rst_64_2 Verilog__main.reset_64_2) (= Verilog__main.i_tx_phy.fs_ce_64_2 Verilog__main.fs_ce_64_2) (= Verilog__main.i_tx_phy.phy_mode_64_2 Verilog__main.phy_tx_mode_64_2) (= Verilog__main.i_tx_phy.txdp_64_2 Verilog__main.txdp_64_2) (= Verilog__main.i_tx_phy.txdn_64_2 Verilog__main.txdn_64_2) (= Verilog__main.i_tx_phy.txoe_64_2 Verilog__main.txoe_64_2) (= Verilog__main.i_tx_phy.DataOut_i_64_2 Verilog__main.DataOut_i_64_2) (= Verilog__main.i_tx_phy.TxValid_i_64_2 Verilog__main.TxValid_i_64_2) (= Verilog__main.i_tx_phy.TxReady_o_64_2 Verilog__main.TxReady_o_64_2) (and (= Verilog__main.i_rx_phy.RxActive_o_64_2 Verilog__main.i_rx_phy.rx_active_64_2) (= Verilog__main.i_rx_phy.RxValid_o_64_2 Verilog__main.i_rx_phy.rx_valid_64_2) (= Verilog__main.i_rx_phy.RxError_o_64_2 false) (= Verilog__main.i_rx_phy.DataIn_o_64_2 Verilog__main.i_rx_phy.hold_reg_64_2) (= Verilog__main.i_rx_phy.LineState_64_2 (concat (ite Verilog__main.i_rx_phy.rxdp_s1_64_2 (_ bv1 1) (_ bv0 1)) (ite Verilog__main.i_rx_phy.rxdn_s1_64_2 (_ bv1 1) (_ bv0 1)))) (= Verilog__main.i_rx_phy.k_64_2 (and (not Verilog__main.i_rx_phy.rxdp_s_64_2) Verilog__main.i_rx_phy.rxdn_s_64_2)) (= Verilog__main.i_rx_phy.j_64_2 (and Verilog__main.i_rx_phy.rxdp_s_64_2 (not Verilog__main.i_rx_phy.rxdn_s_64_2))) (= Verilog__main.i_rx_phy.se0_64_2 (and (not Verilog__main.i_rx_phy.rxdp_s_64_2) (not Verilog__main.i_rx_phy.rxdn_s_64_2))) (= Verilog__main.i_rx_phy.lock_en_64_2 Verilog__main.i_rx_phy.rx_en_64_2) (= Verilog__main.i_rx_phy.change_64_2 (or (xor Verilog__main.i_rx_phy.rxdp_s1r_64_2 Verilog__main.i_rx_phy.rxdp_s1_64_2) (xor Verilog__main.i_rx_phy.rxdn_s1r_64_2 Verilog__main.i_rx_phy.rxdn_s1_64_2))) (= Verilog__main.i_rx_phy.drop_bit_64_2 (= Verilog__main.i_rx_phy.one_cnt_64_2 (_ bv6 3)))) (= Verilog__main.i_rx_phy.clk_64_2 Verilog__main.clk_64_2) (= Verilog__main.i_rx_phy.rst_64_2 Verilog__main.reset_64_2) (= Verilog__main.i_rx_phy.fs_ce_64_2 Verilog__main.fs_ce_64_2) (= Verilog__main.i_rx_phy.rxd_64_2 Verilog__main.rxd_64_2) (= Verilog__main.i_rx_phy.rxdp_64_2 Verilog__main.rxdp_64_2) (= Verilog__main.i_rx_phy.rxdn_64_2 Verilog__main.rxdn_64_2) (= Verilog__main.i_rx_phy.DataIn_o_64_2 Verilog__main.DataIn_o_64_2) (= Verilog__main.i_rx_phy.RxValid_o_64_2 Verilog__main.RxValid_o_64_2) (= Verilog__main.i_rx_phy.RxActive_o_64_2 Verilog__main.RxActive_o_64_2) (= Verilog__main.i_rx_phy.RxError_o_64_2 Verilog__main.RxError_o_64_2) (= Verilog__main.i_rx_phy.RxEn_i_64_2 Verilog__main.txoe_64_2) (= Verilog__main.i_rx_phy.LineState_64_2 Verilog__main.LineState_o_64_2)) (and (and (= Verilog__main.i_tx_phy.sd_bs_o_64_0 false) (= Verilog__main.i_tx_phy.sd_nrzi_o_64_0 true) (= Verilog__main.i_tx_phy.append_eop_64_0 false) (= Verilog__main.i_tx_phy.append_eop_sync1_64_0 false) (= Verilog__main.i_tx_phy.append_eop_sync2_64_0 false) (= Verilog__main.i_tx_phy.append_eop_sync3_64_0 false) (= Verilog__main.i_tx_phy.txoe_r1_64_0 false) (= Verilog__main.i_tx_phy.txoe_r2_64_0 false) (= Verilog__main.i_tx_phy.txdp_64_0 true) (= Verilog__main.i_tx_phy.txdn_64_0 false) (= Verilog__main.i_tx_phy.txoe_64_0 true) (= Verilog__main.i_tx_phy.TxReady_o_64_0 false) (= Verilog__main.i_tx_phy.state_64_0 (_ bv0 3)) (= Verilog__main.i_tx_phy.tx_ready_64_0 false) (= Verilog__main.i_tx_phy.tx_ready_d_64_0 false) (= Verilog__main.i_tx_phy.ld_sop_d_64_0 false) (= Verilog__main.i_tx_phy.ld_data_d_64_0 false) (= Verilog__main.i_tx_phy.ld_eop_d_64_0 false) (= Verilog__main.i_tx_phy.tx_ip_64_0 false) (= Verilog__main.i_tx_phy.tx_ip_sync_64_0 false) (= Verilog__main.i_tx_phy.bit_cnt_64_0 (_ bv0 3)) (= Verilog__main.i_tx_phy.hold_reg_64_0 (_ bv0 8)) (= Verilog__main.i_tx_phy.sd_raw_o_64_0 false) (= Verilog__main.i_tx_phy.data_done_64_0 false) (= Verilog__main.i_tx_phy.sft_done_64_0 false) (= Verilog__main.i_tx_phy.sft_done_r_64_0 false) (= Verilog__main.i_tx_phy.ld_data_64_0 false) (= Verilog__main.i_tx_phy.one_cnt_64_0 (_ bv0 3))) (and (= Verilog__main.i_rx_phy.fs_ce_64_0 false) (= Verilog__main.i_rx_phy.rxd_t1_64_0 false) (= Verilog__main.i_rx_phy.rxd_s1_64_0 false) (= Verilog__main.i_rx_phy.rxd_s_64_0 false) (= Verilog__main.i_rx_phy.rxdp_t1_64_0 false) (= Verilog__main.i_rx_phy.rxdp_s1_64_0 false) (= Verilog__main.i_rx_phy.rxdp_s_64_0 false) (= Verilog__main.i_rx_phy.rxdn_t1_64_0 false) (= Verilog__main.i_rx_phy.rxdn_s1_64_0 false) (= Verilog__main.i_rx_phy.rxdn_s_64_0 false) (= Verilog__main.i_rx_phy.synced_d_64_0 false) (= Verilog__main.i_rx_phy.rx_en_64_0 false) (= Verilog__main.i_rx_phy.rx_active_64_0 false) (= Verilog__main.i_rx_phy.bit_cnt_64_0 (_ bv0 3)) (= Verilog__main.i_rx_phy.rx_valid1_64_0 false) (= Verilog__main.i_rx_phy.rx_valid_64_0 false) (= Verilog__main.i_rx_phy.shift_en_64_0 false) (= Verilog__main.i_rx_phy.sd_r_64_0 false) (= Verilog__main.i_rx_phy.sd_nrzi_64_0 false) (= Verilog__main.i_rx_phy.hold_reg_64_0 (_ bv0 8)) (= Verilog__main.i_rx_phy.one_cnt_64_0 (_ bv0 3)) (= Verilog__main.i_rx_phy.dpll_state_64_0 (_ bv1 2)) (= Verilog__main.i_rx_phy.fs_ce_d_64_0 false) (= Verilog__main.i_rx_phy.rxdp_s1r_64_0 false) (= Verilog__main.i_rx_phy.rxdn_s1r_64_0 false) (= Verilog__main.i_rx_phy.fs_ce_r1_64_0 false) (= Verilog__main.i_rx_phy.fs_ce_r2_64_0 false) (= Verilog__main.i_rx_phy.fs_ce_r3_64_0 false) (= Verilog__main.i_rx_phy.fs_state_64_0 (_ bv0 3)) (= Verilog__main.i_rx_phy.rx_valid_r_64_0 false)) (= Verilog__main.usb_rst_64_0 false) (= Verilog__main.rst_cnt_64_0 (_ bv0 5))) (and (and (= Verilog__main.i_tx_phy.sd_bs_o_64_1 (ite (not Verilog__main.i_tx_phy.rst_64_0) false (ite Verilog__main.i_tx_phy.fs_ce_64_0 (ite (not Verilog__main.i_tx_phy.tx_ip_sync_64_0) false (ite Verilog__main.i_tx_phy.stuff_64_0 false (= ((_ extract 0 0) (ite Verilog__main.i_tx_phy.sd_raw_o_64_0 (_ bv1 1) (_ bv0 1))) (_ bv1 1)))) Verilog__main.i_tx_phy.sd_bs_o_64_0))) (= Verilog__main.i_tx_phy.sd_nrzi_o_64_1 (ite (not Verilog__main.i_tx_phy.rst_64_0) true (ite (or (not Verilog__main.i_tx_phy.tx_ip_sync_64_0) (not Verilog__main.i_tx_phy.txoe_r1_64_0)) true (ite Verilog__main.i_tx_phy.fs_ce_64_0 (ite Verilog__main.i_tx_phy.sd_bs_o_64_0 Verilog__main.i_tx_phy.sd_nrzi_o_64_0 (not Verilog__main.i_tx_phy.sd_nrzi_o_64_0)) Verilog__main.i_tx_phy.sd_nrzi_o_64_0)))) (= Verilog__main.i_tx_phy.append_eop_64_1 (ite (not Verilog__main.i_tx_phy.rst_64_0) false (ite Verilog__main.i_tx_phy.ld_eop_d_64_0 true (ite Verilog__main.i_tx_phy.append_eop_sync2_64_0 false Verilog__main.i_tx_phy.append_eop_64_0)))) (= Verilog__main.i_tx_phy.append_eop_sync1_64_1 (ite (not Verilog__main.i_tx_phy.rst_64_0) false (ite Verilog__main.i_tx_phy.fs_ce_64_0 Verilog__main.i_tx_phy.append_eop_64_0 Verilog__main.i_tx_phy.append_eop_sync1_64_0))) (= Verilog__main.i_tx_phy.append_eop_sync2_64_1 (ite (not Verilog__main.i_tx_phy.rst_64_0) false (ite Verilog__main.i_tx_phy.fs_ce_64_0 Verilog__main.i_tx_phy.append_eop_sync1_64_0 Verilog__main.i_tx_phy.append_eop_sync2_64_0))) (= Verilog__main.i_tx_phy.append_eop_sync3_64_1 (ite (not Verilog__main.i_tx_phy.rst_64_0) false (ite Verilog__main.i_tx_phy.fs_ce_64_0 Verilog__main.i_tx_phy.append_eop_sync2_64_0 Verilog__main.i_tx_phy.append_eop_sync3_64_0))) (= Verilog__main.i_tx_phy.txoe_r1_64_1 (ite (not Verilog__main.i_tx_phy.rst_64_0) false (ite Verilog__main.i_tx_phy.fs_ce_64_0 Verilog__main.i_tx_phy.tx_ip_sync_64_0 Verilog__main.i_tx_phy.txoe_r1_64_0))) (= Verilog__main.i_tx_phy.txoe_r2_64_1 (ite (not Verilog__main.i_tx_phy.rst_64_0) false (ite Verilog__main.i_tx_phy.fs_ce_64_0 Verilog__main.i_tx_phy.txoe_r1_64_0 Verilog__main.i_tx_phy.txoe_r2_64_0))) (= Verilog__main.i_tx_phy.txdp_64_1 (ite (not Verilog__main.i_tx_phy.rst_64_0) true (ite Verilog__main.i_tx_phy.fs_ce_64_0 (ite Verilog__main.i_tx_phy.phy_mode_64_0 (and (not Verilog__main.i_tx_phy.append_eop_sync3_64_0) Verilog__main.i_tx_phy.sd_nrzi_o_64_0) Verilog__main.i_tx_phy.sd_nrzi_o_64_0) Verilog__main.i_tx_phy.txdp_64_0))) (= Verilog__main.i_tx_phy.txdn_64_1 (ite (not Verilog__main.i_tx_phy.rst_64_0) false (ite Verilog__main.i_tx_phy.fs_ce_64_0 (ite Verilog__main.i_tx_phy.phy_mode_64_0 (and (not Verilog__main.i_tx_phy.append_eop_sync3_64_0) (not Verilog__main.i_tx_phy.sd_nrzi_o_64_0)) Verilog__main.i_tx_phy.append_eop_sync3_64_0) Verilog__main.i_tx_phy.txdn_64_0))) (= Verilog__main.i_tx_phy.txoe_64_1 (ite (not Verilog__main.i_tx_phy.rst_64_0) true (ite Verilog__main.i_tx_phy.fs_ce_64_0 (not (or Verilog__main.i_tx_phy.txoe_r1_64_0 Verilog__main.i_tx_phy.txoe_r2_64_0)) Verilog__main.i_tx_phy.txoe_64_0))) (= Verilog__main.i_tx_phy.TxReady_o_64_1 (ite (not Verilog__main.i_tx_phy.rst_64_0) false (and Verilog__main.i_tx_phy.tx_ready_d_64_0 Verilog__main.i_tx_phy.TxValid_i_64_0))) (= Verilog__main.i_tx_phy.state_64_1 (ite (not Verilog__main.i_tx_phy.rst_64_0) (_ bv0 3) (ite (= Verilog__main.i_tx_phy.state_64_0 (_ bv0 3)) (ite Verilog__main.i_tx_phy.TxValid_i_64_0 (_ bv1 3) Verilog__main.i_tx_phy.state_64_0) (ite (= Verilog__main.i_tx_phy.state_64_0 (_ bv1 3)) (ite Verilog__main.i_tx_phy.sft_done_e_64_0 (_ bv3 3) Verilog__main.i_tx_phy.state_64_0) (ite (= Verilog__main.i_tx_phy.state_64_0 (_ bv3 3)) (ite (and (not Verilog__main.i_tx_phy.data_done_64_0) Verilog__main.i_tx_phy.sft_done_e_64_0) (_ bv4 3) Verilog__main.i_tx_phy.state_64_0) (ite (= Verilog__main.i_tx_phy.state_64_0 (_ bv4 3)) (ite Verilog__main.i_tx_phy.eop_done_64_0 (_ bv5 3) Verilog__main.i_tx_phy.state_64_0) (ite (= Verilog__main.i_tx_phy.state_64_0 (_ bv5 3)) (ite (and (not Verilog__main.i_tx_phy.eop_done_64_0) Verilog__main.i_tx_phy.fs_ce_64_0) (_ bv6 3) Verilog__main.i_tx_phy.state_64_0) (ite (= Verilog__main.i_tx_phy.state_64_0 (_ bv6 3)) (ite Verilog__main.i_tx_phy.fs_ce_64_0 (_ bv0 3) Verilog__main.i_tx_phy.state_64_0) Verilog__main.i_tx_phy.state_64_0)))))))) (= Verilog__main.i_tx_phy.tx_ready_64_1 Verilog__main.i_tx_phy.tx_ready_d_64_0) (= Verilog__main.i_tx_phy.tx_ready_d_64_1 (ite (not Verilog__main.i_tx_phy.rst_64_0) Verilog__main.i_tx_phy.tx_ready_d_64_0 (ite (= Verilog__main.i_tx_phy.state_64_0 (_ bv0 3)) false (ite (= Verilog__main.i_tx_phy.state_64_0 (_ bv1 3)) (ite Verilog__main.i_tx_phy.sft_done_e_64_0 true false) (ite (= Verilog__main.i_tx_phy.state_64_0 (_ bv3 3)) (ite (and Verilog__main.i_tx_phy.data_done_64_0 Verilog__main.i_tx_phy.sft_done_e_64_0) true false) false))))) (= Verilog__main.i_tx_phy.ld_sop_d_64_1 (ite (not Verilog__main.i_tx_phy.rst_64_0) Verilog__main.i_tx_phy.ld_sop_d_64_0 (ite (= Verilog__main.i_tx_phy.state_64_0 (_ bv0 3)) (ite Verilog__main.i_tx_phy.TxValid_i_64_0 true false) false))) (= Verilog__main.i_tx_phy.ld_data_d_64_1 (ite (not Verilog__main.i_tx_phy.rst_64_0) Verilog__main.i_tx_phy.ld_data_d_64_0 (ite (= Verilog__main.i_tx_phy.state_64_0 (_ bv0 3)) false (ite (= Verilog__main.i_tx_phy.state_64_0 (_ bv1 3)) (ite Verilog__main.i_tx_phy.sft_done_e_64_0 true false) (ite (= Verilog__main.i_tx_phy.state_64_0 (_ bv3 3)) (ite (and Verilog__main.i_tx_phy.data_done_64_0 Verilog__main.i_tx_phy.sft_done_e_64_0) true false) false))))) (= Verilog__main.i_tx_phy.ld_eop_d_64_1 (ite (not Verilog__main.i_tx_phy.rst_64_0) Verilog__main.i_tx_phy.ld_eop_d_64_0 (ite (= Verilog__main.i_tx_phy.state_64_0 (_ bv0 3)) false (ite (= Verilog__main.i_tx_phy.state_64_0 (_ bv1 3)) false (ite (= Verilog__main.i_tx_phy.state_64_0 (_ bv3 3)) (ite (and (not Verilog__main.i_tx_phy.data_done_64_0) Verilog__main.i_tx_phy.sft_done_e_64_0) true false) false))))) (= Verilog__main.i_tx_phy.tx_ip_64_1 (ite (not Verilog__main.i_tx_phy.rst_64_0) false (ite Verilog__main.i_tx_phy.ld_sop_d_64_0 true (ite Verilog__main.i_tx_phy.eop_done_64_0 false Verilog__main.i_tx_phy.tx_ip_64_0)))) (= Verilog__main.i_tx_phy.tx_ip_sync_64_1 (ite (not Verilog__main.i_tx_phy.rst_64_0) false (ite Verilog__main.i_tx_phy.fs_ce_64_0 Verilog__main.i_tx_phy.tx_ip_64_0 Verilog__main.i_tx_phy.tx_ip_sync_64_0))) (= Verilog__main.i_tx_phy.bit_cnt_64_1 (ite (not Verilog__main.i_tx_phy.rst_64_0) (_ bv0 3) (ite (not Verilog__main.i_tx_phy.tx_ip_sync_64_0) (_ bv0 3) (ite (and Verilog__main.i_tx_phy.fs_ce_64_0 (not Verilog__main.i_tx_phy.hold_64_0)) (bvadd Verilog__main.i_tx_phy.bit_cnt_64_0 (_ bv1 3)) Verilog__main.i_tx_phy.bit_cnt_64_0)))) (= Verilog__main.i_tx_phy.hold_reg_64_1 (ite Verilog__main.i_tx_phy.ld_sop_d_64_0 (_ bv128 8) (ite Verilog__main.i_tx_phy.ld_data_64_0 Verilog__main.i_tx_phy.DataOut_i_64_0 Verilog__main.i_tx_phy.hold_reg_64_0))) (= Verilog__main.i_tx_phy.sd_raw_o_64_1 (ite (not Verilog__main.i_tx_phy.tx_ip_sync_64_0) false (ite (= Verilog__main.i_tx_phy.bit_cnt_64_0 (_ bv0 3)) (= ((_ extract 0 0) Verilog__main.i_tx_phy.hold_reg_64_0) (_ bv1 1)) (ite (= Verilog__main.i_tx_phy.bit_cnt_64_0 (_ bv1 3)) (= ((_ extract 1 1) Verilog__main.i_tx_phy.hold_reg_64_0) (_ bv1 1)) (ite (= Verilog__main.i_tx_phy.bit_cnt_64_0 (_ bv2 3)) (= ((_ extract 2 2) Verilog__main.i_tx_phy.hold_reg_64_0) (_ bv1 1)) (ite (= Verilog__main.i_tx_phy.bit_cnt_64_0 (_ bv3 3)) (= ((_ extract 3 3) Verilog__main.i_tx_phy.hold_reg_64_0) (_ bv1 1)) (ite (= Verilog__main.i_tx_phy.bit_cnt_64_0 (_ bv4 3)) (= ((_ extract 4 4) Verilog__main.i_tx_phy.hold_reg_64_0) (_ bv1 1)) (ite (= Verilog__main.i_tx_phy.bit_cnt_64_0 (_ bv5 3)) (= ((_ extract 5 5) Verilog__main.i_tx_phy.hold_reg_64_0) (_ bv1 1)) (ite (= Verilog__main.i_tx_phy.bit_cnt_64_0 (_ bv6 3)) (= ((_ extract 6 6) Verilog__main.i_tx_phy.hold_reg_64_0) (_ bv1 1)) (ite (= Verilog__main.i_tx_phy.bit_cnt_64_0 (_ bv7 3)) (= ((_ extract 7 7) Verilog__main.i_tx_phy.hold_reg_64_0) (_ bv1 1)) Verilog__main.i_tx_phy.sd_raw_o_64_0)))))))))) (= Verilog__main.i_tx_phy.data_done_64_1 (ite (not Verilog__main.i_tx_phy.rst_64_0) false (ite (and Verilog__main.i_tx_phy.TxValid_i_64_0 (not Verilog__main.i_tx_phy.tx_ip_64_0)) true (ite (not Verilog__main.i_tx_phy.TxValid_i_64_0) false Verilog__main.i_tx_phy.data_done_64_0)))) (= Verilog__main.i_tx_phy.sft_done_64_1 (and (not Verilog__main.i_tx_phy.hold_64_0) (= Verilog__main.i_tx_phy.bit_cnt_64_0 (_ bv7 3)))) (= Verilog__main.i_tx_phy.sft_done_r_64_1 Verilog__main.i_tx_phy.sft_done_64_0) (= Verilog__main.i_tx_phy.ld_data_64_1 Verilog__main.i_tx_phy.ld_data_d_64_0) (= Verilog__main.i_tx_phy.one_cnt_64_1 (ite (not Verilog__main.i_tx_phy.rst_64_0) (_ bv0 3) (ite (not Verilog__main.i_tx_phy.tx_ip_sync_64_0) (_ bv0 3) (ite Verilog__main.i_tx_phy.fs_ce_64_0 (ite (or (not Verilog__main.i_tx_phy.sd_raw_o_64_0) Verilog__main.i_tx_phy.stuff_64_0) (_ bv0 3) (bvadd Verilog__main.i_tx_phy.one_cnt_64_0 (_ bv1 3))) Verilog__main.i_tx_phy.one_cnt_64_0))))) (and (= Verilog__main.i_rx_phy.fs_ce_64_1 Verilog__main.i_rx_phy.fs_ce_r3_64_0) (= Verilog__main.i_rx_phy.rxd_t1_64_1 Verilog__main.i_rx_phy.rxd_64_0) (= Verilog__main.i_rx_phy.rxd_s1_64_1 Verilog__main.i_rx_phy.rxd_t1_64_0) (= Verilog__main.i_rx_phy.rxd_s_64_1 Verilog__main.i_rx_phy.rxd_s1_64_0) (= Verilog__main.i_rx_phy.rxdp_t1_64_1 Verilog__main.i_rx_phy.rxdp_64_0) (= Verilog__main.i_rx_phy.rxdp_s1_64_1 Verilog__main.i_rx_phy.rxdp_t1_64_0) (= Verilog__main.i_rx_phy.rxdp_s_64_1 Verilog__main.i_rx_phy.rxdp_s1_64_0) (= Verilog__main.i_rx_phy.rxdn_t1_64_1 Verilog__main.i_rx_phy.rxdn_64_0) (= Verilog__main.i_rx_phy.rxdn_s1_64_1 Verilog__main.i_rx_phy.rxdn_t1_64_0) (= Verilog__main.i_rx_phy.rxdn_s_64_1 Verilog__main.i_rx_phy.rxdn_s1_64_0) (= Verilog__main.i_rx_phy.synced_d_64_1 (ite (not Verilog__main.i_rx_phy.rst_64_0) Verilog__main.i_rx_phy.synced_d_64_0 (ite Verilog__main.i_rx_phy.fs_ce_64_0 (ite (= Verilog__main.i_rx_phy.fs_state_64_0 (_ bv0 3)) false (ite (= Verilog__main.i_rx_phy.fs_state_64_0 (_ bv1 3)) false (ite (= Verilog__main.i_rx_phy.fs_state_64_0 (_ bv2 3)) false (ite (= Verilog__main.i_rx_phy.fs_state_64_0 (_ bv3 3)) false (ite (= Verilog__main.i_rx_phy.fs_state_64_0 (_ bv4 3)) false (ite (= Verilog__main.i_rx_phy.fs_state_64_0 (_ bv5 3)) false (ite (= Verilog__main.i_rx_phy.fs_state_64_0 (_ bv6 3)) false (ite (= Verilog__main.i_rx_phy.fs_state_64_0 (_ bv7 3)) (ite Verilog__main.i_rx_phy.k_64_0 true false) false)))))))) false))) (= Verilog__main.i_rx_phy.rx_en_64_1 Verilog__main.i_rx_phy.RxEn_i_64_0) (= Verilog__main.i_rx_phy.rx_active_64_1 (ite (not Verilog__main.i_rx_phy.rst_64_0) false (ite (and Verilog__main.i_rx_phy.synced_d_64_0 Verilog__main.i_rx_phy.rx_en_64_0) true (ite (and Verilog__main.i_rx_phy.se0_64_0 Verilog__main.i_rx_phy.rx_valid_r_64_0) false Verilog__main.i_rx_phy.rx_active_64_0)))) (= Verilog__main.i_rx_phy.bit_cnt_64_1 (ite (not Verilog__main.i_rx_phy.rst_64_0) (_ bv0 3) (ite (not Verilog__main.i_rx_phy.shift_en_64_0) (_ bv0 3) (ite (and Verilog__main.i_rx_phy.fs_ce_64_0 (not Verilog__main.i_rx_phy.drop_bit_64_0)) (bvadd Verilog__main.i_rx_phy.bit_cnt_64_0 (_ bv1 3)) Verilog__main.i_rx_phy.bit_cnt_64_0)))) (= Verilog__main.i_rx_phy.rx_valid1_64_1 (ite (not Verilog__main.i_rx_phy.rst_64_0) false (ite (and (and Verilog__main.i_rx_phy.fs_ce_64_0 (not Verilog__main.i_rx_phy.drop_bit_64_0)) (= Verilog__main.i_rx_phy.bit_cnt_64_0 (_ bv7 3))) true (ite (and (and Verilog__main.i_rx_phy.rx_valid1_64_0 Verilog__main.i_rx_phy.fs_ce_64_0) (not Verilog__main.i_rx_phy.drop_bit_64_0)) false Verilog__main.i_rx_phy.rx_valid1_64_0)))) (= Verilog__main.i_rx_phy.rx_valid_64_1 (and (and (not Verilog__main.i_rx_phy.drop_bit_64_0) Verilog__main.i_rx_phy.rx_valid1_64_0) Verilog__main.i_rx_phy.fs_ce_64_0)) (= Verilog__main.i_rx_phy.shift_en_64_1 (ite Verilog__main.i_rx_phy.fs_ce_64_0 (or Verilog__main.i_rx_phy.synced_d_64_0 Verilog__main.i_rx_phy.rx_active_64_0) Verilog__main.i_rx_phy.shift_en_64_0)) (= Verilog__main.i_rx_phy.sd_r_64_1 (ite Verilog__main.i_rx_phy.fs_ce_64_0 Verilog__main.i_rx_phy.rxd_s_64_0 Verilog__main.i_rx_phy.sd_r_64_0)) (= Verilog__main.i_rx_phy.sd_nrzi_64_1 (ite (not Verilog__main.i_rx_phy.rst_64_0) false (ite (and Verilog__main.i_rx_phy.rx_active_64_0 Verilog__main.i_rx_phy.fs_ce_64_0) (not (xor Verilog__main.i_rx_phy.rxd_s_64_0 Verilog__main.i_rx_phy.sd_r_64_0)) Verilog__main.i_rx_phy.sd_nrzi_64_0))) (= Verilog__main.i_rx_phy.hold_reg_64_1 (ite (and (and Verilog__main.i_rx_phy.fs_ce_64_0 Verilog__main.i_rx_phy.shift_en_64_0) (not Verilog__main.i_rx_phy.drop_bit_64_0)) (concat (ite Verilog__main.i_rx_phy.sd_nrzi_64_0 (_ bv1 1) (_ bv0 1)) ((_ extract 7 1) Verilog__main.i_rx_phy.hold_reg_64_0)) Verilog__main.i_rx_phy.hold_reg_64_0)) (= Verilog__main.i_rx_phy.one_cnt_64_1 (ite (not Verilog__main.i_rx_phy.rst_64_0) (_ bv0 3) (ite (not Verilog__main.i_rx_phy.shift_en_64_0) (_ bv0 3) (ite Verilog__main.i_rx_phy.fs_ce_64_0 (ite (or (not Verilog__main.i_rx_phy.sd_nrzi_64_0) Verilog__main.i_rx_phy.drop_bit_64_0) (_ bv0 3) (bvadd Verilog__main.i_rx_phy.one_cnt_64_0 (_ bv1 3))) Verilog__main.i_rx_phy.one_cnt_64_0)))) (= Verilog__main.i_rx_phy.dpll_state_64_1 (ite (not Verilog__main.i_rx_phy.rst_64_0) (_ bv1 2) (ite (= Verilog__main.i_rx_phy.dpll_state_64_0 (_ bv0 2)) (ite (and Verilog__main.i_rx_phy.lock_en_64_0 Verilog__main.i_rx_phy.change_64_0) (_ bv0 2) (_ bv1 2)) (ite (= Verilog__main.i_rx_phy.dpll_state_64_0 (_ bv1 2)) (ite (and Verilog__main.i_rx_phy.lock_en_64_0 Verilog__main.i_rx_phy.change_64_0) (_ bv3 2) (_ bv2 2)) (ite (= Verilog__main.i_rx_phy.dpll_state_64_0 (_ bv2 2)) (ite (and Verilog__main.i_rx_phy.lock_en_64_0 Verilog__main.i_rx_phy.change_64_0) (_ bv0 2) (_ bv3 2)) (ite (= Verilog__main.i_rx_phy.dpll_state_64_0 (_ bv3 2)) (ite (and Verilog__main.i_rx_phy.lock_en_64_0 Verilog__main.i_rx_phy.change_64_0) (_ bv0 2) (_ bv0 2)) Verilog__main.i_rx_phy.dpll_state_64_0)))))) (= Verilog__main.i_rx_phy.fs_ce_d_64_1 (ite (not Verilog__main.i_rx_phy.rst_64_0) Verilog__main.i_rx_phy.fs_ce_d_64_0 (ite (= Verilog__main.i_rx_phy.dpll_state_64_0 (_ bv0 2)) false (ite (= Verilog__main.i_rx_phy.dpll_state_64_0 (_ bv1 2)) true false)))) (= Verilog__main.i_rx_phy.rxdp_s1r_64_1 Verilog__main.i_rx_phy.rxdp_s1_64_0) (= Verilog__main.i_rx_phy.rxdn_s1r_64_1 Verilog__main.i_rx_phy.rxdn_s1_64_0) (= Verilog__main.i_rx_phy.fs_ce_r1_64_1 Verilog__main.i_rx_phy.fs_ce_d_64_0) (= Verilog__main.i_rx_phy.fs_ce_r2_64_1 Verilog__main.i_rx_phy.fs_ce_r1_64_0) (= Verilog__main.i_rx_phy.fs_ce_r3_64_1 Verilog__main.i_rx_phy.fs_ce_r2_64_0) (= Verilog__main.i_rx_phy.fs_state_64_1 (ite (not Verilog__main.i_rx_phy.rst_64_0) (_ bv0 3) (ite Verilog__main.i_rx_phy.fs_ce_64_0 (ite (= Verilog__main.i_rx_phy.fs_state_64_0 (_ bv0 3)) (ite (and Verilog__main.i_rx_phy.k_64_0 Verilog__main.i_rx_phy.rx_en_64_0) (_ bv1 3) Verilog__main.i_rx_phy.fs_state_64_0) (ite (= Verilog__main.i_rx_phy.fs_state_64_0 (_ bv1 3)) (ite (and Verilog__main.i_rx_phy.j_64_0 Verilog__main.i_rx_phy.rx_en_64_0) (_ bv2 3) (_ bv0 3)) (ite (= Verilog__main.i_rx_phy.fs_state_64_0 (_ bv2 3)) (ite (and Verilog__main.i_rx_phy.k_64_0 Verilog__main.i_rx_phy.rx_en_64_0) (_ bv3 3) (_ bv0 3)) (ite (= Verilog__main.i_rx_phy.fs_state_64_0 (_ bv3 3)) (ite (and Verilog__main.i_rx_phy.j_64_0 Verilog__main.i_rx_phy.rx_en_64_0) (_ bv4 3) (_ bv0 3)) (ite (= Verilog__main.i_rx_phy.fs_state_64_0 (_ bv4 3)) (ite (and Verilog__main.i_rx_phy.k_64_0 Verilog__main.i_rx_phy.rx_en_64_0) (_ bv5 3) (_ bv0 3)) (ite (= Verilog__main.i_rx_phy.fs_state_64_0 (_ bv5 3)) (ite (and Verilog__main.i_rx_phy.j_64_0 Verilog__main.i_rx_phy.rx_en_64_0) (_ bv6 3) (ite (and Verilog__main.i_rx_phy.k_64_0 Verilog__main.i_rx_phy.rx_en_64_0) (_ bv7 3) (_ bv0 3))) (ite (= Verilog__main.i_rx_phy.fs_state_64_0 (_ bv6 3)) (ite (and Verilog__main.i_rx_phy.k_64_0 Verilog__main.i_rx_phy.rx_en_64_0) (_ bv7 3) (_ bv0 3)) (ite (= Verilog__main.i_rx_phy.fs_state_64_0 (_ bv7 3)) (_ bv0 3) Verilog__main.i_rx_phy.fs_state_64_0)))))))) Verilog__main.i_rx_phy.fs_state_64_0))) (= Verilog__main.i_rx_phy.rx_valid_r_64_1 (ite Verilog__main.i_rx_phy.rx_valid_64_0 true (ite Verilog__main.i_rx_phy.fs_ce_64_0 false Verilog__main.i_rx_phy.rx_valid_r_64_0)))) (= Verilog__main.usb_rst_64_1 (= Verilog__main.rst_cnt_64_0 (_ bv31 5))) (= Verilog__main.rst_cnt_64_1 (ite (not Verilog__main.rst_64_0) (_ bv0 5) (ite (not (= Verilog__main.LineState_o_64_0 (_ bv0 2))) (_ bv0 5) (ite (and (not Verilog__main.usb_rst_64_0) Verilog__main.fs_ce_64_0) (bvadd Verilog__main.rst_cnt_64_0 (_ bv1 5)) Verilog__main.rst_cnt_64_0))))) (and (and (= Verilog__main.i_tx_phy.sd_bs_o_64_2 (ite (not Verilog__main.i_tx_phy.rst_64_1) false (ite Verilog__main.i_tx_phy.fs_ce_64_1 (ite (not Verilog__main.i_tx_phy.tx_ip_sync_64_1) false (ite Verilog__main.i_tx_phy.stuff_64_1 false (= ((_ extract 0 0) (ite Verilog__main.i_tx_phy.sd_raw_o_64_1 (_ bv1 1) (_ bv0 1))) (_ bv1 1)))) Verilog__main.i_tx_phy.sd_bs_o_64_1))) (= Verilog__main.i_tx_phy.sd_nrzi_o_64_2 (ite (not Verilog__main.i_tx_phy.rst_64_1) true (ite (or (not Verilog__main.i_tx_phy.tx_ip_sync_64_1) (not Verilog__main.i_tx_phy.txoe_r1_64_1)) true (ite Verilog__main.i_tx_phy.fs_ce_64_1 (ite Verilog__main.i_tx_phy.sd_bs_o_64_1 Verilog__main.i_tx_phy.sd_nrzi_o_64_1 (not Verilog__main.i_tx_phy.sd_nrzi_o_64_1)) Verilog__main.i_tx_phy.sd_nrzi_o_64_1)))) (= Verilog__main.i_tx_phy.append_eop_64_2 (ite (not Verilog__main.i_tx_phy.rst_64_1) false (ite Verilog__main.i_tx_phy.ld_eop_d_64_1 true (ite Verilog__main.i_tx_phy.append_eop_sync2_64_1 false Verilog__main.i_tx_phy.append_eop_64_1)))) (= Verilog__main.i_tx_phy.append_eop_sync1_64_2 (ite (not Verilog__main.i_tx_phy.rst_64_1) false (ite Verilog__main.i_tx_phy.fs_ce_64_1 Verilog__main.i_tx_phy.append_eop_64_1 Verilog__main.i_tx_phy.append_eop_sync1_64_1))) (= Verilog__main.i_tx_phy.append_eop_sync2_64_2 (ite (not Verilog__main.i_tx_phy.rst_64_1) false (ite Verilog__main.i_tx_phy.fs_ce_64_1 Verilog__main.i_tx_phy.append_eop_sync1_64_1 Verilog__main.i_tx_phy.append_eop_sync2_64_1))) (= Verilog__main.i_tx_phy.append_eop_sync3_64_2 (ite (not Verilog__main.i_tx_phy.rst_64_1) false (ite Verilog__main.i_tx_phy.fs_ce_64_1 Verilog__main.i_tx_phy.append_eop_sync2_64_1 Verilog__main.i_tx_phy.append_eop_sync3_64_1))) (= Verilog__main.i_tx_phy.txoe_r1_64_2 (ite (not Verilog__main.i_tx_phy.rst_64_1) false (ite Verilog__main.i_tx_phy.fs_ce_64_1 Verilog__main.i_tx_phy.tx_ip_sync_64_1 Verilog__main.i_tx_phy.txoe_r1_64_1))) (= Verilog__main.i_tx_phy.txoe_r2_64_2 (ite (not Verilog__main.i_tx_phy.rst_64_1) false (ite Verilog__main.i_tx_phy.fs_ce_64_1 Verilog__main.i_tx_phy.txoe_r1_64_1 Verilog__main.i_tx_phy.txoe_r2_64_1))) (= Verilog__main.i_tx_phy.txdp_64_2 (ite (not Verilog__main.i_tx_phy.rst_64_1) true (ite Verilog__main.i_tx_phy.fs_ce_64_1 (ite Verilog__main.i_tx_phy.phy_mode_64_1 (and (not Verilog__main.i_tx_phy.append_eop_sync3_64_1) Verilog__main.i_tx_phy.sd_nrzi_o_64_1) Verilog__main.i_tx_phy.sd_nrzi_o_64_1) Verilog__main.i_tx_phy.txdp_64_1))) (= Verilog__main.i_tx_phy.txdn_64_2 (ite (not Verilog__main.i_tx_phy.rst_64_1) false (ite Verilog__main.i_tx_phy.fs_ce_64_1 (ite Verilog__main.i_tx_phy.phy_mode_64_1 (and (not Verilog__main.i_tx_phy.append_eop_sync3_64_1) (not Verilog__main.i_tx_phy.sd_nrzi_o_64_1)) Verilog__main.i_tx_phy.append_eop_sync3_64_1) Verilog__main.i_tx_phy.txdn_64_1))) (= Verilog__main.i_tx_phy.txoe_64_2 (ite (not Verilog__main.i_tx_phy.rst_64_1) true (ite Verilog__main.i_tx_phy.fs_ce_64_1 (not (or Verilog__main.i_tx_phy.txoe_r1_64_1 Verilog__main.i_tx_phy.txoe_r2_64_1)) Verilog__main.i_tx_phy.txoe_64_1))) (= Verilog__main.i_tx_phy.TxReady_o_64_2 (ite (not Verilog__main.i_tx_phy.rst_64_1) false (and Verilog__main.i_tx_phy.tx_ready_d_64_1 Verilog__main.i_tx_phy.TxValid_i_64_1))) (= Verilog__main.i_tx_phy.state_64_2 (ite (not Verilog__main.i_tx_phy.rst_64_1) (_ bv0 3) (ite (= Verilog__main.i_tx_phy.state_64_1 (_ bv0 3)) (ite Verilog__main.i_tx_phy.TxValid_i_64_1 (_ bv1 3) Verilog__main.i_tx_phy.state_64_1) (ite (= Verilog__main.i_tx_phy.state_64_1 (_ bv1 3)) (ite Verilog__main.i_tx_phy.sft_done_e_64_1 (_ bv3 3) Verilog__main.i_tx_phy.state_64_1) (ite (= Verilog__main.i_tx_phy.state_64_1 (_ bv3 3)) (ite (and (not Verilog__main.i_tx_phy.data_done_64_1) Verilog__main.i_tx_phy.sft_done_e_64_1) (_ bv4 3) Verilog__main.i_tx_phy.state_64_1) (ite (= Verilog__main.i_tx_phy.state_64_1 (_ bv4 3)) (ite Verilog__main.i_tx_phy.eop_done_64_1 (_ bv5 3) Verilog__main.i_tx_phy.state_64_1) (ite (= Verilog__main.i_tx_phy.state_64_1 (_ bv5 3)) (ite (and (not Verilog__main.i_tx_phy.eop_done_64_1) Verilog__main.i_tx_phy.fs_ce_64_1) (_ bv6 3) Verilog__main.i_tx_phy.state_64_1) (ite (= Verilog__main.i_tx_phy.state_64_1 (_ bv6 3)) (ite Verilog__main.i_tx_phy.fs_ce_64_1 (_ bv0 3) Verilog__main.i_tx_phy.state_64_1) Verilog__main.i_tx_phy.state_64_1)))))))) (= Verilog__main.i_tx_phy.tx_ready_64_2 Verilog__main.i_tx_phy.tx_ready_d_64_1) (= Verilog__main.i_tx_phy.tx_ready_d_64_2 (ite (not Verilog__main.i_tx_phy.rst_64_1) Verilog__main.i_tx_phy.tx_ready_d_64_1 (ite (= Verilog__main.i_tx_phy.state_64_1 (_ bv0 3)) false (ite (= Verilog__main.i_tx_phy.state_64_1 (_ bv1 3)) (ite Verilog__main.i_tx_phy.sft_done_e_64_1 true false) (ite (= Verilog__main.i_tx_phy.state_64_1 (_ bv3 3)) (ite (and Verilog__main.i_tx_phy.data_done_64_1 Verilog__main.i_tx_phy.sft_done_e_64_1) true false) false))))) (= Verilog__main.i_tx_phy.ld_sop_d_64_2 (ite (not Verilog__main.i_tx_phy.rst_64_1) Verilog__main.i_tx_phy.ld_sop_d_64_1 (ite (= Verilog__main.i_tx_phy.state_64_1 (_ bv0 3)) (ite Verilog__main.i_tx_phy.TxValid_i_64_1 true false) false))) (= Verilog__main.i_tx_phy.ld_data_d_64_2 (ite (not Verilog__main.i_tx_phy.rst_64_1) Verilog__main.i_tx_phy.ld_data_d_64_1 (ite (= Verilog__main.i_tx_phy.state_64_1 (_ bv0 3)) false (ite (= Verilog__main.i_tx_phy.state_64_1 (_ bv1 3)) (ite Verilog__main.i_tx_phy.sft_done_e_64_1 true false) (ite (= Verilog__main.i_tx_phy.state_64_1 (_ bv3 3)) (ite (and Verilog__main.i_tx_phy.data_done_64_1 Verilog__main.i_tx_phy.sft_done_e_64_1) true false) false))))) (= Verilog__main.i_tx_phy.ld_eop_d_64_2 (ite (not Verilog__main.i_tx_phy.rst_64_1) Verilog__main.i_tx_phy.ld_eop_d_64_1 (ite (= Verilog__main.i_tx_phy.state_64_1 (_ bv0 3)) false (ite (= Verilog__main.i_tx_phy.state_64_1 (_ bv1 3)) false (ite (= Verilog__main.i_tx_phy.state_64_1 (_ bv3 3)) (ite (and (not Verilog__main.i_tx_phy.data_done_64_1) Verilog__main.i_tx_phy.sft_done_e_64_1) true false) false))))) (= Verilog__main.i_tx_phy.tx_ip_64_2 (ite (not Verilog__main.i_tx_phy.rst_64_1) false (ite Verilog__main.i_tx_phy.ld_sop_d_64_1 true (ite Verilog__main.i_tx_phy.eop_done_64_1 false Verilog__main.i_tx_phy.tx_ip_64_1)))) (= Verilog__main.i_tx_phy.tx_ip_sync_64_2 (ite (not Verilog__main.i_tx_phy.rst_64_1) false (ite Verilog__main.i_tx_phy.fs_ce_64_1 Verilog__main.i_tx_phy.tx_ip_64_1 Verilog__main.i_tx_phy.tx_ip_sync_64_1))) (= Verilog__main.i_tx_phy.bit_cnt_64_2 (ite (not Verilog__main.i_tx_phy.rst_64_1) (_ bv0 3) (ite (not Verilog__main.i_tx_phy.tx_ip_sync_64_1) (_ bv0 3) (ite (and Verilog__main.i_tx_phy.fs_ce_64_1 (not Verilog__main.i_tx_phy.hold_64_1)) (bvadd Verilog__main.i_tx_phy.bit_cnt_64_1 (_ bv1 3)) Verilog__main.i_tx_phy.bit_cnt_64_1)))) (= Verilog__main.i_tx_phy.hold_reg_64_2 (ite Verilog__main.i_tx_phy.ld_sop_d_64_1 (_ bv128 8) (ite Verilog__main.i_tx_phy.ld_data_64_1 Verilog__main.i_tx_phy.DataOut_i_64_1 Verilog__main.i_tx_phy.hold_reg_64_1))) (= Verilog__main.i_tx_phy.sd_raw_o_64_2 (ite (not Verilog__main.i_tx_phy.tx_ip_sync_64_1) false (ite (= Verilog__main.i_tx_phy.bit_cnt_64_1 (_ bv0 3)) (= ((_ extract 0 0) Verilog__main.i_tx_phy.hold_reg_64_1) (_ bv1 1)) (ite (= Verilog__main.i_tx_phy.bit_cnt_64_1 (_ bv1 3)) (= ((_ extract 1 1) Verilog__main.i_tx_phy.hold_reg_64_1) (_ bv1 1)) (ite (= Verilog__main.i_tx_phy.bit_cnt_64_1 (_ bv2 3)) (= ((_ extract 2 2) Verilog__main.i_tx_phy.hold_reg_64_1) (_ bv1 1)) (ite (= Verilog__main.i_tx_phy.bit_cnt_64_1 (_ bv3 3)) (= ((_ extract 3 3) Verilog__main.i_tx_phy.hold_reg_64_1) (_ bv1 1)) (ite (= Verilog__main.i_tx_phy.bit_cnt_64_1 (_ bv4 3)) (= ((_ extract 4 4) Verilog__main.i_tx_phy.hold_reg_64_1) (_ bv1 1)) (ite (= Verilog__main.i_tx_phy.bit_cnt_64_1 (_ bv5 3)) (= ((_ extract 5 5) Verilog__main.i_tx_phy.hold_reg_64_1) (_ bv1 1)) (ite (= Verilog__main.i_tx_phy.bit_cnt_64_1 (_ bv6 3)) (= ((_ extract 6 6) Verilog__main.i_tx_phy.hold_reg_64_1) (_ bv1 1)) (ite (= Verilog__main.i_tx_phy.bit_cnt_64_1 (_ bv7 3)) (= ((_ extract 7 7) Verilog__main.i_tx_phy.hold_reg_64_1) (_ bv1 1)) Verilog__main.i_tx_phy.sd_raw_o_64_1)))))))))) (= Verilog__main.i_tx_phy.data_done_64_2 (ite (not Verilog__main.i_tx_phy.rst_64_1) false (ite (and Verilog__main.i_tx_phy.TxValid_i_64_1 (not Verilog__main.i_tx_phy.tx_ip_64_1)) true (ite (not Verilog__main.i_tx_phy.TxValid_i_64_1) false Verilog__main.i_tx_phy.data_done_64_1)))) (= Verilog__main.i_tx_phy.sft_done_64_2 (and (not Verilog__main.i_tx_phy.hold_64_1) (= Verilog__main.i_tx_phy.bit_cnt_64_1 (_ bv7 3)))) (= Verilog__main.i_tx_phy.sft_done_r_64_2 Verilog__main.i_tx_phy.sft_done_64_1) (= Verilog__main.i_tx_phy.ld_data_64_2 Verilog__main.i_tx_phy.ld_data_d_64_1) (= Verilog__main.i_tx_phy.one_cnt_64_2 (ite (not Verilog__main.i_tx_phy.rst_64_1) (_ bv0 3) (ite (not Verilog__main.i_tx_phy.tx_ip_sync_64_1) (_ bv0 3) (ite Verilog__main.i_tx_phy.fs_ce_64_1 (ite (or (not Verilog__main.i_tx_phy.sd_raw_o_64_1) Verilog__main.i_tx_phy.stuff_64_1) (_ bv0 3) (bvadd Verilog__main.i_tx_phy.one_cnt_64_1 (_ bv1 3))) Verilog__main.i_tx_phy.one_cnt_64_1))))) (and (= Verilog__main.i_rx_phy.fs_ce_64_2 Verilog__main.i_rx_phy.fs_ce_r3_64_1) (= Verilog__main.i_rx_phy.rxd_t1_64_2 Verilog__main.i_rx_phy.rxd_64_1) (= Verilog__main.i_rx_phy.rxd_s1_64_2 Verilog__main.i_rx_phy.rxd_t1_64_1) (= Verilog__main.i_rx_phy.rxd_s_64_2 Verilog__main.i_rx_phy.rxd_s1_64_1) (= Verilog__main.i_rx_phy.rxdp_t1_64_2 Verilog__main.i_rx_phy.rxdp_64_1) (= Verilog__main.i_rx_phy.rxdp_s1_64_2 Verilog__main.i_rx_phy.rxdp_t1_64_1) (= Verilog__main.i_rx_phy.rxdp_s_64_2 Verilog__main.i_rx_phy.rxdp_s1_64_1) (= Verilog__main.i_rx_phy.rxdn_t1_64_2 Verilog__main.i_rx_phy.rxdn_64_1) (= Verilog__main.i_rx_phy.rxdn_s1_64_2 Verilog__main.i_rx_phy.rxdn_t1_64_1) (= Verilog__main.i_rx_phy.rxdn_s_64_2 Verilog__main.i_rx_phy.rxdn_s1_64_1) (= Verilog__main.i_rx_phy.synced_d_64_2 (ite (not Verilog__main.i_rx_phy.rst_64_1) Verilog__main.i_rx_phy.synced_d_64_1 (ite Verilog__main.i_rx_phy.fs_ce_64_1 (ite (= Verilog__main.i_rx_phy.fs_state_64_1 (_ bv0 3)) false (ite (= Verilog__main.i_rx_phy.fs_state_64_1 (_ bv1 3)) false (ite (= Verilog__main.i_rx_phy.fs_state_64_1 (_ bv2 3)) false (ite (= Verilog__main.i_rx_phy.fs_state_64_1 (_ bv3 3)) false (ite (= Verilog__main.i_rx_phy.fs_state_64_1 (_ bv4 3)) false (ite (= Verilog__main.i_rx_phy.fs_state_64_1 (_ bv5 3)) false (ite (= Verilog__main.i_rx_phy.fs_state_64_1 (_ bv6 3)) false (ite (= Verilog__main.i_rx_phy.fs_state_64_1 (_ bv7 3)) (ite Verilog__main.i_rx_phy.k_64_1 true false) false)))))))) false))) (= Verilog__main.i_rx_phy.rx_en_64_2 Verilog__main.i_rx_phy.RxEn_i_64_1) (= Verilog__main.i_rx_phy.rx_active_64_2 (ite (not Verilog__main.i_rx_phy.rst_64_1) false (ite (and Verilog__main.i_rx_phy.synced_d_64_1 Verilog__main.i_rx_phy.rx_en_64_1) true (ite (and Verilog__main.i_rx_phy.se0_64_1 Verilog__main.i_rx_phy.rx_valid_r_64_1) false Verilog__main.i_rx_phy.rx_active_64_1)))) (= Verilog__main.i_rx_phy.bit_cnt_64_2 (ite (not Verilog__main.i_rx_phy.rst_64_1) (_ bv0 3) (ite (not Verilog__main.i_rx_phy.shift_en_64_1) (_ bv0 3) (ite (and Verilog__main.i_rx_phy.fs_ce_64_1 (not Verilog__main.i_rx_phy.drop_bit_64_1)) (bvadd Verilog__main.i_rx_phy.bit_cnt_64_1 (_ bv1 3)) Verilog__main.i_rx_phy.bit_cnt_64_1)))) (= Verilog__main.i_rx_phy.rx_valid1_64_2 (ite (not Verilog__main.i_rx_phy.rst_64_1) false (ite (and (and Verilog__main.i_rx_phy.fs_ce_64_1 (not Verilog__main.i_rx_phy.drop_bit_64_1)) (= Verilog__main.i_rx_phy.bit_cnt_64_1 (_ bv7 3))) true (ite (and (and Verilog__main.i_rx_phy.rx_valid1_64_1 Verilog__main.i_rx_phy.fs_ce_64_1) (not Verilog__main.i_rx_phy.drop_bit_64_1)) false Verilog__main.i_rx_phy.rx_valid1_64_1)))) (= Verilog__main.i_rx_phy.rx_valid_64_2 (and (and (not Verilog__main.i_rx_phy.drop_bit_64_1) Verilog__main.i_rx_phy.rx_valid1_64_1) Verilog__main.i_rx_phy.fs_ce_64_1)) (= Verilog__main.i_rx_phy.shift_en_64_2 (ite Verilog__main.i_rx_phy.fs_ce_64_1 (or Verilog__main.i_rx_phy.synced_d_64_1 Verilog__main.i_rx_phy.rx_active_64_1) Verilog__main.i_rx_phy.shift_en_64_1)) (= Verilog__main.i_rx_phy.sd_r_64_2 (ite Verilog__main.i_rx_phy.fs_ce_64_1 Verilog__main.i_rx_phy.rxd_s_64_1 Verilog__main.i_rx_phy.sd_r_64_1)) (= Verilog__main.i_rx_phy.sd_nrzi_64_2 (ite (not Verilog__main.i_rx_phy.rst_64_1) false (ite (and Verilog__main.i_rx_phy.rx_active_64_1 Verilog__main.i_rx_phy.fs_ce_64_1) (not (xor Verilog__main.i_rx_phy.rxd_s_64_1 Verilog__main.i_rx_phy.sd_r_64_1)) Verilog__main.i_rx_phy.sd_nrzi_64_1))) (= Verilog__main.i_rx_phy.hold_reg_64_2 (ite (and (and Verilog__main.i_rx_phy.fs_ce_64_1 Verilog__main.i_rx_phy.shift_en_64_1) (not Verilog__main.i_rx_phy.drop_bit_64_1)) (concat (ite Verilog__main.i_rx_phy.sd_nrzi_64_1 (_ bv1 1) (_ bv0 1)) ((_ extract 7 1) Verilog__main.i_rx_phy.hold_reg_64_1)) Verilog__main.i_rx_phy.hold_reg_64_1)) (= Verilog__main.i_rx_phy.one_cnt_64_2 (ite (not Verilog__main.i_rx_phy.rst_64_1) (_ bv0 3) (ite (not Verilog__main.i_rx_phy.shift_en_64_1) (_ bv0 3) (ite Verilog__main.i_rx_phy.fs_ce_64_1 (ite (or (not Verilog__main.i_rx_phy.sd_nrzi_64_1) Verilog__main.i_rx_phy.drop_bit_64_1) (_ bv0 3) (bvadd Verilog__main.i_rx_phy.one_cnt_64_1 (_ bv1 3))) Verilog__main.i_rx_phy.one_cnt_64_1)))) (= Verilog__main.i_rx_phy.dpll_state_64_2 (ite (not Verilog__main.i_rx_phy.rst_64_1) (_ bv1 2) (ite (= Verilog__main.i_rx_phy.dpll_state_64_1 (_ bv0 2)) (ite (and Verilog__main.i_rx_phy.lock_en_64_1 Verilog__main.i_rx_phy.change_64_1) (_ bv0 2) (_ bv1 2)) (ite (= Verilog__main.i_rx_phy.dpll_state_64_1 (_ bv1 2)) (ite (and Verilog__main.i_rx_phy.lock_en_64_1 Verilog__main.i_rx_phy.change_64_1) (_ bv3 2) (_ bv2 2)) (ite (= Verilog__main.i_rx_phy.dpll_state_64_1 (_ bv2 2)) (ite (and Verilog__main.i_rx_phy.lock_en_64_1 Verilog__main.i_rx_phy.change_64_1) (_ bv0 2) (_ bv3 2)) (ite (= Verilog__main.i_rx_phy.dpll_state_64_1 (_ bv3 2)) (ite (and Verilog__main.i_rx_phy.lock_en_64_1 Verilog__main.i_rx_phy.change_64_1) (_ bv0 2) (_ bv0 2)) Verilog__main.i_rx_phy.dpll_state_64_1)))))) (= Verilog__main.i_rx_phy.fs_ce_d_64_2 (ite (not Verilog__main.i_rx_phy.rst_64_1) Verilog__main.i_rx_phy.fs_ce_d_64_1 (ite (= Verilog__main.i_rx_phy.dpll_state_64_1 (_ bv0 2)) false (ite (= Verilog__main.i_rx_phy.dpll_state_64_1 (_ bv1 2)) true false)))) (= Verilog__main.i_rx_phy.rxdp_s1r_64_2 Verilog__main.i_rx_phy.rxdp_s1_64_1) (= Verilog__main.i_rx_phy.rxdn_s1r_64_2 Verilog__main.i_rx_phy.rxdn_s1_64_1) (= Verilog__main.i_rx_phy.fs_ce_r1_64_2 Verilog__main.i_rx_phy.fs_ce_d_64_1) (= Verilog__main.i_rx_phy.fs_ce_r2_64_2 Verilog__main.i_rx_phy.fs_ce_r1_64_1) (= Verilog__main.i_rx_phy.fs_ce_r3_64_2 Verilog__main.i_rx_phy.fs_ce_r2_64_1) (= Verilog__main.i_rx_phy.fs_state_64_2 (ite (not Verilog__main.i_rx_phy.rst_64_1) (_ bv0 3) (ite Verilog__main.i_rx_phy.fs_ce_64_1 (ite (= Verilog__main.i_rx_phy.fs_state_64_1 (_ bv0 3)) (ite (and Verilog__main.i_rx_phy.k_64_1 Verilog__main.i_rx_phy.rx_en_64_1) (_ bv1 3) Verilog__main.i_rx_phy.fs_state_64_1) (ite (= Verilog__main.i_rx_phy.fs_state_64_1 (_ bv1 3)) (ite (and Verilog__main.i_rx_phy.j_64_1 Verilog__main.i_rx_phy.rx_en_64_1) (_ bv2 3) (_ bv0 3)) (ite (= Verilog__main.i_rx_phy.fs_state_64_1 (_ bv2 3)) (ite (and Verilog__main.i_rx_phy.k_64_1 Verilog__main.i_rx_phy.rx_en_64_1) (_ bv3 3) (_ bv0 3)) (ite (= Verilog__main.i_rx_phy.fs_state_64_1 (_ bv3 3)) (ite (and Verilog__main.i_rx_phy.j_64_1 Verilog__main.i_rx_phy.rx_en_64_1) (_ bv4 3) (_ bv0 3)) (ite (= Verilog__main.i_rx_phy.fs_state_64_1 (_ bv4 3)) (ite (and Verilog__main.i_rx_phy.k_64_1 Verilog__main.i_rx_phy.rx_en_64_1) (_ bv5 3) (_ bv0 3)) (ite (= Verilog__main.i_rx_phy.fs_state_64_1 (_ bv5 3)) (ite (and Verilog__main.i_rx_phy.j_64_1 Verilog__main.i_rx_phy.rx_en_64_1) (_ bv6 3) (ite (and Verilog__main.i_rx_phy.k_64_1 Verilog__main.i_rx_phy.rx_en_64_1) (_ bv7 3) (_ bv0 3))) (ite (= Verilog__main.i_rx_phy.fs_state_64_1 (_ bv6 3)) (ite (and Verilog__main.i_rx_phy.k_64_1 Verilog__main.i_rx_phy.rx_en_64_1) (_ bv7 3) (_ bv0 3)) (ite (= Verilog__main.i_rx_phy.fs_state_64_1 (_ bv7 3)) (_ bv0 3) Verilog__main.i_rx_phy.fs_state_64_1)))))))) Verilog__main.i_rx_phy.fs_state_64_1))) (= Verilog__main.i_rx_phy.rx_valid_r_64_2 (ite Verilog__main.i_rx_phy.rx_valid_64_1 true (ite Verilog__main.i_rx_phy.fs_ce_64_1 false Verilog__main.i_rx_phy.rx_valid_r_64_1)))) (= Verilog__main.usb_rst_64_2 (= Verilog__main.rst_cnt_64_1 (_ bv31 5))) (= Verilog__main.rst_cnt_64_2 (ite (not Verilog__main.rst_64_1) (_ bv0 5) (ite (not (= Verilog__main.LineState_o_64_1 (_ bv0 2))) (_ bv0 5) (ite (and (not Verilog__main.usb_rst_64_1) Verilog__main.fs_ce_64_1) (bvadd Verilog__main.rst_cnt_64_1 (_ bv1 5)) Verilog__main.rst_cnt_64_1)))))) (and (and (and (= Verilog__main.reset_64_0_39_ (and Verilog__main.rst_64_0_39_ (not Verilog__main.usb_rst_64_0_39_))) (and (= Verilog__main.i_tx_phy.hold_64_0_39_ Verilog__main.i_tx_phy.stuff_64_0_39_) (= Verilog__main.i_tx_phy.sft_done_e_64_0_39_ (and Verilog__main.i_tx_phy.sft_done_64_0_39_ (not Verilog__main.i_tx_phy.sft_done_r_64_0_39_))) (= Verilog__main.i_tx_phy.stuff_64_0_39_ (= Verilog__main.i_tx_phy.one_cnt_64_0_39_ (_ bv6 3))) (= Verilog__main.i_tx_phy.eop_done_64_0_39_ Verilog__main.i_tx_phy.append_eop_sync3_64_0_39_)) (= Verilog__main.i_tx_phy.clk_64_0_39_ Verilog__main.clk_64_0_39_) (= Verilog__main.i_tx_phy.rst_64_0_39_ Verilog__main.reset_64_0_39_) (= Verilog__main.i_tx_phy.fs_ce_64_0_39_ Verilog__main.fs_ce_64_0_39_) (= Verilog__main.i_tx_phy.phy_mode_64_0_39_ Verilog__main.phy_tx_mode_64_0_39_) (= Verilog__main.i_tx_phy.txdp_64_0_39_ Verilog__main.txdp_64_0_39_) (= Verilog__main.i_tx_phy.txdn_64_0_39_ Verilog__main.txdn_64_0_39_) (= Verilog__main.i_tx_phy.txoe_64_0_39_ Verilog__main.txoe_64_0_39_) (= Verilog__main.i_tx_phy.DataOut_i_64_0_39_ Verilog__main.DataOut_i_64_0_39_) (= Verilog__main.i_tx_phy.TxValid_i_64_0_39_ Verilog__main.TxValid_i_64_0_39_) (= Verilog__main.i_tx_phy.TxReady_o_64_0_39_ Verilog__main.TxReady_o_64_0_39_) (and (= Verilog__main.i_rx_phy.RxActive_o_64_0_39_ Verilog__main.i_rx_phy.rx_active_64_0_39_) (= Verilog__main.i_rx_phy.RxValid_o_64_0_39_ Verilog__main.i_rx_phy.rx_valid_64_0_39_) (= Verilog__main.i_rx_phy.RxError_o_64_0_39_ false) (= Verilog__main.i_rx_phy.DataIn_o_64_0_39_ Verilog__main.i_rx_phy.hold_reg_64_0_39_) (= Verilog__main.i_rx_phy.LineState_64_0_39_ (concat (ite Verilog__main.i_rx_phy.rxdp_s1_64_0_39_ (_ bv1 1) (_ bv0 1)) (ite Verilog__main.i_rx_phy.rxdn_s1_64_0_39_ (_ bv1 1) (_ bv0 1)))) (= Verilog__main.i_rx_phy.k_64_0_39_ (and (not Verilog__main.i_rx_phy.rxdp_s_64_0_39_) Verilog__main.i_rx_phy.rxdn_s_64_0_39_)) (= Verilog__main.i_rx_phy.j_64_0_39_ (and Verilog__main.i_rx_phy.rxdp_s_64_0_39_ (not Verilog__main.i_rx_phy.rxdn_s_64_0_39_))) (= Verilog__main.i_rx_phy.se0_64_0_39_ (and (not Verilog__main.i_rx_phy.rxdp_s_64_0_39_) (not Verilog__main.i_rx_phy.rxdn_s_64_0_39_))) (= Verilog__main.i_rx_phy.lock_en_64_0_39_ Verilog__main.i_rx_phy.rx_en_64_0_39_) (= Verilog__main.i_rx_phy.change_64_0_39_ (or (xor Verilog__main.i_rx_phy.rxdp_s1r_64_0_39_ Verilog__main.i_rx_phy.rxdp_s1_64_0_39_) (xor Verilog__main.i_rx_phy.rxdn_s1r_64_0_39_ Verilog__main.i_rx_phy.rxdn_s1_64_0_39_))) (= Verilog__main.i_rx_phy.drop_bit_64_0_39_ (= Verilog__main.i_rx_phy.one_cnt_64_0_39_ (_ bv6 3)))) (= Verilog__main.i_rx_phy.clk_64_0_39_ Verilog__main.clk_64_0_39_) (= Verilog__main.i_rx_phy.rst_64_0_39_ Verilog__main.reset_64_0_39_) (= Verilog__main.i_rx_phy.fs_ce_64_0_39_ Verilog__main.fs_ce_64_0_39_) (= Verilog__main.i_rx_phy.rxd_64_0_39_ Verilog__main.rxd_64_0_39_) (= Verilog__main.i_rx_phy.rxdp_64_0_39_ Verilog__main.rxdp_64_0_39_) (= Verilog__main.i_rx_phy.rxdn_64_0_39_ Verilog__main.rxdn_64_0_39_) (= Verilog__main.i_rx_phy.DataIn_o_64_0_39_ Verilog__main.DataIn_o_64_0_39_) (= Verilog__main.i_rx_phy.RxValid_o_64_0_39_ Verilog__main.RxValid_o_64_0_39_) (= Verilog__main.i_rx_phy.RxActive_o_64_0_39_ Verilog__main.RxActive_o_64_0_39_) (= Verilog__main.i_rx_phy.RxError_o_64_0_39_ Verilog__main.RxError_o_64_0_39_) (= Verilog__main.i_rx_phy.RxEn_i_64_0_39_ Verilog__main.txoe_64_0_39_) (= Verilog__main.i_rx_phy.LineState_64_0_39_ Verilog__main.LineState_o_64_0_39_)) (and (= Verilog__main.reset_64_1_39_ (and Verilog__main.rst_64_1_39_ (not Verilog__main.usb_rst_64_1_39_))) (and (= Verilog__main.i_tx_phy.hold_64_1_39_ Verilog__main.i_tx_phy.stuff_64_1_39_) (= Verilog__main.i_tx_phy.sft_done_e_64_1_39_ (and Verilog__main.i_tx_phy.sft_done_64_1_39_ (not Verilog__main.i_tx_phy.sft_done_r_64_1_39_))) (= Verilog__main.i_tx_phy.stuff_64_1_39_ (= Verilog__main.i_tx_phy.one_cnt_64_1_39_ (_ bv6 3))) (= Verilog__main.i_tx_phy.eop_done_64_1_39_ Verilog__main.i_tx_phy.append_eop_sync3_64_1_39_)) (= Verilog__main.i_tx_phy.clk_64_1_39_ Verilog__main.clk_64_1_39_) (= Verilog__main.i_tx_phy.rst_64_1_39_ Verilog__main.reset_64_1_39_) (= Verilog__main.i_tx_phy.fs_ce_64_1_39_ Verilog__main.fs_ce_64_1_39_) (= Verilog__main.i_tx_phy.phy_mode_64_1_39_ Verilog__main.phy_tx_mode_64_1_39_) (= Verilog__main.i_tx_phy.txdp_64_1_39_ Verilog__main.txdp_64_1_39_) (= Verilog__main.i_tx_phy.txdn_64_1_39_ Verilog__main.txdn_64_1_39_) (= Verilog__main.i_tx_phy.txoe_64_1_39_ Verilog__main.txoe_64_1_39_) (= Verilog__main.i_tx_phy.DataOut_i_64_1_39_ Verilog__main.DataOut_i_64_1_39_) (= Verilog__main.i_tx_phy.TxValid_i_64_1_39_ Verilog__main.TxValid_i_64_1_39_) (= Verilog__main.i_tx_phy.TxReady_o_64_1_39_ Verilog__main.TxReady_o_64_1_39_) (and (= Verilog__main.i_rx_phy.RxActive_o_64_1_39_ Verilog__main.i_rx_phy.rx_active_64_1_39_) (= Verilog__main.i_rx_phy.RxValid_o_64_1_39_ Verilog__main.i_rx_phy.rx_valid_64_1_39_) (= Verilog__main.i_rx_phy.RxError_o_64_1_39_ false) (= Verilog__main.i_rx_phy.DataIn_o_64_1_39_ Verilog__main.i_rx_phy.hold_reg_64_1_39_) (= Verilog__main.i_rx_phy.LineState_64_1_39_ (concat (ite Verilog__main.i_rx_phy.rxdp_s1_64_1_39_ (_ bv1 1) (_ bv0 1)) (ite Verilog__main.i_rx_phy.rxdn_s1_64_1_39_ (_ bv1 1) (_ bv0 1)))) (= Verilog__main.i_rx_phy.k_64_1_39_ (and (not Verilog__main.i_rx_phy.rxdp_s_64_1_39_) Verilog__main.i_rx_phy.rxdn_s_64_1_39_)) (= Verilog__main.i_rx_phy.j_64_1_39_ (and Verilog__main.i_rx_phy.rxdp_s_64_1_39_ (not Verilog__main.i_rx_phy.rxdn_s_64_1_39_))) (= Verilog__main.i_rx_phy.se0_64_1_39_ (and (not Verilog__main.i_rx_phy.rxdp_s_64_1_39_) (not Verilog__main.i_rx_phy.rxdn_s_64_1_39_))) (= Verilog__main.i_rx_phy.lock_en_64_1_39_ Verilog__main.i_rx_phy.rx_en_64_1_39_) (= Verilog__main.i_rx_phy.change_64_1_39_ (or (xor Verilog__main.i_rx_phy.rxdp_s1r_64_1_39_ Verilog__main.i_rx_phy.rxdp_s1_64_1_39_) (xor Verilog__main.i_rx_phy.rxdn_s1r_64_1_39_ Verilog__main.i_rx_phy.rxdn_s1_64_1_39_))) (= Verilog__main.i_rx_phy.drop_bit_64_1_39_ (= Verilog__main.i_rx_phy.one_cnt_64_1_39_ (_ bv6 3)))) (= Verilog__main.i_rx_phy.clk_64_1_39_ Verilog__main.clk_64_1_39_) (= Verilog__main.i_rx_phy.rst_64_1_39_ Verilog__main.reset_64_1_39_) (= Verilog__main.i_rx_phy.fs_ce_64_1_39_ Verilog__main.fs_ce_64_1_39_) (= Verilog__main.i_rx_phy.rxd_64_1_39_ Verilog__main.rxd_64_1_39_) (= Verilog__main.i_rx_phy.rxdp_64_1_39_ Verilog__main.rxdp_64_1_39_) (= Verilog__main.i_rx_phy.rxdn_64_1_39_ Verilog__main.rxdn_64_1_39_) (= Verilog__main.i_rx_phy.DataIn_o_64_1_39_ Verilog__main.DataIn_o_64_1_39_) (= Verilog__main.i_rx_phy.RxValid_o_64_1_39_ Verilog__main.RxValid_o_64_1_39_) (= Verilog__main.i_rx_phy.RxActive_o_64_1_39_ Verilog__main.RxActive_o_64_1_39_) (= Verilog__main.i_rx_phy.RxError_o_64_1_39_ Verilog__main.RxError_o_64_1_39_) (= Verilog__main.i_rx_phy.RxEn_i_64_1_39_ Verilog__main.txoe_64_1_39_) (= Verilog__main.i_rx_phy.LineState_64_1_39_ Verilog__main.LineState_o_64_1_39_)) (and (and (= Verilog__main.i_tx_phy.sd_bs_o_64_0_39_ false) (= Verilog__main.i_tx_phy.sd_nrzi_o_64_0_39_ true) (= Verilog__main.i_tx_phy.append_eop_64_0_39_ false) (= Verilog__main.i_tx_phy.append_eop_sync1_64_0_39_ false) (= Verilog__main.i_tx_phy.append_eop_sync2_64_0_39_ false) (= Verilog__main.i_tx_phy.append_eop_sync3_64_0_39_ false) (= Verilog__main.i_tx_phy.txoe_r1_64_0_39_ false) (= Verilog__main.i_tx_phy.txoe_r2_64_0_39_ false) (= Verilog__main.i_tx_phy.txdp_64_0_39_ true) (= Verilog__main.i_tx_phy.txdn_64_0_39_ false) (= Verilog__main.i_tx_phy.txoe_64_0_39_ true) (= Verilog__main.i_tx_phy.TxReady_o_64_0_39_ false) (= Verilog__main.i_tx_phy.state_64_0_39_ (_ bv0 3)) (= Verilog__main.i_tx_phy.tx_ready_64_0_39_ false) (= Verilog__main.i_tx_phy.tx_ready_d_64_0_39_ false) (= Verilog__main.i_tx_phy.ld_sop_d_64_0_39_ false) (= Verilog__main.i_tx_phy.ld_data_d_64_0_39_ false) (= Verilog__main.i_tx_phy.ld_eop_d_64_0_39_ false) (= Verilog__main.i_tx_phy.tx_ip_64_0_39_ false) (= Verilog__main.i_tx_phy.tx_ip_sync_64_0_39_ false) (= Verilog__main.i_tx_phy.bit_cnt_64_0_39_ (_ bv0 3)) (= Verilog__main.i_tx_phy.hold_reg_64_0_39_ (_ bv0 8)) (= Verilog__main.i_tx_phy.sd_raw_o_64_0_39_ false) (= Verilog__main.i_tx_phy.data_done_64_0_39_ false) (= Verilog__main.i_tx_phy.sft_done_64_0_39_ false) (= Verilog__main.i_tx_phy.sft_done_r_64_0_39_ false) (= Verilog__main.i_tx_phy.ld_data_64_0_39_ false) (= Verilog__main.i_tx_phy.one_cnt_64_0_39_ (_ bv0 3))) (and (= Verilog__main.i_rx_phy.fs_ce_64_0_39_ false) (= Verilog__main.i_rx_phy.rxd_t1_64_0_39_ false) (= Verilog__main.i_rx_phy.rxd_s1_64_0_39_ false) (= Verilog__main.i_rx_phy.rxd_s_64_0_39_ false) (= Verilog__main.i_rx_phy.rxdp_t1_64_0_39_ false) (= Verilog__main.i_rx_phy.rxdp_s1_64_0_39_ false) (= Verilog__main.i_rx_phy.rxdp_s_64_0_39_ false) (= Verilog__main.i_rx_phy.rxdn_t1_64_0_39_ false) (= Verilog__main.i_rx_phy.rxdn_s1_64_0_39_ false) (= Verilog__main.i_rx_phy.rxdn_s_64_0_39_ false) (= Verilog__main.i_rx_phy.synced_d_64_0_39_ false) (= Verilog__main.i_rx_phy.rx_en_64_0_39_ false) (= Verilog__main.i_rx_phy.rx_active_64_0_39_ false) (= Verilog__main.i_rx_phy.bit_cnt_64_0_39_ (_ bv0 3)) (= Verilog__main.i_rx_phy.rx_valid1_64_0_39_ false) (= Verilog__main.i_rx_phy.rx_valid_64_0_39_ false) (= Verilog__main.i_rx_phy.shift_en_64_0_39_ false) (= Verilog__main.i_rx_phy.sd_r_64_0_39_ false) (= Verilog__main.i_rx_phy.sd_nrzi_64_0_39_ false) (= Verilog__main.i_rx_phy.hold_reg_64_0_39_ (_ bv0 8)) (= Verilog__main.i_rx_phy.one_cnt_64_0_39_ (_ bv0 3)) (= Verilog__main.i_rx_phy.dpll_state_64_0_39_ (_ bv1 2)) (= Verilog__main.i_rx_phy.fs_ce_d_64_0_39_ false) (= Verilog__main.i_rx_phy.rxdp_s1r_64_0_39_ false) (= Verilog__main.i_rx_phy.rxdn_s1r_64_0_39_ false) (= Verilog__main.i_rx_phy.fs_ce_r1_64_0_39_ false) (= Verilog__main.i_rx_phy.fs_ce_r2_64_0_39_ false) (= Verilog__main.i_rx_phy.fs_ce_r3_64_0_39_ false) (= Verilog__main.i_rx_phy.fs_state_64_0_39_ (_ bv0 3)) (= Verilog__main.i_rx_phy.rx_valid_r_64_0_39_ false)) (= Verilog__main.usb_rst_64_0_39_ false) (= Verilog__main.rst_cnt_64_0_39_ (_ bv0 5))) (and (and (= Verilog__main.i_tx_phy.sd_bs_o_64_1_39_ (ite (not Verilog__main.i_tx_phy.rst_64_0_39_) false (ite Verilog__main.i_tx_phy.fs_ce_64_0_39_ (ite (not Verilog__main.i_tx_phy.tx_ip_sync_64_0_39_) false (ite Verilog__main.i_tx_phy.stuff_64_0_39_ false (= ((_ extract 0 0) (ite Verilog__main.i_tx_phy.sd_raw_o_64_0_39_ (_ bv1 1) (_ bv0 1))) (_ bv1 1)))) Verilog__main.i_tx_phy.sd_bs_o_64_0_39_))) (= Verilog__main.i_tx_phy.sd_nrzi_o_64_1_39_ (ite (not Verilog__main.i_tx_phy.rst_64_0_39_) true (ite (or (not Verilog__main.i_tx_phy.tx_ip_sync_64_0_39_) (not Verilog__main.i_tx_phy.txoe_r1_64_0_39_)) true (ite Verilog__main.i_tx_phy.fs_ce_64_0_39_ (ite Verilog__main.i_tx_phy.sd_bs_o_64_0_39_ Verilog__main.i_tx_phy.sd_nrzi_o_64_0_39_ (not Verilog__main.i_tx_phy.sd_nrzi_o_64_0_39_)) Verilog__main.i_tx_phy.sd_nrzi_o_64_0_39_)))) (= Verilog__main.i_tx_phy.append_eop_64_1_39_ (ite (not Verilog__main.i_tx_phy.rst_64_0_39_) false (ite Verilog__main.i_tx_phy.ld_eop_d_64_0_39_ true (ite Verilog__main.i_tx_phy.append_eop_sync2_64_0_39_ false Verilog__main.i_tx_phy.append_eop_64_0_39_)))) (= Verilog__main.i_tx_phy.append_eop_sync1_64_1_39_ (ite (not Verilog__main.i_tx_phy.rst_64_0_39_) false (ite Verilog__main.i_tx_phy.fs_ce_64_0_39_ Verilog__main.i_tx_phy.append_eop_64_0_39_ Verilog__main.i_tx_phy.append_eop_sync1_64_0_39_))) (= Verilog__main.i_tx_phy.append_eop_sync2_64_1_39_ (ite (not Verilog__main.i_tx_phy.rst_64_0_39_) false (ite Verilog__main.i_tx_phy.fs_ce_64_0_39_ Verilog__main.i_tx_phy.append_eop_sync1_64_0_39_ Verilog__main.i_tx_phy.append_eop_sync2_64_0_39_))) (= Verilog__main.i_tx_phy.append_eop_sync3_64_1_39_ (ite (not Verilog__main.i_tx_phy.rst_64_0_39_) false (ite Verilog__main.i_tx_phy.fs_ce_64_0_39_ Verilog__main.i_tx_phy.append_eop_sync2_64_0_39_ Verilog__main.i_tx_phy.append_eop_sync3_64_0_39_))) (= Verilog__main.i_tx_phy.txoe_r1_64_1_39_ (ite (not Verilog__main.i_tx_phy.rst_64_0_39_) false (ite Verilog__main.i_tx_phy.fs_ce_64_0_39_ Verilog__main.i_tx_phy.tx_ip_sync_64_0_39_ Verilog__main.i_tx_phy.txoe_r1_64_0_39_))) (= Verilog__main.i_tx_phy.txoe_r2_64_1_39_ (ite (not Verilog__main.i_tx_phy.rst_64_0_39_) false (ite Verilog__main.i_tx_phy.fs_ce_64_0_39_ Verilog__main.i_tx_phy.txoe_r1_64_0_39_ Verilog__main.i_tx_phy.txoe_r2_64_0_39_))) (= Verilog__main.i_tx_phy.txdp_64_1_39_ (ite (not Verilog__main.i_tx_phy.rst_64_0_39_) true (ite Verilog__main.i_tx_phy.fs_ce_64_0_39_ (ite Verilog__main.i_tx_phy.phy_mode_64_0_39_ (and (not Verilog__main.i_tx_phy.append_eop_sync3_64_0_39_) Verilog__main.i_tx_phy.sd_nrzi_o_64_0_39_) Verilog__main.i_tx_phy.sd_nrzi_o_64_0_39_) Verilog__main.i_tx_phy.txdp_64_0_39_))) (= Verilog__main.i_tx_phy.txdn_64_1_39_ (ite (not Verilog__main.i_tx_phy.rst_64_0_39_) false (ite Verilog__main.i_tx_phy.fs_ce_64_0_39_ (ite Verilog__main.i_tx_phy.phy_mode_64_0_39_ (and (not Verilog__main.i_tx_phy.append_eop_sync3_64_0_39_) (not Verilog__main.i_tx_phy.sd_nrzi_o_64_0_39_)) Verilog__main.i_tx_phy.append_eop_sync3_64_0_39_) Verilog__main.i_tx_phy.txdn_64_0_39_))) (= Verilog__main.i_tx_phy.txoe_64_1_39_ (ite (not Verilog__main.i_tx_phy.rst_64_0_39_) true (ite Verilog__main.i_tx_phy.fs_ce_64_0_39_ (not (or Verilog__main.i_tx_phy.txoe_r1_64_0_39_ Verilog__main.i_tx_phy.txoe_r2_64_0_39_)) Verilog__main.i_tx_phy.txoe_64_0_39_))) (= Verilog__main.i_tx_phy.TxReady_o_64_1_39_ (ite (not Verilog__main.i_tx_phy.rst_64_0_39_) false (and Verilog__main.i_tx_phy.tx_ready_d_64_0_39_ Verilog__main.i_tx_phy.TxValid_i_64_0_39_))) (= Verilog__main.i_tx_phy.state_64_1_39_ (ite (not Verilog__main.i_tx_phy.rst_64_0_39_) (_ bv0 3) (ite (= Verilog__main.i_tx_phy.state_64_0_39_ (_ bv0 3)) (ite Verilog__main.i_tx_phy.TxValid_i_64_0_39_ (_ bv1 3) Verilog__main.i_tx_phy.state_64_0_39_) (ite (= Verilog__main.i_tx_phy.state_64_0_39_ (_ bv1 3)) (ite Verilog__main.i_tx_phy.sft_done_e_64_0_39_ (_ bv3 3) Verilog__main.i_tx_phy.state_64_0_39_) (ite (= Verilog__main.i_tx_phy.state_64_0_39_ (_ bv3 3)) (ite (and (not Verilog__main.i_tx_phy.data_done_64_0_39_) Verilog__main.i_tx_phy.sft_done_e_64_0_39_) (_ bv4 3) Verilog__main.i_tx_phy.state_64_0_39_) (ite (= Verilog__main.i_tx_phy.state_64_0_39_ (_ bv4 3)) (ite Verilog__main.i_tx_phy.eop_done_64_0_39_ (_ bv5 3) Verilog__main.i_tx_phy.state_64_0_39_) (ite (= Verilog__main.i_tx_phy.state_64_0_39_ (_ bv5 3)) (ite (and (not Verilog__main.i_tx_phy.eop_done_64_0_39_) Verilog__main.i_tx_phy.fs_ce_64_0_39_) (_ bv6 3) Verilog__main.i_tx_phy.state_64_0_39_) (ite (= Verilog__main.i_tx_phy.state_64_0_39_ (_ bv6 3)) (ite Verilog__main.i_tx_phy.fs_ce_64_0_39_ (_ bv0 3) Verilog__main.i_tx_phy.state_64_0_39_) Verilog__main.i_tx_phy.state_64_0_39_)))))))) (= Verilog__main.i_tx_phy.tx_ready_64_1_39_ Verilog__main.i_tx_phy.tx_ready_d_64_0_39_) (= Verilog__main.i_tx_phy.tx_ready_d_64_1_39_ (ite (not Verilog__main.i_tx_phy.rst_64_0_39_) Verilog__main.i_tx_phy.tx_ready_d_64_0_39_ (ite (= Verilog__main.i_tx_phy.state_64_0_39_ (_ bv0 3)) false (ite (= Verilog__main.i_tx_phy.state_64_0_39_ (_ bv1 3)) (ite Verilog__main.i_tx_phy.sft_done_e_64_0_39_ true false) (ite (= Verilog__main.i_tx_phy.state_64_0_39_ (_ bv3 3)) (ite (and Verilog__main.i_tx_phy.data_done_64_0_39_ Verilog__main.i_tx_phy.sft_done_e_64_0_39_) true false) false))))) (= Verilog__main.i_tx_phy.ld_sop_d_64_1_39_ (ite (not Verilog__main.i_tx_phy.rst_64_0_39_) Verilog__main.i_tx_phy.ld_sop_d_64_0_39_ (ite (= Verilog__main.i_tx_phy.state_64_0_39_ (_ bv0 3)) (ite Verilog__main.i_tx_phy.TxValid_i_64_0_39_ true false) false))) (= Verilog__main.i_tx_phy.ld_data_d_64_1_39_ (ite (not Verilog__main.i_tx_phy.rst_64_0_39_) Verilog__main.i_tx_phy.ld_data_d_64_0_39_ (ite (= Verilog__main.i_tx_phy.state_64_0_39_ (_ bv0 3)) false (ite (= Verilog__main.i_tx_phy.state_64_0_39_ (_ bv1 3)) (ite Verilog__main.i_tx_phy.sft_done_e_64_0_39_ true false) (ite (= Verilog__main.i_tx_phy.state_64_0_39_ (_ bv3 3)) (ite (and Verilog__main.i_tx_phy.data_done_64_0_39_ Verilog__main.i_tx_phy.sft_done_e_64_0_39_) true false) false))))) (= Verilog__main.i_tx_phy.ld_eop_d_64_1_39_ (ite (not Verilog__main.i_tx_phy.rst_64_0_39_) Verilog__main.i_tx_phy.ld_eop_d_64_0_39_ (ite (= Verilog__main.i_tx_phy.state_64_0_39_ (_ bv0 3)) false (ite (= Verilog__main.i_tx_phy.state_64_0_39_ (_ bv1 3)) false (ite (= Verilog__main.i_tx_phy.state_64_0_39_ (_ bv3 3)) (ite (and (not Verilog__main.i_tx_phy.data_done_64_0_39_) Verilog__main.i_tx_phy.sft_done_e_64_0_39_) true false) false))))) (= Verilog__main.i_tx_phy.tx_ip_64_1_39_ (ite (not Verilog__main.i_tx_phy.rst_64_0_39_) false (ite Verilog__main.i_tx_phy.ld_sop_d_64_0_39_ true (ite Verilog__main.i_tx_phy.eop_done_64_0_39_ false Verilog__main.i_tx_phy.tx_ip_64_0_39_)))) (= Verilog__main.i_tx_phy.tx_ip_sync_64_1_39_ (ite (not Verilog__main.i_tx_phy.rst_64_0_39_) false (ite Verilog__main.i_tx_phy.fs_ce_64_0_39_ Verilog__main.i_tx_phy.tx_ip_64_0_39_ Verilog__main.i_tx_phy.tx_ip_sync_64_0_39_))) (= Verilog__main.i_tx_phy.bit_cnt_64_1_39_ (ite (not Verilog__main.i_tx_phy.rst_64_0_39_) (_ bv0 3) (ite (not Verilog__main.i_tx_phy.tx_ip_sync_64_0_39_) (_ bv0 3) (ite (and Verilog__main.i_tx_phy.fs_ce_64_0_39_ (not Verilog__main.i_tx_phy.hold_64_0_39_)) (bvadd Verilog__main.i_tx_phy.bit_cnt_64_0_39_ (_ bv1 3)) Verilog__main.i_tx_phy.bit_cnt_64_0_39_)))) (= Verilog__main.i_tx_phy.hold_reg_64_1_39_ (ite Verilog__main.i_tx_phy.ld_sop_d_64_0_39_ (_ bv128 8) (ite Verilog__main.i_tx_phy.ld_data_64_0_39_ Verilog__main.i_tx_phy.DataOut_i_64_0_39_ Verilog__main.i_tx_phy.hold_reg_64_0_39_))) (= Verilog__main.i_tx_phy.sd_raw_o_64_1_39_ (ite (not Verilog__main.i_tx_phy.tx_ip_sync_64_0_39_) false (ite (= Verilog__main.i_tx_phy.bit_cnt_64_0_39_ (_ bv0 3)) (= ((_ extract 0 0) Verilog__main.i_tx_phy.hold_reg_64_0_39_) (_ bv1 1)) (ite (= Verilog__main.i_tx_phy.bit_cnt_64_0_39_ (_ bv1 3)) (= ((_ extract 1 1) Verilog__main.i_tx_phy.hold_reg_64_0_39_) (_ bv1 1)) (ite (= Verilog__main.i_tx_phy.bit_cnt_64_0_39_ (_ bv2 3)) (= ((_ extract 2 2) Verilog__main.i_tx_phy.hold_reg_64_0_39_) (_ bv1 1)) (ite (= Verilog__main.i_tx_phy.bit_cnt_64_0_39_ (_ bv3 3)) (= ((_ extract 3 3) Verilog__main.i_tx_phy.hold_reg_64_0_39_) (_ bv1 1)) (ite (= Verilog__main.i_tx_phy.bit_cnt_64_0_39_ (_ bv4 3)) (= ((_ extract 4 4) Verilog__main.i_tx_phy.hold_reg_64_0_39_) (_ bv1 1)) (ite (= Verilog__main.i_tx_phy.bit_cnt_64_0_39_ (_ bv5 3)) (= ((_ extract 5 5) Verilog__main.i_tx_phy.hold_reg_64_0_39_) (_ bv1 1)) (ite (= Verilog__main.i_tx_phy.bit_cnt_64_0_39_ (_ bv6 3)) (= ((_ extract 6 6) Verilog__main.i_tx_phy.hold_reg_64_0_39_) (_ bv1 1)) (ite (= Verilog__main.i_tx_phy.bit_cnt_64_0_39_ (_ bv7 3)) (= ((_ extract 7 7) Verilog__main.i_tx_phy.hold_reg_64_0_39_) (_ bv1 1)) Verilog__main.i_tx_phy.sd_raw_o_64_0_39_)))))))))) (= Verilog__main.i_tx_phy.data_done_64_1_39_ (ite (not Verilog__main.i_tx_phy.rst_64_0_39_) false (ite (and Verilog__main.i_tx_phy.TxValid_i_64_0_39_ (not Verilog__main.i_tx_phy.tx_ip_64_0_39_)) true (ite (not Verilog__main.i_tx_phy.TxValid_i_64_0_39_) false Verilog__main.i_tx_phy.data_done_64_0_39_)))) (= Verilog__main.i_tx_phy.sft_done_64_1_39_ (and (not Verilog__main.i_tx_phy.hold_64_0_39_) (= Verilog__main.i_tx_phy.bit_cnt_64_0_39_ (_ bv7 3)))) (= Verilog__main.i_tx_phy.sft_done_r_64_1_39_ Verilog__main.i_tx_phy.sft_done_64_0_39_) (= Verilog__main.i_tx_phy.ld_data_64_1_39_ Verilog__main.i_tx_phy.ld_data_d_64_0_39_) (= Verilog__main.i_tx_phy.one_cnt_64_1_39_ (ite (not Verilog__main.i_tx_phy.rst_64_0_39_) (_ bv0 3) (ite (not Verilog__main.i_tx_phy.tx_ip_sync_64_0_39_) (_ bv0 3) (ite Verilog__main.i_tx_phy.fs_ce_64_0_39_ (ite (or (not Verilog__main.i_tx_phy.sd_raw_o_64_0_39_) Verilog__main.i_tx_phy.stuff_64_0_39_) (_ bv0 3) (bvadd Verilog__main.i_tx_phy.one_cnt_64_0_39_ (_ bv1 3))) Verilog__main.i_tx_phy.one_cnt_64_0_39_))))) (and (= Verilog__main.i_rx_phy.fs_ce_64_1_39_ Verilog__main.i_rx_phy.fs_ce_r3_64_0_39_) (= Verilog__main.i_rx_phy.rxd_t1_64_1_39_ Verilog__main.i_rx_phy.rxd_64_0_39_) (= Verilog__main.i_rx_phy.rxd_s1_64_1_39_ Verilog__main.i_rx_phy.rxd_t1_64_0_39_) (= Verilog__main.i_rx_phy.rxd_s_64_1_39_ Verilog__main.i_rx_phy.rxd_s1_64_0_39_) (= Verilog__main.i_rx_phy.rxdp_t1_64_1_39_ Verilog__main.i_rx_phy.rxdp_64_0_39_) (= Verilog__main.i_rx_phy.rxdp_s1_64_1_39_ Verilog__main.i_rx_phy.rxdp_t1_64_0_39_) (= Verilog__main.i_rx_phy.rxdp_s_64_1_39_ Verilog__main.i_rx_phy.rxdp_s1_64_0_39_) (= Verilog__main.i_rx_phy.rxdn_t1_64_1_39_ Verilog__main.i_rx_phy.rxdn_64_0_39_) (= Verilog__main.i_rx_phy.rxdn_s1_64_1_39_ Verilog__main.i_rx_phy.rxdn_t1_64_0_39_) (= Verilog__main.i_rx_phy.rxdn_s_64_1_39_ Verilog__main.i_rx_phy.rxdn_s1_64_0_39_) (= Verilog__main.i_rx_phy.synced_d_64_1_39_ (ite (not Verilog__main.i_rx_phy.rst_64_0_39_) Verilog__main.i_rx_phy.synced_d_64_0_39_ (ite Verilog__main.i_rx_phy.fs_ce_64_0_39_ (ite (= Verilog__main.i_rx_phy.fs_state_64_0_39_ (_ bv0 3)) false (ite (= Verilog__main.i_rx_phy.fs_state_64_0_39_ (_ bv1 3)) false (ite (= Verilog__main.i_rx_phy.fs_state_64_0_39_ (_ bv2 3)) false (ite (= Verilog__main.i_rx_phy.fs_state_64_0_39_ (_ bv3 3)) false (ite (= Verilog__main.i_rx_phy.fs_state_64_0_39_ (_ bv4 3)) false (ite (= Verilog__main.i_rx_phy.fs_state_64_0_39_ (_ bv5 3)) false (ite (= Verilog__main.i_rx_phy.fs_state_64_0_39_ (_ bv6 3)) false (ite (= Verilog__main.i_rx_phy.fs_state_64_0_39_ (_ bv7 3)) (ite Verilog__main.i_rx_phy.k_64_0_39_ true false) false)))))))) false))) (= Verilog__main.i_rx_phy.rx_en_64_1_39_ Verilog__main.i_rx_phy.RxEn_i_64_0_39_) (= Verilog__main.i_rx_phy.rx_active_64_1_39_ (ite (not Verilog__main.i_rx_phy.rst_64_0_39_) false (ite (and Verilog__main.i_rx_phy.synced_d_64_0_39_ Verilog__main.i_rx_phy.rx_en_64_0_39_) true (ite (and Verilog__main.i_rx_phy.se0_64_0_39_ Verilog__main.i_rx_phy.rx_valid_r_64_0_39_) false Verilog__main.i_rx_phy.rx_active_64_0_39_)))) (= Verilog__main.i_rx_phy.bit_cnt_64_1_39_ (ite (not Verilog__main.i_rx_phy.rst_64_0_39_) (_ bv0 3) (ite (not Verilog__main.i_rx_phy.shift_en_64_0_39_) (_ bv0 3) (ite (and Verilog__main.i_rx_phy.fs_ce_64_0_39_ (not Verilog__main.i_rx_phy.drop_bit_64_0_39_)) (bvadd Verilog__main.i_rx_phy.bit_cnt_64_0_39_ (_ bv1 3)) Verilog__main.i_rx_phy.bit_cnt_64_0_39_)))) (= Verilog__main.i_rx_phy.rx_valid1_64_1_39_ (ite (not Verilog__main.i_rx_phy.rst_64_0_39_) false (ite (and (and Verilog__main.i_rx_phy.fs_ce_64_0_39_ (not Verilog__main.i_rx_phy.drop_bit_64_0_39_)) (= Verilog__main.i_rx_phy.bit_cnt_64_0_39_ (_ bv7 3))) true (ite (and (and Verilog__main.i_rx_phy.rx_valid1_64_0_39_ Verilog__main.i_rx_phy.fs_ce_64_0_39_) (not Verilog__main.i_rx_phy.drop_bit_64_0_39_)) false Verilog__main.i_rx_phy.rx_valid1_64_0_39_)))) (= Verilog__main.i_rx_phy.rx_valid_64_1_39_ (and (and (not Verilog__main.i_rx_phy.drop_bit_64_0_39_) Verilog__main.i_rx_phy.rx_valid1_64_0_39_) Verilog__main.i_rx_phy.fs_ce_64_0_39_)) (= Verilog__main.i_rx_phy.shift_en_64_1_39_ (ite Verilog__main.i_rx_phy.fs_ce_64_0_39_ (or Verilog__main.i_rx_phy.synced_d_64_0_39_ Verilog__main.i_rx_phy.rx_active_64_0_39_) Verilog__main.i_rx_phy.shift_en_64_0_39_)) (= Verilog__main.i_rx_phy.sd_r_64_1_39_ (ite Verilog__main.i_rx_phy.fs_ce_64_0_39_ Verilog__main.i_rx_phy.rxd_s_64_0_39_ Verilog__main.i_rx_phy.sd_r_64_0_39_)) (= Verilog__main.i_rx_phy.sd_nrzi_64_1_39_ (ite (not Verilog__main.i_rx_phy.rst_64_0_39_) false (ite (and Verilog__main.i_rx_phy.rx_active_64_0_39_ Verilog__main.i_rx_phy.fs_ce_64_0_39_) (not (xor Verilog__main.i_rx_phy.rxd_s_64_0_39_ Verilog__main.i_rx_phy.sd_r_64_0_39_)) Verilog__main.i_rx_phy.sd_nrzi_64_0_39_))) (= Verilog__main.i_rx_phy.hold_reg_64_1_39_ (ite (and (and Verilog__main.i_rx_phy.fs_ce_64_0_39_ Verilog__main.i_rx_phy.shift_en_64_0_39_) (not Verilog__main.i_rx_phy.drop_bit_64_0_39_)) (concat (ite Verilog__main.i_rx_phy.sd_nrzi_64_0_39_ (_ bv1 1) (_ bv0 1)) ((_ extract 7 1) Verilog__main.i_rx_phy.hold_reg_64_0_39_)) Verilog__main.i_rx_phy.hold_reg_64_0_39_)) (= Verilog__main.i_rx_phy.one_cnt_64_1_39_ (ite (not Verilog__main.i_rx_phy.rst_64_0_39_) (_ bv0 3) (ite (not Verilog__main.i_rx_phy.shift_en_64_0_39_) (_ bv0 3) (ite Verilog__main.i_rx_phy.fs_ce_64_0_39_ (ite (or (not Verilog__main.i_rx_phy.sd_nrzi_64_0_39_) Verilog__main.i_rx_phy.drop_bit_64_0_39_) (_ bv0 3) (bvadd Verilog__main.i_rx_phy.one_cnt_64_0_39_ (_ bv1 3))) Verilog__main.i_rx_phy.one_cnt_64_0_39_)))) (= Verilog__main.i_rx_phy.dpll_state_64_1_39_ (ite (not Verilog__main.i_rx_phy.rst_64_0_39_) (_ bv1 2) (ite (= Verilog__main.i_rx_phy.dpll_state_64_0_39_ (_ bv0 2)) (ite (and Verilog__main.i_rx_phy.lock_en_64_0_39_ Verilog__main.i_rx_phy.change_64_0_39_) (_ bv0 2) (_ bv1 2)) (ite (= Verilog__main.i_rx_phy.dpll_state_64_0_39_ (_ bv1 2)) (ite (and Verilog__main.i_rx_phy.lock_en_64_0_39_ Verilog__main.i_rx_phy.change_64_0_39_) (_ bv3 2) (_ bv2 2)) (ite (= Verilog__main.i_rx_phy.dpll_state_64_0_39_ (_ bv2 2)) (ite (and Verilog__main.i_rx_phy.lock_en_64_0_39_ Verilog__main.i_rx_phy.change_64_0_39_) (_ bv0 2) (_ bv3 2)) (ite (= Verilog__main.i_rx_phy.dpll_state_64_0_39_ (_ bv3 2)) (ite (and Verilog__main.i_rx_phy.lock_en_64_0_39_ Verilog__main.i_rx_phy.change_64_0_39_) (_ bv0 2) (_ bv0 2)) Verilog__main.i_rx_phy.dpll_state_64_0_39_)))))) (= Verilog__main.i_rx_phy.fs_ce_d_64_1_39_ (ite (not Verilog__main.i_rx_phy.rst_64_0_39_) Verilog__main.i_rx_phy.fs_ce_d_64_0_39_ (ite (= Verilog__main.i_rx_phy.dpll_state_64_0_39_ (_ bv0 2)) false (ite (= Verilog__main.i_rx_phy.dpll_state_64_0_39_ (_ bv1 2)) true false)))) (= Verilog__main.i_rx_phy.rxdp_s1r_64_1_39_ Verilog__main.i_rx_phy.rxdp_s1_64_0_39_) (= Verilog__main.i_rx_phy.rxdn_s1r_64_1_39_ Verilog__main.i_rx_phy.rxdn_s1_64_0_39_) (= Verilog__main.i_rx_phy.fs_ce_r1_64_1_39_ Verilog__main.i_rx_phy.fs_ce_d_64_0_39_) (= Verilog__main.i_rx_phy.fs_ce_r2_64_1_39_ Verilog__main.i_rx_phy.fs_ce_r1_64_0_39_) (= Verilog__main.i_rx_phy.fs_ce_r3_64_1_39_ Verilog__main.i_rx_phy.fs_ce_r2_64_0_39_) (= Verilog__main.i_rx_phy.fs_state_64_1_39_ (ite (not Verilog__main.i_rx_phy.rst_64_0_39_) (_ bv0 3) (ite Verilog__main.i_rx_phy.fs_ce_64_0_39_ (ite (= Verilog__main.i_rx_phy.fs_state_64_0_39_ (_ bv0 3)) (ite (and Verilog__main.i_rx_phy.k_64_0_39_ Verilog__main.i_rx_phy.rx_en_64_0_39_) (_ bv1 3) Verilog__main.i_rx_phy.fs_state_64_0_39_) (ite (= Verilog__main.i_rx_phy.fs_state_64_0_39_ (_ bv1 3)) (ite (and Verilog__main.i_rx_phy.j_64_0_39_ Verilog__main.i_rx_phy.rx_en_64_0_39_) (_ bv2 3) (_ bv0 3)) (ite (= Verilog__main.i_rx_phy.fs_state_64_0_39_ (_ bv2 3)) (ite (and Verilog__main.i_rx_phy.k_64_0_39_ Verilog__main.i_rx_phy.rx_en_64_0_39_) (_ bv3 3) (_ bv0 3)) (ite (= Verilog__main.i_rx_phy.fs_state_64_0_39_ (_ bv3 3)) (ite (and Verilog__main.i_rx_phy.j_64_0_39_ Verilog__main.i_rx_phy.rx_en_64_0_39_) (_ bv4 3) (_ bv0 3)) (ite (= Verilog__main.i_rx_phy.fs_state_64_0_39_ (_ bv4 3)) (ite (and Verilog__main.i_rx_phy.k_64_0_39_ Verilog__main.i_rx_phy.rx_en_64_0_39_) (_ bv5 3) (_ bv0 3)) (ite (= Verilog__main.i_rx_phy.fs_state_64_0_39_ (_ bv5 3)) (ite (and Verilog__main.i_rx_phy.j_64_0_39_ Verilog__main.i_rx_phy.rx_en_64_0_39_) (_ bv6 3) (ite (and Verilog__main.i_rx_phy.k_64_0_39_ Verilog__main.i_rx_phy.rx_en_64_0_39_) (_ bv7 3) (_ bv0 3))) (ite (= Verilog__main.i_rx_phy.fs_state_64_0_39_ (_ bv6 3)) (ite (and Verilog__main.i_rx_phy.k_64_0_39_ Verilog__main.i_rx_phy.rx_en_64_0_39_) (_ bv7 3) (_ bv0 3)) (ite (= Verilog__main.i_rx_phy.fs_state_64_0_39_ (_ bv7 3)) (_ bv0 3) Verilog__main.i_rx_phy.fs_state_64_0_39_)))))))) Verilog__main.i_rx_phy.fs_state_64_0_39_))) (= Verilog__main.i_rx_phy.rx_valid_r_64_1_39_ (ite Verilog__main.i_rx_phy.rx_valid_64_0_39_ true (ite Verilog__main.i_rx_phy.fs_ce_64_0_39_ false Verilog__main.i_rx_phy.rx_valid_r_64_0_39_)))) (= Verilog__main.usb_rst_64_1_39_ (= Verilog__main.rst_cnt_64_0_39_ (_ bv31 5))) (= Verilog__main.rst_cnt_64_1_39_ (ite (not Verilog__main.rst_64_0_39_) (_ bv0 5) (ite (not (= Verilog__main.LineState_o_64_0_39_ (_ bv0 2))) (_ bv0 5) (ite (and (not Verilog__main.usb_rst_64_0_39_) Verilog__main.fs_ce_64_0_39_) (bvadd Verilog__main.rst_cnt_64_0_39_ (_ bv1 5)) Verilog__main.rst_cnt_64_0_39_)))))) (or (and (= Verilog__main.reset_64_2 Verilog__main.reset_64_0_39_) (= Verilog__main.rst_64_2 Verilog__main.rst_64_0_39_) (= Verilog__main.usb_rst_64_2 Verilog__main.usb_rst_64_0_39_) (= Verilog__main.i_tx_phy.hold_64_2 Verilog__main.i_tx_phy.hold_64_0_39_) (= Verilog__main.i_tx_phy.stuff_64_2 Verilog__main.i_tx_phy.stuff_64_0_39_) (= Verilog__main.i_tx_phy.sft_done_e_64_2 Verilog__main.i_tx_phy.sft_done_e_64_0_39_) (= Verilog__main.i_tx_phy.sft_done_64_2 Verilog__main.i_tx_phy.sft_done_64_0_39_) (= Verilog__main.i_tx_phy.sft_done_r_64_2 Verilog__main.i_tx_phy.sft_done_r_64_0_39_) (= Verilog__main.i_tx_phy.one_cnt_64_2 Verilog__main.i_tx_phy.one_cnt_64_0_39_) (= Verilog__main.i_tx_phy.eop_done_64_2 Verilog__main.i_tx_phy.eop_done_64_0_39_) (= Verilog__main.i_tx_phy.append_eop_sync3_64_2 Verilog__main.i_tx_phy.append_eop_sync3_64_0_39_) (= Verilog__main.i_tx_phy.clk_64_2 Verilog__main.i_tx_phy.clk_64_0_39_) (= Verilog__main.clk_64_2 Verilog__main.clk_64_0_39_) (= Verilog__main.i_tx_phy.rst_64_2 Verilog__main.i_tx_phy.rst_64_0_39_) (= Verilog__main.i_tx_phy.fs_ce_64_2 Verilog__main.i_tx_phy.fs_ce_64_0_39_) (= Verilog__main.fs_ce_64_2 Verilog__main.fs_ce_64_0_39_) (= Verilog__main.i_tx_phy.phy_mode_64_2 Verilog__main.i_tx_phy.phy_mode_64_0_39_) (= Verilog__main.phy_tx_mode_64_2 Verilog__main.phy_tx_mode_64_0_39_) (= Verilog__main.i_tx_phy.txdp_64_2 Verilog__main.i_tx_phy.txdp_64_0_39_) (= Verilog__main.txdp_64_2 Verilog__main.txdp_64_0_39_) (= Verilog__main.i_tx_phy.txdn_64_2 Verilog__main.i_tx_phy.txdn_64_0_39_) (= Verilog__main.txdn_64_2 Verilog__main.txdn_64_0_39_) (= Verilog__main.i_tx_phy.txoe_64_2 Verilog__main.i_tx_phy.txoe_64_0_39_) (= Verilog__main.txoe_64_2 Verilog__main.txoe_64_0_39_) (= Verilog__main.i_tx_phy.DataOut_i_64_2 Verilog__main.i_tx_phy.DataOut_i_64_0_39_) (= Verilog__main.DataOut_i_64_2 Verilog__main.DataOut_i_64_0_39_) (= Verilog__main.i_tx_phy.TxValid_i_64_2 Verilog__main.i_tx_phy.TxValid_i_64_0_39_) (= Verilog__main.TxValid_i_64_2 Verilog__main.TxValid_i_64_0_39_) (= Verilog__main.i_tx_phy.TxReady_o_64_2 Verilog__main.i_tx_phy.TxReady_o_64_0_39_) (= Verilog__main.TxReady_o_64_2 Verilog__main.TxReady_o_64_0_39_) (= Verilog__main.i_rx_phy.RxActive_o_64_2 Verilog__main.i_rx_phy.RxActive_o_64_0_39_) (= Verilog__main.i_rx_phy.rx_active_64_2 Verilog__main.i_rx_phy.rx_active_64_0_39_) (= Verilog__main.i_rx_phy.RxValid_o_64_2 Verilog__main.i_rx_phy.RxValid_o_64_0_39_) (= Verilog__main.i_rx_phy.rx_valid_64_2 Verilog__main.i_rx_phy.rx_valid_64_0_39_) (= Verilog__main.i_rx_phy.RxError_o_64_2 Verilog__main.i_rx_phy.RxError_o_64_0_39_) (= Verilog__main.i_rx_phy.DataIn_o_64_2 Verilog__main.i_rx_phy.DataIn_o_64_0_39_) (= Verilog__main.i_rx_phy.hold_reg_64_2 Verilog__main.i_rx_phy.hold_reg_64_0_39_) (= Verilog__main.i_rx_phy.LineState_64_2 Verilog__main.i_rx_phy.LineState_64_0_39_) (= Verilog__main.i_rx_phy.rxdp_s1_64_2 Verilog__main.i_rx_phy.rxdp_s1_64_0_39_) (= Verilog__main.i_rx_phy.rxdn_s1_64_2 Verilog__main.i_rx_phy.rxdn_s1_64_0_39_) (= Verilog__main.i_rx_phy.k_64_2 Verilog__main.i_rx_phy.k_64_0_39_) (= Verilog__main.i_rx_phy.rxdp_s_64_2 Verilog__main.i_rx_phy.rxdp_s_64_0_39_) (= Verilog__main.i_rx_phy.rxdn_s_64_2 Verilog__main.i_rx_phy.rxdn_s_64_0_39_) (= Verilog__main.i_rx_phy.j_64_2 Verilog__main.i_rx_phy.j_64_0_39_) (= Verilog__main.i_rx_phy.se0_64_2 Verilog__main.i_rx_phy.se0_64_0_39_) (= Verilog__main.i_rx_phy.lock_en_64_2 Verilog__main.i_rx_phy.lock_en_64_0_39_) (= Verilog__main.i_rx_phy.rx_en_64_2 Verilog__main.i_rx_phy.rx_en_64_0_39_) (= Verilog__main.i_rx_phy.change_64_2 Verilog__main.i_rx_phy.change_64_0_39_) (= Verilog__main.i_rx_phy.rxdp_s1r_64_2 Verilog__main.i_rx_phy.rxdp_s1r_64_0_39_) (= Verilog__main.i_rx_phy.rxdn_s1r_64_2 Verilog__main.i_rx_phy.rxdn_s1r_64_0_39_) (= Verilog__main.i_rx_phy.drop_bit_64_2 Verilog__main.i_rx_phy.drop_bit_64_0_39_) (= Verilog__main.i_rx_phy.one_cnt_64_2 Verilog__main.i_rx_phy.one_cnt_64_0_39_) (= Verilog__main.i_rx_phy.clk_64_2 Verilog__main.i_rx_phy.clk_64_0_39_) (= Verilog__main.i_rx_phy.rst_64_2 Verilog__main.i_rx_phy.rst_64_0_39_) (= Verilog__main.i_rx_phy.fs_ce_64_2 Verilog__main.i_rx_phy.fs_ce_64_0_39_) (= Verilog__main.i_rx_phy.rxd_64_2 Verilog__main.i_rx_phy.rxd_64_0_39_) (= Verilog__main.rxd_64_2 Verilog__main.rxd_64_0_39_) (= Verilog__main.i_rx_phy.rxdp_64_2 Verilog__main.i_rx_phy.rxdp_64_0_39_) (= Verilog__main.rxdp_64_2 Verilog__main.rxdp_64_0_39_) (= Verilog__main.i_rx_phy.rxdn_64_2 Verilog__main.i_rx_phy.rxdn_64_0_39_) (= Verilog__main.rxdn_64_2 Verilog__main.rxdn_64_0_39_) (= Verilog__main.DataIn_o_64_2 Verilog__main.DataIn_o_64_0_39_) (= Verilog__main.RxValid_o_64_2 Verilog__main.RxValid_o_64_0_39_) (= Verilog__main.RxActive_o_64_2 Verilog__main.RxActive_o_64_0_39_) (= Verilog__main.RxError_o_64_2 Verilog__main.RxError_o_64_0_39_) (= Verilog__main.i_rx_phy.RxEn_i_64_2 Verilog__main.i_rx_phy.RxEn_i_64_0_39_) (= Verilog__main.LineState_o_64_2 Verilog__main.LineState_o_64_0_39_) (= Verilog__main.i_tx_phy.sd_bs_o_64_2 Verilog__main.i_tx_phy.sd_bs_o_64_0_39_) (= Verilog__main.i_tx_phy.sd_nrzi_o_64_2 Verilog__main.i_tx_phy.sd_nrzi_o_64_0_39_) (= Verilog__main.i_tx_phy.append_eop_64_2 Verilog__main.i_tx_phy.append_eop_64_0_39_) (= Verilog__main.i_tx_phy.append_eop_sync1_64_2 Verilog__main.i_tx_phy.append_eop_sync1_64_0_39_) (= Verilog__main.i_tx_phy.append_eop_sync2_64_2 Verilog__main.i_tx_phy.append_eop_sync2_64_0_39_) (= Verilog__main.i_tx_phy.txoe_r1_64_2 Verilog__main.i_tx_phy.txoe_r1_64_0_39_) (= Verilog__main.i_tx_phy.txoe_r2_64_2 Verilog__main.i_tx_phy.txoe_r2_64_0_39_) (= Verilog__main.i_tx_phy.state_64_2 Verilog__main.i_tx_phy.state_64_0_39_) (= Verilog__main.i_tx_phy.tx_ready_64_2 Verilog__main.i_tx_phy.tx_ready_64_0_39_) (= Verilog__main.i_tx_phy.tx_ready_d_64_2 Verilog__main.i_tx_phy.tx_ready_d_64_0_39_) (= Verilog__main.i_tx_phy.ld_sop_d_64_2 Verilog__main.i_tx_phy.ld_sop_d_64_0_39_) (= Verilog__main.i_tx_phy.ld_data_d_64_2 Verilog__main.i_tx_phy.ld_data_d_64_0_39_) (= Verilog__main.i_tx_phy.ld_eop_d_64_2 Verilog__main.i_tx_phy.ld_eop_d_64_0_39_) (= Verilog__main.i_tx_phy.tx_ip_64_2 Verilog__main.i_tx_phy.tx_ip_64_0_39_) (= Verilog__main.i_tx_phy.tx_ip_sync_64_2 Verilog__main.i_tx_phy.tx_ip_sync_64_0_39_) (= Verilog__main.i_tx_phy.bit_cnt_64_2 Verilog__main.i_tx_phy.bit_cnt_64_0_39_) (= Verilog__main.i_tx_phy.hold_reg_64_2 Verilog__main.i_tx_phy.hold_reg_64_0_39_) (= Verilog__main.i_tx_phy.sd_raw_o_64_2 Verilog__main.i_tx_phy.sd_raw_o_64_0_39_) (= Verilog__main.i_tx_phy.data_done_64_2 Verilog__main.i_tx_phy.data_done_64_0_39_) (= Verilog__main.i_tx_phy.ld_data_64_2 Verilog__main.i_tx_phy.ld_data_64_0_39_) (= Verilog__main.i_rx_phy.rxd_t1_64_2 Verilog__main.i_rx_phy.rxd_t1_64_0_39_) (= Verilog__main.i_rx_phy.rxd_s1_64_2 Verilog__main.i_rx_phy.rxd_s1_64_0_39_) (= Verilog__main.i_rx_phy.rxd_s_64_2 Verilog__main.i_rx_phy.rxd_s_64_0_39_) (= Verilog__main.i_rx_phy.rxdp_t1_64_2 Verilog__main.i_rx_phy.rxdp_t1_64_0_39_) (= Verilog__main.i_rx_phy.rxdn_t1_64_2 Verilog__main.i_rx_phy.rxdn_t1_64_0_39_) (= Verilog__main.i_rx_phy.synced_d_64_2 Verilog__main.i_rx_phy.synced_d_64_0_39_) (= Verilog__main.i_rx_phy.bit_cnt_64_2 Verilog__main.i_rx_phy.bit_cnt_64_0_39_) (= Verilog__main.i_rx_phy.rx_valid1_64_2 Verilog__main.i_rx_phy.rx_valid1_64_0_39_) (= Verilog__main.i_rx_phy.shift_en_64_2 Verilog__main.i_rx_phy.shift_en_64_0_39_) (= Verilog__main.i_rx_phy.sd_r_64_2 Verilog__main.i_rx_phy.sd_r_64_0_39_) (= Verilog__main.i_rx_phy.sd_nrzi_64_2 Verilog__main.i_rx_phy.sd_nrzi_64_0_39_) (= Verilog__main.i_rx_phy.dpll_state_64_2 Verilog__main.i_rx_phy.dpll_state_64_0_39_) (= Verilog__main.i_rx_phy.fs_ce_d_64_2 Verilog__main.i_rx_phy.fs_ce_d_64_0_39_) (= Verilog__main.i_rx_phy.fs_ce_r1_64_2 Verilog__main.i_rx_phy.fs_ce_r1_64_0_39_) (= Verilog__main.i_rx_phy.fs_ce_r2_64_2 Verilog__main.i_rx_phy.fs_ce_r2_64_0_39_) (= Verilog__main.i_rx_phy.fs_ce_r3_64_2 Verilog__main.i_rx_phy.fs_ce_r3_64_0_39_) (= Verilog__main.i_rx_phy.fs_state_64_2 Verilog__main.i_rx_phy.fs_state_64_0_39_) (= Verilog__main.i_rx_phy.rx_valid_r_64_2 Verilog__main.i_rx_phy.rx_valid_r_64_0_39_) (= Verilog__main.rst_cnt_64_2 Verilog__main.rst_cnt_64_0_39_)) (and (= Verilog__main.reset_64_2 Verilog__main.reset_64_1_39_) (= Verilog__main.rst_64_2 Verilog__main.rst_64_1_39_) (= Verilog__main.usb_rst_64_2 Verilog__main.usb_rst_64_1_39_) (= Verilog__main.i_tx_phy.hold_64_2 Verilog__main.i_tx_phy.hold_64_1_39_) (= Verilog__main.i_tx_phy.stuff_64_2 Verilog__main.i_tx_phy.stuff_64_1_39_) (= Verilog__main.i_tx_phy.sft_done_e_64_2 Verilog__main.i_tx_phy.sft_done_e_64_1_39_) (= Verilog__main.i_tx_phy.sft_done_64_2 Verilog__main.i_tx_phy.sft_done_64_1_39_) (= Verilog__main.i_tx_phy.sft_done_r_64_2 Verilog__main.i_tx_phy.sft_done_r_64_1_39_) (= Verilog__main.i_tx_phy.one_cnt_64_2 Verilog__main.i_tx_phy.one_cnt_64_1_39_) (= Verilog__main.i_tx_phy.eop_done_64_2 Verilog__main.i_tx_phy.eop_done_64_1_39_) (= Verilog__main.i_tx_phy.append_eop_sync3_64_2 Verilog__main.i_tx_phy.append_eop_sync3_64_1_39_) (= Verilog__main.i_tx_phy.clk_64_2 Verilog__main.i_tx_phy.clk_64_1_39_) (= Verilog__main.clk_64_2 Verilog__main.clk_64_1_39_) (= Verilog__main.i_tx_phy.rst_64_2 Verilog__main.i_tx_phy.rst_64_1_39_) (= Verilog__main.i_tx_phy.fs_ce_64_2 Verilog__main.i_tx_phy.fs_ce_64_1_39_) (= Verilog__main.fs_ce_64_2 Verilog__main.fs_ce_64_1_39_) (= Verilog__main.i_tx_phy.phy_mode_64_2 Verilog__main.i_tx_phy.phy_mode_64_1_39_) (= Verilog__main.phy_tx_mode_64_2 Verilog__main.phy_tx_mode_64_1_39_) (= Verilog__main.i_tx_phy.txdp_64_2 Verilog__main.i_tx_phy.txdp_64_1_39_) (= Verilog__main.txdp_64_2 Verilog__main.txdp_64_1_39_) (= Verilog__main.i_tx_phy.txdn_64_2 Verilog__main.i_tx_phy.txdn_64_1_39_) (= Verilog__main.txdn_64_2 Verilog__main.txdn_64_1_39_) (= Verilog__main.i_tx_phy.txoe_64_2 Verilog__main.i_tx_phy.txoe_64_1_39_) (= Verilog__main.txoe_64_2 Verilog__main.txoe_64_1_39_) (= Verilog__main.i_tx_phy.DataOut_i_64_2 Verilog__main.i_tx_phy.DataOut_i_64_1_39_) (= Verilog__main.DataOut_i_64_2 Verilog__main.DataOut_i_64_1_39_) (= Verilog__main.i_tx_phy.TxValid_i_64_2 Verilog__main.i_tx_phy.TxValid_i_64_1_39_) (= Verilog__main.TxValid_i_64_2 Verilog__main.TxValid_i_64_1_39_) (= Verilog__main.i_tx_phy.TxReady_o_64_2 Verilog__main.i_tx_phy.TxReady_o_64_1_39_) (= Verilog__main.TxReady_o_64_2 Verilog__main.TxReady_o_64_1_39_) (= Verilog__main.i_rx_phy.RxActive_o_64_2 Verilog__main.i_rx_phy.RxActive_o_64_1_39_) (= Verilog__main.i_rx_phy.rx_active_64_2 Verilog__main.i_rx_phy.rx_active_64_1_39_) (= Verilog__main.i_rx_phy.RxValid_o_64_2 Verilog__main.i_rx_phy.RxValid_o_64_1_39_) (= Verilog__main.i_rx_phy.rx_valid_64_2 Verilog__main.i_rx_phy.rx_valid_64_1_39_) (= Verilog__main.i_rx_phy.RxError_o_64_2 Verilog__main.i_rx_phy.RxError_o_64_1_39_) (= Verilog__main.i_rx_phy.DataIn_o_64_2 Verilog__main.i_rx_phy.DataIn_o_64_1_39_) (= Verilog__main.i_rx_phy.hold_reg_64_2 Verilog__main.i_rx_phy.hold_reg_64_1_39_) (= Verilog__main.i_rx_phy.LineState_64_2 Verilog__main.i_rx_phy.LineState_64_1_39_) (= Verilog__main.i_rx_phy.rxdp_s1_64_2 Verilog__main.i_rx_phy.rxdp_s1_64_1_39_) (= Verilog__main.i_rx_phy.rxdn_s1_64_2 Verilog__main.i_rx_phy.rxdn_s1_64_1_39_) (= Verilog__main.i_rx_phy.k_64_2 Verilog__main.i_rx_phy.k_64_1_39_) (= Verilog__main.i_rx_phy.rxdp_s_64_2 Verilog__main.i_rx_phy.rxdp_s_64_1_39_) (= Verilog__main.i_rx_phy.rxdn_s_64_2 Verilog__main.i_rx_phy.rxdn_s_64_1_39_) (= Verilog__main.i_rx_phy.j_64_2 Verilog__main.i_rx_phy.j_64_1_39_) (= Verilog__main.i_rx_phy.se0_64_2 Verilog__main.i_rx_phy.se0_64_1_39_) (= Verilog__main.i_rx_phy.lock_en_64_2 Verilog__main.i_rx_phy.lock_en_64_1_39_) (= Verilog__main.i_rx_phy.rx_en_64_2 Verilog__main.i_rx_phy.rx_en_64_1_39_) (= Verilog__main.i_rx_phy.change_64_2 Verilog__main.i_rx_phy.change_64_1_39_) (= Verilog__main.i_rx_phy.rxdp_s1r_64_2 Verilog__main.i_rx_phy.rxdp_s1r_64_1_39_) (= Verilog__main.i_rx_phy.rxdn_s1r_64_2 Verilog__main.i_rx_phy.rxdn_s1r_64_1_39_) (= Verilog__main.i_rx_phy.drop_bit_64_2 Verilog__main.i_rx_phy.drop_bit_64_1_39_) (= Verilog__main.i_rx_phy.one_cnt_64_2 Verilog__main.i_rx_phy.one_cnt_64_1_39_) (= Verilog__main.i_rx_phy.clk_64_2 Verilog__main.i_rx_phy.clk_64_1_39_) (= Verilog__main.i_rx_phy.rst_64_2 Verilog__main.i_rx_phy.rst_64_1_39_) (= Verilog__main.i_rx_phy.fs_ce_64_2 Verilog__main.i_rx_phy.fs_ce_64_1_39_) (= Verilog__main.i_rx_phy.rxd_64_2 Verilog__main.i_rx_phy.rxd_64_1_39_) (= Verilog__main.rxd_64_2 Verilog__main.rxd_64_1_39_) (= Verilog__main.i_rx_phy.rxdp_64_2 Verilog__main.i_rx_phy.rxdp_64_1_39_) (= Verilog__main.rxdp_64_2 Verilog__main.rxdp_64_1_39_) (= Verilog__main.i_rx_phy.rxdn_64_2 Verilog__main.i_rx_phy.rxdn_64_1_39_) (= Verilog__main.rxdn_64_2 Verilog__main.rxdn_64_1_39_) (= Verilog__main.DataIn_o_64_2 Verilog__main.DataIn_o_64_1_39_) (= Verilog__main.RxValid_o_64_2 Verilog__main.RxValid_o_64_1_39_) (= Verilog__main.RxActive_o_64_2 Verilog__main.RxActive_o_64_1_39_) (= Verilog__main.RxError_o_64_2 Verilog__main.RxError_o_64_1_39_) (= Verilog__main.i_rx_phy.RxEn_i_64_2 Verilog__main.i_rx_phy.RxEn_i_64_1_39_) (= Verilog__main.LineState_o_64_2 Verilog__main.LineState_o_64_1_39_) (= Verilog__main.i_tx_phy.sd_bs_o_64_2 Verilog__main.i_tx_phy.sd_bs_o_64_1_39_) (= Verilog__main.i_tx_phy.sd_nrzi_o_64_2 Verilog__main.i_tx_phy.sd_nrzi_o_64_1_39_) (= Verilog__main.i_tx_phy.append_eop_64_2 Verilog__main.i_tx_phy.append_eop_64_1_39_) (= Verilog__main.i_tx_phy.append_eop_sync1_64_2 Verilog__main.i_tx_phy.append_eop_sync1_64_1_39_) (= Verilog__main.i_tx_phy.append_eop_sync2_64_2 Verilog__main.i_tx_phy.append_eop_sync2_64_1_39_) (= Verilog__main.i_tx_phy.txoe_r1_64_2 Verilog__main.i_tx_phy.txoe_r1_64_1_39_) (= Verilog__main.i_tx_phy.txoe_r2_64_2 Verilog__main.i_tx_phy.txoe_r2_64_1_39_) (= Verilog__main.i_tx_phy.state_64_2 Verilog__main.i_tx_phy.state_64_1_39_) (= Verilog__main.i_tx_phy.tx_ready_64_2 Verilog__main.i_tx_phy.tx_ready_64_1_39_) (= Verilog__main.i_tx_phy.tx_ready_d_64_2 Verilog__main.i_tx_phy.tx_ready_d_64_1_39_) (= Verilog__main.i_tx_phy.ld_sop_d_64_2 Verilog__main.i_tx_phy.ld_sop_d_64_1_39_) (= Verilog__main.i_tx_phy.ld_data_d_64_2 Verilog__main.i_tx_phy.ld_data_d_64_1_39_) (= Verilog__main.i_tx_phy.ld_eop_d_64_2 Verilog__main.i_tx_phy.ld_eop_d_64_1_39_) (= Verilog__main.i_tx_phy.tx_ip_64_2 Verilog__main.i_tx_phy.tx_ip_64_1_39_) (= Verilog__main.i_tx_phy.tx_ip_sync_64_2 Verilog__main.i_tx_phy.tx_ip_sync_64_1_39_) (= Verilog__main.i_tx_phy.bit_cnt_64_2 Verilog__main.i_tx_phy.bit_cnt_64_1_39_) (= Verilog__main.i_tx_phy.hold_reg_64_2 Verilog__main.i_tx_phy.hold_reg_64_1_39_) (= Verilog__main.i_tx_phy.sd_raw_o_64_2 Verilog__main.i_tx_phy.sd_raw_o_64_1_39_) (= Verilog__main.i_tx_phy.data_done_64_2 Verilog__main.i_tx_phy.data_done_64_1_39_) (= Verilog__main.i_tx_phy.ld_data_64_2 Verilog__main.i_tx_phy.ld_data_64_1_39_) (= Verilog__main.i_rx_phy.rxd_t1_64_2 Verilog__main.i_rx_phy.rxd_t1_64_1_39_) (= Verilog__main.i_rx_phy.rxd_s1_64_2 Verilog__main.i_rx_phy.rxd_s1_64_1_39_) (= Verilog__main.i_rx_phy.rxd_s_64_2 Verilog__main.i_rx_phy.rxd_s_64_1_39_) (= Verilog__main.i_rx_phy.rxdp_t1_64_2 Verilog__main.i_rx_phy.rxdp_t1_64_1_39_) (= Verilog__main.i_rx_phy.rxdn_t1_64_2 Verilog__main.i_rx_phy.rxdn_t1_64_1_39_) (= Verilog__main.i_rx_phy.synced_d_64_2 Verilog__main.i_rx_phy.synced_d_64_1_39_) (= Verilog__main.i_rx_phy.bit_cnt_64_2 Verilog__main.i_rx_phy.bit_cnt_64_1_39_) (= Verilog__main.i_rx_phy.rx_valid1_64_2 Verilog__main.i_rx_phy.rx_valid1_64_1_39_) (= Verilog__main.i_rx_phy.shift_en_64_2 Verilog__main.i_rx_phy.shift_en_64_1_39_) (= Verilog__main.i_rx_phy.sd_r_64_2 Verilog__main.i_rx_phy.sd_r_64_1_39_) (= Verilog__main.i_rx_phy.sd_nrzi_64_2 Verilog__main.i_rx_phy.sd_nrzi_64_1_39_) (= Verilog__main.i_rx_phy.dpll_state_64_2 Verilog__main.i_rx_phy.dpll_state_64_1_39_) (= Verilog__main.i_rx_phy.fs_ce_d_64_2 Verilog__main.i_rx_phy.fs_ce_d_64_1_39_) (= Verilog__main.i_rx_phy.fs_ce_r1_64_2 Verilog__main.i_rx_phy.fs_ce_r1_64_1_39_) (= Verilog__main.i_rx_phy.fs_ce_r2_64_2 Verilog__main.i_rx_phy.fs_ce_r2_64_1_39_) (= Verilog__main.i_rx_phy.fs_ce_r3_64_2 Verilog__main.i_rx_phy.fs_ce_r3_64_1_39_) (= Verilog__main.i_rx_phy.fs_state_64_2 Verilog__main.i_rx_phy.fs_state_64_1_39_) (= Verilog__main.i_rx_phy.rx_valid_r_64_2 Verilog__main.i_rx_phy.rx_valid_r_64_1_39_) (= Verilog__main.rst_cnt_64_2 Verilog__main.rst_cnt_64_1_39_))))) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )) +(check-sat) +(exit) diff --git a/test/unit/util/stats_black.h b/test/unit/util/stats_black.h index 9f06b469f..c63648581 100644 --- a/test/unit/util/stats_black.h +++ b/test/unit/util/stats_black.h @@ -172,7 +172,6 @@ public: "true\n" "[(0 : 1), (5 : 2), (6 : 1), (10 : 2)]\n" "<unsupported>"; - std::cout << buf << std::endl; TS_ASSERT(strncmp(expected, buf, file_size) == 0); delete[] buf; |