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

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

信号灯模块 end
module S1: if (count==′d24)
signal_light(clk,rst,count,light1,light2); begin
input clk, rst; state<=S2;
input [5:0] count; light1<=3′b100;
output [2:0] light1, light2; light2<=3′b010;
reg [2:0] light1, light2; end
reg [2:0] state; S2: if (count==′d29)
parameter begin
Idle=3′b000, state<=S3;
S1=3′b001, light1<=3′b001;
S2=3′b010, light2<=3′b100;
S3=3′b011, end
S4=3′b100; S3: if (count==′d54)
always@(posedgeclk) begin
begin state<=S4;
if (!rst) light1<=3′b010;
begin light2<=3′b100;
state<=Idle; end
light1<=3′b010; S4: if (count==′d59)
light2<=3′b010; begin
end state<=S1;
else light1<=3′b100;
case(state) light2<=3′b001;
Idle: if (rst) end
begin default: state<=Idle;
state<=S1; endcase
light1<=3′b100; end
light2<=3′b001; endmodule

附录 2. 转换得到的信号灯控制电路系统 MSVL 代码
function Bit_not(int a,intRValue)
{if (a=1) then {RValue:=0}
else
{RValue:=1}};
function counter(int counter_clk,intcounter_rst)
{if (counter_clk=Old_counter_clk+1
OR counter_rst=Old_counter_rst−1)
then {if (counter_rst≤0)
then {reg_counter_count:=0;
TEMP<==reg_counter_count and skip;
every_i:=0;