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