From: ajreynol Date: Mon, 15 May 2017 14:48:07 +0000 (-0500) Subject: Fix issue in ceg_instantiator related to types and theoryOf, fixes bug 802. X-Git-Tag: cvc5-1.0.0~5803 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=07dd06978875e3275bdebe6bd8495aef34861e8c;p=cvc5.git Fix issue in ceg_instantiator related to types and theoryOf, fixes bug 802. --- 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 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; igetTheoryEngine()->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 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/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/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)