picorv32.py

# SMT-LIBv2 description generated by Yosys 0.8+369 (git sha1 3619dfa3, clang 3.8.1-24 -fPIC -Os)
from z3 import *
from functools import reduce
import operator
from collections import OrderedDict
# yosys-smt2-module picorv32
picorv32_s = DeclareSort('picorv32_s')
clocks = []
inputs = []
outputs = []
registers = []
memories = []
picorv32_is = Function('picorv32_is', picorv32_s, BoolSort())
# yosys-smt2-register alu_out_q 32
registers.append('alu_out_q')
picorv32__0 = Function('picorv32__0', picorv32_s, BitVecSort(32)) # \alu_out_q
def picorv32_n_alu_out_q(state): return picorv32__0(state)
# yosys-smt2-input clk 1
inputs.append('clk')
# yosys-smt2-clock clk posedge
clocks.append('clk')
picorv32__1 = Function('picorv32__1', picorv32_s, BoolSort()) # \clk
def picorv32_n_clk(state): return picorv32__1(state)
# yosys-smt2-register compressed_instr 1
registers.append('compressed_instr')
picorv32__2 = Function('picorv32__2', picorv32_s, BitVecSort(1)) # \compressed_instr
def picorv32_n_compressed_instr(state): return (Extract(0, 0, picorv32__2(state)) == 0b1)
# yosys-smt2-register count_cycle 64
registers.append('count_cycle')
picorv32__3 = Function('picorv32__3', picorv32_s, BitVecSort(64)) # \count_cycle
def picorv32_n_count_cycle(state): return picorv32__3(state)
# yosys-smt2-register count_instr 64
registers.append('count_instr')
picorv32__4 = Function('picorv32__4', picorv32_s, BitVecSort(64)) # \count_instr
def picorv32_n_count_instr(state): return picorv32__4(state)
# yosys-smt2-register cpu_state 8
registers.append('cpu_state')
picorv32__5 = Function('picorv32__5', picorv32_s, BitVecSort(8)) # \cpu_state
def picorv32_n_cpu_state(state): return picorv32__5(state)
# yosys-smt2-register decoded_imm 32
registers.append('decoded_imm')
picorv32__6 = Function('picorv32__6', picorv32_s, BitVecSort(32)) # \decoded_imm
def picorv32_n_decoded_imm(state): return picorv32__6(state)
# yosys-smt2-register decoded_imm_j 32
registers.append('decoded_imm_j')
picorv32__7 = Function('picorv32__7', picorv32_s, BitVecSort(32)) # \decoded_imm_j
def picorv32_n_decoded_imm_j(state): return picorv32__7(state)
# yosys-smt2-register decoded_rd 5
registers.append('decoded_rd')
picorv32__8 = Function('picorv32__8', picorv32_s, BitVecSort(5)) # \decoded_rd
def picorv32_n_decoded_rd(state): return picorv32__8(state)
# yosys-smt2-register decoded_rs1 5
registers.append('decoded_rs1')
picorv32__9 = Function('picorv32__9', picorv32_s, BitVecSort(5)) # \decoded_rs1
def picorv32_n_decoded_rs1(state): return picorv32__9(state)
# yosys-smt2-register decoded_rs2 5
registers.append('decoded_rs2')
picorv32__10 = Function('picorv32__10', picorv32_s, BitVecSort(5)) # \decoded_rs2
def picorv32_n_decoded_rs2(state): return picorv32__10(state)
# yosys-smt2-register decoder_pseudo_trigger 1
registers.append('decoder_pseudo_trigger')
picorv32__11 = Function('picorv32__11', picorv32_s, BitVecSort(1)) # \decoder_pseudo_trigger
def picorv32_n_decoder_pseudo_trigger(state): return (Extract(0, 0, picorv32__11(state)) == 0b1)
# yosys-smt2-register decoder_trigger 1
registers.append('decoder_trigger')
picorv32__12 = Function('picorv32__12', picorv32_s, BitVecSort(1)) # \decoder_trigger
def picorv32_n_decoder_trigger(state): return (Extract(0, 0, picorv32__12(state)) == 0b1)
# yosys-smt2-output eoi 32
outputs.append('eoi')
# yosys-smt2-register eoi 32
registers.append('eoi')
picorv32__13 = Function('picorv32__13', picorv32_s, BitVecSort(32)) # \eoi
def picorv32_n_eoi(state): return picorv32__13(state)
# yosys-smt2-register instr_add 1
registers.append('instr_add')
picorv32__14 = Function('picorv32__14', picorv32_s, BitVecSort(1)) # \instr_add
def picorv32_n_instr_add(state): return (Extract(0, 0, picorv32__14(state)) == 0b1)
# yosys-smt2-register instr_addi 1
registers.append('instr_addi')
picorv32__15 = Function('picorv32__15', picorv32_s, BitVecSort(1)) # \instr_addi
def picorv32_n_instr_addi(state): return (Extract(0, 0, picorv32__15(state)) == 0b1)
# yosys-smt2-register instr_and 1
registers.append('instr_and')
picorv32__16 = Function('picorv32__16', picorv32_s, BitVecSort(1)) # \instr_and
def picorv32_n_instr_and(state): return (Extract(0, 0, picorv32__16(state)) == 0b1)
# yosys-smt2-register instr_andi 1
registers.append('instr_andi')
picorv32__17 = Function('picorv32__17', picorv32_s, BitVecSort(1)) # \instr_andi
def picorv32_n_instr_andi(state): return (Extract(0, 0, picorv32__17(state)) == 0b1)
# yosys-smt2-register instr_auipc 1
registers.append('instr_auipc')
picorv32__18 = Function('picorv32__18', picorv32_s, BitVecSort(1)) # \instr_auipc
def picorv32_n_instr_auipc(state): return (Extract(0, 0, picorv32__18(state)) == 0b1)
# yosys-smt2-register instr_beq 1
registers.append('instr_beq')
picorv32__19 = Function('picorv32__19', picorv32_s, BitVecSort(1)) # \instr_beq
def picorv32_n_instr_beq(state): return (Extract(0, 0, picorv32__19(state)) == 0b1)
# yosys-smt2-register instr_bge 1
registers.append('instr_bge')
picorv32__20 = Function('picorv32__20', picorv32_s, BitVecSort(1)) # \instr_bge
def picorv32_n_instr_bge(state): return (Extract(0, 0, picorv32__20(state)) == 0b1)
# yosys-smt2-register instr_bgeu 1
registers.append('instr_bgeu')
picorv32__21 = Function('picorv32__21', picorv32_s, BitVecSort(1)) # \instr_bgeu
def picorv32_n_instr_bgeu(state): return (Extract(0, 0, picorv32__21(state)) == 0b1)
# yosys-smt2-register instr_blt 1
registers.append('instr_blt')
picorv32__22 = Function('picorv32__22', picorv32_s, BitVecSort(1)) # \instr_blt
def picorv32_n_instr_blt(state): return (Extract(0, 0, picorv32__22(state)) == 0b1)
# yosys-smt2-register instr_bltu 1
registers.append('instr_bltu')
picorv32__23 = Function('picorv32__23', picorv32_s, BitVecSort(1)) # \instr_bltu
def picorv32_n_instr_bltu(state): return (Extract(0, 0, picorv32__23(state)) == 0b1)
# yosys-smt2-register instr_bne 1
registers.append('instr_bne')
picorv32__24 = Function('picorv32__24', picorv32_s, BitVecSort(1)) # \instr_bne
def picorv32_n_instr_bne(state): return (Extract(0, 0, picorv32__24(state)) == 0b1)
# yosys-smt2-register instr_getq 1
registers.append('instr_getq')
picorv32__25 = Function('picorv32__25', picorv32_s, BitVecSort(1)) # \instr_getq
def picorv32_n_instr_getq(state): return (Extract(0, 0, picorv32__25(state)) == 0b1)
# yosys-smt2-register instr_jal 1
registers.append('instr_jal')
picorv32__26 = Function('picorv32__26', picorv32_s, BitVecSort(1)) # \instr_jal
def picorv32_n_instr_jal(state): return (Extract(0, 0, picorv32__26(state)) == 0b1)
# yosys-smt2-register instr_jalr 1
registers.append('instr_jalr')
picorv32__27 = Function('picorv32__27', picorv32_s, BitVecSort(1)) # \instr_jalr
def picorv32_n_instr_jalr(state): return (Extract(0, 0, picorv32__27(state)) == 0b1)
# yosys-smt2-register instr_lb 1
registers.append('instr_lb')
picorv32__28 = Function('picorv32__28', picorv32_s, BitVecSort(1)) # \instr_lb
def picorv32_n_instr_lb(state): return (Extract(0, 0, picorv32__28(state)) == 0b1)
# yosys-smt2-register instr_lbu 1
registers.append('instr_lbu')
picorv32__29 = Function('picorv32__29', picorv32_s, BitVecSort(1)) # \instr_lbu
def picorv32_n_instr_lbu(state): return (Extract(0, 0, picorv32__29(state)) == 0b1)
# yosys-smt2-register instr_lh 1
registers.append('instr_lh')
picorv32__30 = Function('picorv32__30', picorv32_s, BitVecSort(1)) # \instr_lh
def picorv32_n_instr_lh(state): return (Extract(0, 0, picorv32__30(state)) == 0b1)
# yosys-smt2-register instr_lhu 1
registers.append('instr_lhu')
picorv32__31 = Function('picorv32__31', picorv32_s, BitVecSort(1)) # \instr_lhu
def picorv32_n_instr_lhu(state): return (Extract(0, 0, picorv32__31(state)) == 0b1)
# yosys-smt2-register instr_lui 1
registers.append('instr_lui')
picorv32__32 = Function('picorv32__32', picorv32_s, BitVecSort(1)) # \instr_lui
def picorv32_n_instr_lui(state): return (Extract(0, 0, picorv32__32(state)) == 0b1)
# yosys-smt2-register instr_lw 1
registers.append('instr_lw')
picorv32__33 = Function('picorv32__33', picorv32_s, BitVecSort(1)) # \instr_lw
def picorv32_n_instr_lw(state): return (Extract(0, 0, picorv32__33(state)) == 0b1)
# yosys-smt2-register instr_maskirq 1
registers.append('instr_maskirq')
picorv32__34 = Function('picorv32__34', picorv32_s, BitVecSort(1)) # \instr_maskirq
def picorv32_n_instr_maskirq(state): return (Extract(0, 0, picorv32__34(state)) == 0b1)
# yosys-smt2-register instr_or 1
registers.append('instr_or')
picorv32__35 = Function('picorv32__35', picorv32_s, BitVecSort(1)) # \instr_or
def picorv32_n_instr_or(state): return (Extract(0, 0, picorv32__35(state)) == 0b1)
# yosys-smt2-register instr_ori 1
registers.append('instr_ori')
picorv32__36 = Function('picorv32__36', picorv32_s, BitVecSort(1)) # \instr_ori
def picorv32_n_instr_ori(state): return (Extract(0, 0, picorv32__36(state)) == 0b1)
# yosys-smt2-register instr_rdcycle 1
registers.append('instr_rdcycle')
picorv32__37 = Function('picorv32__37', picorv32_s, BitVecSort(1)) # \instr_rdcycle
def picorv32_n_instr_rdcycle(state): return (Extract(0, 0, picorv32__37(state)) == 0b1)
# yosys-smt2-register instr_rdcycleh 1
registers.append('instr_rdcycleh')
picorv32__38 = Function('picorv32__38', picorv32_s, BitVecSort(1)) # \instr_rdcycleh
def picorv32_n_instr_rdcycleh(state): return (Extract(0, 0, picorv32__38(state)) == 0b1)
# yosys-smt2-register instr_rdinstr 1
registers.append('instr_rdinstr')
picorv32__39 = Function('picorv32__39', picorv32_s, BitVecSort(1)) # \instr_rdinstr
def picorv32_n_instr_rdinstr(state): return (Extract(0, 0, picorv32__39(state)) == 0b1)
# yosys-smt2-register instr_rdinstrh 1
registers.append('instr_rdinstrh')
picorv32__40 = Function('picorv32__40', picorv32_s, BitVecSort(1)) # \instr_rdinstrh
def picorv32_n_instr_rdinstrh(state): return (Extract(0, 0, picorv32__40(state)) == 0b1)
# yosys-smt2-register instr_retirq 1
registers.append('instr_retirq')
picorv32__41 = Function('picorv32__41', picorv32_s, BitVecSort(1)) # \instr_retirq
def picorv32_n_instr_retirq(state): return (Extract(0, 0, picorv32__41(state)) == 0b1)
# yosys-smt2-register instr_sb 1
registers.append('instr_sb')
picorv32__42 = Function('picorv32__42', picorv32_s, BitVecSort(1)) # \instr_sb
def picorv32_n_instr_sb(state): return (Extract(0, 0, picorv32__42(state)) == 0b1)
# yosys-smt2-register instr_setq 1
registers.append('instr_setq')
picorv32__43 = Function('picorv32__43', picorv32_s, BitVecSort(1)) # \instr_setq
def picorv32_n_instr_setq(state): return (Extract(0, 0, picorv32__43(state)) == 0b1)
# yosys-smt2-register instr_sh 1
registers.append('instr_sh')
picorv32__44 = Function('picorv32__44', picorv32_s, BitVecSort(1)) # \instr_sh
def picorv32_n_instr_sh(state): return (Extract(0, 0, picorv32__44(state)) == 0b1)
# yosys-smt2-register instr_sll 1
registers.append('instr_sll')
picorv32__45 = Function('picorv32__45', picorv32_s, BitVecSort(1)) # \instr_sll
def picorv32_n_instr_sll(state): return (Extract(0, 0, picorv32__45(state)) == 0b1)
# yosys-smt2-register instr_slli 1
registers.append('instr_slli')
picorv32__46 = Function('picorv32__46', picorv32_s, BitVecSort(1)) # \instr_slli
def picorv32_n_instr_slli(state): return (Extract(0, 0, picorv32__46(state)) == 0b1)
# yosys-smt2-register instr_slt 1
registers.append('instr_slt')
picorv32__47 = Function('picorv32__47', picorv32_s, BitVecSort(1)) # \instr_slt
def picorv32_n_instr_slt(state): return (Extract(0, 0, picorv32__47(state)) == 0b1)
# yosys-smt2-register instr_slti 1
registers.append('instr_slti')
picorv32__48 = Function('picorv32__48', picorv32_s, BitVecSort(1)) # \instr_slti
def picorv32_n_instr_slti(state): return (Extract(0, 0, picorv32__48(state)) == 0b1)
# yosys-smt2-register instr_sltiu 1
registers.append('instr_sltiu')
picorv32__49 = Function('picorv32__49', picorv32_s, BitVecSort(1)) # \instr_sltiu
def picorv32_n_instr_sltiu(state): return (Extract(0, 0, picorv32__49(state)) == 0b1)
# yosys-smt2-register instr_sltu 1
registers.append('instr_sltu')
picorv32__50 = Function('picorv32__50', picorv32_s, BitVecSort(1)) # \instr_sltu
def picorv32_n_instr_sltu(state): return (Extract(0, 0, picorv32__50(state)) == 0b1)
# yosys-smt2-register instr_sra 1
registers.append('instr_sra')
picorv32__51 = Function('picorv32__51', picorv32_s, BitVecSort(1)) # \instr_sra
def picorv32_n_instr_sra(state): return (Extract(0, 0, picorv32__51(state)) == 0b1)
# yosys-smt2-register instr_srai 1
registers.append('instr_srai')
picorv32__52 = Function('picorv32__52', picorv32_s, BitVecSort(1)) # \instr_srai
def picorv32_n_instr_srai(state): return (Extract(0, 0, picorv32__52(state)) == 0b1)
# yosys-smt2-register instr_srl 1
registers.append('instr_srl')
picorv32__53 = Function('picorv32__53', picorv32_s, BitVecSort(1)) # \instr_srl
def picorv32_n_instr_srl(state): return (Extract(0, 0, picorv32__53(state)) == 0b1)
# yosys-smt2-register instr_srli 1
registers.append('instr_srli')
picorv32__54 = Function('picorv32__54', picorv32_s, BitVecSort(1)) # \instr_srli
def picorv32_n_instr_srli(state): return (Extract(0, 0, picorv32__54(state)) == 0b1)
# yosys-smt2-register instr_sub 1
registers.append('instr_sub')
picorv32__55 = Function('picorv32__55', picorv32_s, BitVecSort(1)) # \instr_sub
def picorv32_n_instr_sub(state): return (Extract(0, 0, picorv32__55(state)) == 0b1)
# yosys-smt2-register instr_sw 1
registers.append('instr_sw')
picorv32__56 = Function('picorv32__56', picorv32_s, BitVecSort(1)) # \instr_sw
def picorv32_n_instr_sw(state): return (Extract(0, 0, picorv32__56(state)) == 0b1)
# yosys-smt2-register instr_timer 1
registers.append('instr_timer')
picorv32__57 = Function('picorv32__57', picorv32_s, BitVecSort(1)) # \instr_timer
def picorv32_n_instr_timer(state): return (Extract(0, 0, picorv32__57(state)) == 0b1)
# yosys-smt2-register instr_waitirq 1
registers.append('instr_waitirq')
picorv32__58 = Function('picorv32__58', picorv32_s, BitVecSort(1)) # \instr_waitirq
def picorv32_n_instr_waitirq(state): return (Extract(0, 0, picorv32__58(state)) == 0b1)
# yosys-smt2-register instr_xor 1
registers.append('instr_xor')
picorv32__59 = Function('picorv32__59', picorv32_s, BitVecSort(1)) # \instr_xor
def picorv32_n_instr_xor(state): return (Extract(0, 0, picorv32__59(state)) == 0b1)
# yosys-smt2-register instr_xori 1
registers.append('instr_xori')
picorv32__60 = Function('picorv32__60', picorv32_s, BitVecSort(1)) # \instr_xori
def picorv32_n_instr_xori(state): return (Extract(0, 0, picorv32__60(state)) == 0b1)
# yosys-smt2-input irq 32
inputs.append('irq')
picorv32__61 = Function('picorv32__61', picorv32_s, BitVecSort(32)) # \irq
def picorv32_n_irq(state): return picorv32__61(state)
# yosys-smt2-register is_alu_reg_imm 1
registers.append('is_alu_reg_imm')
picorv32__62 = Function('picorv32__62', picorv32_s, BitVecSort(1)) # \is_alu_reg_imm
def picorv32_n_is_alu_reg_imm(state): return (Extract(0, 0, picorv32__62(state)) == 0b1)
# yosys-smt2-register is_alu_reg_reg 1
registers.append('is_alu_reg_reg')
picorv32__63 = Function('picorv32__63', picorv32_s, BitVecSort(1)) # \is_alu_reg_reg
def picorv32_n_is_alu_reg_reg(state): return (Extract(0, 0, picorv32__63(state)) == 0b1)
# yosys-smt2-register is_beq_bne_blt_bge_bltu_bgeu 1
registers.append('is_beq_bne_blt_bge_bltu_bgeu')
picorv32__64 = Function('picorv32__64', picorv32_s, BitVecSort(1)) # \is_beq_bne_blt_bge_bltu_bgeu
def picorv32_n_is_beq_bne_blt_bge_bltu_bgeu(state): return (Extract(0, 0, picorv32__64(state)) == 0b1)
# yosys-smt2-register is_compare 1
registers.append('is_compare')
picorv32__65 = Function('picorv32__65', picorv32_s, BitVecSort(1)) # \is_compare
def picorv32_n_is_compare(state): return (Extract(0, 0, picorv32__65(state)) == 0b1)
# yosys-smt2-register is_jalr_addi_slti_sltiu_xori_ori_andi 1
registers.append('is_jalr_addi_slti_sltiu_xori_ori_andi')
picorv32__66 = Function('picorv32__66', picorv32_s, BitVecSort(1)) # \is_jalr_addi_slti_sltiu_xori_ori_andi
def picorv32_n_is_jalr_addi_slti_sltiu_xori_ori_andi(state): return (Extract(0, 0, picorv32__66(state)) == 0b1)
# yosys-smt2-register is_lb_lh_lw_lbu_lhu 1
registers.append('is_lb_lh_lw_lbu_lhu')
picorv32__67 = Function('picorv32__67', picorv32_s, BitVecSort(1)) # \is_lb_lh_lw_lbu_lhu
def picorv32_n_is_lb_lh_lw_lbu_lhu(state): return (Extract(0, 0, picorv32__67(state)) == 0b1)
# yosys-smt2-register is_lbu_lhu_lw 1
registers.append('is_lbu_lhu_lw')
picorv32__68 = Function('picorv32__68', picorv32_s, BitVecSort(1)) # \is_lbu_lhu_lw
def picorv32_n_is_lbu_lhu_lw(state): return (Extract(0, 0, picorv32__68(state)) == 0b1)
# yosys-smt2-register is_lui_auipc_jal 1
registers.append('is_lui_auipc_jal')
picorv32__69 = Function('picorv32__69', picorv32_s, BitVecSort(1)) # \is_lui_auipc_jal
def picorv32_n_is_lui_auipc_jal(state): return (Extract(0, 0, picorv32__69(state)) == 0b1)
# yosys-smt2-register is_lui_auipc_jal_jalr_addi_add_sub 1
registers.append('is_lui_auipc_jal_jalr_addi_add_sub')
picorv32__70 = Function('picorv32__70', picorv32_s, BitVecSort(1)) # \is_lui_auipc_jal_jalr_addi_add_sub
def picorv32_n_is_lui_auipc_jal_jalr_addi_add_sub(state): return (Extract(0, 0, picorv32__70(state)) == 0b1)
# yosys-smt2-register is_sb_sh_sw 1
registers.append('is_sb_sh_sw')
picorv32__71 = Function('picorv32__71', picorv32_s, BitVecSort(1)) # \is_sb_sh_sw
def picorv32_n_is_sb_sh_sw(state): return (Extract(0, 0, picorv32__71(state)) == 0b1)
# yosys-smt2-register is_sll_srl_sra 1
registers.append('is_sll_srl_sra')
picorv32__72 = Function('picorv32__72', picorv32_s, BitVecSort(1)) # \is_sll_srl_sra
def picorv32_n_is_sll_srl_sra(state): return (Extract(0, 0, picorv32__72(state)) == 0b1)
# yosys-smt2-register is_slli_srli_srai 1
registers.append('is_slli_srli_srai')
picorv32__73 = Function('picorv32__73', picorv32_s, BitVecSort(1)) # \is_slli_srli_srai
def picorv32_n_is_slli_srli_srai(state): return (Extract(0, 0, picorv32__73(state)) == 0b1)
# yosys-smt2-register is_slti_blt_slt 1
registers.append('is_slti_blt_slt')
picorv32__74 = Function('picorv32__74', picorv32_s, BitVecSort(1)) # \is_slti_blt_slt
def picorv32_n_is_slti_blt_slt(state): return (Extract(0, 0, picorv32__74(state)) == 0b1)
# yosys-smt2-register is_sltiu_bltu_sltu 1
registers.append('is_sltiu_bltu_sltu')
picorv32__75 = Function('picorv32__75', picorv32_s, BitVecSort(1)) # \is_sltiu_bltu_sltu
def picorv32_n_is_sltiu_bltu_sltu(state): return (Extract(0, 0, picorv32__75(state)) == 0b1)
# yosys-smt2-register latched_branch 1
registers.append('latched_branch')
picorv32__76 = Function('picorv32__76', picorv32_s, BitVecSort(1)) # \latched_branch
def picorv32_n_latched_branch(state): return (Extract(0, 0, picorv32__76(state)) == 0b1)
# yosys-smt2-register latched_compr 1
registers.append('latched_compr')
picorv32__77 = Function('picorv32__77', picorv32_s, BitVecSort(1)) # \latched_compr
def picorv32_n_latched_compr(state): return (Extract(0, 0, picorv32__77(state)) == 0b1)
# yosys-smt2-register latched_is_lb 1
registers.append('latched_is_lb')
picorv32__78 = Function('picorv32__78', picorv32_s, BitVecSort(1)) # \latched_is_lb
def picorv32_n_latched_is_lb(state): return (Extract(0, 0, picorv32__78(state)) == 0b1)
# yosys-smt2-register latched_is_lh 1
registers.append('latched_is_lh')
picorv32__79 = Function('picorv32__79', picorv32_s, BitVecSort(1)) # \latched_is_lh
def picorv32_n_latched_is_lh(state): return (Extract(0, 0, picorv32__79(state)) == 0b1)
# yosys-smt2-register latched_is_lu 1
registers.append('latched_is_lu')
picorv32__80 = Function('picorv32__80', picorv32_s, BitVecSort(1)) # \latched_is_lu
def picorv32_n_latched_is_lu(state): return (Extract(0, 0, picorv32__80(state)) == 0b1)
# yosys-smt2-register latched_rd 5
registers.append('latched_rd')
picorv32__81 = Function('picorv32__81', picorv32_s, BitVecSort(5)) # \latched_rd
def picorv32_n_latched_rd(state): return picorv32__81(state)
# yosys-smt2-register latched_stalu 1
registers.append('latched_stalu')
picorv32__82 = Function('picorv32__82', picorv32_s, BitVecSort(1)) # \latched_stalu
def picorv32_n_latched_stalu(state): return (Extract(0, 0, picorv32__82(state)) == 0b1)
# yosys-smt2-register latched_store 1
registers.append('latched_store')
picorv32__83 = Function('picorv32__83', picorv32_s, BitVecSort(1)) # \latched_store
def picorv32_n_latched_store(state): return (Extract(0, 0, picorv32__83(state)) == 0b1)
# yosys-smt2-output mem_addr 32
outputs.append('mem_addr')
# yosys-smt2-register mem_addr 32
registers.append('mem_addr')
picorv32__84 = Function('picorv32__84', picorv32_s, BitVecSort(32)) # \mem_addr
def picorv32_n_mem_addr(state): return picorv32__84(state)
# yosys-smt2-register mem_do_prefetch 1
registers.append('mem_do_prefetch')
picorv32__85 = Function('picorv32__85', picorv32_s, BitVecSort(1)) # \mem_do_prefetch
def picorv32_n_mem_do_prefetch(state): return (Extract(0, 0, picorv32__85(state)) == 0b1)
# yosys-smt2-register mem_do_rdata 1
registers.append('mem_do_rdata')
picorv32__86 = Function('picorv32__86', picorv32_s, BitVecSort(1)) # \mem_do_rdata
def picorv32_n_mem_do_rdata(state): return (Extract(0, 0, picorv32__86(state)) == 0b1)
# yosys-smt2-register mem_do_rinst 1
registers.append('mem_do_rinst')
picorv32__87 = Function('picorv32__87', picorv32_s, BitVecSort(1)) # \mem_do_rinst
def picorv32_n_mem_do_rinst(state): return (Extract(0, 0, picorv32__87(state)) == 0b1)
# yosys-smt2-register mem_do_wdata 1
registers.append('mem_do_wdata')
picorv32__88 = Function('picorv32__88', picorv32_s, BitVecSort(1)) # \mem_do_wdata
def picorv32_n_mem_do_wdata(state): return (Extract(0, 0, picorv32__88(state)) == 0b1)
# yosys-smt2-output mem_instr 1
outputs.append('mem_instr')
# yosys-smt2-register mem_instr 1
registers.append('mem_instr')
picorv32__89 = Function('picorv32__89', picorv32_s, BitVecSort(1)) # \mem_instr
def picorv32_n_mem_instr(state): return (Extract(0, 0, picorv32__89(state)) == 0b1)
# yosys-smt2-output mem_la_addr 32
outputs.append('mem_la_addr')
picorv32__90 = Function('picorv32__90', picorv32_s, BitVecSort(32)) # \reg_op1
picorv32__91 = Function('picorv32__91', picorv32_s, BitVecSort(32)) # \reg_next_pc
picorv32__92 = Function('picorv32__92', picorv32_s, BitVecSort(32)) # \reg_out
def picorv32__93(state): return (picorv32__92(state) & BitVecVal(0b11111111111111111111111111111110, 32)) # $and$picorv32.v:1192$438_Y
def picorv32__94(state): return And(Or((Extract(0, 0, picorv32__83(state)) == 0b1), False), Or((Extract(0, 0, picorv32__76(state)) == 0b1), False)) # $logic_and$picorv32.v:1192$437_Y
def picorv32__95(state): return If(picorv32__94(state), picorv32__93(state), picorv32__91(state)) # \next_pc
def picorv32__96(state): return (Extract(31, 2, picorv32__95(state)) + BitVecVal(0b000000000000000000000000000000, 30)) # $add$picorv32.v:366$79_Y
def picorv32__97(state): return Or((Extract(0, 0, picorv32__87(state)) == 0b1), False, (Extract(0, 0, picorv32__85(state)) == 0b1), False) # $logic_or$picorv32.v:364$65_Y
def picorv32__98(state): return If(picorv32__97(state), Concat(picorv32__96(state), BitVecVal(0b00, 2)), Concat(Extract(31, 2, picorv32__90(state)), BitVecVal(0b00, 2))) # \mem_la_addr
def picorv32_n_mem_la_addr(state): return picorv32__98(state)
# yosys-smt2-output mem_la_read 1
outputs.append('mem_la_read')
picorv32__99 = Function('picorv32__99', picorv32_s, BoolSort()) # \resetn
picorv32__100 = Function('picorv32__100', picorv32_s, BitVecSort(2)) # \mem_state
def picorv32__101(state): return Not(Or((Extract(0, 0, picorv32__100(state)) == 0b1),(Extract(1, 1, picorv32__100(state)) == 0b1),)) # $logic_and$picorv32.v:364$64_Y
def picorv32__102(state): return Or(picorv32__97(state), False, (Extract(0, 0, picorv32__86(state)) == 0b1), False) # $logic_or$picorv32.v:364$66_Y
def picorv32__103(state): return And(Or(picorv32__101(state), False), Or(picorv32__102(state), False)) # $logic_and$picorv32.v:364$67_Y
def picorv32__104(state): return And(Or(picorv32__99(state), False), Or(picorv32__103(state), False)) # \mem_la_read
def picorv32_n_mem_la_read(state): return picorv32__104(state)
# yosys-smt2-output mem_la_wdata 32
outputs.append('mem_la_wdata')
picorv32__105 = Function('picorv32__105', picorv32_s, BitVecSort(32)) # \reg_op2
picorv32__106 = Function('picorv32__106', picorv32_s, BitVecSort(2)) # \mem_wordsize
def picorv32__107(state): return (picorv32__106(state) == BitVecVal(0b10, 2)) # $procmux$3566_CMP
def picorv32__108(state): return (picorv32__106(state) == BitVecVal(0b01, 2)) # $eq$picorv32.v:1902$654_Y
def picorv32__109(state): return Not(Or((Extract(0, 0, picorv32__106(state)) == 0b1),(Extract(1, 1, picorv32__106(state)) == 0b1),)) # $eq$picorv32.v:1895$647_Y
def picorv32__110(state): return If(picorv32__109(state), picorv32__105(state), If(picorv32__108(state), Concat(Extract(15, 0, picorv32__105(state)), Extract(15, 0, picorv32__105(state))), If(picorv32__107(state), Concat(Extract(7, 0, picorv32__105(state)),  Concat(Extract(7, 0, picorv32__105(state)),  Concat(Extract(7, 0, picorv32__105(state)), Extract(7, 0, picorv32__105(state))))), BitVecVal(0b00000000000000000000000000000000, 32)))) # \mem_la_wdata
def picorv32_n_mem_la_wdata(state): return picorv32__110(state)
# yosys-smt2-output mem_la_write 1
outputs.append('mem_la_write')
def picorv32__111(state): return And(Or(picorv32__99(state), False), Or(picorv32__101(state), False)) # $logic_and$picorv32.v:363$60_Y
def picorv32__112(state): return And(Or(picorv32__111(state), False), Or((Extract(0, 0, picorv32__88(state)) == 0b1), False)) # \mem_la_write
def picorv32_n_mem_la_write(state): return picorv32__112(state)
# yosys-smt2-output mem_la_wstrb 4
outputs.append('mem_la_wstrb')
def picorv32__113(state): return (BitVecVal(0b0001, 4) << Concat(BitVecVal(0b00, 2), Extract(1, 0, picorv32__90(state)))) # $shl$picorv32.v:403$96_Y
def picorv32__114(state): return If((Extract(1, 1, picorv32__90(state)) == 0b1), BitVecVal(0b1100, 4), BitVecVal(0b0011, 4)) # $ternary$picorv32.v:395$95_Y
def picorv32__115(state): return If(picorv32__109(state), BitVecVal(0b1111, 4), If(picorv32__108(state), picorv32__114(state), If(picorv32__107(state), picorv32__113(state), BitVecVal(0b0000, 4)))) # \mem_la_wstrb
def picorv32_n_mem_la_wstrb(state): return picorv32__115(state)
# yosys-smt2-input mem_rdata 32
inputs.append('mem_rdata')
picorv32__116 = Function('picorv32__116', picorv32_s, BitVecSort(32)) # \mem_rdata
def picorv32_n_mem_rdata(state): return picorv32__116(state)
# yosys-smt2-register mem_rdata_q 32
registers.append('mem_rdata_q')
picorv32__117 = Function('picorv32__117', picorv32_s, BitVecSort(32)) # \mem_rdata_q
def picorv32_n_mem_rdata_q(state): return picorv32__117(state)
# yosys-smt2-input mem_ready 1
inputs.append('mem_ready')
picorv32__118 = Function('picorv32__118', picorv32_s, BoolSort()) # \mem_ready
def picorv32_n_mem_ready(state): return picorv32__118(state)
# yosys-smt2-register mem_state 2
registers.append('mem_state')
def picorv32_n_mem_state(state): return picorv32__100(state)
# yosys-smt2-output mem_valid 1
outputs.append('mem_valid')
# yosys-smt2-register mem_valid 1
registers.append('mem_valid')
picorv32__119 = Function('picorv32__119', picorv32_s, BitVecSort(1)) # \mem_valid
def picorv32_n_mem_valid(state): return (Extract(0, 0, picorv32__119(state)) == 0b1)
# yosys-smt2-output mem_wdata 32
outputs.append('mem_wdata')
# yosys-smt2-register mem_wdata 32
registers.append('mem_wdata')
picorv32__120 = Function('picorv32__120', picorv32_s, BitVecSort(32)) # \mem_wdata
def picorv32_n_mem_wdata(state): return picorv32__120(state)
# yosys-smt2-register mem_wordsize 2
registers.append('mem_wordsize')
def picorv32_n_mem_wordsize(state): return picorv32__106(state)
# yosys-smt2-output mem_wstrb 4
outputs.append('mem_wstrb')
# yosys-smt2-register mem_wstrb 4
registers.append('mem_wstrb')
picorv32__121 = Function('picorv32__121', picorv32_s, BitVecSort(4)) # \mem_wstrb
def picorv32_n_mem_wstrb(state): return picorv32__121(state)
# yosys-smt2-output pcpi_insn 32
outputs.append('pcpi_insn')
def picorv32_n_pcpi_insn(state): return BitVecVal(0b00000000000000000000000000000000, 32)
# yosys-smt2-input pcpi_rd 32
inputs.append('pcpi_rd')
picorv32__122 = Function('picorv32__122', picorv32_s, BitVecSort(32)) # \pcpi_rd
def picorv32_n_pcpi_rd(state): return picorv32__122(state)
# yosys-smt2-input pcpi_ready 1
inputs.append('pcpi_ready')
picorv32__123 = Function('picorv32__123', picorv32_s, BoolSort()) # \pcpi_ready
def picorv32_n_pcpi_ready(state): return picorv32__123(state)
# yosys-smt2-output pcpi_rs1 32
outputs.append('pcpi_rs1')
def picorv32_n_pcpi_rs1(state): return picorv32__90(state)
# yosys-smt2-output pcpi_rs2 32
outputs.append('pcpi_rs2')
def picorv32_n_pcpi_rs2(state): return picorv32__105(state)
# yosys-smt2-output pcpi_valid 1
outputs.append('pcpi_valid')
# yosys-smt2-register pcpi_valid 1
registers.append('pcpi_valid')
picorv32__124 = Function('picorv32__124', picorv32_s, BitVecSort(1)) # \pcpi_valid
def picorv32_n_pcpi_valid(state): return (Extract(0, 0, picorv32__124(state)) == 0b1)
# yosys-smt2-input pcpi_wait 1
inputs.append('pcpi_wait')
picorv32__125 = Function('picorv32__125', picorv32_s, BoolSort()) # \pcpi_wait
def picorv32_n_pcpi_wait(state): return picorv32__125(state)
# yosys-smt2-input pcpi_wr 1
inputs.append('pcpi_wr')
picorv32__126 = Function('picorv32__126', picorv32_s, BoolSort()) # \pcpi_wr
def picorv32_n_pcpi_wr(state): return picorv32__126(state)
# yosys-smt2-register reg_next_pc 32
registers.append('reg_next_pc')
def picorv32_n_reg_next_pc(state): return picorv32__91(state)
# yosys-smt2-register reg_op1 32
registers.append('reg_op1')
def picorv32_n_reg_op1(state): return picorv32__90(state)
# yosys-smt2-register reg_op2 32
registers.append('reg_op2')
def picorv32_n_reg_op2(state): return picorv32__105(state)
# yosys-smt2-register reg_out 32
registers.append('reg_out')
def picorv32_n_reg_out(state): return picorv32__92(state)
# yosys-smt2-register reg_pc 32
registers.append('reg_pc')
picorv32__127 = Function('picorv32__127', picorv32_s, BitVecSort(32)) # \reg_pc
def picorv32_n_reg_pc(state): return picorv32__127(state)
# yosys-smt2-register reg_sh 5
registers.append('reg_sh')
picorv32__128 = Function('picorv32__128', picorv32_s, BitVecSort(5)) # \reg_sh
def picorv32_n_reg_sh(state): return picorv32__128(state)
# yosys-smt2-input resetn 1
inputs.append('resetn')
def picorv32_n_resetn(state): return picorv32__99(state)
# yosys-smt2-output trace_data 36
outputs.append('trace_data')
def picorv32_n_trace_data(state): return BitVecVal(0b000000000000000000000000000000000000, 36)
# yosys-smt2-output trace_valid 1
outputs.append('trace_valid')
def picorv32_n_trace_valid(state): return False
# yosys-smt2-output trap 1
outputs.append('trap')
# yosys-smt2-register trap 1
registers.append('trap')
picorv32__129 = Function('picorv32__129', picorv32_s, BitVecSort(1)) # \trap
def picorv32_n_trap(state): return (Extract(0, 0, picorv32__129(state)) == 0b1)
def picorv32__130(state): return (picorv32__5(state) == BitVecVal(0b10000000, 8)) # $procmux$1261_CMP
def picorv32__131(state): return If(picorv32__130(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)) # $procmux$1568_Y
def picorv32__132(state): return If(picorv32__99(state), picorv32__131(state), BitVecVal(0b0, 1)) # $0\trap[0:0]
def picorv32__133(state): return (picorv32__128(state) - BitVecVal(0b00001, 5)) # $sub$picorv32.v:1829$629_Y [4:0]
def picorv32__134(state): return (picorv32__128(state) - BitVecVal(0b00100, 5)) # $auto$wreduce.cc:452:run$3796 [4:0]
def picorv32__135(state): return UGE(picorv32__128(state), BitVecVal(0b00100, 5)) # $ge$picorv32.v:1814$614_Y
def picorv32__136(state): return If(picorv32__135(state), picorv32__134(state), picorv32__133(state)) # $procmux$1535_Y
# yosys-smt2-memory cpuregs 5 32 2 1 sync
memories.append('cpuregs')
picorv32__137__0 = Function('picorv32__137__0', picorv32_s, ArraySort(BitVecSort(5), BitVecSort(32))) # cpuregs
picorv32_m_cpuregs = picorv32__137__0
def picorv32_m_R0A_cpuregs(state): return picorv32__9(state) # \decoded_rs1
def picorv32__138(state): return Select(picorv32__137__0(state), picorv32_m_R0A_cpuregs(state)) # $memrd$\cpuregs$picorv32.v:1325$487_DATA
picorv32_m_R0D_cpuregs = picorv32__138
def picorv32_m_R1A_cpuregs(state): return picorv32__10(state) # \decoded_rs2
def picorv32__139(state): return Select(picorv32__137__0(state), picorv32_m_R1A_cpuregs(state)) # $memrd$\cpuregs$picorv32.v:1326$490_DATA
picorv32_m_R1D_cpuregs = picorv32__139
def picorv32__140(state): return (picorv32__10(state) != 0b00000) # $reduce_bool$picorv32.v:1326$491_Y
def picorv32__141(state): return If(picorv32__140(state), picorv32__139(state), BitVecVal(0b00000000000000000000000000000000, 32)) # \cpuregs_rs2
def picorv32__142(state): return Not(Or((Extract(0, 0, picorv32__57(state)) == 0b1),(Extract(0, 0, picorv32__58(state)) == 0b1),(Extract(0, 0, picorv32__34(state)) == 0b1),(Extract(0, 0, picorv32__41(state)) == 0b1),(Extract(0, 0, picorv32__43(state)) == 0b1),(Extract(0, 0, picorv32__25(state)) == 0b1),(Extract(0, 0, picorv32__40(state)) == 0b1),(Extract(0, 0, picorv32__39(state)) == 0b1),(Extract(0, 0, picorv32__38(state)) == 0b1),(Extract(0, 0, picorv32__37(state)) == 0b1),(Extract(0, 0, picorv32__16(state)) == 0b1),(Extract(0, 0, picorv32__35(state)) == 0b1),(Extract(0, 0, picorv32__51(state)) == 0b1),(Extract(0, 0, picorv32__53(state)) == 0b1),(Extract(0, 0, picorv32__59(state)) == 0b1),(Extract(0, 0, picorv32__50(state)) == 0b1),(Extract(0, 0, picorv32__47(state)) == 0b1),(Extract(0, 0, picorv32__45(state)) == 0b1),(Extract(0, 0, picorv32__55(state)) == 0b1),(Extract(0, 0, picorv32__14(state)) == 0b1),(Extract(0, 0, picorv32__52(state)) == 0b1),(Extract(0, 0, picorv32__54(state)) == 0b1),(Extract(0, 0, picorv32__46(state)) == 0b1),(Extract(0, 0, picorv32__17(state)) == 0b1),(Extract(0, 0, picorv32__36(state)) == 0b1),(Extract(0, 0, picorv32__60(state)) == 0b1),(Extract(0, 0, picorv32__49(state)) == 0b1),(Extract(0, 0, picorv32__48(state)) == 0b1),(Extract(0, 0, picorv32__15(state)) == 0b1),(Extract(0, 0, picorv32__56(state)) == 0b1),(Extract(0, 0, picorv32__44(state)) == 0b1),(Extract(0, 0, picorv32__42(state)) == 0b1),(Extract(0, 0, picorv32__31(state)) == 0b1),(Extract(0, 0, picorv32__29(state)) == 0b1),(Extract(0, 0, picorv32__33(state)) == 0b1),(Extract(0, 0, picorv32__30(state)) == 0b1),(Extract(0, 0, picorv32__28(state)) == 0b1),(Extract(0, 0, picorv32__21(state)) == 0b1),(Extract(0, 0, picorv32__23(state)) == 0b1),(Extract(0, 0, picorv32__20(state)) == 0b1),(Extract(0, 0, picorv32__22(state)) == 0b1),(Extract(0, 0, picorv32__24(state)) == 0b1),(Extract(0, 0, picorv32__19(state)) == 0b1),(Extract(0, 0, picorv32__27(state)) == 0b1),(Extract(0, 0, picorv32__26(state)) == 0b1),(Extract(0, 0, picorv32__18(state)) == 0b1),(Extract(0, 0, picorv32__32(state)) == 0b1),)) # \instr_trap
def picorv32__143(state): return Not(Or(picorv32__142(state), False)) # $logic_not$picorv32.v:1675$581_Y
def picorv32__144(state): return And(Or((Extract(0, 0, picorv32__67(state)) == 0b1), False), Or(picorv32__143(state), False)) # $logic_and$picorv32.v:1675$582_Y
def picorv32__145(state): return Or(picorv32__144(state),(Extract(0, 0, picorv32__66(state)) == 0b1),(Extract(0, 0, picorv32__69(state)) == 0b1),picorv32__142(state),(Extract(0, 0, picorv32__40(state)) == 0b1),(Extract(0, 0, picorv32__39(state)) == 0b1),(Extract(0, 0, picorv32__38(state)) == 0b1),(Extract(0, 0, picorv32__37(state)) == 0b1),) # $auto$opt_reduce.cc:132:opt_mux$3767
def picorv32__146(state): return If((Extract(0, 0, picorv32__73(state)) == 0b1), picorv32__10(state), If(picorv32__145(state), BitVecVal(0b00000, 5), Extract(4, 0, picorv32__141(state)))) # $procmux$1544_Y
def picorv32__147(state): return (picorv32__5(state) == BitVecVal(0b00000100, 8)) # $procmux$1256_CMP
def picorv32__148(state): return (picorv32__5(state) == BitVecVal(0b00010000, 8)) # $procmux$1258_CMP
def picorv32__149(state): return (picorv32__5(state) == BitVecVal(0b00100000, 8)) # $procmux$1259_CMP
def picorv32__150(state): return If(picorv32__149(state), picorv32__146(state), If(picorv32__148(state), Extract(4, 0, picorv32__141(state)), If(picorv32__147(state), picorv32__136(state), BitVecVal(0b00000, 5)))) # $0\reg_sh[4:0]
def picorv32__151(state): return If((Extract(0, 0, picorv32__82(state)) == 0b1), picorv32__0(state), picorv32__92(state)) # $ternary$picorv32.v:1300$474_Y
def picorv32__152(state): return (picorv32__151(state) & BitVecVal(0b11111111111111111111111111111110, 32)) # $and$picorv32.v:1479$516_Y
def picorv32__153(state): return If((Extract(0, 0, picorv32__83(state)) == 0b1), picorv32__152(state), picorv32__91(state)) # $ternary$picorv32.v:1479$517_Y
def picorv32__154(state): return If((Extract(0, 0, picorv32__76(state)) == 0b1), picorv32__153(state), picorv32__91(state)) # $3\current_pc[31:0]
def picorv32__155(state): return (picorv32__5(state) == BitVecVal(0b01000000, 8)) # $eq$picorv32.v:1292$469_Y
def picorv32__156(state): return If(picorv32__155(state), picorv32__154(state), picorv32__127(state)) # $procmux$2309_Y
def picorv32__157(state): return If(picorv32__99(state), picorv32__156(state), BitVecVal(0b00000000000000000000000000000000, 32)) # $0\reg_pc[31:0]
def picorv32__158(state): return If(picorv32__99(state), picorv32__124(state), BitVecVal(0b0, 1)) # $0\pcpi_valid[0:0]
def picorv32__159(state): return (picorv32__115(state) & Concat(If(picorv32__112(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)),  Concat(If(picorv32__112(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)),  Concat(If(picorv32__112(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), If(picorv32__112(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)))))) # $and$picorv32.v:560$144_Y
def picorv32__160(state): return Or(picorv32__104(state), False, picorv32__112(state), False) # $logic_or$picorv32.v:558$143_Y
def picorv32__161(state): return If(picorv32__160(state), picorv32__159(state), picorv32__121(state)) # $procmux$3287_Y
def picorv32__162(state): return If(picorv32__102(state), BitVecVal(0b0000, 4), picorv32__161(state)) # $procmux$3292_Y
def picorv32__163(state): return If(picorv32__101(state), picorv32__162(state), picorv32__161(state)) # $procmux$3294_Y
def picorv32__164(state): return Not(Or(picorv32__99(state), False)) # $logic_not$picorv32.v:1921$674_Y
def picorv32__165(state): return Or(picorv32__164(state), False, (Extract(0, 0, picorv32__129(state)) == 0b1), False) # $logic_or$picorv32.v:550$139_Y
def picorv32__166(state): return If(picorv32__165(state), picorv32__121(state), picorv32__163(state)) # $0\mem_wstrb[3:0]
def picorv32__167(state): return If(picorv32__112(state), picorv32__110(state), picorv32__120(state)) # $procmux$3299_Y
def picorv32__168(state): return If(picorv32__165(state), picorv32__120(state), picorv32__167(state)) # $0\mem_wdata[31:0]
def picorv32__169(state): return And(Or((Extract(0, 0, picorv32__119(state)) == 0b1), False), Or(picorv32__118(state), False)) # \mem_xfer
def picorv32__170(state): return If(picorv32__169(state), BitVecVal(0b0, 1), picorv32__119(state)) # $procmux$3322_Y
def picorv32__171(state): return If(picorv32__102(state), BitVecVal(0b1, 1), picorv32__119(state)) # $procmux$3332_Y
def picorv32__172(state): return If((Extract(0, 0, picorv32__88(state)) == 0b1), BitVecVal(0b1, 1), picorv32__171(state)) # $procmux$3334_Y
def picorv32__173(state): return (picorv32__100(state) == BitVecVal(0b01, 2)) # $procmux$3276_CMP
def picorv32__174(state): return (picorv32__100(state) == BitVecVal(0b10, 2)) # $procmux$3270_CMP
def picorv32__175(state): return Or(picorv32__173(state),picorv32__174(state),) # $auto$opt_reduce.cc:132:opt_mux$3793
def picorv32__176(state): return If(picorv32__101(state), picorv32__172(state), If(picorv32__175(state), picorv32__170(state), picorv32__119(state))) # $procmux$3324_Y
def picorv32__177(state): return Or(picorv32__164(state), False, picorv32__118(state), False) # $logic_or$picorv32.v:553$142_Y
def picorv32__178(state): return If(picorv32__177(state), BitVecVal(0b0, 1), picorv32__119(state)) # $procmux$3338_Y
def picorv32__179(state): return If(picorv32__165(state), picorv32__178(state), picorv32__176(state)) # $0\mem_valid[0:0]
def picorv32__180(state): return If(picorv32__169(state), Extract(6, 0, picorv32__116(state)), Extract(6, 0, picorv32__117(state))) # $0\mem_rdata_q[31:0] [6:0]
def picorv32__181(state): return If(picorv32__169(state), Extract(7, 7, picorv32__116(state)), Extract(7, 7, picorv32__117(state))) # $0\mem_rdata_q[31:0] [7]
def picorv32__182(state): return If(picorv32__169(state), Extract(11, 8, picorv32__116(state)), Extract(11, 8, picorv32__117(state))) # $0\mem_rdata_q[31:0] [11:8]
def picorv32__183(state): return If(picorv32__169(state), Extract(14, 12, picorv32__116(state)), Extract(14, 12, picorv32__117(state))) # $0\mem_rdata_q[31:0] [14:12]
def picorv32__184(state): return If(picorv32__169(state), Extract(19, 15, picorv32__116(state)), Extract(19, 15, picorv32__117(state))) # $0\mem_rdata_q[31:0] [19:15]
def picorv32__185(state): return If(picorv32__169(state), Extract(24, 20, picorv32__116(state)), Extract(24, 20, picorv32__117(state))) # $0\mem_rdata_q[31:0] [24:20]
def picorv32__186(state): return If(picorv32__169(state), Extract(30, 25, picorv32__116(state)), Extract(30, 25, picorv32__117(state))) # $0\mem_rdata_q[31:0] [30:25]
def picorv32__187(state): return If(picorv32__169(state), Extract(31, 31, picorv32__116(state)), Extract(31, 31, picorv32__117(state))) # $0\mem_rdata_q[31:0] [31]
def picorv32__188(state): return Or((Extract(0, 0, picorv32__30(state)) == 0b1), False, (Extract(0, 0, picorv32__31(state)) == 0b1), False) # $logic_or$picorv32.v:1866$640_Y
def picorv32__189(state): return Or((Extract(0, 0, picorv32__28(state)) == 0b1), False, (Extract(0, 0, picorv32__29(state)) == 0b1), False) # $logic_or$picorv32.v:1865$639_Y
def picorv32__190(state): return If(picorv32__189(state), BitVecVal(0b10, 2), If(picorv32__188(state), BitVecVal(0b01, 2), If((Extract(0, 0, picorv32__33(state)) == 0b1), BitVecVal(0b00, 2), BitVecVal(0b00, 2)))) # $procmux$2097_Y
def picorv32__191(state): return If((Extract(0, 0, picorv32__86(state)) == 0b1), picorv32__106(state), picorv32__190(state)) # $procmux$2101_Y
def picorv32__192(state): return Not(Or((Extract(0, 0, picorv32__85(state)) == 0b1), False)) # $logic_not$picorv32.v:1836$630_Y
def picorv32__193(state): return Or((Extract(1, 1, picorv32__100(state)) == 0b1),(Extract(0, 0, picorv32__100(state)) == 0b1),) # $reduce_or$picorv32.v:360$44_Y
def picorv32__194(state): return And(Or(picorv32__169(state), False), Or(picorv32__193(state), False)) # $logic_and$picorv32.v:360$45_Y
def picorv32__195(state): return Or((Extract(0, 0, picorv32__87(state)) == 0b1), False, (Extract(0, 0, picorv32__86(state)) == 0b1), False) # $logic_or$picorv32.v:360$46_Y
def picorv32__196(state): return Or(picorv32__195(state), False, (Extract(0, 0, picorv32__88(state)) == 0b1), False) # $logic_or$picorv32.v:360$47_Y
def picorv32__197(state): return And(Or(picorv32__194(state), False), Or(picorv32__196(state), False)) # $logic_and$picorv32.v:360$48_Y
def picorv32__198(state): return And((Extract(1, 1, picorv32__100(state)) == 0b1),(Extract(0, 0, picorv32__100(state)) == 0b1),) # $reduce_and$picorv32.v:360$49_Y
def picorv32__199(state): return And(Or(picorv32__198(state), False), Or((Extract(0, 0, picorv32__87(state)) == 0b1), False)) # $logic_and$picorv32.v:360$50_Y
def picorv32__200(state): return Or(picorv32__197(state), False, picorv32__199(state), False) # $logic_or$picorv32.v:360$51_Y
def picorv32__201(state): return And(Or(picorv32__99(state), False), Or(picorv32__200(state), False)) # \mem_done
def picorv32__202(state): return Or(picorv32__192(state), False, picorv32__201(state), False) # $logic_or$picorv32.v:1836$631_Y
def picorv32__203(state): return If(picorv32__202(state), picorv32__191(state), picorv32__106(state)) # $procmux$2103_Y
def picorv32__204(state): return If((Extract(0, 0, picorv32__42(state)) == 0b1), BitVecVal(0b10, 2), If((Extract(0, 0, picorv32__44(state)) == 0b1), BitVecVal(0b01, 2), If((Extract(0, 0, picorv32__56(state)) == 0b1), BitVecVal(0b00, 2), BitVecVal(0b00, 2)))) # $procmux$2109_Y
def picorv32__205(state): return If((Extract(0, 0, picorv32__88(state)) == 0b1), picorv32__106(state), picorv32__204(state)) # $procmux$2113_Y
def picorv32__206(state): return If(picorv32__202(state), picorv32__205(state), picorv32__106(state)) # $procmux$2115_Y
def picorv32__207(state): return (picorv32__5(state) == BitVecVal(0b00000001, 8)) # $procmux$1086_CMP
def picorv32__208(state): return (picorv32__5(state) == BitVecVal(0b00000010, 8)) # $procmux$1020_CMP
def picorv32__209(state): return If(picorv32__155(state), BitVecVal(0b00, 2), If(picorv32__208(state), picorv32__206(state), If(picorv32__207(state), picorv32__203(state), picorv32__106(state)))) # $procmux$2105_Y
def picorv32__210(state): return If(picorv32__99(state), picorv32__209(state), picorv32__106(state)) # $0\mem_wordsize[1:0]
def picorv32__211(state): return Or((Extract(0, 0, picorv32__66(state)) == 0b1),(Extract(0, 0, picorv32__69(state)) == 0b1),) # $auto$opt_reduce.cc:132:opt_mux$3771
def picorv32__212(state): return Or(picorv32__144(state),(Extract(0, 0, picorv32__73(state)) == 0b1),picorv32__142(state),(Extract(0, 0, picorv32__40(state)) == 0b1),(Extract(0, 0, picorv32__39(state)) == 0b1),(Extract(0, 0, picorv32__38(state)) == 0b1),(Extract(0, 0, picorv32__37(state)) == 0b1),) # $auto$opt_reduce.cc:132:opt_mux$3779
def picorv32__213(state): return If(picorv32__212(state), BitVecVal(0b00000000000000000000000000000000, 32), If(picorv32__211(state), picorv32__6(state), picorv32__141(state))) # $procmux$2212_Y
def picorv32__214(state): return If(picorv32__149(state), picorv32__213(state), If(picorv32__148(state), picorv32__141(state), picorv32__105(state))) # $procmux$2209_Y
def picorv32__215(state): return If(picorv32__99(state), picorv32__214(state), picorv32__105(state)) # $0\reg_op2[31:0]
def picorv32__216(state): return If((Extract(0, 0, picorv32__87(state)) == 0b1), BitVecVal(0b00, 2), picorv32__100(state)) # $procmux$3264_Y
def picorv32__217(state): return If(picorv32__169(state), BitVecVal(0b00, 2), picorv32__100(state)) # $procmux$3268_Y
def picorv32__218(state): return If(picorv32__195(state), BitVecVal(0b00, 2), BitVecVal(0b11, 2)) # $procmux$3272_Y
def picorv32__219(state): return If(picorv32__169(state), picorv32__218(state), picorv32__100(state)) # $procmux$3274_Y
def picorv32__220(state): return If(picorv32__102(state), BitVecVal(0b01, 2), picorv32__100(state)) # $procmux$3277_Y
def picorv32__221(state): return If((Extract(0, 0, picorv32__88(state)) == 0b1), BitVecVal(0b10, 2), picorv32__220(state)) # $procmux$3279_Y
def picorv32__222(state): return (picorv32__100(state) == BitVecVal(0b11, 2)) # $procmux$3267_CMP
def picorv32__223(state): return If(picorv32__101(state), picorv32__221(state), If(picorv32__173(state), picorv32__219(state), If(picorv32__174(state), picorv32__217(state), If(picorv32__222(state), picorv32__216(state), picorv32__100(state))))) # $procmux$3266_Y
def picorv32__224(state): return If(picorv32__99(state), picorv32__100(state), BitVecVal(0b00, 2)) # $procmux$3283_Y
def picorv32__225(state): return If(picorv32__165(state), picorv32__224(state), picorv32__223(state)) # $0\mem_state[1:0]
def picorv32__226(state): return (Extract(1, 0, picorv32__90(state)) == BitVecVal(0b11, 2)) # $procmux$3561_CMP
def picorv32__227(state): return (Extract(1, 0, picorv32__90(state)) == BitVecVal(0b10, 2)) # $procmux$3562_CMP
def picorv32__228(state): return (Extract(1, 0, picorv32__90(state)) == BitVecVal(0b01, 2)) # $procmux$3563_CMP
def picorv32__229(state): return Not(Or((Extract(0, 0, picorv32__90(state)) == 0b1),(Extract(1, 1, picorv32__90(state)) == 0b1),)) # $procmux$3564_CMP
def picorv32__230(state): return If(picorv32__229(state), Extract(7, 0, picorv32__116(state)), If(picorv32__228(state), Extract(15, 8, picorv32__116(state)), If(picorv32__227(state), Extract(23, 16, picorv32__116(state)), If(picorv32__226(state), Extract(31, 24, picorv32__116(state)), BitVecVal(0b00000000, 8))))) # $3\mem_rdata_word[31:0] [7:0]
def picorv32__231(state): return (~Extract(1, 1, picorv32__90(state))) # $procmux$3571_CMP
def picorv32__232(state): return If((Extract(0, 0, picorv32__231(state)) == 0b1), Extract(15, 0, picorv32__116(state)), If((Extract(1, 1, picorv32__90(state)) == 0b1), Extract(31, 16, picorv32__116(state)), BitVecVal(0b0000000000000000, 16))) # $2\mem_rdata_word[31:0]
def picorv32__233(state): return If(picorv32__109(state), picorv32__116(state), If(picorv32__108(state), Concat(BitVecVal(0b0000000000000000, 16), picorv32__232(state)), If(picorv32__107(state), Concat(BitVecVal(0b000000000000000000000000, 24), picorv32__230(state)), BitVecVal(0b00000000000000000000000000000000, 32)))) # \mem_rdata_word
def picorv32__234(state): return If((Extract(0, 0, picorv32__80(state)) == 0b1), picorv32__233(state), If((Extract(0, 0, picorv32__79(state)) == 0b1), Concat(Extract(15, 15, picorv32__233(state)),  Concat(Extract(15, 15, picorv32__233(state)),  Concat(Extract(15, 15, picorv32__233(state)),  Concat(Extract(15, 15, picorv32__233(state)),  Concat(Extract(15, 15, picorv32__233(state)),  Concat(Extract(15, 15, picorv32__233(state)),  Concat(Extract(15, 15, picorv32__233(state)),  Concat(Extract(15, 15, picorv32__233(state)),  Concat(Extract(15, 15, picorv32__233(state)),  Concat(Extract(15, 15, picorv32__233(state)),  Concat(Extract(15, 15, picorv32__233(state)),  Concat(Extract(15, 15, picorv32__233(state)),  Concat(Extract(15, 15, picorv32__233(state)),  Concat(Extract(15, 15, picorv32__233(state)),  Concat(Extract(15, 15, picorv32__233(state)),  Concat(Extract(15, 15, picorv32__233(state)), Extract(15, 0, picorv32__233(state)))))))))))))))))), If((Extract(0, 0, picorv32__78(state)) == 0b1), Concat(Extract(7, 7, picorv32__233(state)),  Concat(Extract(7, 7, picorv32__233(state)),  Concat(Extract(7, 7, picorv32__233(state)),  Concat(Extract(7, 7, picorv32__233(state)),  Concat(Extract(7, 7, picorv32__233(state)),  Concat(Extract(7, 7, picorv32__233(state)),  Concat(Extract(7, 7, picorv32__233(state)),  Concat(Extract(7, 7, picorv32__233(state)),  Concat(Extract(7, 7, picorv32__233(state)),  Concat(Extract(7, 7, picorv32__233(state)),  Concat(Extract(7, 7, picorv32__233(state)),  Concat(Extract(7, 7, picorv32__233(state)),  Concat(Extract(7, 7, picorv32__233(state)),  Concat(Extract(7, 7, picorv32__233(state)),  Concat(Extract(7, 7, picorv32__233(state)),  Concat(Extract(7, 7, picorv32__233(state)),  Concat(Extract(7, 7, picorv32__233(state)),  Concat(Extract(7, 7, picorv32__233(state)),  Concat(Extract(7, 7, picorv32__233(state)),  Concat(Extract(7, 7, picorv32__233(state)),  Concat(Extract(7, 7, picorv32__233(state)),  Concat(Extract(7, 7, picorv32__233(state)),  Concat(Extract(7, 7, picorv32__233(state)),  Concat(Extract(7, 7, picorv32__233(state)), Extract(7, 0, picorv32__233(state)))))))))))))))))))))))))), BitVecVal(0b00000000000000000000000000000000, 32)))) # $procmux$1477_Y
def picorv32__235(state): return (picorv32__127(state) + picorv32__6(state)) # $add$picorv32.v:1785$605_Y
def picorv32__236(state): return If((Extract(0, 0, picorv32__37(state)) == 0b1), Extract(31, 0, picorv32__3(state)), If((Extract(0, 0, picorv32__38(state)) == 0b1), Extract(63, 32, picorv32__3(state)), If((Extract(0, 0, picorv32__39(state)) == 0b1), Extract(31, 0, picorv32__4(state)), If((Extract(0, 0, picorv32__40(state)) == 0b1), Extract(63, 32, picorv32__4(state)), BitVecVal(0b00000000000000000000000000000000, 32))))) # $procmux$1505_Y
def picorv32__237(state): return (picorv32__5(state) == BitVecVal(0b00001000, 8)) # $procmux$1007_CMP
def picorv32__238(state): return If(picorv32__149(state), picorv32__236(state), If(picorv32__237(state), picorv32__235(state), If(picorv32__147(state), picorv32__90(state), If(picorv32__207(state), picorv32__234(state), BitVecVal(0b00000000000000000000000000000000, 32))))) # $0\reg_out[31:0]
def picorv32__239(state): return If((Extract(0, 0, picorv32__2(state)) == 0b1), BitVecVal(0b010, 3), BitVecVal(0b100, 3)) # $auto$wreduce.cc:452:run$3798 [2:0]
def picorv32__240(state): return (picorv32__154(state) + Concat(BitVecVal(0b00000000000000000000000000000, 29), picorv32__239(state))) # $add$picorv32.v:1539$557_Y
def picorv32__241(state): return (picorv32__154(state) + picorv32__7(state)) # $add$picorv32.v:1548$559_Y
def picorv32__242(state): return If((Extract(0, 0, picorv32__26(state)) == 0b1), picorv32__241(state), picorv32__240(state)) # $procmux$2284_Y
def picorv32__243(state): return If((Extract(0, 0, picorv32__12(state)) == 0b1), picorv32__242(state), picorv32__154(state)) # $procmux$2286_Y
def picorv32__244(state): return If(picorv32__155(state), picorv32__243(state), picorv32__91(state)) # $procmux$2297_Y
def picorv32__245(state): return If(picorv32__99(state), picorv32__244(state), BitVecVal(0b00000000000000000000000000000000, 32)) # $0\reg_next_pc[31:0]
def picorv32__246(state): return (picorv32__90(state) + picorv32__6(state)) # $add$picorv32.v:1848$633_Y
def picorv32__247(state): return If((Extract(0, 0, picorv32__86(state)) == 0b1), picorv32__90(state), picorv32__246(state)) # $procmux$2231_Y
def picorv32__248(state): return If(picorv32__202(state), picorv32__247(state), picorv32__90(state)) # $procmux$2233_Y
def picorv32__249(state): return If((Extract(0, 0, picorv32__88(state)) == 0b1), picorv32__90(state), picorv32__246(state)) # $procmux$2239_Y
def picorv32__250(state): return If(picorv32__202(state), picorv32__249(state), picorv32__90(state)) # $procmux$2241_Y
def picorv32__251(state): return Or((Extract(0, 0, picorv32__51(state)) == 0b1), False, (Extract(0, 0, picorv32__52(state)) == 0b1), False) # $logic_or$picorv32.v:1224$685_Y
def picorv32__252(state): return Or((Extract(0, 0, picorv32__54(state)) == 0b1), False, (Extract(0, 0, picorv32__53(state)) == 0b1), False) # $logic_or$picorv32.v:1818$618_Y
def picorv32__253(state): return Or((Extract(0, 0, picorv32__46(state)) == 0b1), False, (Extract(0, 0, picorv32__45(state)) == 0b1), False) # $logic_or$picorv32.v:1817$616_Y
def picorv32__254(state): return If(picorv32__253(state), Concat(Extract(30, 0, picorv32__90(state)), BitVecVal(0b0, 1)), If(picorv32__252(state), Concat(BitVecVal(0b0, 1), Extract(31, 1, picorv32__90(state))), If(picorv32__251(state), Concat(Extract(31, 31, picorv32__90(state)), Extract(31, 1, picorv32__90(state))), BitVecVal(0b00000000000000000000000000000000, 32)))) # $procmux$2244_Y
def picorv32__255(state): return If(picorv32__253(state), Concat(Extract(27, 0, picorv32__90(state)), BitVecVal(0b0000, 4)), If(picorv32__252(state), Concat(BitVecVal(0b0000, 4), Extract(31, 4, picorv32__90(state))), If(picorv32__251(state), Concat(Extract(31, 31, picorv32__90(state)),  Concat(Extract(31, 31, picorv32__90(state)),  Concat(Extract(31, 31, picorv32__90(state)),  Concat(Extract(31, 31, picorv32__90(state)), Extract(31, 4, picorv32__90(state)))))), BitVecVal(0b00000000000000000000000000000000, 32)))) # $procmux$2249_Y
def picorv32__256(state): return If(picorv32__135(state), picorv32__255(state), picorv32__254(state)) # $procmux$2253_Y
def picorv32__257(state): return Not(Or((Extract(0, 0, picorv32__128(state)) == 0b1),(Extract(1, 1, picorv32__128(state)) == 0b1),(Extract(2, 2, picorv32__128(state)) == 0b1),(Extract(3, 3, picorv32__128(state)) == 0b1),(Extract(4, 4, picorv32__128(state)) == 0b1),)) # $eq$picorv32.v:1810$613_Y
def picorv32__258(state): return If(picorv32__257(state), picorv32__90(state), picorv32__256(state)) # $procmux$2256_Y
def picorv32__259(state): return (picorv32__9(state) != 0b00000) # $reduce_bool$picorv32.v:1325$488_Y
def picorv32__260(state): return If(picorv32__259(state), picorv32__138(state), BitVecVal(0b00000000000000000000000000000000, 32)) # \cpuregs_rs1
def picorv32__261(state): return If((Extract(0, 0, picorv32__32(state)) == 0b1), BitVecVal(0b00000000000000000000000000000000, 32), picorv32__127(state)) # $ternary$picorv32.v:1621$571_Y
def picorv32__262(state): return Or(picorv32__142(state),(Extract(0, 0, picorv32__40(state)) == 0b1),(Extract(0, 0, picorv32__39(state)) == 0b1),(Extract(0, 0, picorv32__38(state)) == 0b1),(Extract(0, 0, picorv32__37(state)) == 0b1),) # $auto$opt_reduce.cc:132:opt_mux$3781
def picorv32__263(state): return If(picorv32__262(state), BitVecVal(0b00000000000000000000000000000000, 32), If((Extract(0, 0, picorv32__69(state)) == 0b1), picorv32__261(state), picorv32__260(state))) # $procmux$2263_Y
def picorv32__264(state): return If(picorv32__149(state), picorv32__263(state), If(picorv32__147(state), picorv32__258(state), If(picorv32__208(state), picorv32__250(state), If(picorv32__207(state), picorv32__248(state), picorv32__90(state))))) # $procmux$2235_Y
def picorv32__265(state): return If(picorv32__99(state), picorv32__264(state), picorv32__90(state)) # $0\reg_op1[31:0]
def picorv32__266(state): return If(picorv32__102(state), If(picorv32__97(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__89(state)) # $procmux$3312_Y
def picorv32__267(state): return If((Extract(0, 0, picorv32__88(state)) == 0b1), BitVecVal(0b0, 1), picorv32__266(state)) # $procmux$3314_Y
def picorv32__268(state): return If(picorv32__101(state), picorv32__267(state), picorv32__89(state)) # $procmux$3316_Y
def picorv32__269(state): return If(picorv32__165(state), picorv32__89(state), picorv32__268(state)) # $0\mem_instr[0:0]
def picorv32__270(state): return Or(picorv32__164(state), False, picorv32__201(state), False) # $logic_or$picorv32.v:1921$675_Y
def picorv32__271(state): return If(picorv32__270(state), BitVecVal(0b0, 1), picorv32__88(state)) # $procmux$1990_Y
def picorv32__272(state): return If((Extract(0, 0, picorv32__88(state)) == 0b1), BitVecVal(0b0, 1), BitVecVal(0b1, 1)) # $4\set_mem_do_wdata[0:0]
def picorv32__273(state): return If(picorv32__202(state), picorv32__272(state), BitVecVal(0b0, 1)) # $3\set_mem_do_wdata[0:0]
def picorv32__274(state): return Or(picorv32__147(state),picorv32__148(state),picorv32__149(state),picorv32__130(state),picorv32__207(state),picorv32__237(state),picorv32__155(state),) # $auto$opt_reduce.cc:132:opt_mux$3761
def picorv32__275(state): return If(picorv32__208(state), picorv32__273(state), If(picorv32__274(state), BitVecVal(0b0, 1), BitVecVal(0b0, 1))) # $2\set_mem_do_wdata[0:0]
def picorv32__276(state): return If(picorv32__99(state), picorv32__275(state), BitVecVal(0b0, 1)) # $0\set_mem_do_wdata[0:0]
def picorv32__277(state): return If((Extract(0, 0, picorv32__276(state)) == 0b1), BitVecVal(0b1, 1), picorv32__271(state)) # $0\mem_do_wdata[0:0]
def picorv32__278(state): return If(picorv32__257(state), picorv32__85(state), picorv32__87(state)) # $procmux$2002_Y
def picorv32__279(state): return If((Extract(0, 0, picorv32__71(state)) == 0b1), BitVecVal(0b1, 1), If((Extract(0, 0, picorv32__72(state)) == 0b1), picorv32__87(state), picorv32__85(state))) # $procmux$2014_Y
def picorv32__280(state): return Or((Extract(0, 0, picorv32__73(state)) == 0b1),picorv32__142(state),(Extract(0, 0, picorv32__40(state)) == 0b1),(Extract(0, 0, picorv32__39(state)) == 0b1),(Extract(0, 0, picorv32__38(state)) == 0b1),(Extract(0, 0, picorv32__37(state)) == 0b1),) # $auto$opt_reduce.cc:132:opt_mux$3775
def picorv32__281(state): return If(picorv32__144(state), BitVecVal(0b1, 1), If(picorv32__280(state), picorv32__87(state), If(picorv32__211(state), picorv32__85(state), picorv32__279(state)))) # $procmux$2030_Y
def picorv32__282(state): return Not(Or((Extract(0, 0, picorv32__12(state)) == 0b1), False)) # $logic_and$picorv32.v:1471$514_Y
def picorv32__283(state): return If((Extract(0, 0, picorv32__26(state)) == 0b1), BitVecVal(0b1, 1), BitVecVal(0b0, 1)) # $procmux$1695_Y
def picorv32__284(state): return If((Extract(0, 0, picorv32__12(state)) == 0b1), picorv32__283(state), If(picorv32__282(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1))) # $procmux$2050_Y
def picorv32__285(state): return If(picorv32__155(state), picorv32__284(state), If(picorv32__149(state), picorv32__281(state), If(picorv32__148(state), picorv32__279(state), If(picorv32__147(state), picorv32__278(state), picorv32__87(state))))) # $procmux$2004_Y
def picorv32__286(state): return If(picorv32__99(state), picorv32__285(state), picorv32__87(state)) # $procmux$2063_Y
def picorv32__287(state): return If(picorv32__270(state), BitVecVal(0b0, 1), picorv32__286(state)) # $procmux$2065_Y
def picorv32__288(state): return ULT(picorv32__90(state), picorv32__105(state)) # \alu_ltu
def picorv32__289(state): return (picorv32__90(state) < picorv32__105(state)) # \alu_lts
def picorv32__290(state): return Not(Or(picorv32__288(state), False)) # $logic_not$picorv32.v:1239$443_Y
def picorv32__291(state): return Not(Or(picorv32__289(state), False)) # $logic_not$picorv32.v:1237$442_Y
def picorv32__292(state): return (picorv32__90(state) == picorv32__105(state)) # \alu_eq
def picorv32__293(state): return Not(Or(picorv32__292(state), False)) # $logic_not$picorv32.v:1235$441_Y
def picorv32__294(state): return If((Extract(0, 0, picorv32__19(state)) == 0b1), If(picorv32__292(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), If((Extract(0, 0, picorv32__24(state)) == 0b1), If(picorv32__293(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), If((Extract(0, 0, picorv32__20(state)) == 0b1), If(picorv32__291(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), If((Extract(0, 0, picorv32__21(state)) == 0b1), If(picorv32__290(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), If((Extract(0, 0, picorv32__74(state)) == 0b1), If(picorv32__289(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), If((Extract(0, 0, picorv32__75(state)) == 0b1), If(picorv32__288(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), BitVecVal(0b0, 1))))))) # \alu_out_0
def picorv32__295(state): return If((Extract(0, 0, picorv32__294(state)) == 0b1), BitVecVal(0b1, 1), BitVecVal(0b0, 1)) # $5\set_mem_do_rinst[0:0]
def picorv32__296(state): return If((Extract(0, 0, picorv32__64(state)) == 0b1), picorv32__295(state), BitVecVal(0b0, 1)) # $3\set_mem_do_rinst[0:0]
def picorv32__297(state): return Or(picorv32__147(state),picorv32__148(state),picorv32__149(state),picorv32__130(state),picorv32__207(state),picorv32__208(state),picorv32__155(state),) # $auto$opt_reduce.cc:132:opt_mux$3765
def picorv32__298(state): return If(picorv32__237(state), picorv32__296(state), If(picorv32__297(state), BitVecVal(0b0, 1), BitVecVal(0b0, 1))) # $2\set_mem_do_rinst[0:0]
def picorv32__299(state): return If(picorv32__99(state), picorv32__298(state), BitVecVal(0b0, 1)) # $0\set_mem_do_rinst[0:0]
def picorv32__300(state): return If((Extract(0, 0, picorv32__299(state)) == 0b1), BitVecVal(0b1, 1), picorv32__287(state)) # $0\mem_do_rinst[0:0]
def picorv32__301(state): return If(picorv32__270(state), BitVecVal(0b0, 1), picorv32__86(state)) # $procmux$1994_Y
def picorv32__302(state): return If((Extract(0, 0, picorv32__86(state)) == 0b1), BitVecVal(0b0, 1), BitVecVal(0b1, 1)) # $4\set_mem_do_rdata[0:0]
def picorv32__303(state): return If(picorv32__202(state), picorv32__302(state), BitVecVal(0b0, 1)) # $3\set_mem_do_rdata[0:0]
def picorv32__304(state): return Or(picorv32__147(state),picorv32__148(state),picorv32__149(state),picorv32__130(state),picorv32__237(state),picorv32__208(state),picorv32__155(state),) # $auto$opt_reduce.cc:132:opt_mux$3763
def picorv32__305(state): return If(picorv32__304(state), BitVecVal(0b0, 1), If(picorv32__207(state), picorv32__303(state), BitVecVal(0b0, 1))) # $2\set_mem_do_rdata[0:0]
def picorv32__306(state): return If(picorv32__99(state), picorv32__305(state), BitVecVal(0b0, 1)) # $0\set_mem_do_rdata[0:0]
def picorv32__307(state): return If((Extract(0, 0, picorv32__306(state)) == 0b1), BitVecVal(0b1, 1), picorv32__301(state)) # $0\mem_do_rdata[0:0]
def picorv32__308(state): return Not(Or((Extract(0, 0, picorv32__27(state)) == 0b1), False)) # $logic_not$picorv32.v:1552$560_Y
def picorv32__309(state): return Not(Or((Extract(0, 0, picorv32__41(state)) == 0b1), False)) # $logic_not$picorv32.v:1552$561_Y
def picorv32__310(state): return And(Or(picorv32__308(state), False), Or(picorv32__309(state), False)) # $logic_and$picorv32.v:1552$562_Y
def picorv32__311(state): return If((Extract(0, 0, picorv32__26(state)) == 0b1), picorv32__85(state), If(picorv32__310(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1))) # $procmux$2077_Y
def picorv32__312(state): return If((Extract(0, 0, picorv32__12(state)) == 0b1), picorv32__311(state), picorv32__85(state)) # $procmux$2079_Y
def picorv32__313(state): return If(picorv32__155(state), picorv32__312(state), picorv32__85(state)) # $procmux$2087_Y
def picorv32__314(state): return If(picorv32__99(state), picorv32__313(state), picorv32__85(state)) # $procmux$2090_Y
def picorv32__315(state): return If(picorv32__270(state), BitVecVal(0b0, 1), picorv32__314(state)) # $0\mem_do_prefetch[0:0]
def picorv32__316(state): return If(picorv32__160(state), picorv32__98(state), picorv32__84(state)) # $procmux$3304_Y
def picorv32__317(state): return If(picorv32__165(state), picorv32__84(state), picorv32__316(state)) # $0\mem_addr[31:0]
def picorv32__318(state): return If((Extract(0, 0, picorv32__64(state)) == 0b1), picorv32__294(state), BitVecVal(0b1, 1)) # $procmux$1730_Y
def picorv32__319(state): return Or((Extract(0, 0, picorv32__40(state)) == 0b1),(Extract(0, 0, picorv32__39(state)) == 0b1),(Extract(0, 0, picorv32__38(state)) == 0b1),(Extract(0, 0, picorv32__37(state)) == 0b1),) # \is_rdcycle_rdcycleh_rdinstr_rdinstrh
def picorv32__320(state): return If(picorv32__319(state), BitVecVal(0b1, 1), picorv32__83(state)) # $procmux$1749_Y
def picorv32__321(state): return Or(picorv32__147(state),picorv32__207(state),) # $auto$opt_reduce.cc:132:opt_mux$3769
def picorv32__322(state): return If(picorv32__155(state), BitVecVal(0b0, 1), If(picorv32__149(state), picorv32__320(state), If(picorv32__237(state), picorv32__318(state), If(picorv32__321(state), BitVecVal(0b1, 1), picorv32__83(state))))) # $procmux$1726_Y
def picorv32__323(state): return If(picorv32__99(state), picorv32__322(state), BitVecVal(0b0, 1)) # $0\latched_store[0:0]
def picorv32__324(state): return If((Extract(0, 0, picorv32__64(state)) == 0b1), picorv32__82(state), BitVecVal(0b1, 1)) # $procmux$1714_Y
def picorv32__325(state): return If(picorv32__155(state), BitVecVal(0b0, 1), If(picorv32__237(state), picorv32__324(state), picorv32__82(state))) # $procmux$1719_Y
def picorv32__326(state): return If(picorv32__99(state), picorv32__325(state), BitVecVal(0b0, 1)) # $0\latched_stalu[0:0]
def picorv32__327(state): return If((Extract(0, 0, picorv32__64(state)) == 0b1), BitVecVal(0b00000, 5), picorv32__81(state)) # $procmux$1581_Y
def picorv32__328(state): return If(picorv32__155(state), picorv32__8(state), If(picorv32__237(state), picorv32__327(state), picorv32__81(state))) # $procmux$1586_Y
def picorv32__329(state): return If(picorv32__99(state), picorv32__328(state), picorv32__81(state)) # $0\latched_rd[4:0]
def picorv32__330(state): return If((Extract(0, 0, picorv32__86(state)) == 0b1), picorv32__80(state), picorv32__68(state)) # $procmux$1634_Y
def picorv32__331(state): return If(picorv32__202(state), picorv32__330(state), picorv32__80(state)) # $procmux$1636_Y
def picorv32__332(state): return If(picorv32__155(state), BitVecVal(0b0, 1), If(picorv32__207(state), picorv32__331(state), picorv32__80(state))) # $procmux$1638_Y
def picorv32__333(state): return If(picorv32__99(state), picorv32__332(state), BitVecVal(0b0, 1)) # $0\latched_is_lu[0:0]
def picorv32__334(state): return If((Extract(0, 0, picorv32__86(state)) == 0b1), picorv32__79(state), picorv32__30(state)) # $procmux$1621_Y
def picorv32__335(state): return If(picorv32__202(state), picorv32__334(state), picorv32__79(state)) # $procmux$1623_Y
def picorv32__336(state): return If(picorv32__155(state), BitVecVal(0b0, 1), If(picorv32__207(state), picorv32__335(state), picorv32__79(state))) # $procmux$1625_Y
def picorv32__337(state): return If(picorv32__99(state), picorv32__336(state), BitVecVal(0b0, 1)) # $0\latched_is_lh[0:0]
def picorv32__338(state): return If((Extract(0, 0, picorv32__86(state)) == 0b1), picorv32__78(state), picorv32__28(state)) # $procmux$1608_Y
def picorv32__339(state): return If(picorv32__202(state), picorv32__338(state), picorv32__78(state)) # $procmux$1610_Y
def picorv32__340(state): return If(picorv32__155(state), BitVecVal(0b0, 1), If(picorv32__207(state), picorv32__339(state), picorv32__78(state))) # $procmux$1612_Y
def picorv32__341(state): return If(picorv32__99(state), picorv32__340(state), BitVecVal(0b0, 1)) # $0\latched_is_lb[0:0]
def picorv32__342(state): return If(picorv32__155(state), picorv32__2(state), picorv32__77(state)) # $procmux$1668_Y
def picorv32__343(state): return If(picorv32__99(state), picorv32__342(state), picorv32__77(state)) # $0\latched_compr[0:0]
def picorv32__344(state): return If((Extract(0, 0, picorv32__64(state)) == 0b1), picorv32__294(state), picorv32__27(state)) # $procmux$1678_Y
def picorv32__345(state): return If((Extract(0, 0, picorv32__12(state)) == 0b1), picorv32__283(state), BitVecVal(0b0, 1)) # $procmux$1697_Y
def picorv32__346(state): return If(picorv32__155(state), picorv32__345(state), If(picorv32__237(state), picorv32__344(state), picorv32__76(state))) # $procmux$1683_Y
def picorv32__347(state): return If(picorv32__99(state), picorv32__346(state), BitVecVal(0b0, 1)) # $0\latched_branch[0:0]
def picorv32__348(state): return Or((Extract(0, 0, picorv32__50(state)) == 0b1),(Extract(0, 0, picorv32__49(state)) == 0b1),(Extract(0, 0, picorv32__23(state)) == 0b1),) # $0\is_sltiu_bltu_sltu[0:0]
def picorv32__349(state): return Or((Extract(0, 0, picorv32__47(state)) == 0b1),(Extract(0, 0, picorv32__48(state)) == 0b1),(Extract(0, 0, picorv32__22(state)) == 0b1),) # $0\is_slti_blt_slt[0:0]
def picorv32__350(state): return (Extract(14, 12, picorv32__117(state)) == BitVecVal(0b001, 3)) # $eq$picorv32.v:1023$250_Y
def picorv32__351(state): return Not(Or((Extract(25, 25, picorv32__117(state)) == 0b1),(Extract(26, 26, picorv32__117(state)) == 0b1),(Extract(27, 27, picorv32__117(state)) == 0b1),(Extract(28, 28, picorv32__117(state)) == 0b1),(Extract(29, 29, picorv32__117(state)) == 0b1),(Extract(30, 30, picorv32__117(state)) == 0b1),(Extract(31, 31, picorv32__117(state)) == 0b1),)) # $eq$picorv32.v:1046$290_Y
def picorv32__352(state): return And(Or(picorv32__350(state), False), Or(picorv32__351(state), False)) # $logic_and$picorv32.v:1077$401_Y
def picorv32__353(state): return (Extract(14, 12, picorv32__117(state)) == BitVecVal(0b101, 3)) # $eq$picorv32.v:1025$254_Y
def picorv32__354(state): return And(Or(picorv32__353(state), False), Or(picorv32__351(state), False)) # $logic_and$picorv32.v:1078$398_Y
def picorv32__355(state): return (Extract(31, 25, picorv32__117(state)) == BitVecVal(0b0100000, 7)) # $eq$picorv32.v:1048$298_Y
def picorv32__356(state): return And(Or(picorv32__353(state), False), Or(picorv32__355(state), False)) # $logic_and$picorv32.v:1080$395_Y
def picorv32__357(state): return Or(picorv32__352(state),picorv32__354(state),picorv32__356(state),) # $reduce_or$picorv32.v:1080$402_Y
def picorv32__358(state): return And(Or((Extract(0, 0, picorv32__62(state)) == 0b1), False), Or(picorv32__357(state), False)) # $logic_and$picorv32.v:1080$403_Y
def picorv32__359(state): return Not(Or((Extract(0, 0, picorv32__11(state)) == 0b1), False)) # $logic_not$picorv32.v:1019$246_Y
def picorv32__360(state): return And(Or((Extract(0, 0, picorv32__12(state)) == 0b1), False), Or(picorv32__359(state), False)) # $logic_and$picorv32.v:1019$247_Y
def picorv32__361(state): return If(picorv32__360(state), If(picorv32__358(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__73(state)) # $0\is_slli_srli_srai[0:0]
def picorv32__362(state): return And(Or((Extract(0, 0, picorv32__63(state)) == 0b1), False), Or(picorv32__357(state), False)) # $logic_and$picorv32.v:1095$423_Y
def picorv32__363(state): return If(picorv32__360(state), If(picorv32__362(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__72(state)) # $0\is_sll_srl_sra[0:0]
def picorv32__364(state): return If(picorv32__169(state), picorv32__116(state), picorv32__117(state)) # \mem_rdata_latched
def picorv32__365(state): return (Extract(6, 0, picorv32__364(state)) == BitVecVal(0b0100011, 7)) # $eq$picorv32.v:858$192_Y
def picorv32__366(state): return And(Or((Extract(0, 0, picorv32__87(state)) == 0b1), False), Or(picorv32__201(state), False)) # $logic_and$picorv32.v:1425$510_Y
def picorv32__367(state): return If(picorv32__366(state), If(picorv32__365(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__71(state)) # $0\is_sb_sh_sw[0:0]
def picorv32__368(state): return Or((Extract(0, 0, picorv32__55(state)) == 0b1),(Extract(0, 0, picorv32__14(state)) == 0b1),(Extract(0, 0, picorv32__15(state)) == 0b1),(Extract(0, 0, picorv32__27(state)) == 0b1),(Extract(0, 0, picorv32__26(state)) == 0b1),(Extract(0, 0, picorv32__18(state)) == 0b1),(Extract(0, 0, picorv32__32(state)) == 0b1),) # $reduce_or$picorv32.v:842$170_Y
def picorv32__369(state): return If(picorv32__360(state), BitVecVal(0b0, 1), If(picorv32__368(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1))) # $0\is_lui_auipc_jal_jalr_addi_add_sub[0:0]
def picorv32__370(state): return Or((Extract(0, 0, picorv32__26(state)) == 0b1),(Extract(0, 0, picorv32__18(state)) == 0b1),(Extract(0, 0, picorv32__32(state)) == 0b1),) # $0\is_lui_auipc_jal[0:0]
def picorv32__371(state): return Or((Extract(0, 0, picorv32__31(state)) == 0b1),(Extract(0, 0, picorv32__29(state)) == 0b1),(Extract(0, 0, picorv32__33(state)) == 0b1),) # $0\is_lbu_lhu_lw[0:0]
def picorv32__372(state): return (Extract(6, 0, picorv32__364(state)) == BitVecVal(0b0000011, 7)) # $eq$picorv32.v:857$191_Y
def picorv32__373(state): return If(picorv32__366(state), If(picorv32__372(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__67(state)) # $0\is_lb_lh_lw_lbu_lhu[0:0]
def picorv32__374(state): return (Extract(14, 12, picorv32__117(state)) == BitVecVal(0b011, 3)) # $eq$picorv32.v:1041$280_Y
def picorv32__375(state): return (Extract(14, 12, picorv32__117(state)) == BitVecVal(0b010, 3)) # $eq$picorv32.v:1031$264_Y
def picorv32__376(state): return (Extract(14, 12, picorv32__117(state)) == BitVecVal(0b111, 3)) # $eq$picorv32.v:1027$258_Y
def picorv32__377(state): return (Extract(14, 12, picorv32__117(state)) == BitVecVal(0b110, 3)) # $eq$picorv32.v:1026$256_Y
def picorv32__378(state): return (Extract(14, 12, picorv32__117(state)) == BitVecVal(0b100, 3)) # $eq$picorv32.v:1024$252_Y
def picorv32__379(state): return Not(Or((Extract(12, 12, picorv32__117(state)) == 0b1),(Extract(13, 13, picorv32__117(state)) == 0b1),(Extract(14, 14, picorv32__117(state)) == 0b1),)) # $eq$picorv32.v:1022$248_Y
def picorv32__380(state): return Or(picorv32__374(state),picorv32__375(state),picorv32__376(state),picorv32__377(state),picorv32__378(state),picorv32__379(state),) # $reduce_or$picorv32.v:1089$410_Y
def picorv32__381(state): return And(Or((Extract(0, 0, picorv32__62(state)) == 0b1), False), Or(picorv32__380(state), False)) # $logic_and$picorv32.v:1089$411_Y
def picorv32__382(state): return Or((Extract(0, 0, picorv32__27(state)) == 0b1), False, picorv32__381(state), False) # $logic_or$picorv32.v:1089$412_Y
def picorv32__383(state): return If(picorv32__360(state), If(picorv32__382(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__66(state)) # $0\is_jalr_addi_slti_sltiu_xori_ori_andi[0:0]
def picorv32__384(state): return Or((Extract(0, 0, picorv32__64(state)) == 0b1),(Extract(0, 0, picorv32__50(state)) == 0b1),(Extract(0, 0, picorv32__47(state)) == 0b1),(Extract(0, 0, picorv32__49(state)) == 0b1),(Extract(0, 0, picorv32__48(state)) == 0b1),) # $reduce_or$picorv32.v:846$174_Y
def picorv32__385(state): return If(picorv32__360(state), BitVecVal(0b0, 1), If(picorv32__384(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1))) # $procmux$2716_Y
def picorv32__386(state): return If(picorv32__99(state), picorv32__385(state), BitVecVal(0b0, 1)) # $0\is_compare[0:0]
def picorv32__387(state): return (Extract(6, 0, picorv32__364(state)) == BitVecVal(0b1100011, 7)) # $eq$picorv32.v:856$190_Y
def picorv32__388(state): return If(picorv32__366(state), If(picorv32__387(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__64(state)) # $procmux$2675_Y
def picorv32__389(state): return If(picorv32__99(state), picorv32__388(state), BitVecVal(0b0, 1)) # $0\is_beq_bne_blt_bge_bltu_bgeu[0:0]
def picorv32__390(state): return (Extract(6, 0, picorv32__364(state)) == BitVecVal(0b0110011, 7)) # $eq$picorv32.v:860$194_Y
def picorv32__391(state): return If(picorv32__366(state), If(picorv32__390(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__63(state)) # $0\is_alu_reg_reg[0:0]
def picorv32__392(state): return (Extract(6, 0, picorv32__364(state)) == BitVecVal(0b0010011, 7)) # $eq$picorv32.v:859$193_Y
def picorv32__393(state): return If(picorv32__366(state), If(picorv32__392(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__62(state)) # $0\is_alu_reg_imm[0:0]
def picorv32__394(state): return And(Or((Extract(0, 0, picorv32__62(state)) == 0b1), False), Or(picorv32__378(state), False)) # $logic_and$picorv32.v:1042$283_Y
def picorv32__395(state): return If(picorv32__360(state), If(picorv32__394(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__60(state)) # $procmux$2885_Y
def picorv32__396(state): return If(picorv32__99(state), picorv32__395(state), BitVecVal(0b0, 1)) # $0\instr_xori[0:0]
def picorv32__397(state): return And(Or((Extract(0, 0, picorv32__63(state)) == 0b1), False), Or(picorv32__378(state), False)) # $logic_and$picorv32.v:1055$321_Y
def picorv32__398(state): return And(Or(picorv32__397(state), False), Or(picorv32__351(state), False)) # $logic_and$picorv32.v:1055$323_Y
def picorv32__399(state): return If(picorv32__360(state), If(picorv32__398(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__59(state)) # $procmux$2847_Y
def picorv32__400(state): return If(picorv32__99(state), picorv32__399(state), BitVecVal(0b0, 1)) # $0\instr_xor[0:0]
def picorv32__401(state): return If(picorv32__366(state), BitVecVal(0b0, 1), picorv32__58(state)) # $0\instr_waitirq[0:0]
def picorv32__402(state): return If(picorv32__360(state), BitVecVal(0b0, 1), picorv32__57(state)) # $0\instr_timer[0:0]
def picorv32__403(state): return And(Or((Extract(0, 0, picorv32__71(state)) == 0b1), False), Or(picorv32__375(state), False)) # $logic_and$picorv32.v:1037$275_Y
def picorv32__404(state): return If(picorv32__360(state), If(picorv32__403(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__56(state)) # $0\instr_sw[0:0]
def picorv32__405(state): return And(Or((Extract(0, 0, picorv32__63(state)) == 0b1), False), Or(picorv32__379(state), False)) # $logic_and$picorv32.v:1050$301_Y
def picorv32__406(state): return And(Or(picorv32__405(state), False), Or(picorv32__355(state), False)) # $logic_and$picorv32.v:1051$307_Y
def picorv32__407(state): return If(picorv32__360(state), If(picorv32__406(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__55(state)) # $procmux$2863_Y
def picorv32__408(state): return If(picorv32__99(state), picorv32__407(state), BitVecVal(0b0, 1)) # $0\instr_sub[0:0]
def picorv32__409(state): return And(Or((Extract(0, 0, picorv32__62(state)) == 0b1), False), Or(picorv32__353(state), False)) # $logic_and$picorv32.v:1047$293_Y
def picorv32__410(state): return And(Or(picorv32__409(state), False), Or(picorv32__351(state), False)) # $logic_and$picorv32.v:1047$295_Y
def picorv32__411(state): return If(picorv32__360(state), If(picorv32__410(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__54(state)) # $0\instr_srli[0:0]
def picorv32__412(state): return And(Or((Extract(0, 0, picorv32__63(state)) == 0b1), False), Or(picorv32__353(state), False)) # $logic_and$picorv32.v:1056$325_Y
def picorv32__413(state): return And(Or(picorv32__412(state), False), Or(picorv32__351(state), False)) # $logic_and$picorv32.v:1056$327_Y
def picorv32__414(state): return If(picorv32__360(state), If(picorv32__413(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__53(state)) # $procmux$2843_Y
def picorv32__415(state): return If(picorv32__99(state), picorv32__414(state), BitVecVal(0b0, 1)) # $0\instr_srl[0:0]
def picorv32__416(state): return And(Or(picorv32__409(state), False), Or(picorv32__355(state), False)) # $logic_and$picorv32.v:1048$299_Y
def picorv32__417(state): return If(picorv32__360(state), If(picorv32__416(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__52(state)) # $0\instr_srai[0:0]
def picorv32__418(state): return And(Or(picorv32__412(state), False), Or(picorv32__355(state), False)) # $logic_and$picorv32.v:1057$331_Y
def picorv32__419(state): return If(picorv32__360(state), If(picorv32__418(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__51(state)) # $procmux$2839_Y
def picorv32__420(state): return If(picorv32__99(state), picorv32__419(state), BitVecVal(0b0, 1)) # $0\instr_sra[0:0]
def picorv32__421(state): return And(Or((Extract(0, 0, picorv32__63(state)) == 0b1), False), Or(picorv32__374(state), False)) # $logic_and$picorv32.v:1054$317_Y
def picorv32__422(state): return And(Or(picorv32__421(state), False), Or(picorv32__351(state), False)) # $logic_and$picorv32.v:1054$319_Y
def picorv32__423(state): return If(picorv32__360(state), If(picorv32__422(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__50(state)) # $procmux$2851_Y
def picorv32__424(state): return If(picorv32__99(state), picorv32__423(state), BitVecVal(0b0, 1)) # $0\instr_sltu[0:0]
def picorv32__425(state): return And(Or((Extract(0, 0, picorv32__62(state)) == 0b1), False), Or(picorv32__374(state), False)) # $logic_and$picorv32.v:1041$281_Y
def picorv32__426(state): return If(picorv32__360(state), If(picorv32__425(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__49(state)) # $procmux$2889_Y
def picorv32__427(state): return If(picorv32__99(state), picorv32__426(state), BitVecVal(0b0, 1)) # $0\instr_sltiu[0:0]
def picorv32__428(state): return And(Or((Extract(0, 0, picorv32__62(state)) == 0b1), False), Or(picorv32__375(state), False)) # $logic_and$picorv32.v:1040$279_Y
def picorv32__429(state): return If(picorv32__360(state), If(picorv32__428(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__48(state)) # $procmux$2893_Y
def picorv32__430(state): return If(picorv32__99(state), picorv32__429(state), BitVecVal(0b0, 1)) # $0\instr_slti[0:0]
def picorv32__431(state): return And(Or((Extract(0, 0, picorv32__63(state)) == 0b1), False), Or(picorv32__375(state), False)) # $logic_and$picorv32.v:1053$313_Y
def picorv32__432(state): return And(Or(picorv32__431(state), False), Or(picorv32__351(state), False)) # $logic_and$picorv32.v:1053$315_Y
def picorv32__433(state): return If(picorv32__360(state), If(picorv32__432(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__47(state)) # $procmux$2855_Y
def picorv32__434(state): return If(picorv32__99(state), picorv32__433(state), BitVecVal(0b0, 1)) # $0\instr_slt[0:0]
def picorv32__435(state): return And(Or((Extract(0, 0, picorv32__62(state)) == 0b1), False), Or(picorv32__350(state), False)) # $logic_and$picorv32.v:1046$289_Y
def picorv32__436(state): return And(Or(picorv32__435(state), False), Or(picorv32__351(state), False)) # $logic_and$picorv32.v:1046$291_Y
def picorv32__437(state): return If(picorv32__360(state), If(picorv32__436(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__46(state)) # $0\instr_slli[0:0]
def picorv32__438(state): return And(Or((Extract(0, 0, picorv32__63(state)) == 0b1), False), Or(picorv32__350(state), False)) # $logic_and$picorv32.v:1052$309_Y
def picorv32__439(state): return And(Or(picorv32__438(state), False), Or(picorv32__351(state), False)) # $logic_and$picorv32.v:1052$311_Y
def picorv32__440(state): return If(picorv32__360(state), If(picorv32__439(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__45(state)) # $procmux$2859_Y
def picorv32__441(state): return If(picorv32__99(state), picorv32__440(state), BitVecVal(0b0, 1)) # $0\instr_sll[0:0]
def picorv32__442(state): return And(Or((Extract(0, 0, picorv32__71(state)) == 0b1), False), Or(picorv32__350(state), False)) # $logic_and$picorv32.v:1036$273_Y
def picorv32__443(state): return If(picorv32__360(state), If(picorv32__442(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__44(state)) # $0\instr_sh[0:0]
def picorv32__444(state): return If(picorv32__360(state), BitVecVal(0b0, 1), picorv32__43(state)) # $0\instr_setq[0:0]
def picorv32__445(state): return And(Or((Extract(0, 0, picorv32__71(state)) == 0b1), False), Or(picorv32__379(state), False)) # $logic_and$picorv32.v:1035$271_Y
def picorv32__446(state): return If(picorv32__360(state), If(picorv32__445(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__42(state)) # $0\instr_sb[0:0]
def picorv32__447(state): return If(picorv32__366(state), BitVecVal(0b0, 1), picorv32__41(state)) # $0\instr_retirq[0:0]
def picorv32__448(state): return (Extract(6, 0, picorv32__117(state)) == BitVecVal(0b1110011, 7)) # $eq$picorv32.v:1061$340_Y
def picorv32__449(state): return (Extract(31, 12, picorv32__117(state)) == BitVecVal(0b11001000001000000010, 20)) # $eq$picorv32.v:1066$362_Y
def picorv32__450(state): return And(Or(picorv32__448(state), False), Or(picorv32__449(state), False)) # $logic_and$picorv32.v:1066$363_Y
def picorv32__451(state): return If(picorv32__360(state), If(picorv32__450(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__40(state)) # $0\instr_rdinstrh[0:0]
def picorv32__452(state): return (Extract(31, 12, picorv32__117(state)) == BitVecVal(0b11000000001000000010, 20)) # $eq$picorv32.v:1065$358_Y
def picorv32__453(state): return And(Or(picorv32__448(state), False), Or(picorv32__452(state), False)) # $logic_and$picorv32.v:1065$359_Y
def picorv32__454(state): return If(picorv32__360(state), If(picorv32__453(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__39(state)) # $0\instr_rdinstr[0:0]
def picorv32__455(state): return (Extract(31, 12, picorv32__117(state)) == BitVecVal(0b11001000000000000010, 20)) # $eq$picorv32.v:1063$349_Y
def picorv32__456(state): return And(Or(picorv32__448(state), False), Or(picorv32__455(state), False)) # $logic_and$picorv32.v:1063$350_Y
def picorv32__457(state): return (Extract(31, 12, picorv32__117(state)) == BitVecVal(0b11001000000100000010, 20)) # $eq$picorv32.v:1064$352_Y
def picorv32__458(state): return And(Or(picorv32__448(state), False), Or(picorv32__457(state), False)) # $logic_and$picorv32.v:1064$353_Y
def picorv32__459(state): return Or(picorv32__456(state), False, picorv32__458(state), False) # $logic_and$picorv32.v:1064$355_Y
def picorv32__460(state): return If(picorv32__360(state), If(picorv32__459(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__38(state)) # $0\instr_rdcycleh[0:0]
def picorv32__461(state): return (Extract(31, 12, picorv32__117(state)) == BitVecVal(0b11000000000000000010, 20)) # $eq$picorv32.v:1061$341_Y
def picorv32__462(state): return And(Or(picorv32__448(state), False), Or(picorv32__461(state), False)) # $logic_and$picorv32.v:1061$342_Y
def picorv32__463(state): return (Extract(31, 12, picorv32__117(state)) == BitVecVal(0b11000000000100000010, 20)) # $eq$picorv32.v:1062$344_Y
def picorv32__464(state): return And(Or(picorv32__448(state), False), Or(picorv32__463(state), False)) # $logic_and$picorv32.v:1062$345_Y
def picorv32__465(state): return Or(picorv32__462(state), False, picorv32__464(state), False) # $logic_and$picorv32.v:1062$347_Y
def picorv32__466(state): return If(picorv32__360(state), If(picorv32__465(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__37(state)) # $0\instr_rdcycle[0:0]
def picorv32__467(state): return And(Or((Extract(0, 0, picorv32__62(state)) == 0b1), False), Or(picorv32__377(state), False)) # $logic_and$picorv32.v:1043$285_Y
def picorv32__468(state): return If(picorv32__360(state), If(picorv32__467(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__36(state)) # $procmux$2881_Y
def picorv32__469(state): return If(picorv32__99(state), picorv32__468(state), BitVecVal(0b0, 1)) # $0\instr_ori[0:0]
def picorv32__470(state): return And(Or((Extract(0, 0, picorv32__63(state)) == 0b1), False), Or(picorv32__377(state), False)) # $logic_and$picorv32.v:1058$333_Y
def picorv32__471(state): return And(Or(picorv32__470(state), False), Or(picorv32__351(state), False)) # $logic_and$picorv32.v:1058$335_Y
def picorv32__472(state): return If(picorv32__360(state), If(picorv32__471(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__35(state)) # $procmux$2835_Y
def picorv32__473(state): return If(picorv32__99(state), picorv32__472(state), BitVecVal(0b0, 1)) # $0\instr_or[0:0]
def picorv32__474(state): return If(picorv32__360(state), BitVecVal(0b0, 1), picorv32__34(state)) # $0\instr_maskirq[0:0]
def picorv32__475(state): return And(Or((Extract(0, 0, picorv32__67(state)) == 0b1), False), Or(picorv32__375(state), False)) # $logic_and$picorv32.v:1031$265_Y
def picorv32__476(state): return If(picorv32__360(state), If(picorv32__475(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__33(state)) # $0\instr_lw[0:0]
def picorv32__477(state): return (Extract(6, 0, picorv32__364(state)) == BitVecVal(0b0110111, 7)) # $eq$picorv32.v:849$176_Y
def picorv32__478(state): return If(picorv32__366(state), If(picorv32__477(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__32(state)) # $0\instr_lui[0:0]
def picorv32__479(state): return And(Or((Extract(0, 0, picorv32__67(state)) == 0b1), False), Or(picorv32__353(state), False)) # $logic_and$picorv32.v:1033$269_Y
def picorv32__480(state): return If(picorv32__360(state), If(picorv32__479(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__31(state)) # $0\instr_lhu[0:0]
def picorv32__481(state): return And(Or((Extract(0, 0, picorv32__67(state)) == 0b1), False), Or(picorv32__350(state), False)) # $logic_and$picorv32.v:1030$263_Y
def picorv32__482(state): return If(picorv32__360(state), If(picorv32__481(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__30(state)) # $0\instr_lh[0:0]
def picorv32__483(state): return And(Or((Extract(0, 0, picorv32__67(state)) == 0b1), False), Or(picorv32__378(state), False)) # $logic_and$picorv32.v:1032$267_Y
def picorv32__484(state): return If(picorv32__360(state), If(picorv32__483(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__29(state)) # $0\instr_lbu[0:0]
def picorv32__485(state): return And(Or((Extract(0, 0, picorv32__67(state)) == 0b1), False), Or(picorv32__379(state), False)) # $logic_and$picorv32.v:1029$261_Y
def picorv32__486(state): return If(picorv32__360(state), If(picorv32__485(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__28(state)) # $0\instr_lb[0:0]
def picorv32__487(state): return (Extract(6, 0, picorv32__364(state)) == BitVecVal(0b1100111, 7)) # $eq$picorv32.v:852$179_Y
def picorv32__488(state): return Not(Or((Extract(12, 12, picorv32__364(state)) == 0b1),(Extract(13, 13, picorv32__364(state)) == 0b1),(Extract(14, 14, picorv32__364(state)) == 0b1),)) # $eq$picorv32.v:852$180_Y
def picorv32__489(state): return And(Or(picorv32__487(state), False), Or(picorv32__488(state), False)) # $logic_and$picorv32.v:852$181_Y
def picorv32__490(state): return If(picorv32__366(state), If(picorv32__489(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__27(state)) # $0\instr_jalr[0:0]
def picorv32__491(state): return (Extract(6, 0, picorv32__364(state)) == BitVecVal(0b1101111, 7)) # $eq$picorv32.v:851$178_Y
def picorv32__492(state): return If(picorv32__366(state), If(picorv32__491(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__26(state)) # $0\instr_jal[0:0]
def picorv32__493(state): return If(picorv32__360(state), BitVecVal(0b0, 1), picorv32__25(state)) # $0\instr_getq[0:0]
def picorv32__494(state): return And(Or((Extract(0, 0, picorv32__64(state)) == 0b1), False), Or(picorv32__350(state), False)) # $logic_and$picorv32.v:1023$251_Y
def picorv32__495(state): return If(picorv32__360(state), If(picorv32__494(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__24(state)) # $procmux$2933_Y
def picorv32__496(state): return If(picorv32__99(state), picorv32__495(state), BitVecVal(0b0, 1)) # $0\instr_bne[0:0]
def picorv32__497(state): return And(Or((Extract(0, 0, picorv32__64(state)) == 0b1), False), Or(picorv32__377(state), False)) # $logic_and$picorv32.v:1026$257_Y
def picorv32__498(state): return If(picorv32__360(state), If(picorv32__497(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__23(state)) # $procmux$2921_Y
def picorv32__499(state): return If(picorv32__99(state), picorv32__498(state), BitVecVal(0b0, 1)) # $0\instr_bltu[0:0]
def picorv32__500(state): return And(Or((Extract(0, 0, picorv32__64(state)) == 0b1), False), Or(picorv32__378(state), False)) # $logic_and$picorv32.v:1024$253_Y
def picorv32__501(state): return If(picorv32__360(state), If(picorv32__500(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__22(state)) # $procmux$2929_Y
def picorv32__502(state): return If(picorv32__99(state), picorv32__501(state), BitVecVal(0b0, 1)) # $0\instr_blt[0:0]
def picorv32__503(state): return And(Or((Extract(0, 0, picorv32__64(state)) == 0b1), False), Or(picorv32__376(state), False)) # $logic_and$picorv32.v:1027$259_Y
def picorv32__504(state): return If(picorv32__360(state), If(picorv32__503(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__21(state)) # $procmux$2917_Y
def picorv32__505(state): return If(picorv32__99(state), picorv32__504(state), BitVecVal(0b0, 1)) # $0\instr_bgeu[0:0]
def picorv32__506(state): return And(Or((Extract(0, 0, picorv32__64(state)) == 0b1), False), Or(picorv32__353(state), False)) # $logic_and$picorv32.v:1025$255_Y
def picorv32__507(state): return If(picorv32__360(state), If(picorv32__506(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__20(state)) # $procmux$2925_Y
def picorv32__508(state): return If(picorv32__99(state), picorv32__507(state), BitVecVal(0b0, 1)) # $0\instr_bge[0:0]
def picorv32__509(state): return And(Or((Extract(0, 0, picorv32__64(state)) == 0b1), False), Or(picorv32__379(state), False)) # $logic_and$picorv32.v:1022$249_Y
def picorv32__510(state): return If(picorv32__360(state), If(picorv32__509(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__19(state)) # $procmux$2937_Y
def picorv32__511(state): return If(picorv32__99(state), picorv32__510(state), BitVecVal(0b0, 1)) # $0\instr_beq[0:0]
def picorv32__512(state): return (Extract(6, 0, picorv32__364(state)) == BitVecVal(0b0010111, 7)) # $eq$picorv32.v:850$177_Y
def picorv32__513(state): return If(picorv32__366(state), If(picorv32__512(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__18(state)) # $0\instr_auipc[0:0]
def picorv32__514(state): return And(Or((Extract(0, 0, picorv32__62(state)) == 0b1), False), Or(picorv32__376(state), False)) # $logic_and$picorv32.v:1044$287_Y
def picorv32__515(state): return If(picorv32__360(state), If(picorv32__514(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__17(state)) # $procmux$2877_Y
def picorv32__516(state): return If(picorv32__99(state), picorv32__515(state), BitVecVal(0b0, 1)) # $0\instr_andi[0:0]
def picorv32__517(state): return And(Or((Extract(0, 0, picorv32__63(state)) == 0b1), False), Or(picorv32__376(state), False)) # $logic_and$picorv32.v:1059$337_Y
def picorv32__518(state): return And(Or(picorv32__517(state), False), Or(picorv32__351(state), False)) # $logic_and$picorv32.v:1059$339_Y
def picorv32__519(state): return If(picorv32__360(state), If(picorv32__518(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__16(state)) # $procmux$2831_Y
def picorv32__520(state): return If(picorv32__99(state), picorv32__519(state), BitVecVal(0b0, 1)) # $0\instr_and[0:0]
def picorv32__521(state): return And(Or((Extract(0, 0, picorv32__62(state)) == 0b1), False), Or(picorv32__379(state), False)) # $logic_and$picorv32.v:1039$277_Y
def picorv32__522(state): return If(picorv32__360(state), If(picorv32__521(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__15(state)) # $procmux$2897_Y
def picorv32__523(state): return If(picorv32__99(state), picorv32__522(state), BitVecVal(0b0, 1)) # $0\instr_addi[0:0]
def picorv32__524(state): return And(Or(picorv32__405(state), False), Or(picorv32__351(state), False)) # $logic_and$picorv32.v:1050$303_Y
def picorv32__525(state): return If(picorv32__360(state), If(picorv32__524(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)), picorv32__14(state)) # $procmux$2867_Y
def picorv32__526(state): return If(picorv32__99(state), picorv32__525(state), BitVecVal(0b0, 1)) # $0\instr_add[0:0]
def picorv32__527(state): return If(picorv32__99(state), picorv32__13(state), BitVecVal(0b00000000000000000000000000000000, 32)) # $0\eoi[31:0]
def picorv32__528(state): return And(Or(picorv32__192(state), False), Or(picorv32__201(state), False)) # $logic_and$picorv32.v:1851$635_Y
def picorv32__529(state): return If(picorv32__528(state), BitVecVal(0b1, 1), If(picorv32__366(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1))) # $procmux$1369_Y
def picorv32__530(state): return If(picorv32__202(state), picorv32__529(state), If(picorv32__366(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1))) # $procmux$1371_Y
def picorv32__531(state): return If((Extract(0, 0, picorv32__294(state)) == 0b1), BitVecVal(0b0, 1), If(picorv32__366(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1))) # $procmux$1383_Y
def picorv32__532(state): return If((Extract(0, 0, picorv32__64(state)) == 0b1), picorv32__531(state), If(picorv32__366(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1))) # $procmux$1385_Y
def picorv32__533(state): return Or(picorv32__207(state),picorv32__208(state),) # $auto$opt_reduce.cc:132:opt_mux$3787
def picorv32__534(state): return If(picorv32__237(state), picorv32__532(state), If(picorv32__533(state), picorv32__530(state), If(picorv32__366(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)))) # $procmux$1373_Y
def picorv32__535(state): return If(picorv32__99(state), picorv32__534(state), If(picorv32__366(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1))) # $0\decoder_trigger[0:0]
def picorv32__536(state): return If(picorv32__528(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)) # $procmux$1352_Y
def picorv32__537(state): return If(picorv32__202(state), picorv32__536(state), BitVecVal(0b0, 1)) # $procmux$1354_Y
def picorv32__538(state): return If(picorv32__533(state), picorv32__537(state), BitVecVal(0b0, 1)) # $procmux$1356_Y
def picorv32__539(state): return If(picorv32__99(state), picorv32__538(state), BitVecVal(0b0, 1)) # $0\decoder_pseudo_trigger[0:0]
def picorv32__540(state): return If(picorv32__366(state), Extract(24, 20, picorv32__364(state)), picorv32__10(state)) # $0\decoded_rs2[4:0]
def picorv32__541(state): return If(picorv32__366(state), Extract(18, 15, picorv32__364(state)), Extract(3, 0, picorv32__9(state))) # $0\decoded_rs1[4:0] [3:0]
def picorv32__542(state): return If(picorv32__366(state), Extract(19, 19, picorv32__364(state)), Extract(4, 4, picorv32__9(state))) # $0\decoded_rs1[4:0] [4]
def picorv32__543(state): return If(picorv32__366(state), Extract(11, 7, picorv32__364(state)), picorv32__8(state)) # $0\decoded_rd[4:0]
def picorv32__544(state): return If(picorv32__366(state), BitVecVal(0b0, 1), Extract(0, 0, picorv32__7(state))) # $0\decoded_imm_j[31:0] [0]
def picorv32__545(state): return If(picorv32__366(state), Extract(23, 21, picorv32__364(state)), Extract(3, 1, picorv32__7(state))) # $0\decoded_imm_j[31:0] [3:1]
def picorv32__546(state): return If(picorv32__366(state), Extract(24, 24, picorv32__364(state)), Extract(4, 4, picorv32__7(state))) # $0\decoded_imm_j[31:0] [4]
def picorv32__547(state): return If(picorv32__366(state), Extract(25, 25, picorv32__364(state)), Extract(5, 5, picorv32__7(state))) # $0\decoded_imm_j[31:0] [5]
def picorv32__548(state): return If(picorv32__366(state), Extract(26, 26, picorv32__364(state)), Extract(6, 6, picorv32__7(state))) # $0\decoded_imm_j[31:0] [6]
def picorv32__549(state): return If(picorv32__366(state), Extract(27, 27, picorv32__364(state)), Extract(7, 7, picorv32__7(state))) # $0\decoded_imm_j[31:0] [7]
def picorv32__550(state): return If(picorv32__366(state), Extract(29, 28, picorv32__364(state)), Extract(9, 8, picorv32__7(state))) # $0\decoded_imm_j[31:0] [9:8]
def picorv32__551(state): return If(picorv32__366(state), Extract(30, 30, picorv32__364(state)), Extract(10, 10, picorv32__7(state))) # $0\decoded_imm_j[31:0] [10]
def picorv32__552(state): return If(picorv32__366(state), Extract(20, 20, picorv32__364(state)), Extract(11, 11, picorv32__7(state))) # $0\decoded_imm_j[31:0] [11]
def picorv32__553(state): return If(picorv32__366(state), Extract(19, 12, picorv32__364(state)), Extract(19, 12, picorv32__7(state))) # $0\decoded_imm_j[31:0] [19:12]
def picorv32__554(state): return If(picorv32__366(state), Concat(Extract(31, 31, picorv32__364(state)),  Concat(Extract(31, 31, picorv32__364(state)),  Concat(Extract(31, 31, picorv32__364(state)),  Concat(Extract(31, 31, picorv32__364(state)),  Concat(Extract(31, 31, picorv32__364(state)),  Concat(Extract(31, 31, picorv32__364(state)),  Concat(Extract(31, 31, picorv32__364(state)),  Concat(Extract(31, 31, picorv32__364(state)),  Concat(Extract(31, 31, picorv32__364(state)),  Concat(Extract(31, 31, picorv32__364(state)),  Concat(Extract(31, 31, picorv32__364(state)), Extract(31, 31, picorv32__364(state))))))))))))), Extract(31, 20, picorv32__7(state))) # $0\decoded_imm_j[31:0] [31:20]
def picorv32__555(state): return Or((Extract(0, 0, picorv32__62(state)) == 0b1),(Extract(0, 0, picorv32__67(state)) == 0b1),(Extract(0, 0, picorv32__27(state)) == 0b1),) # $procmux$2724_CMP
def picorv32__556(state): return Or((Extract(0, 0, picorv32__18(state)) == 0b1),(Extract(0, 0, picorv32__32(state)) == 0b1),) # $procmux$2725_CMP
def picorv32__557(state): return If((Extract(0, 0, picorv32__26(state)) == 0b1), picorv32__7(state), If(picorv32__556(state), Concat(Extract(31, 12, picorv32__117(state)), BitVecVal(0b000000000000, 12)), If(picorv32__555(state), Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)), Extract(31, 20, picorv32__117(state)))))))))))))))))))))), If((Extract(0, 0, picorv32__64(state)) == 0b1), Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(7, 7, picorv32__117(state)),  Concat(Extract(30, 25, picorv32__117(state)),  Concat(Extract(11, 8, picorv32__117(state)), BitVecVal(0b0, 1)))))))))))))))))))))))), If((Extract(0, 0, picorv32__71(state)) == 0b1), Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 31, picorv32__117(state)),  Concat(Extract(31, 25, picorv32__117(state)), Extract(11, 7, picorv32__117(state))))))))))))))))))))))), BitVecVal(0b00000000000000000000000000000000, 32)))))) # $procmux$2721_Y
def picorv32__558(state): return If(picorv32__360(state), picorv32__557(state), picorv32__6(state)) # $0\decoded_imm[31:0]
def picorv32__559(state): return If(picorv32__528(state), BitVecVal(0b01000000, 8), picorv32__5(state)) # $procmux$1787_Y
def picorv32__560(state): return If(picorv32__202(state), picorv32__559(state), picorv32__5(state)) # $procmux$1789_Y
def picorv32__561(state): return If(picorv32__257(state), BitVecVal(0b01000000, 8), picorv32__5(state)) # $procmux$1800_Y
def picorv32__562(state): return If(picorv32__201(state), BitVecVal(0b01000000, 8), picorv32__5(state)) # $procmux$1804_Y
def picorv32__563(state): return If((Extract(0, 0, picorv32__64(state)) == 0b1), picorv32__562(state), BitVecVal(0b01000000, 8)) # $procmux$1806_Y
def picorv32__564(state): return If((Extract(0, 0, picorv32__71(state)) == 0b1), BitVecVal(0b0010, 4), If((Extract(0, 0, picorv32__72(state)) == 0b1), BitVecVal(0b0100, 4), BitVecVal(0b1000, 4))) # $auto$wreduce.cc:452:run$3795 [3:0]
def picorv32__565(state): return If(picorv32__142(state), BitVecVal(0b10000000, 8), If(picorv32__319(state), BitVecVal(0b01000000, 8), If(picorv32__144(state), BitVecVal(0b00000001, 8), If((Extract(0, 0, picorv32__73(state)) == 0b1), BitVecVal(0b00000100, 8), If(picorv32__211(state), BitVecVal(0b00001000, 8), Concat(BitVecVal(0b0000, 4), picorv32__564(state))))))) # $procmux$1832_Y
def picorv32__566(state): return If((Extract(0, 0, picorv32__26(state)) == 0b1), picorv32__5(state), BitVecVal(0b00100000, 8)) # $procmux$1849_Y
def picorv32__567(state): return If((Extract(0, 0, picorv32__12(state)) == 0b1), picorv32__566(state), picorv32__5(state)) # $procmux$1851_Y
def picorv32__568(state): return If(picorv32__155(state), picorv32__567(state), If(picorv32__149(state), picorv32__565(state), If(picorv32__148(state), Concat(BitVecVal(0b0000, 4), picorv32__564(state)), If(picorv32__237(state), picorv32__563(state), If(picorv32__147(state), picorv32__561(state), If(picorv32__533(state), picorv32__560(state), picorv32__5(state))))))) # $procmux$1791_Y
def picorv32__569(state): return If(picorv32__99(state), picorv32__568(state), BitVecVal(0b01000000, 8)) # $procmux$1861_Y
def picorv32__570(state): return Or((Extract(0, 0, picorv32__90(state)) == 0b1),(Extract(1, 1, picorv32__90(state)) == 0b1),) # $ne$picorv32.v:1895$648_Y
def picorv32__571(state): return And(Or(picorv32__109(state), False), Or(picorv32__570(state), False)) # $logic_and$picorv32.v:1895$649_Y
def picorv32__572(state): return If(picorv32__571(state), BitVecVal(0b10000000, 8), picorv32__569(state)) # $procmux$1868_Y
def picorv32__573(state): return And(Or(picorv32__108(state), False), Or((Extract(0, 0, picorv32__90(state)) == 0b1), False)) # $logic_and$picorv32.v:1902$656_Y
def picorv32__574(state): return If(picorv32__573(state), BitVecVal(0b10000000, 8), picorv32__572(state)) # $procmux$1874_Y
def picorv32__575(state): return Or((Extract(0, 0, picorv32__86(state)) == 0b1), False, (Extract(0, 0, picorv32__88(state)) == 0b1), False) # $logic_or$picorv32.v:1894$645_Y
def picorv32__576(state): return And(Or(picorv32__99(state), False), Or(picorv32__575(state), False)) # $logic_and$picorv32.v:1894$646_Y
def picorv32__577(state): return If(picorv32__576(state), picorv32__574(state), picorv32__569(state)) # $procmux$1876_Y
def picorv32__578(state): return And(Or(picorv32__99(state), False), Or((Extract(0, 0, picorv32__87(state)) == 0b1), False)) # $logic_and$picorv32.v:1910$662_Y
def picorv32__579(state): return Or((Extract(1, 1, picorv32__127(state)) == 0b1),(Extract(0, 0, picorv32__127(state)) == 0b1),) # $reduce_or$picorv32.v:1910$663_Y
def picorv32__580(state): return And(Or(picorv32__578(state), False), Or(picorv32__579(state), False)) # $logic_and$picorv32.v:1910$665_Y
def picorv32__581(state): return If(picorv32__580(state), BitVecVal(0b10000000, 8), picorv32__577(state)) # $0\cpu_state[7:0]
def picorv32__582(state): return (picorv32__4(state) + BitVecVal(0b0000000000000000000000000000000000000000000000000000000000000001, 64)) # $add$picorv32.v:1543$558_Y
def picorv32__583(state): return If((Extract(0, 0, picorv32__12(state)) == 0b1), picorv32__582(state), picorv32__4(state)) # $procmux$2321_Y
def picorv32__584(state): return If(picorv32__155(state), picorv32__583(state), picorv32__4(state)) # $procmux$2329_Y
def picorv32__585(state): return If(picorv32__99(state), picorv32__584(state), BitVecVal(0b0000000000000000000000000000000000000000000000000000000000000000, 64)) # $0\count_instr[63:0]
def picorv32__586(state): return (picorv32__3(state) + BitVecVal(0b0000000000000000000000000000000000000000000000000000000000000001, 64)) # $add$picorv32.v:1406$503_Y
def picorv32__587(state): return If(picorv32__99(state), picorv32__586(state), BitVecVal(0b0000000000000000000000000000000000000000000000000000000000000000, 64)) # $0\count_cycle[63:0]
def picorv32__588(state): return If(picorv32__366(state), BitVecVal(0b0, 1), picorv32__2(state)) # $0\compressed_instr[0:0]
def picorv32__589(state): return (picorv32__90(state) & picorv32__105(state)) # $and$picorv32.v:1258$455_Y
def picorv32__590(state): return (picorv32__90(state) | picorv32__105(state)) # $or$picorv32.v:1256$453_Y
def picorv32__591(state): return (picorv32__90(state) ^ picorv32__105(state)) # $xor$picorv32.v:1254$451_Y
def picorv32__592(state): return (picorv32__90(state) + picorv32__105(state)) # $add$picorv32.v:1219$679_Y
def picorv32__593(state): return (picorv32__90(state) - picorv32__105(state)) # $sub$picorv32.v:1219$678_Y
def picorv32__594(state): return If((Extract(0, 0, picorv32__55(state)) == 0b1), picorv32__593(state), picorv32__592(state)) # \alu_add_sub
def picorv32__595(state): return Or((Extract(0, 0, picorv32__17(state)) == 0b1), False, (Extract(0, 0, picorv32__16(state)) == 0b1), False) # $logic_or$picorv32.v:1257$454_Y
def picorv32__596(state): return Or((Extract(0, 0, picorv32__36(state)) == 0b1), False, (Extract(0, 0, picorv32__35(state)) == 0b1), False) # $logic_or$picorv32.v:1255$452_Y
def picorv32__597(state): return Or((Extract(0, 0, picorv32__60(state)) == 0b1), False, (Extract(0, 0, picorv32__59(state)) == 0b1), False) # $logic_or$picorv32.v:1253$450_Y
def picorv32__598(state): return If((Extract(0, 0, picorv32__70(state)) == 0b1), picorv32__594(state), If((Extract(0, 0, picorv32__65(state)) == 0b1), Concat(BitVecVal(0b0000000000000000000000000000000, 31), picorv32__294(state)), If(picorv32__597(state), picorv32__591(state), If(picorv32__596(state), picorv32__590(state), If(picorv32__595(state), picorv32__589(state), BitVecVal(0b00000000000000000000000000000000, 32)))))) # \alu_out
def picorv32__599(state): return If((Extract(0, 0, picorv32__77(state)) == 0b1), BitVecVal(0b010, 3), BitVecVal(0b100, 3)) # $auto$wreduce.cc:452:run$3797 [2:0]
def picorv32__600(state): return (picorv32__127(state) + Concat(BitVecVal(0b00000000000000000000000000000, 29), picorv32__599(state))) # $add$picorv32.v:1296$471_Y
def picorv32__601(state): return Not(Or((Extract(0, 0, picorv32__76(state)) == 0b1), False)) # $logic_not$picorv32.v:1299$472_Y
def picorv32__602(state): return And(Or((Extract(0, 0, picorv32__83(state)) == 0b1), False), Or(picorv32__601(state), False)) # $logic_and$picorv32.v:1299$473_Y
def picorv32__603(state): return If((Extract(0, 0, picorv32__76(state)) == 0b1), picorv32__600(state), If(picorv32__602(state), picorv32__151(state), BitVecVal(0b00000000000000000000000000000000, 32))) # \cpuregs_wrdata
def picorv32__604(state): return Or(picorv32__602(state),(Extract(0, 0, picorv32__76(state)) == 0b1),) # $auto$opt_reduce.cc:132:opt_mux$3783
def picorv32__605(state): return If(picorv32__604(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)) # $2\cpuregs_write[0:0]
def picorv32__606(state): return If(picorv32__155(state), picorv32__605(state), BitVecVal(0b0, 1)) # \cpuregs_write
def picorv32__607(state): return And(Or(picorv32__99(state), False), Or((Extract(0, 0, picorv32__606(state)) == 0b1), False)) # $logic_and$picorv32.v:1317$484_Y
def picorv32__608(state): return And(Or(picorv32__607(state), False), Or((Extract(0, 0, picorv32__81(state)) == 0b1),(Extract(1, 1, picorv32__81(state)) == 0b1),(Extract(2, 2, picorv32__81(state)) == 0b1),(Extract(3, 3, picorv32__81(state)) == 0b1),(Extract(4, 4, picorv32__81(state)) == 0b1),)) # $logic_and$picorv32.v:1317$485_Y
def picorv32__609(state): return If(picorv32__608(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)) # $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31]
def picorv32_m_W0A_cpuregs(state): return picorv32__81(state) # \latched_rd
def picorv32_m_W0D_cpuregs(state): return picorv32__603(state) # \cpuregs_wrdata
def picorv32_m_W0M_cpuregs(state): return Concat(picorv32__609(state),  Concat(picorv32__609(state),  Concat(picorv32__609(state),  Concat(picorv32__609(state),  Concat(picorv32__609(state),  Concat(picorv32__609(state),  Concat(picorv32__609(state),  Concat(picorv32__609(state),  Concat(picorv32__609(state),  Concat(picorv32__609(state),  Concat(picorv32__609(state),  Concat(picorv32__609(state),  Concat(picorv32__609(state),  Concat(picorv32__609(state),  Concat(picorv32__609(state),  Concat(picorv32__609(state),  Concat(picorv32__609(state),  Concat(picorv32__609(state),  Concat(picorv32__609(state),  Concat(picorv32__609(state),  Concat(picorv32__609(state),  Concat(picorv32__609(state),  Concat(picorv32__609(state),  Concat(picorv32__609(state),  Concat(picorv32__609(state),  Concat(picorv32__609(state),  Concat(picorv32__609(state),  Concat(picorv32__609(state),  Concat(picorv32__609(state),  Concat(picorv32__609(state),  Concat(picorv32__609(state), picorv32__609(state)))))))))))))))))))))))))))))))) # { $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] $0$memwr$\cpuregs$picorv32.v:1318$14_EN[31:0]$483 [31] }
def picorv32__137__1(state): return Store(picorv32__137__0(state), picorv32_m_W0A_cpuregs(state), ((picorv32_m_W0D_cpuregs(state) & picorv32_m_W0M_cpuregs(state)) | (Select(picorv32__137__0(state), picorv32_m_W0A_cpuregs(state)) & (~picorv32_m_W0M_cpuregs(state))))) # cpuregs
def picorv32_a(state): return True
def picorv32_u(state): return True
def picorv32_i(state): return True
def picorv32_h(state): return True
def picorv32_t(state, next_state): return And(    (picorv32__132(state) == picorv32__129(next_state)) # _procdff_3606 \trap
,   (picorv32__150(state) == picorv32__128(next_state)) # _procdff_3618 \reg_sh
,   (picorv32__157(state) == picorv32__127(next_state)) # _procdff_3613 \reg_pc
,   (picorv32__158(state) == picorv32__124(next_state)) # _procdff_3607 \pcpi_valid
,   (picorv32__166(state) == picorv32__121(next_state)) # _procdff_3751 \mem_wstrb
,   (picorv32__168(state) == picorv32__120(next_state)) # _procdff_3750 \mem_wdata
,   (picorv32__179(state) == picorv32__119(next_state)) # _procdff_3747 \mem_valid
,   (Concat(picorv32__187(state),  Concat(picorv32__186(state),  Concat(picorv32__185(state),  Concat(picorv32__184(state),  Concat(picorv32__183(state),  Concat(picorv32__182(state),  Concat(picorv32__181(state), picorv32__180(state)))))))) == picorv32__117(next_state)) # _procdff_3757 \mem_rdata_q
,   (picorv32__210(state) == picorv32__106(next_state)) # _procdff_3624 \mem_wordsize
,   (picorv32__215(state) == picorv32__105(next_state)) # _procdff_3616 \reg_op2
,   (picorv32__225(state) == picorv32__100(next_state)) # _procdff_3752 \mem_state
,   (picorv32__238(state) == picorv32__92(next_state)) # _procdff_3617 \reg_out
,   (picorv32__245(state) == picorv32__91(next_state)) # _procdff_3614 \reg_next_pc
,   (picorv32__265(state) == picorv32__90(next_state)) # _procdff_3615 \reg_op1
,   (picorv32__269(state) == picorv32__89(next_state)) # _procdff_3748 \mem_instr
,   (picorv32__277(state) == picorv32__88(next_state)) # _procdff_3628 \mem_do_wdata
,   (picorv32__300(state) == picorv32__87(next_state)) # _procdff_3626 \mem_do_rinst
,   (picorv32__307(state) == picorv32__86(next_state)) # _procdff_3627 \mem_do_rdata
,   (picorv32__315(state) == picorv32__85(next_state)) # _procdff_3625 \mem_do_prefetch
,   (picorv32__317(state) == picorv32__84(next_state)) # _procdff_3749 \mem_addr
,   (picorv32__323(state) == picorv32__83(next_state)) # _procdff_3642 \latched_store
,   (picorv32__326(state) == picorv32__82(next_state)) # _procdff_3643 \latched_stalu
,   (picorv32__329(state) == picorv32__81(next_state)) # _procdff_3650 \latched_rd
,   (picorv32__333(state) == picorv32__80(next_state)) # _procdff_3647 \latched_is_lu
,   (picorv32__337(state) == picorv32__79(next_state)) # _procdff_3648 \latched_is_lh
,   (picorv32__341(state) == picorv32__78(next_state)) # _procdff_3649 \latched_is_lb
,   (picorv32__343(state) == picorv32__77(next_state)) # _procdff_3645 \latched_compr
,   (picorv32__347(state) == picorv32__76(next_state)) # _procdff_3644 \latched_branch
,   (If(picorv32__348(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)) == picorv32__75(next_state)) # _procdff_3726 \is_sltiu_bltu_sltu
,   (If(picorv32__349(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)) == picorv32__74(next_state)) # _procdff_3725 \is_slti_blt_slt
,   (picorv32__361(state) == picorv32__73(next_state)) # _procdff_3720 \is_slli_srli_srai
,   (picorv32__363(state) == picorv32__72(next_state)) # _procdff_3723 \is_sll_srl_sra
,   (picorv32__367(state) == picorv32__71(next_state)) # _procdff_3722 \is_sb_sh_sw
,   (picorv32__369(state) == picorv32__70(next_state)) # _procdff_3724 \is_lui_auipc_jal_jalr_addi_add_sub
,   (If(picorv32__370(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)) == picorv32__69(next_state)) # _procdff_3718 \is_lui_auipc_jal
,   (If(picorv32__371(state), BitVecVal(0b1, 1), BitVecVal(0b0, 1)) == picorv32__68(next_state)) # _procdff_3728 \is_lbu_lhu_lw
,   (picorv32__373(state) == picorv32__67(next_state)) # _procdff_3719 \is_lb_lh_lw_lbu_lhu
,   (picorv32__383(state) == picorv32__66(next_state)) # _procdff_3721 \is_jalr_addi_slti_sltiu_xori_ori_andi
,   (picorv32__386(state) == picorv32__65(next_state)) # _procdff_3731 \is_compare
,   (picorv32__389(state) == picorv32__64(next_state)) # _procdff_3727 \is_beq_bne_blt_bge_bltu_bgeu
,   (picorv32__391(state) == picorv32__63(next_state)) # _procdff_3730 \is_alu_reg_reg
,   (picorv32__393(state) == picorv32__62(next_state)) # _procdff_3729 \is_alu_reg_imm
,   (picorv32__396(state) == picorv32__60(next_state)) # _procdff_3685 \instr_xori
,   (picorv32__400(state) == picorv32__59(next_state)) # _procdff_3696 \instr_xor
,   (picorv32__401(state) == picorv32__58(next_state)) # _procdff_3710 \instr_waitirq
,   (picorv32__402(state) == picorv32__57(next_state)) # _procdff_3711 \instr_timer
,   (picorv32__404(state) == picorv32__56(next_state)) # _procdff_3681 \instr_sw
,   (picorv32__408(state) == picorv32__55(next_state)) # _procdff_3692 \instr_sub
,   (picorv32__411(state) == picorv32__54(next_state)) # _procdff_3689 \instr_srli
,   (picorv32__415(state) == picorv32__53(next_state)) # _procdff_3697 \instr_srl
,   (picorv32__417(state) == picorv32__52(next_state)) # _procdff_3690 \instr_srai
,   (picorv32__420(state) == picorv32__51(next_state)) # _procdff_3698 \instr_sra
,   (picorv32__424(state) == picorv32__50(next_state)) # _procdff_3695 \instr_sltu
,   (picorv32__427(state) == picorv32__49(next_state)) # _procdff_3684 \instr_sltiu
,   (picorv32__430(state) == picorv32__48(next_state)) # _procdff_3683 \instr_slti
,   (picorv32__434(state) == picorv32__47(next_state)) # _procdff_3694 \instr_slt
,   (picorv32__437(state) == picorv32__46(next_state)) # _procdff_3688 \instr_slli
,   (picorv32__441(state) == picorv32__45(next_state)) # _procdff_3693 \instr_sll
,   (picorv32__443(state) == picorv32__44(next_state)) # _procdff_3680 \instr_sh
,   (picorv32__444(state) == picorv32__43(next_state)) # _procdff_3707 \instr_setq
,   (picorv32__446(state) == picorv32__42(next_state)) # _procdff_3679 \instr_sb
,   (picorv32__447(state) == picorv32__41(next_state)) # _procdff_3708 \instr_retirq
,   (picorv32__451(state) == picorv32__40(next_state)) # _procdff_3704 \instr_rdinstrh
,   (picorv32__454(state) == picorv32__39(next_state)) # _procdff_3703 \instr_rdinstr
,   (picorv32__460(state) == picorv32__38(next_state)) # _procdff_3702 \instr_rdcycleh
,   (picorv32__466(state) == picorv32__37(next_state)) # _procdff_3701 \instr_rdcycle
,   (picorv32__469(state) == picorv32__36(next_state)) # _procdff_3686 \instr_ori
,   (picorv32__473(state) == picorv32__35(next_state)) # _procdff_3699 \instr_or
,   (picorv32__474(state) == picorv32__34(next_state)) # _procdff_3709 \instr_maskirq
,   (picorv32__476(state) == picorv32__33(next_state)) # _procdff_3676 \instr_lw
,   (picorv32__478(state) == picorv32__32(next_state)) # _procdff_3664 \instr_lui
,   (picorv32__480(state) == picorv32__31(next_state)) # _procdff_3678 \instr_lhu
,   (picorv32__482(state) == picorv32__30(next_state)) # _procdff_3675 \instr_lh
,   (picorv32__484(state) == picorv32__29(next_state)) # _procdff_3677 \instr_lbu
,   (picorv32__486(state) == picorv32__28(next_state)) # _procdff_3674 \instr_lb
,   (picorv32__490(state) == picorv32__27(next_state)) # _procdff_3667 \instr_jalr
,   (picorv32__492(state) == picorv32__26(next_state)) # _procdff_3666 \instr_jal
,   (picorv32__493(state) == picorv32__25(next_state)) # _procdff_3706 \instr_getq
,   (picorv32__496(state) == picorv32__24(next_state)) # _procdff_3669 \instr_bne
,   (picorv32__499(state) == picorv32__23(next_state)) # _procdff_3672 \instr_bltu
,   (picorv32__502(state) == picorv32__22(next_state)) # _procdff_3670 \instr_blt
,   (picorv32__505(state) == picorv32__21(next_state)) # _procdff_3673 \instr_bgeu
,   (picorv32__508(state) == picorv32__20(next_state)) # _procdff_3671 \instr_bge
,   (picorv32__511(state) == picorv32__19(next_state)) # _procdff_3668 \instr_beq
,   (picorv32__513(state) == picorv32__18(next_state)) # _procdff_3665 \instr_auipc
,   (picorv32__516(state) == picorv32__17(next_state)) # _procdff_3687 \instr_andi
,   (picorv32__520(state) == picorv32__16(next_state)) # _procdff_3700 \instr_and
,   (picorv32__523(state) == picorv32__15(next_state)) # _procdff_3682 \instr_addi
,   (picorv32__526(state) == picorv32__14(next_state)) # _procdff_3691 \instr_add
,   (picorv32__527(state) == picorv32__13(next_state)) # _procdff_3608 \eoi
,   (picorv32__535(state) == picorv32__12(next_state)) # _procdff_3629 \decoder_trigger
,   (picorv32__539(state) == picorv32__11(next_state)) # _procdff_3631 \decoder_pseudo_trigger
,   (picorv32__540(state) == picorv32__10(next_state)) # _procdff_3714 \decoded_rs2
,   (Concat(picorv32__542(state), picorv32__541(state)) == picorv32__9(next_state)) # _procdff_3713 \decoded_rs1
,   (picorv32__543(state) == picorv32__8(next_state)) # _procdff_3712 \decoded_rd
,   (Concat(picorv32__554(state),  Concat(picorv32__553(state),  Concat(picorv32__552(state),  Concat(picorv32__551(state),  Concat(picorv32__550(state),  Concat(picorv32__549(state),  Concat(picorv32__548(state),  Concat(picorv32__547(state),  Concat(picorv32__546(state),  Concat(picorv32__545(state), picorv32__544(state))))))))))) == picorv32__7(next_state)) # _procdff_3716 \decoded_imm_j
,   (picorv32__558(state) == picorv32__6(next_state)) # _procdff_3715 \decoded_imm
,   (picorv32__581(state) == picorv32__5(next_state)) # _procdff_3637 \cpu_state
,   (picorv32__585(state) == picorv32__4(next_state)) # _procdff_3612 \count_instr
,   (picorv32__587(state) == picorv32__3(next_state)) # _procdff_3611 \count_cycle
,   (picorv32__588(state) == picorv32__2(next_state)) # _procdff_3717 \compressed_instr
,   (picorv32__598(state) == picorv32__0(next_state)) # _procdff_3655 \alu_out_q
,   (picorv32__137__1(state) == picorv32__137__0(next_state)) # cpuregs
)
clocks = OrderedDict([(i, eval('picorv32_n_' + i)) for i in clocks])
inputs = OrderedDict([(i, eval('picorv32_n_' + i)) for i in inputs])
outputs = OrderedDict([(i, eval('picorv32_n_' + i)) for i in outputs])
registers = OrderedDict([(i, eval('picorv32_n_' + i)) for i in registers])
memories = OrderedDict([(i, eval('picorv32_m_' + i)) for i in memories])

# end of module picorv32
# yosys-smt2-topmod picorv32
# end of yosys output