4  PLA Description

4.1  Input to meg

INPUTS: RESTART, DEBUG, GSAT_4BC1_OVERFLOW, GSAT_12BC_OVERFLOW, TERM_CLAUSE, SAT_LESS, CLAUSE_OKAY, ISUNSAT;
OUTPUTS: GSAT_8BMR_LOAD, GSAT_12BC_INCR, GSAT_12BC_CLEAR, RAND_WRITE, GSAT_4BC1_INCR, GSAT_4BC1_CLEAR, HIGH_BITS_SELECT0, HIGH_BITS_SELECT1, WRITE_REG_FILE, WRITE_REG_OUT, SOURCE_SELECT, SHR1_WRITE, SHR1_CLEAR, SAT_LOAD, SAT_CLEAR, OLD_SAT_LOAD, OLD_SAT_CLEAR, REG_LOAD_SEL, UNSAT_CLEAR, UNSAT_MARK, FINISH;
RESET ON RESTART TO init;


init: if DEBUG then init else init_vars;

init_vars: if DEBUG then init_vars else init_vars_wait1 (GSAT_4BC1_CLEAR);

init_vars_wait1: if DEBUG then init_vars_wait1 else init_vars_wait2;

init_vars_wait2: if DEBUG then init_vars_wait2 else init_vars_wait3;

init_vars_wait3: if DEBUG then init_vars_wait3 else init_vars_wait4;

init_vars_wait4: if DEBUG then init_vars_wait4 else init_vars_wait5;

init_vars_wait5: if DEBUG then init_vars_wait5 else init_vars_wait6;

init_vars_wait6: if DEBUG then init_vars_wait6 else init_vars_wait7;

init_vars_wait7: if DEBUG then init_vars_wait7 else init_vars_wait8;

init_vars_wait8: if DEBUG then init_vars_wait8 else init_vars_inc (REG_LOAD_SEL, WRITE_REG_FILE, HIGH_BITS_SELECT0, HIGH_BITS_SELECT1);

init_vars_inc: case (DEBUG GSAT_4BC1_OVERFLOW)
		0 1 => start_gsat;
		0 0 => init_vars_wait1 (GSAT_4BC1_INCR);
		1 ? => init_vars_inc;
		ENDCASE => init_vars_inc;

start_gsat: if DEBUG then start_gsat else gsat_init_count0 (GSAT_12BC_CLEAR, UNSAT_CLEAR, SHR1_CLEAR, SAT_CLEAR, OLD_SAT_CLEAR);

gsat_init_count0: case (DEBUG GSAT_12BC_OVERFLOW)
		0 1 => gsat_pick_var;
		0 0 => gsat_init_count0a (GSAT_8BMR_LOAD);
		1 ? => gsat_init_count0;
		ENDCASE => gsat_init_count0;

gsat_init_count0a: if DEBUG then gsat_init_count0a else gsat_init_count0b (GSAT_8BMR_LOAD);

gsat_init_count0b: if DEBUG then gsat_init_count0b else gsat_init_count1 (GSAT_8BMR_LOAD);

gsat_init_count1: if DEBUG then gsat_init_count1 else gsat_init_count2 (GSAT_12BC_INCR, HIGH_BITS_SELECT1, WRITE_REG_OUT, SOURCE_SELECT, SHR1_WRITE);

gsat_init_count2: case (DEBUG GSAT_12BC_OVERFLOW)
		0 1 => gsat_pick_var;
		0 0 => gsat_init_count2a (GSAT_8BMR_LOAD);
		1 ? => gsat_init_count2;
		ENDCASE => gsat_init_count2;

gsat_init_count2a: if DEBUG then gsat_init_count2a else gsat_init_count2b (GSAT_8BMR_LOAD);

gsat_init_count2b: if DEBUG then gsat_init_count2b else gsat_init_count3 (GSAT_8BMR_LOAD);

gsat_init_count3: if DEBUG then gsat_init_count3 else gsat_init_count4 (GSAT_12BC_INCR, HIGH_BITS_SELECT1, WRITE_REG_OUT, SOURCE_SELECT, SHR1_WRITE);

gsat_init_count4: case (DEBUG GSAT_12BC_OVERFLOW)
		0 1 => gsat_pick_var;
		0 0 => gsat_init_count4a (GSAT_8BMR_LOAD);
		1 ? => gsat_init_count4;
		ENDCASE => gsat_init_count4;

gsat_init_count4a: if DEBUG then gsat_init_count4a else gsat_init_count4b (GSAT_8BMR_LOAD);

gsat_init_count4b: if DEBUG then gsat_init_count4b else gsat_init_count5 (GSAT_8BMR_LOAD);

gsat_init_count5: case (DEBUG TERM_CLAUSE CLAUSE_OKAY)
		0 0 1 => gsat_init_count0 (GSAT_12BC_INCR, HIGH_BITS_SELECT1, WRITE_REG_OUT, SOURCE_SELECT, SHR1_WRITE);
		0 0 0 => gsat_init_count0 (GSAT_12BC_INCR, HIGH_BITS_SELECT1, WRITE_REG_OUT, SOURCE_SELECT, SHR1_WRITE, UNSAT_MARK);
		0 1 ? => gsat_pick_var;
		1 ? ? => gsat_init_count5;
		ENDCASE => gsat_init_count5;

gsat_pick_var: case (DEBUG ISUNSAT)
		0 1 => gsat_flip_var0 (RAND_WRITE, OLD_SAT_LOAD);
		0 0 => done (FINISH);
		1 ? => gsat_pick_var;
		ENDCASE => gsat_pick_var;

gsat_flip_var0:	if DEBUG then gsat_flip_var0 else gsat_flip_var1(WRITE_REG_OUT, HIGH_BITS_SELECT0);

gsat_flip_var1: if DEBUG then gsat_flip_var1 else gsat_count0 (WRITE_REG_FILE, GSAT_12BC_CLEAR, UNSAT_CLEAR, SHR1_CLEAR, SAT_CLEAR, HIGH_BITS_SELECT0);

gsat_count0: case (DEBUG GSAT_12BC_OVERFLOW)
		0 1 => gsat_count_compare;
		0 0 => gsat_count0a (GSAT_8BMR_LOAD);
		1 ? => gsat_count0;
		ENDCASE => gsat_count0;

gsat_count0a: if DEBUG then gsat_count0a else gsat_count0b (GSAT_8BMR_LOAD);

gsat_count0b: if DEBUG then gsat_count0b else gsat_count1 (GSAT_8BMR_LOAD);

gsat_count1: if DEBUG then gsat_count1 else gsat_count2 (GSAT_12BC_INCR, HIGH_BITS_SELECT1, WRITE_REG_OUT, SOURCE_SELECT, SHR1_WRITE);

gsat_count2: case (DEBUG GSAT_12BC_OVERFLOW)
		0 1 => gsat_count_compare;
		0 0 => gsat_count2a (GSAT_8BMR_LOAD);
		1 ? => gsat_count2;
		ENDCASE => gsat_count2;

gsat_count2a: if DEBUG then gsat_count2a else gsat_count2b (GSAT_8BMR_LOAD);

gsat_count2b: if DEBUG then gsat_count2b else gsat_count3 (GSAT_8BMR_LOAD);

gsat_count3: if DEBUG then gsat_count3 else gsat_count4 (GSAT_12BC_INCR, HIGH_BITS_SELECT1, WRITE_REG_OUT, SOURCE_SELECT, SHR1_WRITE);

gsat_count4: case (DEBUG GSAT_12BC_OVERFLOW)
		0 1 => gsat_count_compare;
		0 0 => gsat_count4a (GSAT_8BMR_LOAD);
		1 ? => gsat_count4;
		ENDCASE => gsat_count4;

gsat_count4a: if DEBUG then gsat_count4a else gsat_count4b (GSAT_8BMR_LOAD);

gsat_count4b: if DEBUG then gsat_count4b else gsat_count5 (GSAT_8BMR_LOAD);

gsat_count5: case (DEBUG TERM_CLAUSE CLAUSE_OKAY)
		0 0 1 => gsat_count0 (GSAT_12BC_INCR, HIGH_BITS_SELECT1, WRITE_REG_OUT, SOURCE_SELECT, SHR1_WRITE);
		0 0 0 => gsat_count0 (GSAT_12BC_INCR, HIGH_BITS_SELECT1, WRITE_REG_OUT, SOURCE_SELECT, SHR1_WRITE, UNSAT_MARK);
		0 1 ? => gsat_count_compare;
		1 ? ? => gsat_count5;
		ENDCASE => gsat_count5;

gsat_count_compare: case (DEBUG SAT_LESS)
		0 1 => gsat_reflip0 (SAT_LOAD);
		0 0 => gsat_pick_var;
		1 ? => gsat_count_compare;
		ENDCASE => gsat_count_compare;

gsat_reflip0: if DEBUG then gsat_reflip0 else gsat_reflip1 (WRITE_REG_OUT, HIGH_BITS_SELECT0);

gsat_reflip1: if DEBUG then gsat_reflip1 else gsat_pick_var (WRITE_REG_FILE, HIGH_BITS_SELECT0);

done: goto done (FINISH);