Page 241 - 《软件学报》2021年第6期

姚广宇 等:芯片开发功能验证的形式化方法 1815

int every_i<==0 and skip;
unsigned int TEMP<==0 and skip;
int cycle_num<==8 and skip;
input (cycle_num) and skip;
output (cycle_num) and skip;
int reg_counter_count<==0 and int counter_count[6] and skip;
int reg_signal_light_light1<==0 and int signal_light_light1[3] and skip;
int reg_signal_light_light2<==0 and int signal_light_light2[3] and skip;
int counter_counter_count<==0 and skip;
int signal_light_signal_light_light1<==0 and skip;
int signal_light_signal_light_light2<==0 and skip;
int signal_light_state[3] and skip;
int reg_signal_light_state<==0 and skip;
int now and now<==0 and skip;
int*signal_light_top_clk and skip;
signal_light_top_clk:=(int*)malloc(cycle_num*sizeof(int));
now<==0 and skip;
while (now<cycle_num)
{if (now%24=0) then {input (TEMP) and skip}
else {empty};
signal_light_top_clk[now]<==TEMP%2 and skip;
TEMP<==TEMP/2 and skip;
now<==now+1 and skip};
now<==0 and skip;
int*signal_light_top_rst and skip;
signal_light_top_rst:=(int*)malloc(cycle_num*sizeof(int));
now<==0 and skip;
while (now<cycle_num){if (now%24=0) then
{input (TEMP) and skip}
else {empty};
signal_light_top_rst[now]<==TEMP%2 and skip;
TEMP<==TEMP/2 and skip;
now<==now+1 and skip};
now<==0 and skip;
int signal_light_top_light1[3],reg_signal_light_top_light1 and reg_signal_light_top_light1<==0 and skip;
int signal_light_top_light2[3],reg_signal_light_top_light2 and reg_signal_light_top_light2<==0 and skip;
int signal_light_top_count[6],reg_signal_light_top_count and reg_signal_light_top_count<==0 and skip;
int signal_light_Idleand signal_light_Idle<==0 and skip;
signal_light_Idle<==0 and skip;
int signal_light_S1 and signal_light_S1<==0 and skip;
signal_light_S1<==1 and skip;
int signal_light_S2 and signal_light_S2<==0 and skip;