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

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

reg_signal_light_light1:=2;
TEMP<==reg_signal_light_light1 and skip;
every_i:=0;
while (every_i≤2)
{signal_light_light1[every_i]:=TEMP%2;
every_i:=every_i+1;
TEMP:=TEMP/2};
reg_signal_light_light2:=2;
TEMP<==reg_signal_light_light2 and skip;
every_i:=0;
while (every_i≤2)
{signal_light_light2[every_i]:=TEMP%2;
every_i:=every_i+1;
TEMP:=TEMP/2}}
else {if (reg_signal_light_state=signal_light_Idle)
then {if (signal_light_rst≥1)
then {reg_signal_light_state:=signal_light_S1;
TEMP<==reg_signal_light_state and skip;
every_i:=0;
while (every_i≤2)
{signal_light_state[every_i]:=TEMP%2;
every_i:=every_i+1;
TEMP:=TEMP/2};
reg_signal_light_light1:=4;
TEMP<==reg_signal_light_light1 and skip;
every_i:=0;
while (every_i≤2)
{signal_light_light1[every_i]:=TEMP%2;
every_i:=every_i+1;
TEMP:=TEMP/2};
reg_signal_light_light2:=1;
TEMP<==reg_signal_light_light2 and skip;
every_i:=0;
while (every_i≤2)
{signal_light_light2[every_i]:=TEMP%2;
every_i:=every_i+1;
TEMP:=TEMP/2}}
else {empty}}
else {if (reg_signal_light_state=signal_light_S1)
then {if (reg_signal_light_count=25)
then {reg_signal_light_state:=signal_light_S2;
TEMP<==reg_signal_light_state and skip;