Skip to content

Instantly share code, notes, and snippets.

@taegyunkim

taegyunkim/times_two_if_else_raw_stateless_alu_3_3_verify_iter_1.sk

Created June 19, 2019 19:23
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save taegyunkim/b031407b0045352cafe960f9929315b8 to your computer and use it in GitHub Desktop.
Save taegyunkim/b031407b0045352cafe960f9929315b8 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
times_two_if_else_raw_stateless_alu_3_3_verify_iter_1.sk
// This is an autogenerated sketch file corresponding to
// the router's data path and is used to solve the Chipmunk compilation problem.
// program_file = example_specs/times_two.sk num_pipeline_stages = 3
// num_alus_per_stage = 3
// num_phv_containers = 3
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_Opt_2_global = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_0_opcode = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_Opt_1_global = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_2_mux3_ctrl = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_2_immediate = 2;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_0_mux2_ctrl = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_1_opcode = 12;
int times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_2_0_1_ctrl = 0;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_1_immediate = 2;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_2_mux1_ctrl = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_Mux3_0_global = 0;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_1_immediate = 0;
int times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_1_0_0_ctrl = 1;
int times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_1_0_ctrl = 1;
int times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_0_1_ctrl = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_2_mux2_ctrl = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_Mux3_1_global = 3;
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_Mux3_2_global = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_2_0_0_ctrl = 3;
int times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_0_0_0_ctrl = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_Opt_1_global = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_0_immediate = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_const_0_global = 0;
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_const_2_global = 0;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_1_mux3_ctrl = 0;
int times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_0_2_ctrl = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_0_mux1_ctrl = 2;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_1_mux1_ctrl = 3;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_0_immediate = 0;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_2_immediate = 0;
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_const_0_global = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_Mux3_1_global = 3;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_2_mux3_ctrl = 0;
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_Opt_2_global = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_0_mux3_ctrl = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_2_mux1_ctrl = 0;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_0_mux2_ctrl = 3;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_1_mux2_ctrl = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_2_opcode = 5;
int times_two_if_else_raw_stateless_alu_3_3_salu_config_0_0 = 0;
int times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_2_1_ctrl = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_0_mux3_ctrl = 1;
int times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_0_0_ctrl = 1;
int times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_1_2_ctrl = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_rel_op_0_global = 3;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_2_opcode = 0;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_0_immediate = 0;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_2_mux1_ctrl = 0;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_2_opcode = 4;
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_Mux3_0_global = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_1_mux3_ctrl = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_0_mux1_ctrl = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_Opt_0_global = 1;
int times_two_if_else_raw_stateless_alu_3_3_salu_config_2_0 = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_0_mux1_ctrl = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_Opt_2_global = 0;
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_Mux3_2_global = 3;
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_const_2_global = 3;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_1_mux2_ctrl = 3;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_1_immediate = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_2_mux2_ctrl = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_Mux3_0_global = 0;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_0_opcode = 5;
int times_two_if_else_raw_stateless_alu_3_3_salu_config_1_0 = 0;
int times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_0_0_1_ctrl = 3;
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_Mux3_2_global = 2;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_0_mux2_ctrl = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_0_opcode = 8;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_1_opcode = 5;
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_rel_op_0_global = 0;
int times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_2_2_ctrl = 0;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_2_immediate = 0;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_1_opcode = 5;
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_rel_op_0_global = 2;
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_const_2_global = 0;
int times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_1_0_1_ctrl = 2;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_2_mux2_ctrl = 1;
int times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_2_0_ctrl = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_1_mux2_ctrl = 3;
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_Opt_1_global = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_1_mux1_ctrl = 2;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_1_mux1_ctrl = 0;
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_const_1_global = 2;
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_Opt_0_global = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_Opt_0_global = 0;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_1_mux3_ctrl = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_const_1_global = 1;
int times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_1_1_ctrl = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_const_1_global = 0;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_2_mux3_ctrl = 0;
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_0_mux3_ctrl = 2;
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_Mux3_1_global = 1;
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_const_0_global = 0;
// Definitions of muxes and ALUs of the router
// Operand muxes for each ALU in each stage
// Total of 3 * 3 * 3 3-to-1 muxes
// The 3 is for two stateless operands and one stateful operand.
int times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_0_0_0(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_0_0_0_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_0_0_0_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_0_0_1(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_0_0_1_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_0_0_1_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_1_0_0(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_1_0_0_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_1_0_0_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_1_0_1(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_1_0_1_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_1_0_1_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_2_0_0(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_2_0_0_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_2_0_0_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_2_0_1(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_2_0_1_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_2_0_1_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}
// Output mux for each PHV container
// Allows the container to be written from either its own stateless ALU or any stateful ALU
int times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_0_0(int input0,int input1, int times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_0_0_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_0_0_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else { return input1; }
}
int times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_0_1(int input0,int input1, int times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_0_1_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_0_1_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else { return input1; }
}
int times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_0_2(int input0,int input1, int times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_0_2_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_0_2_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else { return input1; }
}
int times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_1_0(int input0,int input1, int times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_1_0_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_1_0_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else { return input1; }
}
int times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_1_1(int input0,int input1, int times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_1_1_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_1_1_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else { return input1; }
}
int times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_1_2(int input0,int input1, int times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_1_2_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_1_2_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else { return input1; }
}
int times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_2_0(int input0,int input1, int times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_2_0_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_2_0_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else { return input1; }
}
int times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_2_1(int input0,int input1, int times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_2_1_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_2_1_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else { return input1; }
}
int times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_2_2(int input0,int input1, int times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_2_2_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_2_2_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else { return input1; }
}
// Definition for ALUs
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_0_mux1(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_0_mux1_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_0_mux1_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_0_mux2(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_0_mux2_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_0_mux2_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_0_mux3(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_0_mux3_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_0_mux3_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}// Max value of opcode is 20
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_0(int input0,int input1,int input2, int opcode_hole_local, int immediate_operand_hole_local, int mux1_ctrl_hole_local, int mux2_ctrl_hole_local, int mux3_ctrl_hole_local) {
int opcode = opcode_hole_local;
int immediate_operand = immediate_operand_hole_local;
int x = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_0_mux1(input0,input1,input2, mux1_ctrl_hole_local);
int y = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_0_mux2(input0,input1,input2, mux2_ctrl_hole_local);
int z = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_0_mux3(input0,input1,input2, mux3_ctrl_hole_local);
if (opcode == 0) {
return immediate_operand;
} else if (opcode == 1) {
return x + y;
} else if (opcode == 2) {
return x + immediate_operand;
} else if (opcode == 3) {
return x - y;
} else if (opcode == 4) {
return x - immediate_operand;
} else if (opcode == 5) {
return immediate_operand - x;
} else if (opcode == 6) {
return (x != y) ? 1 : 0;
} else if (opcode == 7) {
return (x != immediate_operand) ? 1 : 0;
} else if (opcode == 8) {
return (x == y) ? 1 : 0;
} else if (opcode == 9) {
return (x == immediate_operand) ? 1 : 0;
} else if (opcode == 10) {
return (x >= y) ? 1 : 0;
} else if (opcode == 11) {
return (x >= immediate_operand) ? 1 : 0;
} else if (opcode == 12) {
return (x < y) ? 1 : 0;
} else if (opcode == 13) {
return (x < immediate_operand) ? 1 : 0;
} else if (opcode == 14) {
return (x != 0) ? y : z;
} else if (opcode == 15) {
return ( x != 0 ) ? (y) : immediate_operand;
} else if (opcode == 16) {
return ((x != 0) || (y != 0)) ? 1 : 0;
} else if (opcode == 17) {
return ((x != 0) || (immediate_operand != 0)) ? 1 : 0;
} else if (opcode == 18) {
return ((x != 0) && (y != 0)) ? 1 : 0;
} else if (opcode == 19) {
return ((x != 0) && (immediate_operand != 0)) ? 1 : 0;
} else {
return (!(x != 0)) ? 1 : 0;
}
}
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_1_mux1(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_1_mux1_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_1_mux1_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_1_mux2(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_1_mux2_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_1_mux2_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_1_mux3(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_1_mux3_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_1_mux3_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}// Max value of opcode is 20
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_1(int input0,int input1,int input2, int opcode_hole_local, int immediate_operand_hole_local, int mux1_ctrl_hole_local, int mux2_ctrl_hole_local, int mux3_ctrl_hole_local) {
int opcode = opcode_hole_local;
int immediate_operand = immediate_operand_hole_local;
int x = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_1_mux1(input0,input1,input2, mux1_ctrl_hole_local);
int y = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_1_mux2(input0,input1,input2, mux2_ctrl_hole_local);
int z = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_1_mux3(input0,input1,input2, mux3_ctrl_hole_local);
if (opcode == 0) {
return immediate_operand;
} else if (opcode == 1) {
return x + y;
} else if (opcode == 2) {
return x + immediate_operand;
} else if (opcode == 3) {
return x - y;
} else if (opcode == 4) {
return x - immediate_operand;
} else if (opcode == 5) {
return immediate_operand - x;
} else if (opcode == 6) {
return (x != y) ? 1 : 0;
} else if (opcode == 7) {
return (x != immediate_operand) ? 1 : 0;
} else if (opcode == 8) {
return (x == y) ? 1 : 0;
} else if (opcode == 9) {
return (x == immediate_operand) ? 1 : 0;
} else if (opcode == 10) {
return (x >= y) ? 1 : 0;
} else if (opcode == 11) {
return (x >= immediate_operand) ? 1 : 0;
} else if (opcode == 12) {
return (x < y) ? 1 : 0;
} else if (opcode == 13) {
return (x < immediate_operand) ? 1 : 0;
} else if (opcode == 14) {
return (x != 0) ? y : z;
} else if (opcode == 15) {
return ( x != 0 ) ? (y) : immediate_operand;
} else if (opcode == 16) {
return ((x != 0) || (y != 0)) ? 1 : 0;
} else if (opcode == 17) {
return ((x != 0) || (immediate_operand != 0)) ? 1 : 0;
} else if (opcode == 18) {
return ((x != 0) && (y != 0)) ? 1 : 0;
} else if (opcode == 19) {
return ((x != 0) && (immediate_operand != 0)) ? 1 : 0;
} else {
return (!(x != 0)) ? 1 : 0;
}
}
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_2_mux1(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_2_mux1_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_2_mux1_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_2_mux2(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_2_mux2_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_2_mux2_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_2_mux3(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_2_mux3_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_2_mux3_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}// Max value of opcode is 20
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_2(int input0,int input1,int input2, int opcode_hole_local, int immediate_operand_hole_local, int mux1_ctrl_hole_local, int mux2_ctrl_hole_local, int mux3_ctrl_hole_local) {
int opcode = opcode_hole_local;
int immediate_operand = immediate_operand_hole_local;
int x = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_2_mux1(input0,input1,input2, mux1_ctrl_hole_local);
int y = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_2_mux2(input0,input1,input2, mux2_ctrl_hole_local);
int z = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_2_mux3(input0,input1,input2, mux3_ctrl_hole_local);
if (opcode == 0) {
return immediate_operand;
} else if (opcode == 1) {
return x + y;
} else if (opcode == 2) {
return x + immediate_operand;
} else if (opcode == 3) {
return x - y;
} else if (opcode == 4) {
return x - immediate_operand;
} else if (opcode == 5) {
return immediate_operand - x;
} else if (opcode == 6) {
return (x != y) ? 1 : 0;
} else if (opcode == 7) {
return (x != immediate_operand) ? 1 : 0;
} else if (opcode == 8) {
return (x == y) ? 1 : 0;
} else if (opcode == 9) {
return (x == immediate_operand) ? 1 : 0;
} else if (opcode == 10) {
return (x >= y) ? 1 : 0;
} else if (opcode == 11) {
return (x >= immediate_operand) ? 1 : 0;
} else if (opcode == 12) {
return (x < y) ? 1 : 0;
} else if (opcode == 13) {
return (x < immediate_operand) ? 1 : 0;
} else if (opcode == 14) {
return (x != 0) ? y : z;
} else if (opcode == 15) {
return ( x != 0 ) ? (y) : immediate_operand;
} else if (opcode == 16) {
return ((x != 0) || (y != 0)) ? 1 : 0;
} else if (opcode == 17) {
return ((x != 0) || (immediate_operand != 0)) ? 1 : 0;
} else if (opcode == 18) {
return ((x != 0) && (y != 0)) ? 1 : 0;
} else if (opcode == 19) {
return ((x != 0) && (immediate_operand != 0)) ? 1 : 0;
} else {
return (!(x != 0)) ? 1 : 0;
}
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_Opt_0(int op1, int enable) {
if (enable != 0) return 0;
return op1;
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_C_0(int const) {
return const;
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_Mux3_0(int op1, int op2, int op3, int choice) {
if (choice == 0) return op1;
else if (choice == 1) return op2;
else return op3;
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_rel_op_0(int operand1, int operand2, int opcode) {
if (opcode == 0) {
return (operand1 != operand2) ? 1 : 0;
} else if (opcode == 1) {
return (operand1 < operand2) ? 1 : 0;
} else if (opcode == 2) {
return (operand1 > operand2) ? 1 : 0;
} else {
return (operand1 == operand2) ? 1 : 0;
}
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_Opt_1(int op1, int enable) {
if (enable != 0) return 0;
return op1;
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_C_1(int const) {
return const;
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_Mux3_1(int op1, int op2, int op3, int choice) {
if (choice == 0) return op1;
else if (choice == 1) return op2;
else return op3;
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_Opt_2(int op1, int enable) {
if (enable != 0) return 0;
return op1;
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_C_2(int const) {
return const;
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_Mux3_2(int op1, int op2, int op3, int choice) {
if (choice == 0) return op1;
else if (choice == 1) return op2;
else return op3;
}
|StateGroup| times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0(ref |StateGroup| state_group, int pkt_0,int pkt_1, int Mux3_0,int Mux3_1,int Mux3_2,int Opt_0,int Opt_1,int Opt_2,int const_0,int const_1,int const_2,int rel_op_0) {
|StateGroup| old_state_group = state_group;
int state_0 = state_group.state_0;if (times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_rel_op_0(times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_Opt_0(state_0,Opt_0),times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_Mux3_0(pkt_0,pkt_1,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_C_0(const_0),Mux3_0),rel_op_0) == 1) {state_0 = times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_Opt_1(state_0,Opt_1)+times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_Mux3_1(pkt_0,pkt_1,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_C_1(const_1),Mux3_1);}else {state_0 = times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_Opt_2(state_0,Opt_2)+times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_Mux3_2(pkt_0,pkt_1,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_C_2(const_2),Mux3_2);}
state_group.state_0 = state_0;
return old_state_group;
}
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_0_mux1(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_0_mux1_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_0_mux1_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_0_mux2(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_0_mux2_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_0_mux2_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_0_mux3(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_0_mux3_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_0_mux3_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}// Max value of opcode is 20
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_0(int input0,int input1,int input2, int opcode_hole_local, int immediate_operand_hole_local, int mux1_ctrl_hole_local, int mux2_ctrl_hole_local, int mux3_ctrl_hole_local) {
int opcode = opcode_hole_local;
int immediate_operand = immediate_operand_hole_local;
int x = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_0_mux1(input0,input1,input2, mux1_ctrl_hole_local);
int y = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_0_mux2(input0,input1,input2, mux2_ctrl_hole_local);
int z = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_0_mux3(input0,input1,input2, mux3_ctrl_hole_local);
if (opcode == 0) {
return immediate_operand;
} else if (opcode == 1) {
return x + y;
} else if (opcode == 2) {
return x + immediate_operand;
} else if (opcode == 3) {
return x - y;
} else if (opcode == 4) {
return x - immediate_operand;
} else if (opcode == 5) {
return immediate_operand - x;
} else if (opcode == 6) {
return (x != y) ? 1 : 0;
} else if (opcode == 7) {
return (x != immediate_operand) ? 1 : 0;
} else if (opcode == 8) {
return (x == y) ? 1 : 0;
} else if (opcode == 9) {
return (x == immediate_operand) ? 1 : 0;
} else if (opcode == 10) {
return (x >= y) ? 1 : 0;
} else if (opcode == 11) {
return (x >= immediate_operand) ? 1 : 0;
} else if (opcode == 12) {
return (x < y) ? 1 : 0;
} else if (opcode == 13) {
return (x < immediate_operand) ? 1 : 0;
} else if (opcode == 14) {
return (x != 0) ? y : z;
} else if (opcode == 15) {
return ( x != 0 ) ? (y) : immediate_operand;
} else if (opcode == 16) {
return ((x != 0) || (y != 0)) ? 1 : 0;
} else if (opcode == 17) {
return ((x != 0) || (immediate_operand != 0)) ? 1 : 0;
} else if (opcode == 18) {
return ((x != 0) && (y != 0)) ? 1 : 0;
} else if (opcode == 19) {
return ((x != 0) && (immediate_operand != 0)) ? 1 : 0;
} else {
return (!(x != 0)) ? 1 : 0;
}
}
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_1_mux1(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_1_mux1_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_1_mux1_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_1_mux2(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_1_mux2_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_1_mux2_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_1_mux3(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_1_mux3_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_1_mux3_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}// Max value of opcode is 20
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_1(int input0,int input1,int input2, int opcode_hole_local, int immediate_operand_hole_local, int mux1_ctrl_hole_local, int mux2_ctrl_hole_local, int mux3_ctrl_hole_local) {
int opcode = opcode_hole_local;
int immediate_operand = immediate_operand_hole_local;
int x = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_1_mux1(input0,input1,input2, mux1_ctrl_hole_local);
int y = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_1_mux2(input0,input1,input2, mux2_ctrl_hole_local);
int z = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_1_mux3(input0,input1,input2, mux3_ctrl_hole_local);
if (opcode == 0) {
return immediate_operand;
} else if (opcode == 1) {
return x + y;
} else if (opcode == 2) {
return x + immediate_operand;
} else if (opcode == 3) {
return x - y;
} else if (opcode == 4) {
return x - immediate_operand;
} else if (opcode == 5) {
return immediate_operand - x;
} else if (opcode == 6) {
return (x != y) ? 1 : 0;
} else if (opcode == 7) {
return (x != immediate_operand) ? 1 : 0;
} else if (opcode == 8) {
return (x == y) ? 1 : 0;
} else if (opcode == 9) {
return (x == immediate_operand) ? 1 : 0;
} else if (opcode == 10) {
return (x >= y) ? 1 : 0;
} else if (opcode == 11) {
return (x >= immediate_operand) ? 1 : 0;
} else if (opcode == 12) {
return (x < y) ? 1 : 0;
} else if (opcode == 13) {
return (x < immediate_operand) ? 1 : 0;
} else if (opcode == 14) {
return (x != 0) ? y : z;
} else if (opcode == 15) {
return ( x != 0 ) ? (y) : immediate_operand;
} else if (opcode == 16) {
return ((x != 0) || (y != 0)) ? 1 : 0;
} else if (opcode == 17) {
return ((x != 0) || (immediate_operand != 0)) ? 1 : 0;
} else if (opcode == 18) {
return ((x != 0) && (y != 0)) ? 1 : 0;
} else if (opcode == 19) {
return ((x != 0) && (immediate_operand != 0)) ? 1 : 0;
} else {
return (!(x != 0)) ? 1 : 0;
}
}
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_2_mux1(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_2_mux1_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_2_mux1_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_2_mux2(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_2_mux2_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_2_mux2_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_2_mux3(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_2_mux3_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_2_mux3_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}// Max value of opcode is 20
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_2(int input0,int input1,int input2, int opcode_hole_local, int immediate_operand_hole_local, int mux1_ctrl_hole_local, int mux2_ctrl_hole_local, int mux3_ctrl_hole_local) {
int opcode = opcode_hole_local;
int immediate_operand = immediate_operand_hole_local;
int x = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_2_mux1(input0,input1,input2, mux1_ctrl_hole_local);
int y = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_2_mux2(input0,input1,input2, mux2_ctrl_hole_local);
int z = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_2_mux3(input0,input1,input2, mux3_ctrl_hole_local);
if (opcode == 0) {
return immediate_operand;
} else if (opcode == 1) {
return x + y;
} else if (opcode == 2) {
return x + immediate_operand;
} else if (opcode == 3) {
return x - y;
} else if (opcode == 4) {
return x - immediate_operand;
} else if (opcode == 5) {
return immediate_operand - x;
} else if (opcode == 6) {
return (x != y) ? 1 : 0;
} else if (opcode == 7) {
return (x != immediate_operand) ? 1 : 0;
} else if (opcode == 8) {
return (x == y) ? 1 : 0;
} else if (opcode == 9) {
return (x == immediate_operand) ? 1 : 0;
} else if (opcode == 10) {
return (x >= y) ? 1 : 0;
} else if (opcode == 11) {
return (x >= immediate_operand) ? 1 : 0;
} else if (opcode == 12) {
return (x < y) ? 1 : 0;
} else if (opcode == 13) {
return (x < immediate_operand) ? 1 : 0;
} else if (opcode == 14) {
return (x != 0) ? y : z;
} else if (opcode == 15) {
return ( x != 0 ) ? (y) : immediate_operand;
} else if (opcode == 16) {
return ((x != 0) || (y != 0)) ? 1 : 0;
} else if (opcode == 17) {
return ((x != 0) || (immediate_operand != 0)) ? 1 : 0;
} else if (opcode == 18) {
return ((x != 0) && (y != 0)) ? 1 : 0;
} else if (opcode == 19) {
return ((x != 0) && (immediate_operand != 0)) ? 1 : 0;
} else {
return (!(x != 0)) ? 1 : 0;
}
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_Opt_0(int op1, int enable) {
if (enable != 0) return 0;
return op1;
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_C_0(int const) {
return const;
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_Mux3_0(int op1, int op2, int op3, int choice) {
if (choice == 0) return op1;
else if (choice == 1) return op2;
else return op3;
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_rel_op_0(int operand1, int operand2, int opcode) {
if (opcode == 0) {
return (operand1 != operand2) ? 1 : 0;
} else if (opcode == 1) {
return (operand1 < operand2) ? 1 : 0;
} else if (opcode == 2) {
return (operand1 > operand2) ? 1 : 0;
} else {
return (operand1 == operand2) ? 1 : 0;
}
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_Opt_1(int op1, int enable) {
if (enable != 0) return 0;
return op1;
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_C_1(int const) {
return const;
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_Mux3_1(int op1, int op2, int op3, int choice) {
if (choice == 0) return op1;
else if (choice == 1) return op2;
else return op3;
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_Opt_2(int op1, int enable) {
if (enable != 0) return 0;
return op1;
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_C_2(int const) {
return const;
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_Mux3_2(int op1, int op2, int op3, int choice) {
if (choice == 0) return op1;
else if (choice == 1) return op2;
else return op3;
}
|StateGroup| times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0(ref |StateGroup| state_group, int pkt_0,int pkt_1, int Mux3_0,int Mux3_1,int Mux3_2,int Opt_0,int Opt_1,int Opt_2,int const_0,int const_1,int const_2,int rel_op_0) {
|StateGroup| old_state_group = state_group;
int state_0 = state_group.state_0;if (times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_rel_op_0(times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_Opt_0(state_0,Opt_0),times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_Mux3_0(pkt_0,pkt_1,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_C_0(const_0),Mux3_0),rel_op_0) == 1) {state_0 = times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_Opt_1(state_0,Opt_1)+times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_Mux3_1(pkt_0,pkt_1,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_C_1(const_1),Mux3_1);}else {state_0 = times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_Opt_2(state_0,Opt_2)+times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_Mux3_2(pkt_0,pkt_1,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_C_2(const_2),Mux3_2);}
state_group.state_0 = state_0;
return old_state_group;
}
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_0_mux1(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_0_mux1_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_0_mux1_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_0_mux2(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_0_mux2_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_0_mux2_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_0_mux3(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_0_mux3_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_0_mux3_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}// Max value of opcode is 20
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_0(int input0,int input1,int input2, int opcode_hole_local, int immediate_operand_hole_local, int mux1_ctrl_hole_local, int mux2_ctrl_hole_local, int mux3_ctrl_hole_local) {
int opcode = opcode_hole_local;
int immediate_operand = immediate_operand_hole_local;
int x = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_0_mux1(input0,input1,input2, mux1_ctrl_hole_local);
int y = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_0_mux2(input0,input1,input2, mux2_ctrl_hole_local);
int z = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_0_mux3(input0,input1,input2, mux3_ctrl_hole_local);
if (opcode == 0) {
return immediate_operand;
} else if (opcode == 1) {
return x + y;
} else if (opcode == 2) {
return x + immediate_operand;
} else if (opcode == 3) {
return x - y;
} else if (opcode == 4) {
return x - immediate_operand;
} else if (opcode == 5) {
return immediate_operand - x;
} else if (opcode == 6) {
return (x != y) ? 1 : 0;
} else if (opcode == 7) {
return (x != immediate_operand) ? 1 : 0;
} else if (opcode == 8) {
return (x == y) ? 1 : 0;
} else if (opcode == 9) {
return (x == immediate_operand) ? 1 : 0;
} else if (opcode == 10) {
return (x >= y) ? 1 : 0;
} else if (opcode == 11) {
return (x >= immediate_operand) ? 1 : 0;
} else if (opcode == 12) {
return (x < y) ? 1 : 0;
} else if (opcode == 13) {
return (x < immediate_operand) ? 1 : 0;
} else if (opcode == 14) {
return (x != 0) ? y : z;
} else if (opcode == 15) {
return ( x != 0 ) ? (y) : immediate_operand;
} else if (opcode == 16) {
return ((x != 0) || (y != 0)) ? 1 : 0;
} else if (opcode == 17) {
return ((x != 0) || (immediate_operand != 0)) ? 1 : 0;
} else if (opcode == 18) {
return ((x != 0) && (y != 0)) ? 1 : 0;
} else if (opcode == 19) {
return ((x != 0) && (immediate_operand != 0)) ? 1 : 0;
} else {
return (!(x != 0)) ? 1 : 0;
}
}
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_1_mux1(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_1_mux1_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_1_mux1_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_1_mux2(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_1_mux2_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_1_mux2_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_1_mux3(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_1_mux3_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_1_mux3_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}// Max value of opcode is 20
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_1(int input0,int input1,int input2, int opcode_hole_local, int immediate_operand_hole_local, int mux1_ctrl_hole_local, int mux2_ctrl_hole_local, int mux3_ctrl_hole_local) {
int opcode = opcode_hole_local;
int immediate_operand = immediate_operand_hole_local;
int x = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_1_mux1(input0,input1,input2, mux1_ctrl_hole_local);
int y = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_1_mux2(input0,input1,input2, mux2_ctrl_hole_local);
int z = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_1_mux3(input0,input1,input2, mux3_ctrl_hole_local);
if (opcode == 0) {
return immediate_operand;
} else if (opcode == 1) {
return x + y;
} else if (opcode == 2) {
return x + immediate_operand;
} else if (opcode == 3) {
return x - y;
} else if (opcode == 4) {
return x - immediate_operand;
} else if (opcode == 5) {
return immediate_operand - x;
} else if (opcode == 6) {
return (x != y) ? 1 : 0;
} else if (opcode == 7) {
return (x != immediate_operand) ? 1 : 0;
} else if (opcode == 8) {
return (x == y) ? 1 : 0;
} else if (opcode == 9) {
return (x == immediate_operand) ? 1 : 0;
} else if (opcode == 10) {
return (x >= y) ? 1 : 0;
} else if (opcode == 11) {
return (x >= immediate_operand) ? 1 : 0;
} else if (opcode == 12) {
return (x < y) ? 1 : 0;
} else if (opcode == 13) {
return (x < immediate_operand) ? 1 : 0;
} else if (opcode == 14) {
return (x != 0) ? y : z;
} else if (opcode == 15) {
return ( x != 0 ) ? (y) : immediate_operand;
} else if (opcode == 16) {
return ((x != 0) || (y != 0)) ? 1 : 0;
} else if (opcode == 17) {
return ((x != 0) || (immediate_operand != 0)) ? 1 : 0;
} else if (opcode == 18) {
return ((x != 0) && (y != 0)) ? 1 : 0;
} else if (opcode == 19) {
return ((x != 0) && (immediate_operand != 0)) ? 1 : 0;
} else {
return (!(x != 0)) ? 1 : 0;
}
}
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_2_mux1(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_2_mux1_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_2_mux1_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_2_mux2(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_2_mux2_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_2_mux2_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_2_mux3(int input0,int input1,int input2, int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_2_mux3_ctrl_local) {
int mux_ctrl = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_2_mux3_ctrl_local;
if (mux_ctrl == 0) {
return input0;
}
else if (mux_ctrl == 1) {
return input1;
}
else { return input2; }
}// Max value of opcode is 20
int times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_2(int input0,int input1,int input2, int opcode_hole_local, int immediate_operand_hole_local, int mux1_ctrl_hole_local, int mux2_ctrl_hole_local, int mux3_ctrl_hole_local) {
int opcode = opcode_hole_local;
int immediate_operand = immediate_operand_hole_local;
int x = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_2_mux1(input0,input1,input2, mux1_ctrl_hole_local);
int y = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_2_mux2(input0,input1,input2, mux2_ctrl_hole_local);
int z = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_2_mux3(input0,input1,input2, mux3_ctrl_hole_local);
if (opcode == 0) {
return immediate_operand;
} else if (opcode == 1) {
return x + y;
} else if (opcode == 2) {
return x + immediate_operand;
} else if (opcode == 3) {
return x - y;
} else if (opcode == 4) {
return x - immediate_operand;
} else if (opcode == 5) {
return immediate_operand - x;
} else if (opcode == 6) {
return (x != y) ? 1 : 0;
} else if (opcode == 7) {
return (x != immediate_operand) ? 1 : 0;
} else if (opcode == 8) {
return (x == y) ? 1 : 0;
} else if (opcode == 9) {
return (x == immediate_operand) ? 1 : 0;
} else if (opcode == 10) {
return (x >= y) ? 1 : 0;
} else if (opcode == 11) {
return (x >= immediate_operand) ? 1 : 0;
} else if (opcode == 12) {
return (x < y) ? 1 : 0;
} else if (opcode == 13) {
return (x < immediate_operand) ? 1 : 0;
} else if (opcode == 14) {
return (x != 0) ? y : z;
} else if (opcode == 15) {
return ( x != 0 ) ? (y) : immediate_operand;
} else if (opcode == 16) {
return ((x != 0) || (y != 0)) ? 1 : 0;
} else if (opcode == 17) {
return ((x != 0) || (immediate_operand != 0)) ? 1 : 0;
} else if (opcode == 18) {
return ((x != 0) && (y != 0)) ? 1 : 0;
} else if (opcode == 19) {
return ((x != 0) && (immediate_operand != 0)) ? 1 : 0;
} else {
return (!(x != 0)) ? 1 : 0;
}
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_Opt_0(int op1, int enable) {
if (enable != 0) return 0;
return op1;
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_C_0(int const) {
return const;
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_Mux3_0(int op1, int op2, int op3, int choice) {
if (choice == 0) return op1;
else if (choice == 1) return op2;
else return op3;
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_rel_op_0(int operand1, int operand2, int opcode) {
if (opcode == 0) {
return (operand1 != operand2) ? 1 : 0;
} else if (opcode == 1) {
return (operand1 < operand2) ? 1 : 0;
} else if (opcode == 2) {
return (operand1 > operand2) ? 1 : 0;
} else {
return (operand1 == operand2) ? 1 : 0;
}
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_Opt_1(int op1, int enable) {
if (enable != 0) return 0;
return op1;
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_C_1(int const) {
return const;
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_Mux3_1(int op1, int op2, int op3, int choice) {
if (choice == 0) return op1;
else if (choice == 1) return op2;
else return op3;
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_Opt_2(int op1, int enable) {
if (enable != 0) return 0;
return op1;
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_C_2(int const) {
return const;
}
int times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_Mux3_2(int op1, int op2, int op3, int choice) {
if (choice == 0) return op1;
else if (choice == 1) return op2;
else return op3;
}
|StateGroup| times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0(ref |StateGroup| state_group, int pkt_0,int pkt_1, int Mux3_0,int Mux3_1,int Mux3_2,int Opt_0,int Opt_1,int Opt_2,int const_0,int const_1,int const_2,int rel_op_0) {
|StateGroup| old_state_group = state_group;
int state_0 = state_group.state_0;if (times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_rel_op_0(times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_Opt_0(state_0,Opt_0),times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_Mux3_0(pkt_0,pkt_1,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_C_0(const_0),Mux3_0),rel_op_0) == 1) {state_0 = times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_Opt_1(state_0,Opt_1)+times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_Mux3_1(pkt_0,pkt_1,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_C_1(const_1),Mux3_1);}else {state_0 = times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_Opt_2(state_0,Opt_2)+times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_Mux3_2(pkt_0,pkt_1,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_C_2(const_2),Mux3_2);}
state_group.state_0 = state_0;
return old_state_group;
}
struct StateGroup {
int state_0;
}
// Data type for holding result from spec and implementation
struct StateAndPacket {
int pkt_0;
int pkt_1;
int state_group_0_state_0;
}
// Specification
| StateAndPacket | program(| StateAndPacket | state_and_packet) {
if (state_and_packet.pkt_0 * 2 == state_and_packet.pkt_1) {
state_and_packet.state_group_0_state_0 = 1;
} else {
state_and_packet.state_group_0_state_0 = 0;
}
return state_and_packet;
}
// Implementation
|StateAndPacket| pipeline (|StateAndPacket| state_and_packet) {
// Any additional constraints to speed up synthesis through parallel execution.
// Consolidate all constraints on holes here.
assert((times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_0_opcode == 1)|| (times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_0_mux1_ctrl <= times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_0_mux2_ctrl));
assert((times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_1_opcode == 1)|| (times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_1_mux1_ctrl <= times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_1_mux2_ctrl));
assert((times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_2_opcode == 1)|| (times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_2_mux1_ctrl <= times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_2_mux2_ctrl));
assert((times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_0_opcode == 1)|| (times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_0_mux1_ctrl <= times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_0_mux2_ctrl));
assert((times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_1_opcode == 1)|| (times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_1_mux1_ctrl <= times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_1_mux2_ctrl));
assert((times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_2_opcode == 1)|| (times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_2_mux1_ctrl <= times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_2_mux2_ctrl));
assert((times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_0_opcode == 1)|| (times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_0_mux1_ctrl <= times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_0_mux2_ctrl));
assert((times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_1_opcode == 1)|| (times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_1_mux1_ctrl <= times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_1_mux2_ctrl));
assert((times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_2_opcode == 1)|| (times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_2_mux1_ctrl <= times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_2_mux2_ctrl));
assert((times_two_if_else_raw_stateless_alu_3_3_salu_config_0_0 + 0) <= 3);
assert((times_two_if_else_raw_stateless_alu_3_3_salu_config_1_0 + 0) <= 3);
assert((times_two_if_else_raw_stateless_alu_3_3_salu_config_2_0 + 0) <= 3);
assert((times_two_if_else_raw_stateless_alu_3_3_salu_config_0_0 + times_two_if_else_raw_stateless_alu_3_3_salu_config_1_0 + times_two_if_else_raw_stateless_alu_3_3_salu_config_2_0 + 0) <= 1);
// One variable for each container in the PHV
// Container i will be allocated to packet field i from the spec.
int input_0_0 = 0;
int input_0_1 = 0;
int input_0_2 = 0;
// One variable for each stateful ALU's state operand
// This will be allocated to a state variable from the program using indicator variables.
|StateGroup| state_operand_salu_0_0 = |StateGroup|(
state_0 = 0
);
|StateGroup| state_operand_salu_1_0 = |StateGroup|(
state_0 = 0
);
|StateGroup| state_operand_salu_2_0 = |StateGroup|(
state_0 = 0
);
/*********** Stage 0 *********/
// Inputs
// Read each PHV container from corresponding packet field.
input_0_0 = state_and_packet.pkt_0;
input_0_1 = state_and_packet.pkt_1;
// Stateless ALUs
int destination_0_0 = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_0(
input_0_0,
input_0_1,
input_0_2
,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_0_opcode,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_0_immediate,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_0_mux1_ctrl,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_0_mux2_ctrl,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_0_mux3_ctrl
);
int destination_0_1 = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_1(
input_0_0,
input_0_1,
input_0_2
,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_1_opcode,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_1_immediate,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_1_mux1_ctrl,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_1_mux2_ctrl,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_1_mux3_ctrl
);
int destination_0_2 = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_2(
input_0_0,
input_0_1,
input_0_2
,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_2_opcode,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_2_immediate,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_2_mux1_ctrl,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_2_mux2_ctrl,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_0_2_mux3_ctrl
);
// Stateful operands
int packet_operand_salu0_0_0 = times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_0_0_0(
input_0_0,
input_0_1,
input_0_2
, times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_0_0_0_ctrl);
int packet_operand_salu0_0_1 = times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_0_0_1(
input_0_0,
input_0_1,
input_0_2
, times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_0_0_1_ctrl);
// Read stateful ALU slots from allocated state vars.
if (times_two_if_else_raw_stateless_alu_3_3_salu_config_0_0 == 1) {
state_operand_salu_0_0 =
|StateGroup|( state_0 = state_and_packet.state_group_0_state_0
);}
// Stateful ALUs
|StateGroup| old_state_group_0_0 = times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0(state_operand_salu_0_0,
packet_operand_salu0_0_0,
packet_operand_salu0_0_1,
times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_Mux3_0_global,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_Mux3_1_global,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_Mux3_2_global,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_Opt_0_global,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_Opt_1_global,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_Opt_2_global,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_const_0_global,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_const_1_global,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_const_2_global,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_0_0_rel_op_0_global);
// Outputs
int output_0_0 = times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_0_0(
old_state_group_0_0.state_0,
destination_0_0,
times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_0_0_ctrl
);
int output_0_1 = times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_0_1(
old_state_group_0_0.state_0,
destination_0_1,
times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_0_1_ctrl
);
int output_0_2 = times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_0_2(
old_state_group_0_0.state_0,
destination_0_2,
times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_0_2_ctrl
);
// Write state_0
if (times_two_if_else_raw_stateless_alu_3_3_salu_config_0_0 == 1) {
state_and_packet.state_group_0_state_0 = state_operand_salu_0_0.state_0;
}
/*********** Stage 1 *********/
// Inputs
// Input of this stage is the output of the previous one.
int input_1_0 = output_0_0;
int input_1_1 = output_0_1;
int input_1_2 = output_0_2;
// Stateless ALUs
int destination_1_0 = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_0(
input_1_0,
input_1_1,
input_1_2
,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_0_opcode,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_0_immediate,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_0_mux1_ctrl,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_0_mux2_ctrl,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_0_mux3_ctrl
);
int destination_1_1 = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_1(
input_1_0,
input_1_1,
input_1_2
,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_1_opcode,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_1_immediate,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_1_mux1_ctrl,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_1_mux2_ctrl,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_1_mux3_ctrl
);
int destination_1_2 = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_2(
input_1_0,
input_1_1,
input_1_2
,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_2_opcode,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_2_immediate,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_2_mux1_ctrl,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_2_mux2_ctrl,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_1_2_mux3_ctrl
);
// Stateful operands
int packet_operand_salu1_0_0 = times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_1_0_0(
input_1_0,
input_1_1,
input_1_2
, times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_1_0_0_ctrl);
int packet_operand_salu1_0_1 = times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_1_0_1(
input_1_0,
input_1_1,
input_1_2
, times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_1_0_1_ctrl);
// Read stateful ALU slots from allocated state vars.
if (times_two_if_else_raw_stateless_alu_3_3_salu_config_1_0 == 1) {
state_operand_salu_1_0 =
|StateGroup|( state_0 = state_and_packet.state_group_0_state_0
);}
// Stateful ALUs
|StateGroup| old_state_group_1_0 = times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0(state_operand_salu_1_0,
packet_operand_salu1_0_0,
packet_operand_salu1_0_1,
times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_Mux3_0_global,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_Mux3_1_global,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_Mux3_2_global,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_Opt_0_global,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_Opt_1_global,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_Opt_2_global,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_const_0_global,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_const_1_global,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_const_2_global,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_1_0_rel_op_0_global);
// Outputs
int output_1_0 = times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_1_0(
old_state_group_1_0.state_0,
destination_1_0,
times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_1_0_ctrl
);
int output_1_1 = times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_1_1(
old_state_group_1_0.state_0,
destination_1_1,
times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_1_1_ctrl
);
int output_1_2 = times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_1_2(
old_state_group_1_0.state_0,
destination_1_2,
times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_1_2_ctrl
);
// Write state_0
if (times_two_if_else_raw_stateless_alu_3_3_salu_config_1_0 == 1) {
state_and_packet.state_group_0_state_0 = state_operand_salu_1_0.state_0;
}
/*********** Stage 2 *********/
// Inputs
// Input of this stage is the output of the previous one.
int input_2_0 = output_1_0;
int input_2_1 = output_1_1;
int input_2_2 = output_1_2;
// Stateless ALUs
int destination_2_0 = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_0(
input_2_0,
input_2_1,
input_2_2
,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_0_opcode,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_0_immediate,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_0_mux1_ctrl,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_0_mux2_ctrl,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_0_mux3_ctrl
);
int destination_2_1 = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_1(
input_2_0,
input_2_1,
input_2_2
,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_1_opcode,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_1_immediate,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_1_mux1_ctrl,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_1_mux2_ctrl,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_1_mux3_ctrl
);
int destination_2_2 = times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_2(
input_2_0,
input_2_1,
input_2_2
,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_2_opcode,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_2_immediate,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_2_mux1_ctrl,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_2_mux2_ctrl,
times_two_if_else_raw_stateless_alu_3_3_stateless_alu_2_2_mux3_ctrl
);
// Stateful operands
int packet_operand_salu2_0_0 = times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_2_0_0(
input_2_0,
input_2_1,
input_2_2
, times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_2_0_0_ctrl);
int packet_operand_salu2_0_1 = times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_2_0_1(
input_2_0,
input_2_1,
input_2_2
, times_two_if_else_raw_stateless_alu_3_3_stateful_operand_mux_2_0_1_ctrl);
// Read stateful ALU slots from allocated state vars.
if (times_two_if_else_raw_stateless_alu_3_3_salu_config_2_0 == 1) {
state_operand_salu_2_0 =
|StateGroup|( state_0 = state_and_packet.state_group_0_state_0
);}
// Stateful ALUs
|StateGroup| old_state_group_2_0 = times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0(state_operand_salu_2_0,
packet_operand_salu2_0_0,
packet_operand_salu2_0_1,
times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_Mux3_0_global,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_Mux3_1_global,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_Mux3_2_global,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_Opt_0_global,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_Opt_1_global,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_Opt_2_global,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_const_0_global,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_const_1_global,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_const_2_global,times_two_if_else_raw_stateless_alu_3_3_stateful_alu_2_0_rel_op_0_global);
// Outputs
int output_2_0 = times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_2_0(
old_state_group_2_0.state_0,
destination_2_0,
times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_2_0_ctrl
);
int output_2_1 = times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_2_1(
old_state_group_2_0.state_0,
destination_2_1,
times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_2_1_ctrl
);
int output_2_2 = times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_2_2(
old_state_group_2_0.state_0,
destination_2_2,
times_two_if_else_raw_stateless_alu_3_3_output_mux_phv_2_2_ctrl
);
// Write state_0
if (times_two_if_else_raw_stateless_alu_3_3_salu_config_2_0 == 1) {
state_and_packet.state_group_0_state_0 = state_operand_salu_2_0.state_0;
}
// Write pkt_0
state_and_packet.pkt_0 = output_2_0;
// Write pkt_1
state_and_packet.pkt_1 = output_2_1;
// Return updated packet fields and state vars
return state_and_packet;
}
harness void main(
int pkt_0,int pkt_1
, int state_group_0_state_0
) {
|StateAndPacket| x = |StateAndPacket|( pkt_0 = pkt_0,
pkt_1 = pkt_1,
state_group_0_state_0 = state_group_0_state_0
);
|StateAndPacket| pipeline_result = pipeline(x);
|StateAndPacket| program_result = program(x);
assert(pipeline_result.state_group_0_state_0
== program_result.state_group_0_state_0);
assert(pipeline_result.pkt_0 == program_result.pkt_0);
assert(pipeline_result.pkt_1 == program_result.pkt_1);
}
Raw
times_two_if_else_raw_stateless_alu_3_3_verify_iter_1.smt2
(assert (forall ((pkt_0_3_3_0 Int )(pkt_1_4_4_0 Int )(state_group_0_state_0_5_5_0 Int )) (let ((_n0 pkt_1_4_4_0 ))
(let ((_n1 2 ))
(let ((_n2 pkt_0_3_3_0 ))
(let ((_n3 (* _n2 _n1 ) ))
(let ((_n4 (= _n3 _n0 ) ))
(let ((_n5 (- 2) ))
(let ((_n6 (- _n0 )))
(let ((_n7 (< _n6 _n5 ) ))
(let ((_n8 (< _n2 _n0 ) ))
(let ((_n9 (= (ite _n8 1 0) _n2 ) ))
(let ((_n10 false ))
(let ((_n11 (ite _n7 _n10 _n9 ) ))
(let ((_n12 state_group_0_state_0_5_5_0 ))
(let ((_n13 (ite _n7 _n12 (ite _n10 1 0) ) ))
(let ((_n14 (+ _n13 _n11 ) ))
(let ((_n15 (ite _n7 (ite _n10 1 0) _n12 ) ))
(let ((_n16 (ite (= (ite _n7 1 0) 1) _n15 _n14 ) ))
(let ((_n17 (= _n16 (ite _n4 1 0) ) ))
(let ((_n19 (- _n2 )))
(let ((_n20 true ))
(let ((_n21 (+ (ite _n20 1 0) _n19 ) ))
(let ((_n22 (- _n21 )))
(let ((_n23 (+ (ite _n20 1 0) _n22 ) ))
(let ((_n24 (= _n23 _n2 ) ))
(let ((_n26 (+ _n1 _n6 ) ))
(let ((_n27 (- _n26 )))
(let ((_n28 (+ _n1 _n27 ) ))
(let ((_n29 (= _n28 _n0 ) ))
(implies (and (and (>= state_group_0_state_0_5_5_0 0) (< state_group_0_state_0_5_5_0 1024 )) (and (and (>= pkt_1_4_4_0 0) (< pkt_1_4_4_0 1024 )) (and (>= pkt_0_3_3_0 0) (< pkt_0_3_3_0 1024 )) ) ) (and _n17 _n24 _n29 ) )))))))))))))))))))))))))))))))
(check-sat)
(get-model)
(exit)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment