1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
|
`define ST_STOP 3'b001
`define ST_GO 3'b010
`define ST_SLOW 3'b100
module main;
reg clk;
reg go;
wire [2:0] state;
reg [3:0] err_mem[0:15];
reg [4:0] err_cnt;
fsma fsm1( clk, go, state );
fsmb fsm2( clk, go );
initial begin
err_cnt = 0;
forever @(posedge clk)
begin
err_mem[err_cnt] = {(state[0] & state[1]), (state[0] & state[2]), (state[1] & state[2]), (state == 3'b000)};
if( !err_cnt[4] && (err_mem[err_cnt] != 0) )
err_cnt = err_cnt + 1;
end
end
initial begin
$dumpfile( "example.vcd" );
$dumpvars( 0, main );
go = 1'b0;
repeat( 10 ) @(posedge clk);
go = 1'b1;
#10;
$finish;
end
initial begin
clk = 1'b0;
forever #(1) clk = ~clk;
end
endmodule
module fsma( clk, go, state );
input clk;
input go;
output [2:0] state;
reg [2:0] next_state;
reg [2:0] state;
initial begin
state = `ST_SLOW;
end
always @(posedge clk) state <= next_state;
(* covered_fsm, lights, is="state", os="next_state" *)
always @(state or go)
case( state )
`ST_STOP : next_state = go ? `ST_GO : `ST_STOP;
`ST_GO : next_state = go ? `ST_GO : `ST_SLOW;
`ST_SLOW : next_state = `ST_STOP;
endcase
assert_one_hot #(.width(3)) zzz_check_state ( clk, 1'b1, state );
endmodule
module fsmb( clk, go );
input clk;
input go;
reg [2:0] next_state;
reg [2:0] state;
initial begin
state = `ST_STOP;
end
always @(posedge clk) state <= next_state;
(* covered_fsm, lights, is="state", os="next_state",
trans="3'b001->3'b010",
trans="3'b010->3'b100",
trans="3'b100->3'b001" *)
always @(state or go)
case( state )
`ST_STOP : next_state = go ? `ST_GO : `ST_STOP;
`ST_GO : next_state = go ? `ST_GO : `ST_SLOW;
`ST_SLOW : next_state = `ST_STOP;
endcase
assert_one_hot #(.width(3)) zzz_check_state ( clk, 1'b1, state );
endmodule
|
