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

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

TEMP:=TEMP/2}}
else {empty}}
else
{if (reg_signal_light_state=signal_light_S3)
then {if (reg_signal_light_count=55)
then {reg_signal_light_state:=signal_light_S4;
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:=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:=4;
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_S4)
then {if (reg_signal_light_count=60)
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;