change order of outputs / bad / constraints

src/system/analysis.rs

@@ -266,23 +266,23 @@ pub fn analyze_for_serialization(
 
     // add all roots and give them a large other count
     let mut todo: Vec<(ExprRef, SerializeSignalKind)> = vec![];
-    todo.extend(
-        sys.bad_states
-            .iter()
-            .map(|&e| (e, SerializeSignalKind::BadState)),
-    );
-    todo.extend(
-        sys.constraints
-            .iter()
-            .map(|&e| (e, SerializeSignalKind::Constraint)),
-    );
     if include_outputs {
         todo.extend(
             sys.outputs
                 .iter()
                 .map(|o| (o.expr, SerializeSignalKind::Output)),
         );
     }
+    todo.extend(
+        sys.constraints
+            .iter()
+            .map(|&e| (e, SerializeSignalKind::Constraint)),
+    );
+    todo.extend(
+        sys.bad_states
+            .iter()
+            .map(|&e| (e, SerializeSignalKind::BadState)),
+    );
 
     // add state root expressions
     todo.extend(

tests/snapshots/btor2_test__parse_quiz1.snap

@@ -4,12 +4,13 @@ expression: sys.serialize_to_str(&ctx)
 ---
 Quiz1
 input reset : bv<1>
-bad %18 : bv<1> = not(implies(not(reset), not(ugt(counter, zext(4'b1010, 12)))))
 node %15 : bv<1> = ugte(_resetCount, 1'b1)
 node %16 : bv<1> = not(%15)
 constraint %19 : bv<1> = implies(%16, reset)
+bad %18 : bv<1> = not(implies(not(reset), not(ugt(counter, zext(4'b1010, 12)))))
 state counter : bv<16>
   [next] ite(reset, 16'x0000, add(zext(counter, 1), zext(1'b1, 16))[15:0])
 state _resetCount : bv<1>
   [init] 1'b0
   [next] ite(%16, add(zext(_resetCount, 1), zext(1'b1, 1))[0], _resetCount)
+

tests/snapshots/btor2_test__parse_sdram.snap

@@ -11,52 +11,53 @@ input rst_n : bv<1>
 input wr_addr : bv<24>
 input wr_data : bv<16>
 input wr_enable : bv<1>
-output data_oe : bv<1> = eq(state, 5'b11010)
 node _eq_sdram_controller.no_tri_state.v:276_22 : bv<1> = eq(state, 5'b01110)
-node _or_sdram_controller.no_tri_state.v:253_21 : bv<1> = or(eq(state, 5'b10010), data_oe)
+node data_oe_0 : bv<1> = eq(state, 5'b11010)
+node _or_sdram_controller.no_tri_state.v:253_21 : bv<1> = or(eq(state, 5'b10010), data_oe_0)
 node _or_sdram_controller.no_tri_state.v:248_18 : bv<1> = or(eq(state, 5'b10000), eq(state, 5'b11000))
 node %39 : bv<1> = state[4]
-output addr : bv<13> = ite(or(%39, _eq_sdram_controller.no_tri_state.v:276_22), ite(_or_sdram_controller.no_tri_state.v:248_18, haddr_r[21:9], ite(_or_sdram_controller.no_tri_state.v:253_21, concat(4'b0010, haddr_r[8:0]), ite(_eq_sdram_controller.no_tri_state.v:276_22, 13'x0230, 13'x0000))), concat(2'b00, concat(command[0], 10'x000)))
+output addr_0 : bv<13> = ite(or(%39, _eq_sdram_controller.no_tri_state.v:276_22), ite(_or_sdram_controller.no_tri_state.v:248_18, haddr_r[21:9], ite(_or_sdram_controller.no_tri_state.v:253_21, concat(4'b0010, haddr_r[8:0]), ite(_eq_sdram_controller.no_tri_state.v:276_22, 13'x0230, 13'x0000))), concat(2'b00, concat(command[0], 10'x000)))
 node %43 : bv<2> = haddr_r[23:22]
-output bank_addr : bv<2> = ite(%39, ite(_or_sdram_controller.no_tri_state.v:248_18, %43, ite(_or_sdram_controller.no_tri_state.v:253_21, %43, 2'b00)), command[2:1])
-output cas_n : bv<1> = command[4]
-output clock_enable : bv<1> = command[7]
-output cs_n : bv<1> = command[6]
+output bank_addr_0 : bv<2> = ite(%39, ite(_or_sdram_controller.no_tri_state.v:248_18, %43, ite(_or_sdram_controller.no_tri_state.v:253_21, %43, 2'b00)), command[2:1])
+output busy_0 : bv<1>
+output cas_n_0 : bv<1> = command[4]
+output clock_enable_0 : bv<1> = command[7]
+output cs_n_0 : bv<1> = command[6]
 node _procmux_147 : bv<2> = ite(%39, 2'b00, 2'b11)
-output data_mask_high : bv<1> = _procmux_147[0]
-output data_mask_low : bv<1> = _procmux_147[1]
-output ras_n : bv<1> = command[5]
-output we_n : bv<1> = command[3]
-output rd_ready : bv<1>
-output rd_data : bv<16>
-output data_out : bv<16>
-output busy : bv<1>
+output data_mask_high_r : bv<1> = _procmux_147[0]
+output data_mask_low_r : bv<1> = _procmux_147[1]
+output data_out_0 : bv<16>
+output ras_n_0 : bv<1> = command[5]
+output rd_data_0 : bv<16>
+output rd_ready_0 : bv<1>
+output we_n_0 : bv<1> = command[3]
+node %240 : bv<17> = and(17'x00000, 17'x00c00)
 node %152 : bv<17> = _state_5[state]
 node _logic_not_sdram_controller.no_tri_state.v:315_26 : bv<1> = not(not(eq(state_cnt, 4'b0000)))
 node %287 : bv<8> = or(and(8'b00000000, 8'b00000111), 8'b10011000)
 node _ge_sdram_controller.no_tri_state.v:294_25 : bv<1> = ugte(zext(refresh_cnt, 22), 32'x00000207)
 node _eq_sdram_controller.no_tri_state.v:292_24 : bv<1> = not(not(eq(state, 5'b00000)))
 node _auto_opt_dff.cc:195:make_patterns_logic_224 : bv<1> = not(eq(concat(_eq_sdram_controller.no_tri_state.v:292_24, _logic_not_sdram_controller.no_tri_state.v:315_26), 2'b00))
 node _eq_sdram_controller.no_tri_state.v:209_10 : bv<1> = eq(state, 5'b10100)
-node %240 : bv<17> = and(17'x00000, 17'x00c00)
 state command : bv<8>
   [next] ite(rst_n, ite(_auto_opt_dff.cc:195:make_patterns_logic_224, ite(_eq_sdram_controller.no_tri_state.v:292_24, ite(_ge_sdram_controller.no_tri_state.v:294_25, 8'b10010001, ite(rd_enable, %287, ite(wr_enable, %287, 8'b10111000))), ite(_logic_not_sdram_controller.no_tri_state.v:315_26, %152[16:9], 8'b00000000)), command), 8'b10111000)
 state state : bv<5>
   [next] ite(rst_n, ite(_auto_opt_dff.cc:195:make_patterns_logic_224, ite(_eq_sdram_controller.no_tri_state.v:292_24, ite(_ge_sdram_controller.no_tri_state.v:294_25, 5'b00001, ite(rd_enable, 5'b10000, ite(wr_enable, 5'b11000, 5'b00000))), ite(_logic_not_sdram_controller.no_tri_state.v:315_26, %152[8:4], 5'b00000)), state), 5'b01000)
 state haddr_r : bv<24>
   [next] ite(rst_n, ite(not(eq(concat(rd_enable, wr_enable), 2'b00)), ite(rd_enable, rd_addr, ite(wr_enable, wr_addr, 24'x000000)), haddr_r), 24'x000000)
-state busy : bv<1>
+state busy_0 : bv<1>
   [next] ite(rst_n, %39, 1'b0)
-state data_out : bv<16>
-  [next] ite(rst_n, ite(wr_enable, wr_data, data_out), 16'x0000)
-state rd_data : bv<16>
-  [next] ite(rst_n, ite(_eq_sdram_controller.no_tri_state.v:209_10, data_in, rd_data), 16'x0000)
-state rd_ready : bv<1>
-  [next] ite(rst_n, ite(_eq_sdram_controller.no_tri_state.v:209_10, 1'b1, 1'b0), rd_ready)
+state data_out_0 : bv<16>
+  [next] ite(rst_n, ite(wr_enable, wr_data, data_out_0), 16'x0000)
+state rd_data_0 : bv<16>
+  [next] ite(rst_n, ite(_eq_sdram_controller.no_tri_state.v:209_10, data_in, rd_data_0), 16'x0000)
+state rd_ready_0 : bv<1>
+  [next] ite(rst_n, ite(_eq_sdram_controller.no_tri_state.v:209_10, 1'b1, 1'b0), rd_ready_0)
 state _state_5 : bv<5> -> bv<17>
   [init] ([17'x00000] x 2^5)[5'b00000 := 17'x17000][5'b00001 := 17'x17020][5'b00010 := 17'x11030][5'b00011 := 17'x17047][5'b00100 := 17'x17000][5'b00101 := 17'x110a0][5'b00110 := 17'x17000][5'b00111 := 17'x17000][5'b01000 := 17'x12290][5'b01001 := 17'x17050][5'b01010 := 17'x170b7][5'b01011 := 17'x110c0][5'b01100 := 17'x170d7][5'b01101 := or(and(17'x00000, 17'x00200), 17'x100e0)][5'b01110 := 17'x170f1][5'b01111 := 17'x17000][5'b10000 := 17'x17111][5'b10001 := or(%240, 17'x15320)][5'b10010 := 17'x17131][5'b10011 := 17'x17140][5'b10100 := 17'x17000][5'b10101 := 17'x17000][5'b10110 := 17'x17000][5'b10111 := 17'x17000][5'b11000 := 17'x17191][5'b11001 := or(%240, 17'x143a0)][5'b11010 := 17'x171b1][5'b11011 := 17'x17000][5'b11100 := 17'x17000][5'b11101 := 17'x17000][5'b11110 := 17'x17000][5'b11111 := 17'x17000]
   [next] _state_5
 state state_cnt : bv<4>
   [next] ite(rst_n, ite(_logic_not_sdram_controller.no_tri_state.v:315_26, ite(_eq_sdram_controller.no_tri_state.v:292_24, 4'b0000, %152[3:0]), sub(state_cnt, zext(1'b1, 3))), 4'b1111)
 state refresh_cnt : bv<10>
   [next] ite(not(eq(concat(not(rst_n), eq(state, 5'b00100)), 2'b00)), 10'x000, add(refresh_cnt, zext(1'b1, 9)))
+

tests/snapshots/btor2_test__parse_sdram_and_remove_anonymous_inputs.snap

@@ -11,52 +11,53 @@ input rst_n : bv<1>
 input wr_addr : bv<24>
 input wr_data : bv<16>
 input wr_enable : bv<1>
-output data_oe : bv<1> = eq(state, 5'b11010)
 node _eq_sdram_controller.no_tri_state.v:276_22 : bv<1> = eq(state, 5'b01110)
-node _or_sdram_controller.no_tri_state.v:253_21 : bv<1> = or(eq(state, 5'b10010), data_oe)
+node data_oe_0 : bv<1> = eq(state, 5'b11010)
+node _or_sdram_controller.no_tri_state.v:253_21 : bv<1> = or(eq(state, 5'b10010), data_oe_0)
 node _or_sdram_controller.no_tri_state.v:248_18 : bv<1> = or(eq(state, 5'b10000), eq(state, 5'b11000))
 node %39 : bv<1> = state[4]
-output addr : bv<13> = ite(or(%39, _eq_sdram_controller.no_tri_state.v:276_22), ite(_or_sdram_controller.no_tri_state.v:248_18, haddr_r[21:9], ite(_or_sdram_controller.no_tri_state.v:253_21, concat(4'b0010, haddr_r[8:0]), ite(_eq_sdram_controller.no_tri_state.v:276_22, 13'x0230, 13'x0000))), concat(2'b00, concat(command[0], 10'x000)))
+output addr_0 : bv<13> = ite(or(%39, _eq_sdram_controller.no_tri_state.v:276_22), ite(_or_sdram_controller.no_tri_state.v:248_18, haddr_r[21:9], ite(_or_sdram_controller.no_tri_state.v:253_21, concat(4'b0010, haddr_r[8:0]), ite(_eq_sdram_controller.no_tri_state.v:276_22, 13'x0230, 13'x0000))), concat(2'b00, concat(command[0], 10'x000)))
 node %43 : bv<2> = haddr_r[23:22]
-output bank_addr : bv<2> = ite(%39, ite(_or_sdram_controller.no_tri_state.v:248_18, %43, ite(_or_sdram_controller.no_tri_state.v:253_21, %43, 2'b00)), command[2:1])
-output cas_n : bv<1> = command[4]
-output clock_enable : bv<1> = command[7]
-output cs_n : bv<1> = command[6]
+output bank_addr_0 : bv<2> = ite(%39, ite(_or_sdram_controller.no_tri_state.v:248_18, %43, ite(_or_sdram_controller.no_tri_state.v:253_21, %43, 2'b00)), command[2:1])
+output busy_0 : bv<1>
+output cas_n_0 : bv<1> = command[4]
+output clock_enable_0 : bv<1> = command[7]
+output cs_n_0 : bv<1> = command[6]
 node _procmux_147 : bv<2> = ite(%39, 2'b00, 2'b11)
-output data_mask_high : bv<1> = _procmux_147[0]
-output data_mask_low : bv<1> = _procmux_147[1]
-output ras_n : bv<1> = command[5]
-output we_n : bv<1> = command[3]
-output rd_ready : bv<1>
-output rd_data : bv<16>
-output data_out : bv<16>
-output busy : bv<1>
+output data_mask_high_r : bv<1> = _procmux_147[0]
+output data_mask_low_r : bv<1> = _procmux_147[1]
+output data_out_0 : bv<16>
+output ras_n_0 : bv<1> = command[5]
+output rd_data_0 : bv<16>
+output rd_ready_0 : bv<1>
+output we_n_0 : bv<1> = command[3]
+node %240 : bv<17> = and(17'x00000, 17'x00c00)
 node %152 : bv<17> = _state_5[state]
 node _logic_not_sdram_controller.no_tri_state.v:315_26 : bv<1> = not(not(eq(state_cnt, 4'b0000)))
 node %287 : bv<8> = or(and(8'b00000000, 8'b00000111), 8'b10011000)
 node _ge_sdram_controller.no_tri_state.v:294_25 : bv<1> = ugte(zext(refresh_cnt, 22), 32'x00000207)
 node _eq_sdram_controller.no_tri_state.v:292_24 : bv<1> = not(not(eq(state, 5'b00000)))
 node _auto_opt_dff.cc:195:make_patterns_logic_224 : bv<1> = not(eq(concat(_eq_sdram_controller.no_tri_state.v:292_24, _logic_not_sdram_controller.no_tri_state.v:315_26), 2'b00))
 node _eq_sdram_controller.no_tri_state.v:209_10 : bv<1> = eq(state, 5'b10100)
-node %240 : bv<17> = and(17'x00000, 17'x00c00)
 state command : bv<8>
   [next] ite(rst_n, ite(_auto_opt_dff.cc:195:make_patterns_logic_224, ite(_eq_sdram_controller.no_tri_state.v:292_24, ite(_ge_sdram_controller.no_tri_state.v:294_25, 8'b10010001, ite(rd_enable, %287, ite(wr_enable, %287, 8'b10111000))), ite(_logic_not_sdram_controller.no_tri_state.v:315_26, %152[16:9], 8'b00000000)), command), 8'b10111000)
 state state : bv<5>
   [next] ite(rst_n, ite(_auto_opt_dff.cc:195:make_patterns_logic_224, ite(_eq_sdram_controller.no_tri_state.v:292_24, ite(_ge_sdram_controller.no_tri_state.v:294_25, 5'b00001, ite(rd_enable, 5'b10000, ite(wr_enable, 5'b11000, 5'b00000))), ite(_logic_not_sdram_controller.no_tri_state.v:315_26, %152[8:4], 5'b00000)), state), 5'b01000)
 state haddr_r : bv<24>
   [next] ite(rst_n, ite(not(eq(concat(rd_enable, wr_enable), 2'b00)), ite(rd_enable, rd_addr, ite(wr_enable, wr_addr, 24'x000000)), haddr_r), 24'x000000)
-state busy : bv<1>
+state busy_0 : bv<1>
   [next] ite(rst_n, %39, 1'b0)
-state data_out : bv<16>
-  [next] ite(rst_n, ite(wr_enable, wr_data, data_out), 16'x0000)
-state rd_data : bv<16>
-  [next] ite(rst_n, ite(_eq_sdram_controller.no_tri_state.v:209_10, data_in, rd_data), 16'x0000)
-state rd_ready : bv<1>
-  [next] ite(rst_n, ite(_eq_sdram_controller.no_tri_state.v:209_10, 1'b1, 1'b0), rd_ready)
+state data_out_0 : bv<16>
+  [next] ite(rst_n, ite(wr_enable, wr_data, data_out_0), 16'x0000)
+state rd_data_0 : bv<16>
+  [next] ite(rst_n, ite(_eq_sdram_controller.no_tri_state.v:209_10, data_in, rd_data_0), 16'x0000)
+state rd_ready_0 : bv<1>
+  [next] ite(rst_n, ite(_eq_sdram_controller.no_tri_state.v:209_10, 1'b1, 1'b0), rd_ready_0)
 state _state_5 : bv<5> -> bv<17>
   [init] ([17'x00000] x 2^5)[5'b00000 := 17'x17000][5'b00001 := 17'x17020][5'b00010 := 17'x11030][5'b00011 := 17'x17047][5'b00100 := 17'x17000][5'b00101 := 17'x110a0][5'b00110 := 17'x17000][5'b00111 := 17'x17000][5'b01000 := 17'x12290][5'b01001 := 17'x17050][5'b01010 := 17'x170b7][5'b01011 := 17'x110c0][5'b01100 := 17'x170d7][5'b01101 := or(and(17'x00000, 17'x00200), 17'x100e0)][5'b01110 := 17'x170f1][5'b01111 := 17'x17000][5'b10000 := 17'x17111][5'b10001 := or(%240, 17'x15320)][5'b10010 := 17'x17131][5'b10011 := 17'x17140][5'b10100 := 17'x17000][5'b10101 := 17'x17000][5'b10110 := 17'x17000][5'b10111 := 17'x17000][5'b11000 := 17'x17191][5'b11001 := or(%240, 17'x143a0)][5'b11010 := 17'x171b1][5'b11011 := 17'x17000][5'b11100 := 17'x17000][5'b11101 := 17'x17000][5'b11110 := 17'x17000][5'b11111 := 17'x17000]
   [next] _state_5
 state state_cnt : bv<4>
   [next] ite(rst_n, ite(_logic_not_sdram_controller.no_tri_state.v:315_26, ite(_eq_sdram_controller.no_tri_state.v:292_24, 4'b0000, %152[3:0]), sub(state_cnt, zext(1'b1, 3))), 4'b1111)
 state refresh_cnt : bv<10>
   [next] ite(not(eq(concat(not(rst_n), eq(state, 5'b00100)), 2'b00)), 10'x000, add(refresh_cnt, zext(1'b1, 9)))
+

tests/snapshots/btor2_test__parse_sdram_and_simplify_expressions.snap

@@ -11,48 +11,49 @@ input rst_n : bv<1>
 input wr_addr : bv<24>
 input wr_data : bv<16>
 input wr_enable : bv<1>
-output data_oe : bv<1> = eq(state, 5'b11010)
 node _eq_sdram_controller.no_tri_state.v:276_22 : bv<1> = eq(state, 5'b01110)
-node _or_sdram_controller.no_tri_state.v:253_21 : bv<1> = or(eq(state, 5'b10010), data_oe)
+node data_oe_0 : bv<1> = eq(state, 5'b11010)
+node _or_sdram_controller.no_tri_state.v:253_21 : bv<1> = or(eq(state, 5'b10010), data_oe_0)
 node _or_sdram_controller.no_tri_state.v:248_18 : bv<1> = or(eq(state, 5'b10000), eq(state, 5'b11000))
 node %39 : bv<1> = state[4]
-output addr : bv<13> = ite(or(%39, _eq_sdram_controller.no_tri_state.v:276_22), ite(_or_sdram_controller.no_tri_state.v:248_18, haddr_r[21:9], ite(_or_sdram_controller.no_tri_state.v:253_21, concat(4'b0010, haddr_r[8:0]), ite(_eq_sdram_controller.no_tri_state.v:276_22, 13'x0230, 13'x0000))), concat(2'b00, concat(command[0], 10'x000)))
+output addr_0 : bv<13> = ite(or(%39, _eq_sdram_controller.no_tri_state.v:276_22), ite(_or_sdram_controller.no_tri_state.v:248_18, haddr_r[21:9], ite(_or_sdram_controller.no_tri_state.v:253_21, concat(4'b0010, haddr_r[8:0]), ite(_eq_sdram_controller.no_tri_state.v:276_22, 13'x0230, 13'x0000))), concat(2'b00, concat(command[0], 10'x000)))
 node %43 : bv<2> = haddr_r[23:22]
-output bank_addr : bv<2> = ite(%39, ite(_or_sdram_controller.no_tri_state.v:248_18, %43, ite(_or_sdram_controller.no_tri_state.v:253_21, %43, 2'b00)), command[2:1])
-output cas_n : bv<1> = command[4]
-output clock_enable : bv<1> = command[7]
-output cs_n : bv<1> = command[6]
-output ras_n : bv<1> = command[5]
-output we_n : bv<1> = command[3]
-output rd_ready : bv<1>
-output rd_data : bv<16>
-output data_out : bv<16>
-output busy : bv<1>
-output data_mask_low : bv<1> = not(%39)
+output bank_addr_0 : bv<2> = ite(%39, ite(_or_sdram_controller.no_tri_state.v:248_18, %43, ite(_or_sdram_controller.no_tri_state.v:253_21, %43, 2'b00)), command[2:1])
+output busy_0 : bv<1>
+output cas_n_0 : bv<1> = command[4]
+output clock_enable_0 : bv<1> = command[7]
+output cs_n_0 : bv<1> = command[6]
+output %364 : bv<1> = not(%39)
+output data_out_0 : bv<16>
+output ras_n_0 : bv<1> = command[5]
+output rd_data_0 : bv<16>
+output rd_ready_0 : bv<1>
+output we_n_0 : bv<1> = command[3]
 node %152 : bv<17> = _state_5[state]
-node _logic_not_sdram_controller.no_tri_state.v:315_26 : bv<1> = eq(state_cnt, 4'b0000)
-node _ge_sdram_controller.no_tri_state.v:294_25 : bv<1> = ugte(concat(22'x000000, refresh_cnt), 32'x00000207)
-node _eq_sdram_controller.no_tri_state.v:292_24 : bv<1> = eq(state, 5'b00000)
-node _auto_opt_dff.cc:195:make_patterns_logic_224 : bv<1> = not(or(_eq_sdram_controller.no_tri_state.v:292_24, _logic_not_sdram_controller.no_tri_state.v:315_26))
+node %156 : bv<1> = eq(state_cnt, 4'b0000)
+node %344 : bv<1> = ugte(concat(22'x000000, refresh_cnt), 32'x00000207)
+node %177 : bv<1> = eq(state, 5'b00000)
+node %352 : bv<1> = not(or(%177, %156))
 node _eq_sdram_controller.no_tri_state.v:209_10 : bv<1> = eq(state, 5'b10100)
 state command : bv<8>
-  [next] ite(rst_n, ite(_auto_opt_dff.cc:195:make_patterns_logic_224, ite(_eq_sdram_controller.no_tri_state.v:292_24, ite(_ge_sdram_controller.no_tri_state.v:294_25, 8'b10010001, ite(rd_enable, 8'b10011000, ite(wr_enable, 8'b10011000, 8'b10111000))), ite(_logic_not_sdram_controller.no_tri_state.v:315_26, %152[16:9], 8'b00000000)), command), 8'b10111000)
+  [next] ite(rst_n, ite(%352, ite(%177, ite(%344, 8'b10010001, ite(rd_enable, 8'b10011000, ite(wr_enable, 8'b10011000, 8'b10111000))), ite(%156, %152[16:9], 8'b00000000)), command), 8'b10111000)
 state state : bv<5>
-  [next] ite(rst_n, ite(_auto_opt_dff.cc:195:make_patterns_logic_224, ite(_eq_sdram_controller.no_tri_state.v:292_24, ite(_ge_sdram_controller.no_tri_state.v:294_25, 5'b00001, ite(rd_enable, 5'b10000, ite(wr_enable, 5'b11000, 5'b00000))), ite(_logic_not_sdram_controller.no_tri_state.v:315_26, %152[8:4], 5'b00000)), state), 5'b01000)
+  [next] ite(rst_n, ite(%352, ite(%177, ite(%344, 5'b00001, ite(rd_enable, 5'b10000, ite(wr_enable, 5'b11000, 5'b00000))), ite(%156, %152[8:4], 5'b00000)), state), 5'b01000)
 state haddr_r : bv<24>
   [next] ite(rst_n, ite(not(or(rd_enable, wr_enable)), ite(rd_enable, rd_addr, ite(wr_enable, wr_addr, 24'x000000)), haddr_r), 24'x000000)
-state busy : bv<1>
+state busy_0 : bv<1>
   [next] and(rst_n, %39)
-state data_out : bv<16>
-  [next] ite(rst_n, ite(wr_enable, wr_data, data_out), 16'x0000)
-state rd_data : bv<16>
-  [next] ite(rst_n, ite(_eq_sdram_controller.no_tri_state.v:209_10, data_in, rd_data), 16'x0000)
-state rd_ready : bv<1>
-  [next] ite(rst_n, _eq_sdram_controller.no_tri_state.v:209_10, rd_ready)
+state data_out_0 : bv<16>
+  [next] ite(rst_n, ite(wr_enable, wr_data, data_out_0), 16'x0000)
+state rd_data_0 : bv<16>
+  [next] ite(rst_n, ite(_eq_sdram_controller.no_tri_state.v:209_10, data_in, rd_data_0), 16'x0000)
+state rd_ready_0 : bv<1>
+  [next] ite(rst_n, _eq_sdram_controller.no_tri_state.v:209_10, rd_ready_0)
 state _state_5 : bv<5> -> bv<17>
   [init] ([17'x00000] x 2^5)[5'b00000 := 17'x17000][5'b00001 := 17'x17020][5'b00010 := 17'x11030][5'b00011 := 17'x17047][5'b00100 := 17'x17000][5'b00101 := 17'x110a0][5'b00110 := 17'x17000][5'b00111 := 17'x17000][5'b01000 := 17'x12290][5'b01001 := 17'x17050][5'b01010 := 17'x170b7][5'b01011 := 17'x110c0][5'b01100 := 17'x170d7][5'b01101 := 17'x100e0][5'b01110 := 17'x170f1][5'b01111 := 17'x17000][5'b10000 := 17'x17111][5'b10001 := 17'x15320][5'b10010 := 17'x17131][5'b10011 := 17'x17140][5'b10100 := 17'x17000][5'b10101 := 17'x17000][5'b10110 := 17'x17000][5'b10111 := 17'x17000][5'b11000 := 17'x17191][5'b11001 := 17'x143a0][5'b11010 := 17'x171b1][5'b11011 := 17'x17000][5'b11100 := 17'x17000][5'b11101 := 17'x17000][5'b11110 := 17'x17000][5'b11111 := 17'x17000]
   [next] _state_5
 state state_cnt : bv<4>
-  [next] ite(rst_n, ite(_logic_not_sdram_controller.no_tri_state.v:315_26, ite(_eq_sdram_controller.no_tri_state.v:292_24, 4'b0000, %152[3:0]), sub(state_cnt, 4'b0001)), 4'b1111)
+  [next] ite(rst_n, ite(%156, ite(%177, 4'b0000, %152[3:0]), sub(state_cnt, 4'b0001)), 4'b1111)
 state refresh_cnt : bv<10>
   [next] ite(not(and(rst_n, not(eq(state, 5'b00100)))), 10'x000, add(refresh_cnt, 10'x001))
+