verilog/rtl/unit_test/cover/model/design_smt2.smt2

; SMT-LIBv2 description generated by Yosys 0.15+11 (git sha1 cbece4af0, clang 10.0.0-4ubuntu1 -fPIC -Os)
; yosys-smt2-module hyperram
(declare-sort |hyperram_s| 0)
(declare-fun |hyperram_is| (|hyperram_s|) Bool)
(declare-fun |hyperram#0| (|hyperram_s|) (_ BitVec 1)) ; $formal$hyperram.v:296$1_CHECK
; yosys-smt2-register $formal$hyperram.v:296$1_CHECK 1
(define-fun |hyperram_n $formal$hyperram.v:296$1_CHECK| ((state |hyperram_s|)) Bool (= ((_ extract 0 0) (|hyperram#0| state)) #b1))
(declare-fun |hyperram#1| (|hyperram_s|) (_ BitVec 1)) ; $formal$hyperram.v:296$1_EN
; yosys-smt2-register $formal$hyperram.v:296$1_EN 1
(define-fun |hyperram_n $formal$hyperram.v:296$1_EN| ((state |hyperram_s|)) Bool (= ((_ extract 0 0) (|hyperram#1| state)) #b1))
(declare-fun |hyperram#2| (|hyperram_s|) (_ BitVec 1)) ; $formal$hyperram.v:297$2_CHECK
; yosys-smt2-register $formal$hyperram.v:297$2_CHECK 1
(define-fun |hyperram_n $formal$hyperram.v:297$2_CHECK| ((state |hyperram_s|)) Bool (= ((_ extract 0 0) (|hyperram#2| state)) #b1))
(declare-fun |hyperram#3| (|hyperram_s|) (_ BitVec 1)) ; $formal$hyperram.v:298$3_CHECK
; yosys-smt2-register $formal$hyperram.v:298$3_CHECK 1
(define-fun |hyperram_n $formal$hyperram.v:298$3_CHECK| ((state |hyperram_s|)) Bool (= ((_ extract 0 0) (|hyperram#3| state)) #b1))
(declare-fun |hyperram#4| (|hyperram_s|) (_ BitVec 1)) ; $formal$hyperram.v:299$4_CHECK
; yosys-smt2-register $formal$hyperram.v:299$4_CHECK 1
(define-fun |hyperram_n $formal$hyperram.v:299$4_CHECK| ((state |hyperram_s|)) Bool (= ((_ extract 0 0) (|hyperram#4| state)) #b1))
(declare-fun |hyperram#5| (|hyperram_s|) (_ BitVec 1)) ; $formal$hyperram.v:300$5_CHECK
; yosys-smt2-register $formal$hyperram.v:300$5_CHECK 1
(define-fun |hyperram_n $formal$hyperram.v:300$5_CHECK| ((state |hyperram_s|)) Bool (= ((_ extract 0 0) (|hyperram#5| state)) #b1))
(declare-fun |hyperram#6| (|hyperram_s|) (_ BitVec 1)) ; $formal$hyperram.v:301$6_CHECK
; yosys-smt2-register $formal$hyperram.v:301$6_CHECK 1
(define-fun |hyperram_n $formal$hyperram.v:301$6_CHECK| ((state |hyperram_s|)) Bool (= ((_ extract 0 0) (|hyperram#6| state)) #b1))
(declare-fun |hyperram#7| (|hyperram_s|) (_ BitVec 1)) ; $formal$hyperram.v:302$7_CHECK
; yosys-smt2-register $formal$hyperram.v:302$7_CHECK 1
(define-fun |hyperram_n $formal$hyperram.v:302$7_CHECK| ((state |hyperram_s|)) Bool (= ((_ extract 0 0) (|hyperram#7| state)) #b1))
(declare-fun |hyperram#8| (|hyperram_s|) (_ BitVec 1)) ; $formal$hyperram.v:303$8_CHECK
; yosys-smt2-register $formal$hyperram.v:303$8_CHECK 1
(define-fun |hyperram_n $formal$hyperram.v:303$8_CHECK| ((state |hyperram_s|)) Bool (= ((_ extract 0 0) (|hyperram#8| state)) #b1))
(declare-fun |hyperram#9| (|hyperram_s|) (_ BitVec 1)) ; $formal$hyperram.v:304$9_CHECK
; yosys-smt2-register $formal$hyperram.v:304$9_CHECK 1
(define-fun |hyperram_n $formal$hyperram.v:304$9_CHECK| ((state |hyperram_s|)) Bool (= ((_ extract 0 0) (|hyperram#9| state)) #b1))
; yosys-smt2-input address 32
; yosys-smt2-wire address 32
(define-fun |hyperram_n address| ((state |hyperram_s|)) (_ BitVec 32) #b00010010001101000101011001111000)
(declare-fun |hyperram#10| (|hyperram_s|) (_ BitVec 1)) ; \ck
; yosys-smt2-output ck 1
; yosys-smt2-register ck 1
; yosys-smt2-wire ck 1
(define-fun |hyperram_n ck| ((state |hyperram_s|)) Bool (= ((_ extract 0 0) (|hyperram#10| state)) #b1))
(define-fun |hyperram#11| ((state |hyperram_s|)) Bool (not (or  (= ((_ extract 0 0) (|hyperram#10| state)) #b1) false))) ; \ck_bar
; yosys-smt2-output ck_bar 1
; yosys-smt2-wire ck_bar 1
(define-fun |hyperram_n ck_bar| ((state |hyperram_s|)) Bool (|hyperram#11| state))
(declare-fun |hyperram#12| (|hyperram_s|) Bool) ; \clk
; yosys-smt2-input clk 1
; yosys-smt2-wire clk 1
; yosys-smt2-clock clk posedge
(define-fun |hyperram_n clk| ((state |hyperram_s|)) Bool (|hyperram#12| state))
(declare-fun |hyperram#13| (|hyperram_s|) (_ BitVec 48)) ; \command_address
; yosys-smt2-register command_address 48
; yosys-smt2-wire command_address 48
(define-fun |hyperram_n command_address| ((state |hyperram_s|)) (_ BitVec 48) (|hyperram#13| state))
(declare-fun |hyperram#14| (|hyperram_s|) (_ BitVec 7)) ; \control_state
; yosys-smt2-register control_state 7
; yosys-smt2-wire control_state 7
(define-fun |hyperram_n control_state| ((state |hyperram_s|)) (_ BitVec 7) (|hyperram#14| state))
(define-fun |hyperram#15| ((state |hyperram_s|)) Bool (not (or  (= ((_ extract 0 0) (|hyperram#14| state)) #b1) (= ((_ extract 1 1) (|hyperram#14| state)) #b1) (= ((_ extract 2 2) (|hyperram#14| state)) #b1) (= ((_ extract 3 3) (|hyperram#14| state)) #b1) (= ((_ extract 4 4) (|hyperram#14| state)) #b1) (= ((_ extract 5 5) (|hyperram#14| state)) #b1) (= ((_ extract 6 6) (|hyperram#14| state)) #b1)))) ; $0$formal$hyperram.v:296$1_CHECK[0:0]$51
(define-fun |hyperram#16| ((state |hyperram_s|)) (_ BitVec 1) (ite (|hyperram#15| state) #b1 #b0)) ; \transaction_end
; yosys-smt2-output cs_bar 1
; yosys-smt2-wire cs_bar 1
(define-fun |hyperram_n cs_bar| ((state |hyperram_s|)) Bool (= ((_ extract 0 0) (|hyperram#16| state)) #b1))
; yosys-smt2-output data_in 32
; yosys-smt2-wire data_in 32
(define-fun |hyperram_n data_in| ((state |hyperram_s|)) (_ BitVec 32) #b10101010101010101011101110111011)
; yosys-smt2-wire data_in_register 32
(define-fun |hyperram_n data_in_register| ((state |hyperram_s|)) (_ BitVec 32) #b10101010101010101011101110111011)
; yosys-smt2-input data_out 32
; yosys-smt2-wire data_out 32
(define-fun |hyperram_n data_out| ((state |hyperram_s|)) (_ BitVec 32) #b11001100110011001101110111011101)
(declare-fun |hyperram#17| (|hyperram_s|) (_ BitVec 31)) ; \data_out_register [30:0]
; yosys-smt2-register data_out_register 32
; yosys-smt2-wire data_out_register 32
(define-fun |hyperram_n data_out_register| ((state |hyperram_s|)) (_ BitVec 32) (concat ((_ extract 30 30) (|hyperram#17| state)) (|hyperram#17| state)))
(declare-fun |hyperram#18| (|hyperram_s|) (_ BitVec 8)) ; \done_counter
; yosys-smt2-register done_counter 8
; yosys-smt2-wire done_counter 8
(define-fun |hyperram_n done_counter| ((state |hyperram_s|)) (_ BitVec 8) (|hyperram#18| state))
(declare-fun |hyperram#19| (|hyperram_s|) (_ BitVec 6)) ; \done_latency
; yosys-smt2-input done_latency 6
; yosys-smt2-wire done_latency 6
(define-fun |hyperram_n done_latency| ((state |hyperram_s|)) (_ BitVec 6) (|hyperram#19| state))
; yosys-smt2-anyseq hyperram#20 8 $auto$setundef.cc:501:execute$433
(declare-fun |hyperram#20| (|hyperram_s|) (_ BitVec 8)) ; $auto$rtlil.cc:3133:Anyseq$434
; yosys-smt2-anyseq hyperram#21 8 $auto$setundef.cc:501:execute$431
(declare-fun |hyperram#21| (|hyperram_s|) (_ BitVec 8)) ; $auto$rtlil.cc:3133:Anyseq$432
(define-fun |hyperram#22| ((state |hyperram_s|)) Bool (= (|hyperram#14| state) #b0001011)) ; $eq$hyperram.v:272$48_Y
(define-fun |hyperram#23| ((state |hyperram_s|)) Bool (= (|hyperram#14| state) #b0001010)) ; $procmux$217_CMP
(define-fun |hyperram#24| ((state |hyperram_s|)) Bool (= (|hyperram#14| state) #b0001001)) ; $procmux$218_CMP
(define-fun |hyperram#25| ((state |hyperram_s|)) Bool (= (|hyperram#14| state) #b0001000)) ; $0$formal$hyperram.v:299$4_CHECK[0:0]$57
(define-fun |hyperram#26| ((state |hyperram_s|)) Bool (= (|hyperram#14| state) #b0000110)) ; $0$formal$hyperram.v:297$2_CHECK[0:0]$53
(define-fun |hyperram#27| ((state |hyperram_s|)) Bool (= (|hyperram#14| state) #b0000101)) ; $procmux$222_CMP
(define-fun |hyperram#28| ((state |hyperram_s|)) Bool (= (|hyperram#14| state) #b0000100)) ; $procmux$223_CMP
(define-fun |hyperram#29| ((state |hyperram_s|)) Bool (= (|hyperram#14| state) #b0000011)) ; $procmux$224_CMP
(define-fun |hyperram#30| ((state |hyperram_s|)) Bool (= (|hyperram#14| state) #b0000010)) ; $procmux$225_CMP
(define-fun |hyperram#31| ((state |hyperram_s|)) Bool (= (|hyperram#14| state) #b0000001)) ; $procmux$226_CMP
(define-fun |hyperram#32| ((state |hyperram_s|)) (_ BitVec 8) (ite (|hyperram#31| state) ((_ extract 47 40) (|hyperram#13| state)) (ite (|hyperram#30| state) ((_ extract 39 32) (|hyperram#13| state)) (ite (|hyperram#29| state) ((_ extract 31 24) (|hyperram#13| state)) (ite (|hyperram#28| state) ((_ extract 23 16) (|hyperram#13| state)) (ite (|hyperram#27| state) ((_ extract 15 8) (|hyperram#13| state)) (ite (|hyperram#26| state) ((_ extract 7 0) (|hyperram#13| state)) (ite (|hyperram#25| state) ((_ extract 7 0) (|hyperram#17| state)) (ite (|hyperram#24| state) ((_ extract 15 8) (|hyperram#17| state)) (ite (|hyperram#23| state) ((_ extract 23 16) (|hyperram#17| state)) (ite (|hyperram#22| state) (concat ((_ extract 30 30) (|hyperram#17| state)) ((_ extract 30 24) (|hyperram#17| state))) (|hyperram#21| state)))))))))))) ; \dq_out
(define-fun |hyperram#33| ((state |hyperram_s|)) Bool (or  (|hyperram#22| state) (|hyperram#26| state) (|hyperram#25| state) (|hyperram#23| state) (|hyperram#24| state) (|hyperram#27| state) (|hyperram#28| state) (|hyperram#29| state) (|hyperram#30| state) (|hyperram#31| state))) ; $auto$opt_reduce.cc:134:opt_pmux$422
(define-fun |hyperram#34| ((state |hyperram_s|)) (_ BitVec 1) (ite (|hyperram#33| state) #b1 #b0)) ; \dq_oe
(define-fun |hyperram#35| ((state |hyperram_s|)) (_ BitVec 8) (ite (= ((_ extract 0 0) (|hyperram#34| state)) #b1) (|hyperram#32| state) (|hyperram#20| state))) ; \dq
; yosys-smt2-input dq 8
; yosys-smt2-output dq 8
; yosys-smt2-wire dq 8
(define-fun |hyperram_n dq| ((state |hyperram_s|)) (_ BitVec 8) (|hyperram#35| state))
; yosys-smt2-wire dq_oe 1
(define-fun |hyperram_n dq_oe| ((state |hyperram_s|)) Bool (= ((_ extract 0 0) (|hyperram#34| state)) #b1))
; yosys-smt2-wire dq_out 8
(define-fun |hyperram_n dq_out| ((state |hyperram_s|)) (_ BitVec 8) (|hyperram#32| state))
(declare-fun |hyperram#36| (|hyperram_s|) Bool) ; \write_enable
(define-fun |hyperram#37| ((state |hyperram_s|)) Bool (not (or  (|hyperram#36| state) false))) ; \next_command_address [47]
; yosys-smt2-wire next_command_address 48
(define-fun |hyperram_n next_command_address| ((state |hyperram_s|)) (_ BitVec 48) (concat (ite (|hyperram#37| state) #b1 #b0) #b01000000000011010001010110011110000000000000000))
(define-fun |hyperram#38| ((state |hyperram_s|)) Bool (= (|hyperram#18| state) #b00000100)) ; $eq$hyperram.v:227$41_Y
(define-fun |hyperram#39| ((state |hyperram_s|)) (_ BitVec 7) (ite (|hyperram#38| state) #b0000000 #b0000000)) ; $6\next_control_state[6:0]
(define-fun |hyperram#40| ((state |hyperram_s|)) (_ BitVec 7) (bvadd (|hyperram#14| state) #b0000001)) ; $add$hyperram.v:109$23_Y
; yosys-smt2-anyseq hyperram#41 1 $auto$setundef.cc:501:execute$435
(declare-fun |hyperram#41| (|hyperram_s|) (_ BitVec 1)) ; $auto$rtlil.cc:3133:Anyseq$436
; yosys-smt2-anyseq hyperram#42 1 $auto$setundef.cc:501:execute$429
(declare-fun |hyperram#42| (|hyperram_s|) (_ BitVec 1)) ; $auto$rtlil.cc:3133:Anyseq$430
(declare-fun |hyperram#43| (|hyperram_s|) (_ BitVec 4)) ; \write_mask_register
(define-fun |hyperram#44| ((state |hyperram_s|)) (_ BitVec 1) (ite (|hyperram#25| state) ((_ extract 0 0) (|hyperram#43| state)) (ite (|hyperram#24| state) ((_ extract 1 1) (|hyperram#43| state)) (ite (|hyperram#23| state) ((_ extract 2 2) (|hyperram#43| state)) (ite (|hyperram#22| state) ((_ extract 3 3) (|hyperram#43| state)) (|hyperram#42| state)))))) ; \rwds_out
(define-fun |hyperram#45| ((state |hyperram_s|)) Bool (or  (|hyperram#22| state) (|hyperram#25| state) (|hyperram#23| state) (|hyperram#24| state))) ; $auto$opt_reduce.cc:134:opt_pmux$420
(define-fun |hyperram#46| ((state |hyperram_s|)) (_ BitVec 1) (ite (|hyperram#45| state) #b1 #b0)) ; \rwds_oe
(define-fun |hyperram#47| ((state |hyperram_s|)) (_ BitVec 1) (ite (= ((_ extract 0 0) (|hyperram#46| state)) #b1) (|hyperram#44| state) (|hyperram#41| state))) ; \rwds
(declare-fun |hyperram#48| (|hyperram_s|) Bool) ; \timed_read
(define-fun |hyperram#49| ((state |hyperram_s|)) Bool (or  (= ((_ extract 0 0) (|hyperram#47| state)) #b1) false  (|hyperram#48| state) false)) ; $logic_or$hyperram.v:201$35_Y
(define-fun |hyperram#50| ((state |hyperram_s|)) (_ BitVec 7) (ite (|hyperram#49| state) (|hyperram#40| state) #b0000000)) ; $5\next_control_state[6:0]
(define-fun |hyperram#51| ((state |hyperram_s|)) (_ BitVec 3) (ite (= ((_ extract 47 47) (|hyperram#13| state)) #b1) #b100 #b000)) ; $4\next_control_state[6:0]
(declare-fun |hyperram#52| (|hyperram_s|) (_ BitVec 8)) ; \wait_counter
(define-fun |hyperram#53| ((state |hyperram_s|)) Bool (= (|hyperram#52| state) #b00000100)) ; $eq$hyperram.v:154$31_Y
(define-fun |hyperram#54| ((state |hyperram_s|)) (_ BitVec 7) (ite (|hyperram#53| state) (concat #b0001 (|hyperram#51| state)) #b0000000)) ; $3\next_control_state[6:0]
(declare-fun |hyperram#55| (|hyperram_s|) (_ BitVec 1)) ; \transaction_begin
(define-fun |hyperram#56| ((state |hyperram_s|)) (_ BitVec 7) (ite (= ((_ extract 0 0) (|hyperram#55| state)) #b1) (|hyperram#40| state) #b0000000)) ; $2\next_control_state[6:0]
(define-fun |hyperram#57| ((state |hyperram_s|)) Bool (= (|hyperram#14| state) #b0010000)) ; $0$formal$hyperram.v:301$6_CHECK[0:0]$61
(define-fun |hyperram#58| ((state |hyperram_s|)) Bool (= (|hyperram#14| state) #b0001111)) ; $eq$hyperram.v:269$46_Y
(define-fun |hyperram#59| ((state |hyperram_s|)) Bool (= (|hyperram#14| state) #b0001110)) ; $procmux$213_CMP
(define-fun |hyperram#60| ((state |hyperram_s|)) Bool (= (|hyperram#14| state) #b0001101)) ; $procmux$214_CMP
(define-fun |hyperram#61| ((state |hyperram_s|)) Bool (or  (|hyperram#58| state) (|hyperram#26| state) (|hyperram#25| state) (|hyperram#59| state) (|hyperram#60| state) (|hyperram#23| state) (|hyperram#24| state) (|hyperram#27| state) (|hyperram#28| state) (|hyperram#29| state) (|hyperram#30| state) (|hyperram#31| state))) ; $auto$opt_reduce.cc:134:opt_pmux$418
(define-fun |hyperram#62| ((state |hyperram_s|)) Bool (= (|hyperram#14| state) #b0001100)) ; $0$formal$hyperram.v:300$5_CHECK[0:0]$59
(define-fun |hyperram#63| ((state |hyperram_s|)) Bool (= (|hyperram#14| state) #b0000111)) ; $0$formal$hyperram.v:298$3_CHECK[0:0]$55
(define-fun |hyperram#64| ((state |hyperram_s|)) (_ BitVec 7) (ite (|hyperram#15| state) (|hyperram#56| state) (ite (|hyperram#63| state) (|hyperram#54| state) (ite (|hyperram#22| state) #b0010000 (ite (|hyperram#62| state) (|hyperram#50| state) (ite (|hyperram#61| state) (|hyperram#40| state) (ite (|hyperram#57| state) (|hyperram#39| state) #b0000000))))))) ; \next_control_state
; yosys-smt2-wire next_control_state 7
(define-fun |hyperram_n next_control_state| ((state |hyperram_s|)) (_ BitVec 7) (|hyperram#64| state))
; yosys-smt2-wire next_data_out_register 32
(define-fun |hyperram_n next_data_out_register| ((state |hyperram_s|)) (_ BitVec 32) #b11001100110011001101110111011101)
(declare-fun |hyperram#65| (|hyperram_s|) (_ BitVec 4)) ; \write_mask
; yosys-smt2-wire next_write_mask_register 4
(define-fun |hyperram_n next_write_mask_register| ((state |hyperram_s|)) (_ BitVec 4) (|hyperram#65| state))
(declare-fun |hyperram#66| (|hyperram_s|) (_ BitVec 6)) ; \read_count
; yosys-smt2-register read_count 6
; yosys-smt2-wire read_count 6
(define-fun |hyperram_n read_count| ((state |hyperram_s|)) (_ BitVec 6) (|hyperram#66| state))
; yosys-smt2-input rst 1
; yosys-smt2-wire rst 1
(define-fun |hyperram_n rst| ((state |hyperram_s|)) Bool false)
; yosys-smt2-input rwds 1
; yosys-smt2-output rwds 1
; yosys-smt2-wire rwds 1
(define-fun |hyperram_n rwds| ((state |hyperram_s|)) Bool (= ((_ extract 0 0) (|hyperram#47| state)) #b1))
; yosys-smt2-wire rwds_oe 1
(define-fun |hyperram_n rwds_oe| ((state |hyperram_s|)) Bool (= ((_ extract 0 0) (|hyperram#46| state)) #b1))
; yosys-smt2-wire rwds_out 1
(define-fun |hyperram_n rwds_out| ((state |hyperram_s|)) Bool (= ((_ extract 0 0) (|hyperram#44| state)) #b1))
; yosys-smt2-input timed_read 1
; yosys-smt2-wire timed_read 1
(define-fun |hyperram_n timed_read| ((state |hyperram_s|)) Bool (|hyperram#48| state))
; yosys-smt2-input transaction_begin 1
; yosys-smt2-wire transaction_begin 1
(define-fun |hyperram_n transaction_begin| ((state |hyperram_s|)) Bool (= ((_ extract 0 0) (|hyperram#55| state)) #b1))
; yosys-smt2-output transaction_end 1
; yosys-smt2-wire transaction_end 1
(define-fun |hyperram_n transaction_end| ((state |hyperram_s|)) Bool (= ((_ extract 0 0) (|hyperram#16| state)) #b1))
; yosys-smt2-register wait_counter 8
; yosys-smt2-wire wait_counter 8
(define-fun |hyperram_n wait_counter| ((state |hyperram_s|)) (_ BitVec 8) (|hyperram#52| state))
(declare-fun |hyperram#67| (|hyperram_s|) (_ BitVec 6)) ; \wait_latency
; yosys-smt2-input wait_latency 6
; yosys-smt2-wire wait_latency 6
(define-fun |hyperram_n wait_latency| ((state |hyperram_s|)) (_ BitVec 6) (|hyperram#67| state))
(declare-fun |hyperram#68| (|hyperram_s|) (_ BitVec 6)) ; \write_count
; yosys-smt2-register write_count 6
; yosys-smt2-wire write_count 6
(define-fun |hyperram_n write_count| ((state |hyperram_s|)) (_ BitVec 6) (|hyperram#68| state))
; yosys-smt2-input write_enable 1
; yosys-smt2-wire write_enable 1
(define-fun |hyperram_n write_enable| ((state |hyperram_s|)) Bool (|hyperram#36| state))
; yosys-smt2-input write_mask 4
; yosys-smt2-wire write_mask 4
(define-fun |hyperram_n write_mask| ((state |hyperram_s|)) (_ BitVec 4) (|hyperram#65| state))
; yosys-smt2-register write_mask_register 4
; yosys-smt2-wire write_mask_register 4
(define-fun |hyperram_n write_mask_register| ((state |hyperram_s|)) (_ BitVec 4) (|hyperram#43| state))
; yosys-smt2-cover 0 cover_ca
(define-fun |hyperram_c 0| ((state |hyperram_s|)) Bool (and (= ((_ extract 0 0) (|hyperram#2| state)) #b1) (= ((_ extract 0 0) (|hyperram#1| state)) #b1))) ; cover_ca
; yosys-smt2-cover 1 cover_done
(define-fun |hyperram_c 1| ((state |hyperram_s|)) Bool (and (= ((_ extract 0 0) (|hyperram#6| state)) #b1) (= ((_ extract 0 0) (|hyperram#1| state)) #b1))) ; cover_done
; yosys-smt2-cover 2 cover_idle
(define-fun |hyperram_c 2| ((state |hyperram_s|)) Bool (and (= ((_ extract 0 0) (|hyperram#0| state)) #b1) (= ((_ extract 0 0) (|hyperram#1| state)) #b1))) ; cover_idle
; yosys-smt2-cover 3 cover_read
(define-fun |hyperram_c 3| ((state |hyperram_s|)) Bool (and (= ((_ extract 0 0) (|hyperram#5| state)) #b1) (= ((_ extract 0 0) (|hyperram#1| state)) #b1))) ; cover_read
; yosys-smt2-cover 4 cover_read_2
(define-fun |hyperram_c 4| ((state |hyperram_s|)) Bool (and (= ((_ extract 0 0) (|hyperram#8| state)) #b1) (= ((_ extract 0 0) (|hyperram#1| state)) #b1))) ; cover_read_2
; yosys-smt2-cover 5 cover_wait
(define-fun |hyperram_c 5| ((state |hyperram_s|)) Bool (and (= ((_ extract 0 0) (|hyperram#3| state)) #b1) (= ((_ extract 0 0) (|hyperram#1| state)) #b1))) ; cover_wait
; yosys-smt2-cover 6 cover_write
(define-fun |hyperram_c 6| ((state |hyperram_s|)) Bool (and (= ((_ extract 0 0) (|hyperram#4| state)) #b1) (= ((_ extract 0 0) (|hyperram#1| state)) #b1))) ; cover_write
; yosys-smt2-cover 7 cover_write_2
(define-fun |hyperram_c 7| ((state |hyperram_s|)) Bool (and (= ((_ extract 0 0) (|hyperram#7| state)) #b1) (= ((_ extract 0 0) (|hyperram#1| state)) #b1))) ; cover_write_2
; yosys-smt2-cover 8 cover_write_read
(define-fun |hyperram_c 8| ((state |hyperram_s|)) Bool (and (= ((_ extract 0 0) (|hyperram#9| state)) #b1) (= ((_ extract 0 0) (|hyperram#1| state)) #b1))) ; cover_write_read
(define-fun |hyperram#69| ((state |hyperram_s|)) (_ BitVec 6) (bvadd (|hyperram#68| state) #b000001)) ; $add$hyperram.v:273$49_Y
(define-fun |hyperram#70| ((state |hyperram_s|)) (_ BitVec 6) (ite (|hyperram#22| state) (|hyperram#69| state) (|hyperram#68| state))) ; $auto$rtlil.cc:2459:Mux$470
(define-fun |hyperram#71| ((state |hyperram_s|)) (_ BitVec 6) (bvadd (|hyperram#66| state) #b000001)) ; $add$hyperram.v:270$47_Y
(define-fun |hyperram#72| ((state |hyperram_s|)) (_ BitVec 6) (ite (|hyperram#58| state) (|hyperram#71| state) (|hyperram#66| state))) ; $auto$rtlil.cc:2459:Mux$472
(define-fun |hyperram#73| ((state |hyperram_s|)) (_ BitVec 8) (bvadd (|hyperram#52| state) #b00000001)) ; $add$hyperram.v:152$30_Y
(define-fun |hyperram#74| ((state |hyperram_s|)) (_ BitVec 8) (ite (|hyperram#53| state) #b00000000 (|hyperram#73| state))) ; $auto$rtlil.cc:2459:Mux$466
(define-fun |hyperram#75| ((state |hyperram_s|)) (_ BitVec 8) (ite (|hyperram#63| state) (|hyperram#74| state) (|hyperram#52| state))) ; $auto$rtlil.cc:2459:Mux$468
(define-fun |hyperram#76| ((state |hyperram_s|)) (_ BitVec 8) (bvadd (|hyperram#18| state) #b00000001)) ; $add$hyperram.v:225$40_Y
(define-fun |hyperram#77| ((state |hyperram_s|)) (_ BitVec 8) (ite (|hyperram#38| state) #b00000000 (|hyperram#76| state))) ; $auto$rtlil.cc:2459:Mux$462
(define-fun |hyperram#78| ((state |hyperram_s|)) (_ BitVec 8) (ite (|hyperram#57| state) (|hyperram#77| state) (|hyperram#18| state))) ; $auto$rtlil.cc:2459:Mux$464
(define-fun |hyperram#79| ((state |hyperram_s|)) Bool (or  (|hyperram#15| state) (|hyperram#63| state) (|hyperram#62| state) (|hyperram#57| state) (|hyperram#61| state) (|hyperram#22| state))) ; $auto$opt_dff.cc:194:make_patterns_logic$439
(define-fun |hyperram#80| ((state |hyperram_s|)) Bool (distinct (concat (|hyperram#55| state) (ite (|hyperram#15| state) #b1 #b0)) #b01)) ; $auto$opt_dff.cc:194:make_patterns_logic$441
(define-fun |hyperram#81| ((state |hyperram_s|)) Bool (distinct (concat (ite (|hyperram#53| state) #b1 #b0) (ite (|hyperram#63| state) #b1 #b0)) #b01)) ; $auto$opt_dff.cc:194:make_patterns_logic$443
(define-fun |hyperram#82| ((state |hyperram_s|)) Bool (distinct (concat (ite (|hyperram#49| state) #b1 #b0) (ite (|hyperram#62| state) #b1 #b0)) #b01)) ; $auto$opt_dff.cc:194:make_patterns_logic$445
(define-fun |hyperram#83| ((state |hyperram_s|)) Bool (distinct (concat (ite (|hyperram#38| state) #b1 #b0) (ite (|hyperram#57| state) #b1 #b0)) #b01)) ; $auto$opt_dff.cc:194:make_patterns_logic$447
(define-fun |hyperram#84| ((state |hyperram_s|)) Bool (and  (|hyperram#79| state) (|hyperram#80| state) (|hyperram#81| state) (|hyperram#82| state) (|hyperram#83| state))) ; $auto$opt_dff.cc:219:make_patterns_logic$449
(define-fun |hyperram#85| ((state |hyperram_s|)) (_ BitVec 7) (ite (|hyperram#84| state) (|hyperram#64| state) (|hyperram#14| state))) ; $auto$rtlil.cc:2459:Mux$460
(define-fun |hyperram#86| ((state |hyperram_s|)) (_ BitVec 1) (ite (|hyperram#15| state) #b0 (ite (|hyperram#11| state) #b1 #b0))) ; $auto$rtlil.cc:2459:Mux$458
(define-fun |hyperram#87| ((state |hyperram_s|)) Bool (= (|hyperram#66| state) #b000001)) ; $eq$hyperram.v:304$77_Y
(define-fun |hyperram#88| ((state |hyperram_s|)) Bool (= (|hyperram#68| state) #b000001)) ; $eq$hyperram.v:304$78_Y
(define-fun |hyperram#89| ((state |hyperram_s|)) Bool (and (or  (|hyperram#87| state) false) (or  (|hyperram#88| state) false))) ; $0$formal$hyperram.v:304$9_CHECK[0:0]$67
(define-fun |hyperram#90| ((state |hyperram_s|)) Bool (= (|hyperram#66| state) #b000010)) ; $0$formal$hyperram.v:303$8_CHECK[0:0]$65
(define-fun |hyperram#91| ((state |hyperram_s|)) Bool (= (|hyperram#68| state) #b000010)) ; $0$formal$hyperram.v:302$7_CHECK[0:0]$63
(define-fun |hyperram_a| ((state |hyperram_s|)) Bool true)
(define-fun |hyperram_u| ((state |hyperram_s|)) Bool true)
(define-fun |hyperram_i| ((state |hyperram_s|)) Bool (and
  (= (= ((_ extract 0 0) (|hyperram#1| state)) #b1) false) ; $formal$hyperram.v:296$1_EN
  (= (|hyperram#14| state) #b0000000) ; control_state
  (= (|hyperram#18| state) #b00000000) ; done_counter
  (= (|hyperram#66| state) #b000000) ; read_count
  (= (|hyperram#52| state) #b00000000) ; wait_counter
  (= (|hyperram#68| state) #b000000) ; write_count
))
(define-fun |hyperram_h| ((state |hyperram_s|)) Bool true)
(define-fun |hyperram_t| ((state |hyperram_s|) (next_state |hyperram_s|)) Bool (and
  (= (|hyperram#70| state) (|hyperram#68| next_state)) ; $auto$ff.cc:262:slice$455 \write_count
  (= (|hyperram#72| state) (|hyperram#66| next_state)) ; $auto$ff.cc:262:slice$456 \read_count
  (= (|hyperram#75| state) (|hyperram#52| next_state)) ; $auto$ff.cc:262:slice$454 \wait_counter
  (= (|hyperram#65| state) (|hyperram#43| next_state)) ; $procdff$410 \write_mask_register
  (= (|hyperram#78| state) (|hyperram#18| next_state)) ; $auto$ff.cc:262:slice$452 \done_counter
  (= #b1001100110011001101110111011101 (|hyperram#17| next_state)) ; $procdff$411 \data_out_register [30:0]
  (= (|hyperram#85| state) (|hyperram#14| next_state)) ; $auto$ff.cc:262:slice$438 \control_state
  (= (concat (ite (|hyperram#37| state) #b1 #b0) #b01000000000011010001010110011110000000000000000) (|hyperram#13| next_state)) ; $procdff$409 \command_address
  (= (|hyperram#86| state) (|hyperram#10| next_state)) ; $auto$ff.cc:262:slice$437 \ck
  (= (ite (|hyperram#89| state) #b1 #b0) (|hyperram#9| next_state)) ; $procdff$405 $formal$hyperram.v:304$9_CHECK
  (= (ite (|hyperram#90| state) #b1 #b0) (|hyperram#8| next_state)) ; $procdff$403 $formal$hyperram.v:303$8_CHECK
  (= (ite (|hyperram#91| state) #b1 #b0) (|hyperram#7| next_state)) ; $procdff$401 $formal$hyperram.v:302$7_CHECK
  (= (ite (|hyperram#57| state) #b1 #b0) (|hyperram#6| next_state)) ; $procdff$399 $formal$hyperram.v:301$6_CHECK
  (= (ite (|hyperram#62| state) #b1 #b0) (|hyperram#5| next_state)) ; $procdff$397 $formal$hyperram.v:300$5_CHECK
  (= (ite (|hyperram#25| state) #b1 #b0) (|hyperram#4| next_state)) ; $procdff$395 $formal$hyperram.v:299$4_CHECK
  (= (ite (|hyperram#63| state) #b1 #b0) (|hyperram#3| next_state)) ; $procdff$393 $formal$hyperram.v:298$3_CHECK
  (= (ite (|hyperram#26| state) #b1 #b0) (|hyperram#2| next_state)) ; $procdff$391 $formal$hyperram.v:297$2_CHECK
  (= #b1 (|hyperram#1| next_state)) ; $procdff$390 $formal$hyperram.v:296$1_EN
  (= (ite (|hyperram#15| state) #b1 #b0) (|hyperram#0| next_state)) ; $procdff$389 $formal$hyperram.v:296$1_CHECK
)) ; end of module hyperram
; yosys-smt2-topmod hyperram
; end of yosys output