luke
/
verilator
mirror of https://github.com/verilator/verilator.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Extend FSM coverage detection to case-free FSMs - Use - if/else chains (#7561)

This commit is contained in:
Yogish Sekhar 2026-05-10 17:12:58 +00:00 committed by GitHub
parent 303615bb37
commit f67159de30
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
17 changed files with 2630 additions and 121 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
docs/guide/simulating.rst
View File

@ -215,8 +215,8 @@ FSM Coverage
------------
With :vlopt:`--coverage` or :vlopt:`--coverage-fsm`, Verilator can
instrument a conservative subset of single-process FSMs and report both
state coverage (`fsm_state`) and transition coverage (`fsm_arc`).
instrument a conservative subset of FSMs and report both state coverage
(`fsm_state`) and transition coverage (`fsm_arc`).
This feature is currently experimental and might change in subsequent
releases. In particular, the native FSM coverage extraction heuristics,
@ -224,10 +224,26 @@ releases. In particular, the native FSM coverage extraction heuristics,
should be treated as subject to change while the interface settles.
FSM extraction is intentionally narrow. The current implementation targets
clocked, enum-driven state machines that can be recovered directly from the
RTL. It does not claim broad support for two-process FSMs, one-hot
inference, helper-function next-state recovery, or deeply nested control
recovery.
clocked state machines that can be recovered directly from the RTL. It
recognizes scalar enum, parameter, localparam, and selected literal state
encodings in these common forms:
- Single-process FSMs, whose state dispatch is written as ``case (state)``
or as a top-level ``if`` / ``else if`` chain comparing the same state
variable against known state values
- Two-process and three-block FSMs, where a clocked state register is paired
with a combinational next-state block using the same supported
``case`` or top-level ``if`` / ``else if`` dispatch forms
Simple input guards are supported when they appear inside a recognized
state branch, or as a top-level conjunction containing exactly one state
comparison, such as ``(state_q == IDLE) && ready``. Directly traceable
predecoded state aliases, such as ``assign idle_state = (state_q == IDLE)``,
may also be used in these guarded predicates.
Verilator does not claim broad support for arbitrary predicate
decomposition, one-hot inference, helper-function next-state recovery,
deeply nested control recovery, or cross-module state alias tracing.
The following metacomments may be attached to the state variable to steer
the extracted coverage model:

643
src/V3FsmDetect.cpp
View File

File diff suppressed because it is too large Load Diff

594
test_regress/t/t_cover_fsm_beginif.out
View File

@ -7,6 +7,556 @@
// SPDX-FileCopyrightText: 2026 Wilson Snyder
// SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
module fsm_if_enum_oneblock (
input logic clk,
input logic rst,
input logic start
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q;
always_ff @(posedge clk) begin
if (rst) state_q <= S0;
%000008 else if (state_q == S0) state_q <= start ? S1 : S0;
// [FSM coverage]
%000001 // [fsm_arc t.enum_oneblock_u.state_q::ANY->S0[reset]] [reset arc, excluded from %]
%000008 // [fsm_arc t.enum_oneblock_u.state_q::S0->S0]
%000001 // [fsm_arc t.enum_oneblock_u.state_q::S0->S1]
%000001 // [fsm_arc t.enum_oneblock_u.state_q::S1->S2]
%000001 // [fsm_arc t.enum_oneblock_u.state_q::S2->S0]
%000001 // [fsm_state t.enum_oneblock_u.state_q::S0]
%000001 // [fsm_state t.enum_oneblock_u.state_q::S1]
%000001 // [fsm_state t.enum_oneblock_u.state_q::S2]
else if (state_q == S1) state_q <= S2;
else if (state_q == S2) state_q <= S0;
end
endmodule
module fsm_if_enum_twoproc (
input logic clk,
input logic rst,
input logic start
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q;
state_t state_d;
always_comb begin
state_d = state_q;
%000008 if (state_q == S0) state_d = start ? S1 : S0;
// [FSM coverage]
%000001 // [fsm_arc t.enum_twoproc_u.state_q::ANY->S0[reset]] [reset arc, excluded from %]
%000008 // [fsm_arc t.enum_twoproc_u.state_q::S0->S0]
%000001 // [fsm_arc t.enum_twoproc_u.state_q::S0->S1]
%000001 // [fsm_arc t.enum_twoproc_u.state_q::S1->S2]
%000001 // [fsm_arc t.enum_twoproc_u.state_q::S2->S0]
%000001 // [fsm_state t.enum_twoproc_u.state_q::S0]
%000001 // [fsm_state t.enum_twoproc_u.state_q::S1]
%000001 // [fsm_state t.enum_twoproc_u.state_q::S2]
else if (state_q == S1) state_d = S2;
else if (state_q == S2) state_d = S0;
end
always_ff @(posedge clk) begin
if (rst) state_q <= S0;
else state_q <= state_d;
end
endmodule
module fsm_if_localparam (
input logic clk,
input logic rst,
input logic start
);
localparam logic [1:0] IDLE = 2'd0;
localparam logic [1:0] BUSY = 2'd1;
localparam logic [1:0] DONE = 2'd2;
logic [1:0] state_q;
logic [1:0] state_d;
always_comb begin
state_d = state_q;
%000008 if (state_q == IDLE) state_d = start ? BUSY : IDLE;
// [FSM coverage]
%000001 // [fsm_arc t.localparam_u.state_q::ANY->IDLE[reset]] [reset arc, excluded from %]
%000001 // [fsm_arc t.localparam_u.state_q::BUSY->DONE]
%000001 // [fsm_arc t.localparam_u.state_q::DONE->IDLE]
%000001 // [fsm_arc t.localparam_u.state_q::IDLE->BUSY]
%000008 // [fsm_arc t.localparam_u.state_q::IDLE->IDLE]
%000001 // [fsm_state t.localparam_u.state_q::BUSY]
%000001 // [fsm_state t.localparam_u.state_q::DONE]
%000001 // [fsm_state t.localparam_u.state_q::IDLE]
else if (state_q == BUSY) state_d = DONE;
else if (state_q == DONE) state_d = IDLE;
end
always_ff @(posedge clk) begin
if (rst) state_q <= IDLE;
else state_q <= state_d;
end
endmodule
module fsm_if_parameter #(
parameter logic [1:0] IDLE = 2'd0,
parameter logic [1:0] BUSY = 2'd1,
parameter logic [1:0] DONE = 2'd2
) (
input logic clk,
input logic rst,
input logic start
);
logic [1:0] state_q;
logic [1:0] state_d;
always_comb begin
state_d = state_q;
%000008 if (state_q == IDLE) state_d = start ? BUSY : IDLE;
// [FSM coverage]
%000001 // [fsm_arc t.parameter_u.state_q::ANY->IDLE[reset]] [reset arc, excluded from %]
%000001 // [fsm_arc t.parameter_u.state_q::BUSY->DONE]
%000001 // [fsm_arc t.parameter_u.state_q::DONE->IDLE]
%000001 // [fsm_arc t.parameter_u.state_q::IDLE->BUSY]
%000008 // [fsm_arc t.parameter_u.state_q::IDLE->IDLE]
%000001 // [fsm_state t.parameter_u.state_q::BUSY]
%000001 // [fsm_state t.parameter_u.state_q::DONE]
%000001 // [fsm_state t.parameter_u.state_q::IDLE]
else if (state_q == BUSY) state_d = DONE;
else if (state_q == DONE) state_d = IDLE;
end
always_ff @(posedge clk) begin
if (rst) state_q <= IDLE;
else state_q <= state_d;
end
endmodule
module fsm_if_literal_forced (
input logic clk,
input logic rst
);
logic [1:0] state /*verilator fsm_state*/;
always_ff @(posedge clk) begin
if (rst) state <= 2'd0;
%000003 else if (state == 2'd0) state <= 2'd1;
// [FSM coverage]
%000001 // [fsm_arc t.literal_forced_u.state::ANY->S0[reset]] [reset arc, excluded from %]
%000003 // [fsm_arc t.literal_forced_u.state::S0->S1]
%000003 // [fsm_arc t.literal_forced_u.state::S1->S2]
%000003 // [fsm_arc t.literal_forced_u.state::S2->S0]
%000003 // [fsm_state t.literal_forced_u.state::S0]
%000003 // [fsm_state t.literal_forced_u.state::S1]
%000003 // [fsm_state t.literal_forced_u.state::S2]
%000000 // [fsm_state t.literal_forced_u.state::S3] *** UNCOVERED ***
else if (state == 2'd1) state <= 2'd2;
else if (state == 2'd2) state <= 2'd0;
end
endmodule
module fsm_if_guard_state_first (
input logic clk,
input logic rst,
input logic start
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q;
state_t state_d;
always_comb begin
state_d = state_q;
%000001 if ((state_q == S0) && start) state_d = S1;
// [FSM coverage]
%000001 // [fsm_arc t.guard_state_first_u.state_q::ANY->S0[reset]] [reset arc, excluded from %]
%000001 // [fsm_arc t.guard_state_first_u.state_q::S0->S1]
%000001 // [fsm_arc t.guard_state_first_u.state_q::S1->S2]
%000001 // [fsm_arc t.guard_state_first_u.state_q::S2->S0]
%000001 // [fsm_state t.guard_state_first_u.state_q::S0]
%000001 // [fsm_state t.guard_state_first_u.state_q::S1]
%000001 // [fsm_state t.guard_state_first_u.state_q::S2]
else if (state_q == S1) state_d = S2;
else if (state_q == S2) state_d = S0;
end
always_ff @(posedge clk) begin
if (rst) state_q <= S0;
else state_q <= state_d;
end
endmodule
module fsm_if_guard_first (
input logic clk,
input logic rst,
input logic start
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q;
state_t state_d;
always_comb begin
state_d = state_q;
%000001 if (start && (state_q == S0)) state_d = S1;
// [FSM coverage]
%000001 // [fsm_arc t.guard_first_u.state_q::ANY->S0[reset]] [reset arc, excluded from %]
%000001 // [fsm_arc t.guard_first_u.state_q::S0->S1]
%000001 // [fsm_arc t.guard_first_u.state_q::S1->S2]
%000001 // [fsm_arc t.guard_first_u.state_q::S2->S0]
%000001 // [fsm_state t.guard_first_u.state_q::S0]
%000001 // [fsm_state t.guard_first_u.state_q::S1]
%000001 // [fsm_state t.guard_first_u.state_q::S2]
else if (state_q == S1) state_d = S2;
else if (state_q == S2) state_d = S0;
end
always_ff @(posedge clk) begin
if (rst) state_q <= S0;
else state_q <= state_d;
end
endmodule
module fsm_if_local_alias (
input logic clk,
input logic rst,
input logic start
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
logic idle_state;
state_t state_q;
state_t state_d;
always_comb begin
state_d = state_q;
idle_state = (state_q == S0);
%000001 if (idle_state && start) state_d = S1;
// [FSM coverage]
%000001 // [fsm_arc t.local_alias_u.state_q::ANY->S0[reset]] [reset arc, excluded from %]
%000001 // [fsm_arc t.local_alias_u.state_q::S0->S1]
%000001 // [fsm_arc t.local_alias_u.state_q::S1->S2]
%000001 // [fsm_arc t.local_alias_u.state_q::S2->S0]
%000001 // [fsm_state t.local_alias_u.state_q::S0]
%000001 // [fsm_state t.local_alias_u.state_q::S1]
%000001 // [fsm_state t.local_alias_u.state_q::S2]
else if (state_q == S1) state_d = S2;
else if (state_q == S2) state_d = S0;
end
always_ff @(posedge clk) begin
if (rst) state_q <= S0;
else state_q <= state_d;
end
endmodule
module fsm_if_continuous_alias (
input logic clk,
input logic rst,
input logic start
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
logic idle_state;
state_t state_q;
state_t state_d;
assign idle_state = (state_q == S0);
always_comb begin
state_d = state_q;
%000001 if (idle_state && start) state_d = S1;
// [FSM coverage]
%000001 // [fsm_arc t.continuous_alias_u.state_q::ANY->S0[reset]] [reset arc, excluded from %]
%000001 // [fsm_arc t.continuous_alias_u.state_q::S0->S1]
%000001 // [fsm_arc t.continuous_alias_u.state_q::S1->S2]
%000001 // [fsm_arc t.continuous_alias_u.state_q::S2->S0]
%000001 // [fsm_state t.continuous_alias_u.state_q::S0]
%000001 // [fsm_state t.continuous_alias_u.state_q::S1]
%000001 // [fsm_state t.continuous_alias_u.state_q::S2]
else if (state_q == S1) state_d = S2;
else if (state_q == S2) state_d = S0;
end
always_ff @(posedge clk) begin
if (rst) state_q <= S0;
else state_q <= state_d;
end
endmodule
module fsm_if_nested_bitand_guard (
input logic clk,
input logic rst,
input logic start,
input logic choose
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q;
state_t state_d;
always_comb begin
state_d = state_q;
~000011 if ((state_q == S0) & start) begin
// [FSM coverage]
%000001 // [fsm_arc t.nested_bitand_guard_u.state_q::ANY->S0[reset]] [reset arc, excluded from %]
000011 // [fsm_arc t.nested_bitand_guard_u.state_q::S0->S0]
%000000 // [fsm_arc t.nested_bitand_guard_u.state_q::S0->S1]
%000000 // [fsm_arc t.nested_bitand_guard_u.state_q::S1->S2]
%000000 // [fsm_arc t.nested_bitand_guard_u.state_q::S2->S0]
%000000 // [fsm_state t.nested_bitand_guard_u.state_q::S0] *** UNCOVERED ***
%000000 // [fsm_state t.nested_bitand_guard_u.state_q::S1] *** UNCOVERED ***
%000000 // [fsm_state t.nested_bitand_guard_u.state_q::S2] *** UNCOVERED ***
if (choose) state_d = S1;
else state_d = S0;
end else if (state_q == S1) state_d = S2;
else if (state_q == S2) state_d = S0;
end
always_ff @(posedge clk) begin
if (rst) state_q <= S0;
else state_q <= state_d;
end
endmodule
module fsm_if_default_incl (
input logic clk,
input logic rst,
input logic start
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q /*verilator fsm_arc_include_cond*/;
state_t state_d;
always_comb begin
state_d = state_q;
if (state_q == S0) state_d = start ? S1 : S0;
else if (state_q == S1) state_d = S2;
else state_d = S0;
end
always_ff @(posedge clk) begin
if (rst) state_q <= S0;
else state_q <= state_d;
end
endmodule
module fsm_if_oneblock_late_continuous_alias (
input logic clk,
input logic rst,
input logic start
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
logic idle_state;
state_t state_q;
always_ff @(posedge clk) begin
if (rst) state_q <= S0;
%000001 else if (idle_state && start) state_q <= S1;
// [FSM coverage]
%000001 // [fsm_arc t.oneblock_late_continuous_alias_u.state_q::ANY->S0[reset]] [reset arc, excluded from %]
%000001 // [fsm_arc t.oneblock_late_continuous_alias_u.state_q::S0->S1]
%000001 // [fsm_arc t.oneblock_late_continuous_alias_u.state_q::S1->S2]
%000001 // [fsm_arc t.oneblock_late_continuous_alias_u.state_q::S2->S0]
%000001 // [fsm_state t.oneblock_late_continuous_alias_u.state_q::S0]
%000001 // [fsm_state t.oneblock_late_continuous_alias_u.state_q::S1]
%000001 // [fsm_state t.oneblock_late_continuous_alias_u.state_q::S2]
else if (state_q == S1) state_q <= S2;
else if (state_q == S2) state_q <= S0;
end
assign idle_state = (state_q == S0);
endmodule
module fsm_if_nextstate_compare (
input logic clk,
input logic rst,
input logic start
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q;
state_t state_d;
always_comb begin
state_d = state_q;
%000008 if (state_d == S0) state_d = start ? S1 : S0;
// [FSM coverage]
%000001 // [fsm_arc t.nextstate_compare_u.state_q::ANY->S0[reset]] [reset arc, excluded from %]
%000008 // [fsm_arc t.nextstate_compare_u.state_q::S0->S0]
%000001 // [fsm_arc t.nextstate_compare_u.state_q::S0->S1]
%000001 // [fsm_arc t.nextstate_compare_u.state_q::S1->S2]
%000001 // [fsm_arc t.nextstate_compare_u.state_q::S2->S0]
%000001 // [fsm_state t.nextstate_compare_u.state_q::S0]
%000001 // [fsm_state t.nextstate_compare_u.state_q::S1]
%000001 // [fsm_state t.nextstate_compare_u.state_q::S2]
else if (state_d == S1) state_d = S2;
else if (state_d == S2) state_d = S0;
end
always_ff @(posedge clk) begin
if (rst) state_q <= S0;
else state_q <= state_d;
end
endmodule
module fsm_if_reversed_compare (
input logic clk,
input logic rst
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q;
always_ff @(posedge clk) begin
if (rst) state_q <= S0;
%000003 else if (S0 == state_q) state_q <= S1;
// [FSM coverage]
%000001 // [fsm_arc t.reversed_compare_u.state_q::ANY->S0[reset]] [reset arc, excluded from %]
%000003 // [fsm_arc t.reversed_compare_u.state_q::S0->S1]
%000003 // [fsm_arc t.reversed_compare_u.state_q::S1->S2]
%000003 // [fsm_arc t.reversed_compare_u.state_q::S2->S0]
%000003 // [fsm_state t.reversed_compare_u.state_q::S0]
%000003 // [fsm_state t.reversed_compare_u.state_q::S1]
%000003 // [fsm_state t.reversed_compare_u.state_q::S2]
else if (S1 == state_q) state_q <= S2;
else if (S2 == state_q) state_q <= S0;
end
endmodule
module fsm_if_duplicate_alias (
input logic clk,
input logic rst,
input logic start
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
logic idle_state;
state_t state_q;
state_t state_d;
always_comb begin
state_d = state_q;
idle_state = (state_q == S0);
idle_state = (state_q == S0);
%000001 if (idle_state && start) state_d = S1;
// [FSM coverage]
%000001 // [fsm_arc t.duplicate_alias_u.state_q::ANY->S0[reset]] [reset arc, excluded from %]
%000001 // [fsm_arc t.duplicate_alias_u.state_q::S0->S1]
%000001 // [fsm_arc t.duplicate_alias_u.state_q::S1->S2]
%000001 // [fsm_arc t.duplicate_alias_u.state_q::S2->S0]
%000001 // [fsm_state t.duplicate_alias_u.state_q::S0]
%000001 // [fsm_state t.duplicate_alias_u.state_q::S1]
%000001 // [fsm_state t.duplicate_alias_u.state_q::S2]
else if (state_q == S1) state_d = S2;
else if (state_q == S2) state_d = S0;
end
always_ff @(posedge clk) begin
if (rst) state_q <= S0;
else state_q <= state_d;
end
endmodule
module fsm_if_case_priority (
input logic clk,
input logic rst
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q;
state_t state_d;
state_t other_q;
state_t other_d;
always_comb begin
state_d = state_q;
other_d = other_q;
%000003 case (state_q)
// [FSM coverage]
%000001 // [fsm_arc t.case_priority_u.state_q::ANY->S0[reset]] [reset arc, excluded from %]
%000003 // [fsm_arc t.case_priority_u.state_q::S0->S1]
%000003 // [fsm_arc t.case_priority_u.state_q::S1->S2]
%000003 // [fsm_arc t.case_priority_u.state_q::S2->S0]
%000003 // [fsm_state t.case_priority_u.state_q::S0]
%000003 // [fsm_state t.case_priority_u.state_q::S1]
%000003 // [fsm_state t.case_priority_u.state_q::S2]
S0: state_d = S1;
S1: state_d = S2;
S2: state_d = S0;
default: state_d = state_q;
endcase
if (other_q == S0) other_d = S1;
else if (other_q == S1) other_d = S2;
else if (other_q == S2) other_d = S0;
end
always_ff @(posedge clk) begin
if (rst) begin
state_q <= S0;
other_q <= S0;
end else begin
state_q <= state_d;
other_q <= other_d;
end
end
endmodule
module t (
input logic clk
);
@ -19,21 +569,51 @@
logic rst;
logic sel;
logic start;
logic choose;
int cyc;
state_t state /*verilator fsm_reset_arc*/;
fsm_if_enum_oneblock enum_oneblock_u (.clk(clk), .rst(rst), .start(start));
fsm_if_enum_twoproc enum_twoproc_u (.clk(clk), .rst(rst), .start(start));
fsm_if_localparam localparam_u (.clk(clk), .rst(rst), .start(start));
fsm_if_parameter parameter_u (.clk(clk), .rst(rst), .start(start));
fsm_if_literal_forced literal_forced_u (.clk(clk), .rst(rst));
fsm_if_guard_state_first guard_state_first_u (.clk(clk), .rst(rst), .start(start));
fsm_if_guard_first guard_first_u (.clk(clk), .rst(rst), .start(start));
fsm_if_local_alias local_alias_u (.clk(clk), .rst(rst), .start(start));
fsm_if_continuous_alias continuous_alias_u (.clk(clk), .rst(rst), .start(start));
fsm_if_nested_bitand_guard nested_bitand_guard_u (
.clk(clk), .rst(rst), .start(start), .choose(choose));
fsm_if_default_incl default_incl_u (.clk(clk), .rst(rst), .start(start));
fsm_if_oneblock_late_continuous_alias oneblock_late_continuous_alias_u (
.clk(clk), .rst(rst), .start(start));
fsm_if_nextstate_compare nextstate_compare_u (.clk(clk), .rst(rst), .start(start));
fsm_if_reversed_compare reversed_compare_u (.clk(clk), .rst(rst));
fsm_if_duplicate_alias duplicate_alias_u (.clk(clk), .rst(rst), .start(start));
fsm_if_case_priority case_priority_u (.clk(clk), .rst(rst));
initial begin
rst = 1'b1;
sel = 1'b0;
start = 1'b0;
choose = 1'b0;
cyc = 0;
end
always @(posedge clk) begin
cyc <= cyc + 1;
if (cyc == 1) rst <= 1'b0;
if (cyc == 2) sel <= 1'b1;
if (cyc == 3) sel <= 1'b0;
if (cyc == 6) begin
if (cyc == 2) begin
sel <= 1'b1;
start <= 1'b1;
end
if (cyc == 3) begin
sel <= 1'b0;
choose <= 1'b1;
start <= 1'b0;
end
if (cyc == 10) begin
$write("*-* All Finished *-*\n");
$finish;
end
@ -44,15 +624,15 @@
state <= S0;
end
else begin
%000003 case (state)
%000005 case (state)
// [FSM coverage]
%000001 // [fsm_arc t.state::ANY->S0[reset_include]] [reset arc, excluded from %]
%000000 // [fsm_arc t.state::S0->S1]
%000003 // [fsm_arc t.state::S0->S2]
%000005 // [fsm_arc t.state::S0->S2]
%000000 // [fsm_arc t.state::S1->S0]
%000002 // [fsm_state t.state::S0]
%000004 // [fsm_state t.state::S0]
%000000 // [fsm_state t.state::S1] *** UNCOVERED ***
%000003 // [fsm_state t.state::S2]
%000005 // [fsm_state t.state::S2]
S0: begin
if (sel) begin
state <= S1;

459
test_regress/t/t_cover_fsm_beginif.v
View File

@ -6,6 +6,429 @@
// SPDX-FileCopyrightText: 2026 Wilson Snyder
// SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
module fsm_if_enum_oneblock (
input logic clk,
input logic rst,
input logic start
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q;
always_ff @(posedge clk) begin
if (rst) state_q <= S0;
else if (state_q == S0) state_q <= start ? S1 : S0;
else if (state_q == S1) state_q <= S2;
else if (state_q == S2) state_q <= S0;
end
endmodule
module fsm_if_enum_twoproc (
input logic clk,
input logic rst,
input logic start
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q;
state_t state_d;
always_comb begin
state_d = state_q;
if (state_q == S0) state_d = start ? S1 : S0;
else if (state_q == S1) state_d = S2;
else if (state_q == S2) state_d = S0;
end
always_ff @(posedge clk) begin
if (rst) state_q <= S0;
else state_q <= state_d;
end
endmodule
module fsm_if_localparam (
input logic clk,
input logic rst,
input logic start
);
localparam logic [1:0] IDLE = 2'd0;
localparam logic [1:0] BUSY = 2'd1;
localparam logic [1:0] DONE = 2'd2;
logic [1:0] state_q;
logic [1:0] state_d;
always_comb begin
state_d = state_q;
if (state_q == IDLE) state_d = start ? BUSY : IDLE;
else if (state_q == BUSY) state_d = DONE;
else if (state_q == DONE) state_d = IDLE;
end
always_ff @(posedge clk) begin
if (rst) state_q <= IDLE;
else state_q <= state_d;
end
endmodule
module fsm_if_parameter #(
parameter logic [1:0] IDLE = 2'd0,
parameter logic [1:0] BUSY = 2'd1,
parameter logic [1:0] DONE = 2'd2
) (
input logic clk,
input logic rst,
input logic start
);
logic [1:0] state_q;
logic [1:0] state_d;
always_comb begin
state_d = state_q;
if (state_q == IDLE) state_d = start ? BUSY : IDLE;
else if (state_q == BUSY) state_d = DONE;
else if (state_q == DONE) state_d = IDLE;
end
always_ff @(posedge clk) begin
if (rst) state_q <= IDLE;
else state_q <= state_d;
end
endmodule
module fsm_if_literal_forced (
input logic clk,
input logic rst
);
logic [1:0] state /*verilator fsm_state*/;
always_ff @(posedge clk) begin
if (rst) state <= 2'd0;
else if (state == 2'd0) state <= 2'd1;
else if (state == 2'd1) state <= 2'd2;
else if (state == 2'd2) state <= 2'd0;
end
endmodule
module fsm_if_guard_state_first (
input logic clk,
input logic rst,
input logic start
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q;
state_t state_d;
always_comb begin
state_d = state_q;
if ((state_q == S0) && start) state_d = S1;
else if (state_q == S1) state_d = S2;
else if (state_q == S2) state_d = S0;
end
always_ff @(posedge clk) begin
if (rst) state_q <= S0;
else state_q <= state_d;
end
endmodule
module fsm_if_guard_first (
input logic clk,
input logic rst,
input logic start
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q;
state_t state_d;
always_comb begin
state_d = state_q;
if (start && (state_q == S0)) state_d = S1;
else if (state_q == S1) state_d = S2;
else if (state_q == S2) state_d = S0;
end
always_ff @(posedge clk) begin
if (rst) state_q <= S0;
else state_q <= state_d;
end
endmodule
module fsm_if_local_alias (
input logic clk,
input logic rst,
input logic start
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
logic idle_state;
state_t state_q;
state_t state_d;
always_comb begin
state_d = state_q;
idle_state = (state_q == S0);
if (idle_state && start) state_d = S1;
else if (state_q == S1) state_d = S2;
else if (state_q == S2) state_d = S0;
end
always_ff @(posedge clk) begin
if (rst) state_q <= S0;
else state_q <= state_d;
end
endmodule
module fsm_if_continuous_alias (
input logic clk,
input logic rst,
input logic start
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
logic idle_state;
state_t state_q;
state_t state_d;
assign idle_state = (state_q == S0);
always_comb begin
state_d = state_q;
if (idle_state && start) state_d = S1;
else if (state_q == S1) state_d = S2;
else if (state_q == S2) state_d = S0;
end
always_ff @(posedge clk) begin
if (rst) state_q <= S0;
else state_q <= state_d;
end
endmodule
module fsm_if_nested_bitand_guard (
input logic clk,
input logic rst,
input logic start,
input logic choose
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q;
state_t state_d;
always_comb begin
state_d = state_q;
if ((state_q == S0) & start) begin
if (choose) state_d = S1;
else state_d = S0;
end else if (state_q == S1) state_d = S2;
else if (state_q == S2) state_d = S0;
end
always_ff @(posedge clk) begin
if (rst) state_q <= S0;
else state_q <= state_d;
end
endmodule
module fsm_if_default_incl (
input logic clk,
input logic rst,
input logic start
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q /*verilator fsm_arc_include_cond*/;
state_t state_d;
always_comb begin
state_d = state_q;
if (state_q == S0) state_d = start ? S1 : S0;
else if (state_q == S1) state_d = S2;
else state_d = S0;
end
always_ff @(posedge clk) begin
if (rst) state_q <= S0;
else state_q <= state_d;
end
endmodule
module fsm_if_oneblock_late_continuous_alias (
input logic clk,
input logic rst,
input logic start
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
logic idle_state;
state_t state_q;
always_ff @(posedge clk) begin
if (rst) state_q <= S0;
else if (idle_state && start) state_q <= S1;
else if (state_q == S1) state_q <= S2;
else if (state_q == S2) state_q <= S0;
end
assign idle_state = (state_q == S0);
endmodule
module fsm_if_nextstate_compare (
input logic clk,
input logic rst,
input logic start
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q;
state_t state_d;
always_comb begin
state_d = state_q;
if (state_d == S0) state_d = start ? S1 : S0;
else if (state_d == S1) state_d = S2;
else if (state_d == S2) state_d = S0;
end
always_ff @(posedge clk) begin
if (rst) state_q <= S0;
else state_q <= state_d;
end
endmodule
module fsm_if_reversed_compare (
input logic clk,
input logic rst
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q;
always_ff @(posedge clk) begin
if (rst) state_q <= S0;
else if (S0 == state_q) state_q <= S1;
else if (S1 == state_q) state_q <= S2;
else if (S2 == state_q) state_q <= S0;
end
endmodule
module fsm_if_duplicate_alias (
input logic clk,
input logic rst,
input logic start
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
logic idle_state;
state_t state_q;
state_t state_d;
always_comb begin
state_d = state_q;
idle_state = (state_q == S0);
idle_state = (state_q == S0);
if (idle_state && start) state_d = S1;
else if (state_q == S1) state_d = S2;
else if (state_q == S2) state_d = S0;
end
always_ff @(posedge clk) begin
if (rst) state_q <= S0;
else state_q <= state_d;
end
endmodule
module fsm_if_case_priority (
input logic clk,
input logic rst
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q;
state_t state_d;
state_t other_q;
state_t other_d;
always_comb begin
state_d = state_q;
other_d = other_q;
case (state_q)
S0: state_d = S1;
S1: state_d = S2;
S2: state_d = S0;
default: state_d = state_q;
endcase
if (other_q == S0) other_d = S1;
else if (other_q == S1) other_d = S2;
else if (other_q == S2) other_d = S0;
end
always_ff @(posedge clk) begin
if (rst) begin
state_q <= S0;
other_q <= S0;
end else begin
state_q <= state_d;
other_q <= other_d;
end
end
endmodule
module t (
input logic clk
);
@ -18,21 +441,51 @@ module t (
logic rst;
logic sel;
logic start;
logic choose;
int cyc;
state_t state /*verilator fsm_reset_arc*/;
fsm_if_enum_oneblock enum_oneblock_u (.clk(clk), .rst(rst), .start(start));
fsm_if_enum_twoproc enum_twoproc_u (.clk(clk), .rst(rst), .start(start));
fsm_if_localparam localparam_u (.clk(clk), .rst(rst), .start(start));
fsm_if_parameter parameter_u (.clk(clk), .rst(rst), .start(start));
fsm_if_literal_forced literal_forced_u (.clk(clk), .rst(rst));
fsm_if_guard_state_first guard_state_first_u (.clk(clk), .rst(rst), .start(start));
fsm_if_guard_first guard_first_u (.clk(clk), .rst(rst), .start(start));
fsm_if_local_alias local_alias_u (.clk(clk), .rst(rst), .start(start));
fsm_if_continuous_alias continuous_alias_u (.clk(clk), .rst(rst), .start(start));
fsm_if_nested_bitand_guard nested_bitand_guard_u (
.clk(clk), .rst(rst), .start(start), .choose(choose));
fsm_if_default_incl default_incl_u (.clk(clk), .rst(rst), .start(start));
fsm_if_oneblock_late_continuous_alias oneblock_late_continuous_alias_u (
.clk(clk), .rst(rst), .start(start));
fsm_if_nextstate_compare nextstate_compare_u (.clk(clk), .rst(rst), .start(start));
fsm_if_reversed_compare reversed_compare_u (.clk(clk), .rst(rst));
fsm_if_duplicate_alias duplicate_alias_u (.clk(clk), .rst(rst), .start(start));
fsm_if_case_priority case_priority_u (.clk(clk), .rst(rst));
initial begin
rst = 1'b1;
sel = 1'b0;
start = 1'b0;
choose = 1'b0;
cyc = 0;
end
always @(posedge clk) begin
cyc <= cyc + 1;
if (cyc == 1) rst <= 1'b0;
if (cyc == 2) sel <= 1'b1;
if (cyc == 3) sel <= 1'b0;
if (cyc == 6) begin
if (cyc == 2) begin
sel <= 1'b1;
start <= 1'b1;
end
if (cyc == 3) begin
sel <= 1'b0;
choose <= 1'b1;
start <= 1'b0;
end
if (cyc == 10) begin
$write("*-* All Finished *-*\n");
$finish;
end

12
test_regress/t/t_cover_fsm_if_unknown_enum_multi_bad.out
View File

@ -15,4 +15,16 @@
%Warning-COVERIGN: t/t_cover_fsm_if_unknown_enum_multi_bad.v:150:7: Ignoring unsupported: FSM coverage on enum state variable 't.unknown_source_u.state_q': case item value 3 is not present in the declared enum
150 | 2'd3: state_d = S0;
| ^~~~
%Warning-COVERIGN: t/t_cover_fsm_if_unknown_enum_multi_bad.v:175:5: Ignoring unsupported: FSM coverage on enum state variable 't.unknown_if_source_u.state_q': case item value 3 is not present in the declared enum
175 | if (state_q == 2'd3) state_d = S0;
| ^~
%Warning-COVERIGN: t/t_cover_fsm_if_unknown_enum_multi_bad.v:199:32: Ignoring unsupported: FSM coverage on enum state variable 't.unknown_if_direct_target_u.state_q': assigned value 3 is not present in the declared enum
199 | if (state_q == S0) state_d = 2'd3;
| ^
%Warning-COVERIGN: t/t_cover_fsm_if_unknown_enum_multi_bad.v:224:32: Ignoring unsupported: FSM coverage on enum state variable 't.unknown_if_then_target_u.state_q': assigned value 3 is not present in the declared enum
224 | if (state_q == S0) state_d = sel ? 2'd3 : S1;
| ^
%Warning-COVERIGN: t/t_cover_fsm_if_unknown_enum_multi_bad.v:249:32: Ignoring unsupported: FSM coverage on enum state variable 't.unknown_if_else_target_u.state_q': assigned value 3 is not present in the declared enum
249 | if (state_q == S0) state_d = sel ? S1 : 2'd3;
| ^
%Error: Exiting due to

102
test_regress/t/t_cover_fsm_if_unknown_enum_multi_bad.v
View File

@ -158,6 +158,104 @@ module unknown_source (
end
endmodule
module unknown_if_source (
input logic clk
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1
} state_t;
state_t state_q /*verilator fsm_state*/;
state_t state_d;
always_comb begin
state_d = state_q;
/* verilator lint_off ENUMVALUE */
if (state_q == 2'd3) state_d = S0;
/* verilator lint_on ENUMVALUE */
else if (state_q == S1) state_d = S0;
end
always_ff @(posedge clk) begin
state_q <= state_d;
end
endmodule
module unknown_if_direct_target (
input logic clk
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1
} state_t;
state_t state_q /*verilator fsm_state*/;
state_t state_d;
always_comb begin
state_d = state_q;
/* verilator lint_off ENUMVALUE */
if (state_q == S0) state_d = 2'd3;
/* verilator lint_on ENUMVALUE */
else if (state_q == S1) state_d = S0;
end
always_ff @(posedge clk) begin
state_q <= state_d;
end
endmodule
module unknown_if_then_target (
input logic clk
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1
} state_t;
logic sel;
state_t state_q /*verilator fsm_state*/;
state_t state_d;
always_comb begin
state_d = state_q;
/* verilator lint_off ENUMVALUE */
if (state_q == S0) state_d = sel ? 2'd3 : S1;
/* verilator lint_on ENUMVALUE */
else if (state_q == S1) state_d = S0;
end
always_ff @(posedge clk) begin
state_q <= state_d;
end
endmodule
module unknown_if_else_target (
input logic clk
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1
} state_t;
logic sel;
state_t state_q /*verilator fsm_state*/;
state_t state_d;
always_comb begin
state_d = state_q;
/* verilator lint_off ENUMVALUE */
if (state_q == S0) state_d = sel ? S1 : 2'd3;
/* verilator lint_on ENUMVALUE */
else if (state_q == S1) state_d = S0;
end
always_ff @(posedge clk) begin
state_q <= state_d;
end
endmodule
module t;
logic clk;
unknown_then unknown_then_u (.clk(clk));
@ -165,4 +263,8 @@ module t;
unknown_direct unknown_direct_u (.clk(clk));
unknown_reset unknown_reset_u (.clk(clk));
unknown_source unknown_source_u (.clk(clk));
unknown_if_source unknown_if_source_u (.clk(clk));
unknown_if_direct_target unknown_if_direct_target_u (.clk(clk));
unknown_if_then_target unknown_if_then_target_u (.clk(clk));
unknown_if_else_target unknown_if_else_target_u (.clk(clk));
endmodule

352
test_regress/t/t_cover_fsm_negative_extract.out
View File

@ -5,6 +5,340 @@
// SPDX-FileCopyrightText: 2026 Wilson Snyder
// SPDX-License-Identifier: CC0-1.0
module fsm_if_mixed_vars_bad (
input logic clk
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q /*verilator fsm_state*/;
state_t other_q;
state_t state_d;
always_comb begin
state_d = state_q;
if (state_q == S0) state_d = S1;
else if (other_q == S1) state_d = S2;
end
always_ff @(posedge clk) state_q <= state_d;
endmodule
module fsm_if_one_branch_bad (
input logic clk
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1
} state_t;
state_t state_q /*verilator fsm_state*/;
state_t state_d;
always_comb begin
state_d = state_q;
if (state_q == S0) state_d = S1;
end
always_ff @(posedge clk) state_q <= state_d;
endmodule
module fsm_if_duplicate_bad (
input logic clk
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1
} state_t;
state_t state_q /*verilator fsm_state*/;
state_t state_d;
always_comb begin
state_d = state_q;
if (state_q == S0) state_d = S1;
else if (state_q == S0) state_d = S0;
end
always_ff @(posedge clk) state_q <= state_d;
endmodule
module fsm_if_two_comparisons_bad (
input logic clk,
input logic start
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q /*verilator fsm_state*/;
state_t state_d;
always_comb begin
state_d = state_q;
if ((state_q == S0) && (state_q == S1)) state_d = S2;
else if (state_q == S1) state_d = S0;
end
always_ff @(posedge clk) state_q <= start ? state_d : state_q;
endmodule
module fsm_if_or_bad (
input logic clk
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q /*verilator fsm_state*/;
state_t state_d;
always_comb begin
state_d = state_q;
if ((state_q == S0) || (state_q == S1)) state_d = S2;
else if (state_q == S2) state_d = S0;
end
always_ff @(posedge clk) state_q <= state_d;
endmodule
module fsm_if_alias_guard_bad (
input logic clk,
input logic start
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
logic idle_state;
state_t state_q /*verilator fsm_state*/;
state_t state_d;
always_comb begin
state_d = state_q;
idle_state = (state_q == S0) && start;
if (idle_state) state_d = S1;
else if (state_q == S1) state_d = S2;
end
always_ff @(posedge clk) state_q <= state_d;
endmodule
module fsm_if_ambiguous_alias_bad (
input logic clk
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
logic idle_state;
state_t state_q /*verilator fsm_state*/;
state_t state_d;
always_comb begin
state_d = state_q;
idle_state = (state_q == S0);
idle_state = (state_q == S1);
idle_state = (state_q == S2);
if (idle_state) state_d = S2;
else if (state_q == S2) state_d = S0;
end
always_ff @(posedge clk) state_q <= state_d;
endmodule
module fsm_if_missing_default_bad (
input logic clk
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q /*verilator fsm_state*/;
state_t state_d;
always_comb begin
state_d = S0;
if (state_d == S0) state_d = S1;
else if (state_d == S1) state_d = S2;
end
always_ff @(posedge clk) state_q <= state_d;
endmodule
module fsm_if_no_assign_bad (
input logic clk
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1
} state_t;
logic flag;
state_t state_q /*verilator fsm_state*/;
state_t state_d;
always_comb begin
flag = 1'b0;
state_d = state_q;
if (state_q == S0) flag = 1'b1;
else if (state_q == S1) state_d = S0;
end
always_ff @(posedge clk) state_q <= state_d;
endmodule
module fsm_if_nonvar_compare_bad (
input logic clk
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1
} state_t;
state_t state_q /*verilator fsm_state*/;
state_t state_d;
always_comb begin
state_d = state_q;
%000003 if ((state_q + 2'd0) == S0) state_d = S1;
// [FSM coverage]
%000003 // [fsm_arc t.nonvar_compare_u.state_q::S0->S1]
%000003 // [fsm_arc t.nonvar_compare_u.state_q::S1->S0]
%000003 // [fsm_state t.nonvar_compare_u.state_q::S0]
%000003 // [fsm_state t.nonvar_compare_u.state_q::S1]
else if (state_q == S1) state_d = S0;
end
always_ff @(posedge clk) state_q <= state_d;
endmodule
module fsm_if_var_rhs_compare_bad (
input logic clk
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1
} state_t;
state_t state_q /*verilator fsm_state*/;
state_t state_d;
always_comb begin
state_d = state_q;
if (state_q == state_d) state_d = S1;
else if (state_q == S1) state_d = S0;
end
always_ff @(posedge clk) state_q <= state_d;
endmodule
module fsm_if_var_target_bad (
input logic clk,
input logic [1:0] dyn
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q /*verilator fsm_state*/;
state_t state_d;
always_comb begin
state_d = state_q;
if (state_q == S0) state_d = state_t'(dyn);
else if (state_q == S1) state_d = S2;
end
always_ff @(posedge clk) state_q <= state_d;
endmodule
module fsm_if_alias_other_state_bad (
input logic clk
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1
} state_t;
logic idle_state;
state_t state_q /*verilator fsm_state*/;
state_t other_q;
state_t state_d;
always_comb begin
state_d = state_q;
idle_state = (state_q == S0);
idle_state = (other_q == S0);
if (idle_state) state_d = S1;
else if (state_q == S1) state_d = S0;
end
always_ff @(posedge clk) state_q <= state_d;
endmodule
module fsm_if_bit_or_bad (
input logic clk,
input logic start
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q /*verilator fsm_state*/;
state_t state_d;
always_comb begin
state_d = state_q;
if ((state_q == S0) | start) state_d = S1;
else if (state_q == S1) state_d = S2;
end
always_ff @(posedge clk) state_q <= state_d;
endmodule
module fsm_if_reduction_bad (
input logic clk
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q /*verilator fsm_state*/;
state_t state_d;
always_comb begin
state_d = state_q;
if (&state_q) state_d = S1;
else if (state_q == S1) state_d = S2;
if (|state_q) state_d = S2;
else if (state_q == S2) state_d = S0;
if (^state_q) state_d = S0;
else if (state_q == S0) state_d = S1;
end
always_ff @(posedge clk) state_q <= state_d;
endmodule
module t (
input logic clk
);
@ -16,12 +350,30 @@
} state_t;
int cyc;
logic start;
logic side;
logic [2:0] dyn_case;
state_t state /*verilator fsm_reset_arc*/;
fsm_if_mixed_vars_bad mixed_vars_u (.clk(clk));
fsm_if_one_branch_bad one_branch_u (.clk(clk));
fsm_if_duplicate_bad duplicate_u (.clk(clk));
fsm_if_two_comparisons_bad two_comparisons_u (.clk(clk), .start(start));
fsm_if_or_bad or_u (.clk(clk));
fsm_if_alias_guard_bad alias_guard_u (.clk(clk), .start(start));
fsm_if_ambiguous_alias_bad ambiguous_alias_u (.clk(clk));
fsm_if_missing_default_bad missing_default_u (.clk(clk));
fsm_if_no_assign_bad no_assign_u (.clk(clk));
fsm_if_nonvar_compare_bad nonvar_compare_u (.clk(clk));
fsm_if_var_rhs_compare_bad var_rhs_compare_u (.clk(clk));
fsm_if_var_target_bad var_target_u (.clk(clk), .dyn(dyn_case[1:0]));
fsm_if_alias_other_state_bad alias_other_state_u (.clk(clk));
fsm_if_bit_or_bad bit_or_u (.clk(clk), .start(start));
fsm_if_reduction_bad reduction_u (.clk(clk));
initial begin
cyc = 0;
start = 1'b0;
side = 1'b0;
dyn_case = 3'd7;
end

347
test_regress/t/t_cover_fsm_negative_extract.v
View File

@ -4,6 +4,335 @@
// SPDX-FileCopyrightText: 2026 Wilson Snyder
// SPDX-License-Identifier: CC0-1.0
module fsm_if_mixed_vars_bad (
input logic clk
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q /*verilator fsm_state*/;
state_t other_q;
state_t state_d;
always_comb begin
state_d = state_q;
if (state_q == S0) state_d = S1;
else if (other_q == S1) state_d = S2;
end
always_ff @(posedge clk) state_q <= state_d;
endmodule
module fsm_if_one_branch_bad (
input logic clk
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1
} state_t;
state_t state_q /*verilator fsm_state*/;
state_t state_d;
always_comb begin
state_d = state_q;
if (state_q == S0) state_d = S1;
end
always_ff @(posedge clk) state_q <= state_d;
endmodule
module fsm_if_duplicate_bad (
input logic clk
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1
} state_t;
state_t state_q /*verilator fsm_state*/;
state_t state_d;
always_comb begin
state_d = state_q;
if (state_q == S0) state_d = S1;
else if (state_q == S0) state_d = S0;
end
always_ff @(posedge clk) state_q <= state_d;
endmodule
module fsm_if_two_comparisons_bad (
input logic clk,
input logic start
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q /*verilator fsm_state*/;
state_t state_d;
always_comb begin
state_d = state_q;
if ((state_q == S0) && (state_q == S1)) state_d = S2;
else if (state_q == S1) state_d = S0;
end
always_ff @(posedge clk) state_q <= start ? state_d : state_q;
endmodule
module fsm_if_or_bad (
input logic clk
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q /*verilator fsm_state*/;
state_t state_d;
always_comb begin
state_d = state_q;
if ((state_q == S0) || (state_q == S1)) state_d = S2;
else if (state_q == S2) state_d = S0;
end
always_ff @(posedge clk) state_q <= state_d;
endmodule
module fsm_if_alias_guard_bad (
input logic clk,
input logic start
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
logic idle_state;
state_t state_q /*verilator fsm_state*/;
state_t state_d;
always_comb begin
state_d = state_q;
idle_state = (state_q == S0) && start;
if (idle_state) state_d = S1;
else if (state_q == S1) state_d = S2;
end
always_ff @(posedge clk) state_q <= state_d;
endmodule
module fsm_if_ambiguous_alias_bad (
input logic clk
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
logic idle_state;
state_t state_q /*verilator fsm_state*/;
state_t state_d;
always_comb begin
state_d = state_q;
idle_state = (state_q == S0);
idle_state = (state_q == S1);
idle_state = (state_q == S2);
if (idle_state) state_d = S2;
else if (state_q == S2) state_d = S0;
end
always_ff @(posedge clk) state_q <= state_d;
endmodule
module fsm_if_missing_default_bad (
input logic clk
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q /*verilator fsm_state*/;
state_t state_d;
always_comb begin
state_d = S0;
if (state_d == S0) state_d = S1;
else if (state_d == S1) state_d = S2;
end
always_ff @(posedge clk) state_q <= state_d;
endmodule
module fsm_if_no_assign_bad (
input logic clk
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1
} state_t;
logic flag;
state_t state_q /*verilator fsm_state*/;
state_t state_d;
always_comb begin
flag = 1'b0;
state_d = state_q;
if (state_q == S0) flag = 1'b1;
else if (state_q == S1) state_d = S0;
end
always_ff @(posedge clk) state_q <= state_d;
endmodule
module fsm_if_nonvar_compare_bad (
input logic clk
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1
} state_t;
state_t state_q /*verilator fsm_state*/;
state_t state_d;
always_comb begin
state_d = state_q;
if ((state_q + 2'd0) == S0) state_d = S1;
else if (state_q == S1) state_d = S0;
end
always_ff @(posedge clk) state_q <= state_d;
endmodule
module fsm_if_var_rhs_compare_bad (
input logic clk
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1
} state_t;
state_t state_q /*verilator fsm_state*/;
state_t state_d;
always_comb begin
state_d = state_q;
if (state_q == state_d) state_d = S1;
else if (state_q == S1) state_d = S0;
end
always_ff @(posedge clk) state_q <= state_d;
endmodule
module fsm_if_var_target_bad (
input logic clk,
input logic [1:0] dyn
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q /*verilator fsm_state*/;
state_t state_d;
always_comb begin
state_d = state_q;
if (state_q == S0) state_d = state_t'(dyn);
else if (state_q == S1) state_d = S2;
end
always_ff @(posedge clk) state_q <= state_d;
endmodule
module fsm_if_alias_other_state_bad (
input logic clk
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1
} state_t;
logic idle_state;
state_t state_q /*verilator fsm_state*/;
state_t other_q;
state_t state_d;
always_comb begin
state_d = state_q;
idle_state = (state_q == S0);
idle_state = (other_q == S0);
if (idle_state) state_d = S1;
else if (state_q == S1) state_d = S0;
end
always_ff @(posedge clk) state_q <= state_d;
endmodule
module fsm_if_bit_or_bad (
input logic clk,
input logic start
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q /*verilator fsm_state*/;
state_t state_d;
always_comb begin
state_d = state_q;
if ((state_q == S0) | start) state_d = S1;
else if (state_q == S1) state_d = S2;
end
always_ff @(posedge clk) state_q <= state_d;
endmodule
module fsm_if_reduction_bad (
input logic clk
);
typedef enum logic [1:0] {
S0 = 2'd0,
S1 = 2'd1,
S2 = 2'd2
} state_t;
state_t state_q /*verilator fsm_state*/;
state_t state_d;
always_comb begin
state_d = state_q;
if (&state_q) state_d = S1;
else if (state_q == S1) state_d = S2;
if (|state_q) state_d = S2;
else if (state_q == S2) state_d = S0;
if (^state_q) state_d = S0;
else if (state_q == S0) state_d = S1;
end
always_ff @(posedge clk) state_q <= state_d;
endmodule
module t (
input logic clk
);
@ -15,12 +344,30 @@ module t (
} state_t;
int cyc;
logic start;
logic side;
logic [2:0] dyn_case;
state_t state /*verilator fsm_reset_arc*/;
fsm_if_mixed_vars_bad mixed_vars_u (.clk(clk));
fsm_if_one_branch_bad one_branch_u (.clk(clk));
fsm_if_duplicate_bad duplicate_u (.clk(clk));
fsm_if_two_comparisons_bad two_comparisons_u (.clk(clk), .start(start));
fsm_if_or_bad or_u (.clk(clk));
fsm_if_alias_guard_bad alias_guard_u (.clk(clk), .start(start));
fsm_if_ambiguous_alias_bad ambiguous_alias_u (.clk(clk));
fsm_if_missing_default_bad missing_default_u (.clk(clk));
fsm_if_no_assign_bad no_assign_u (.clk(clk));
fsm_if_nonvar_compare_bad nonvar_compare_u (.clk(clk));
fsm_if_var_rhs_compare_bad var_rhs_compare_u (.clk(clk));
fsm_if_var_target_bad var_target_u (.clk(clk), .dyn(dyn_case[1:0]));
fsm_if_alias_other_state_bad alias_other_state_u (.clk(clk));
fsm_if_bit_or_bad bit_or_u (.clk(clk), .start(start));
fsm_if_reduction_bad reduction_u (.clk(clk));
initial begin
cyc = 0;
start = 1'b0;
side = 1'b0;
dyn_case = 3'd7;
end

16
test_regress/t/t_cover_fsm_nonenum_unsupported_bad.out
View File

@ -1,15 +1,15 @@
%Warning-COVERIGN: t/t_cover_fsm_nonenum_unsupported_bad.v:32:7: Ignoring unsupported: FSM coverage on non-enum state variable 't.wide_state' with width 33 wider than 32 bits
32 | case (wide_state)
%Warning-COVERIGN: t/t_cover_fsm_nonenum_unsupported_bad.v:33:7: Ignoring unsupported: FSM coverage on non-enum state variable 't.wide_state' with width 33 wider than 32 bits
33 | case (wide_state)
| ^~~~
... For warning description see https://verilator.org/warn/COVERIGN?v=latest
... Use "/* verilator lint_off COVERIGN */" and lint_on around source to disable this message.
%Warning-COVERIGN: t/t_cover_fsm_nonenum_unsupported_bad.v:47:28: Ignoring unsupported: FSM coverage on non-enum state variable 't.target_state': target value 2 is not present in the inferred state space
47 | 2'h1: target_state <= 2'h2;
%Warning-COVERIGN: t/t_cover_fsm_nonenum_unsupported_bad.v:48:28: Ignoring unsupported: FSM coverage on non-enum state variable 't.target_state': target value 2 is not present in the inferred state space
48 | 2'h1: target_state <= 2'h2;
| ^~
%Warning-COVERIGN: t/t_cover_fsm_nonenum_unsupported_bad.v:61:9: Ignoring unsupported: FSM coverage on non-enum state variable 't.duplicate_state' with multiple labels for the same value 0: IDLE and RESET
61 | RESET: duplicate_state <= IDLE;
%Warning-COVERIGN: t/t_cover_fsm_nonenum_unsupported_bad.v:62:9: Ignoring unsupported: FSM coverage on non-enum state variable 't.duplicate_state' with multiple labels for the same value 0: IDLE and RESET
62 | RESET: duplicate_state <= IDLE;
| ^~~~~
%Warning-COVERIGN: t/t_cover_fsm_nonenum_unsupported_bad.v:77:9: Ignoring unsupported: FSM coverage on non-enum state variable 't.xz_case_state' with X/Z state encoding values
77 | 2'b1x: xz_case_state <= 2'h0;
%Warning-COVERIGN: t/t_cover_fsm_nonenum_unsupported_bad.v:78:9: Ignoring unsupported: FSM coverage on non-enum state variable 't.xz_case_state' with X/Z state encoding values
78 | 2'b1x: xz_case_state <= 2'h0;
| ^~~~~
%Error: Exiting due to

13
test_regress/t/t_cover_fsm_nonenum_unsupported_bad.v
View File

@ -23,6 +23,7 @@ module t (
logic [1:0] underscore_state;
logic [1:0] xz_reset_probe_state;
logic [1:0] xz_rhs_probe_state;
logic [32:0] wide_if_state /*verilator fsm_state*/;
always_ff @(posedge clk) begin
if (rst) begin
@ -136,6 +137,18 @@ module t (
end
end
always_ff @(posedge clk) begin
if (rst) begin
wide_if_state <= 33'h0;
end
else if (wide_if_state == 33'h0) begin
wide_if_state <= 33'h1;
end
else if (wide_if_state == 33'h1) begin
wide_if_state <= 33'h0;
end
end
logic [1:0] not_const_item_state;
always_ff @(posedge clk) begin

15
test_regress/t/t_cover_fsm_transition_shapes_multi.v
View File

@ -731,6 +731,20 @@ module fsm_forced_wide_bad (
endmodule
module fsm_forced_if_wide_bad (
input logic clk
);
// Forced non-enum FSMs enumerate every possible state; 31 bits is too many.
logic [30:0] state /*verilator fsm_state*/;
always_ff @(posedge clk) begin
if (state == 31'd0) state <= 31'd1;
else if (state == 31'd1) state <= 31'd0;
end
endmodule
module fsm_reset_commit_mismatch_bad (
input logic clk
);
@ -852,6 +866,7 @@ module t (
fsm_normalized_if_follow_wronglhs_bad normalized_if_follow_wronglhs_bad_u (.clk(clk));
fsm_case_next_wrongrhs_bad case_next_wrongrhs_bad_u (.clk(clk));
fsm_forced_wide_bad forced_wide_bad_u (.clk(clk));
fsm_forced_if_wide_bad forced_if_wide_bad_u (.clk(clk));
fsm_reset_commit_mismatch_bad reset_commit_mismatch_bad_u (.clk(clk));
fsm_reset_then_bad reset_then_bad_u (.clk(clk));

20
test_regress/t/t_fsmmulti_combo_multi_warn_bad.out
View File

@ -12,4 +12,24 @@
t/t_fsmmulti_combo_multi_warn_bad.v:65:19: ... Location of first supported candidate for 't.split_u.state_q'
65 | S0: state_d = S1;
| ^
%Warning-FSMMULTI: t/t_fsmmulti_combo_multi_warn_bad.v:107:5: FSM coverage: multiple supported transition candidates found in the same combinational always block. Only the first candidate will be instrumented.
107 | if (state_b_q == B0) state_b_d = B1;
| ^~
t/t_fsmmulti_combo_multi_warn_bad.v:105:5: ... Location of first supported candidate for 't.same_if_u.state_a_q'
105 | if (state_a_q == A0) state_a_d = A1;
| ^~
%Warning-FSMMULTI: t/t_fsmmulti_combo_multi_warn_bad.v:140:5: FSM coverage: multiple supported transition candidates found for the same FSM in combinational always blocks. Only the first candidate will be instrumented.
140 | if (state_q == S0) state_d = S1;
| ^~
t/t_fsmmulti_combo_multi_warn_bad.v:134:5: ... Location of first supported candidate for 't.split_if_u.state_q'
134 | if (state_q == S0) state_d = S1;
| ^~
%Warning-COVERIGN: t/t_fsmmulti_combo_multi_warn_bad.v:165:5: Ignoring unsupported: FSM coverage on multiple supported if-chain statements found in the same combinational always block. Only the first candidate will be instrumented.
165 | if (state_q == S1) state_d = S0;
| ^~
t/t_fsmmulti_combo_multi_warn_bad.v:163:5: ... Location of first supported candidate for 't.same_same_if_u.state_q'
163 | if (state_q == S0) state_d = S1;
| ^~
... For warning description see https://verilator.org/warn/COVERIGN?v=latest
... Use "/* verilator lint_off COVERIGN */" and lint_on around source to disable this message.
%Error: Exiting due to

93
test_regress/t/t_fsmmulti_combo_multi_warn_bad.v
View File

@ -81,9 +81,102 @@ module split_always_warn (
/* verilator lint_on MULTIDRIVEN */
endmodule
module same_always_if_warn (
input logic clk
);
typedef enum logic [1:0] {
A0,
A1
} a_state_t;
typedef enum logic [1:0] {
B0,
B1
} b_state_t;
a_state_t state_a_q;
a_state_t state_a_d;
b_state_t state_b_q;
b_state_t state_b_d;
always_comb begin
state_a_d = state_a_q;
state_b_d = state_b_q;
if (state_a_q == A0) state_a_d = A1;
else if (state_a_q == A1) state_a_d = A0;
if (state_b_q == B0) state_b_d = B1;
else if (state_b_q == B1) state_b_d = B0;
end
always_ff @(posedge clk) begin
state_a_q <= state_a_d;
end
always_ff @(posedge clk) begin
state_b_q <= state_b_d;
end
endmodule
module split_always_if_warn (
input logic clk
);
/* verilator lint_off MULTIDRIVEN */
typedef enum logic [1:0] {
S0,
S1
} state_t;
state_t state_q;
state_t state_d;
always_comb begin
state_d = state_q;
if (state_q == S0) state_d = S1;
else if (state_q == S1) state_d = S0;
end
always_comb begin
state_d = state_q;
if (state_q == S0) state_d = S1;
else if (state_q == S1) state_d = S0;
end
always_ff @(posedge clk) begin
state_q <= state_d;
end
/* verilator lint_on MULTIDRIVEN */
endmodule
module same_always_same_if_warn (
input logic clk
);
typedef enum logic [1:0] {
S0,
S1
} state_t;
state_t state_q;
state_t state_d;
always_comb begin
state_d = state_q;
if (state_q == S0) state_d = S1;
else if (state_q == S1) state_d = S0;
if (state_q == S1) state_d = S0;
else if (state_q == S0) state_d = S1;
end
always_ff @(posedge clk) begin
state_q <= state_d;
end
endmodule
module t (
input logic clk
);
same_always_warn same_u (.clk(clk));
split_always_warn split_u (.clk(clk));
same_always_if_warn same_if_u (.clk(clk));
split_always_if_warn split_if_u (.clk(clk));
same_always_same_if_warn same_same_if_u (.clk(clk));
endmodule

14
test_regress/t/t_fsmmulti_same_bad.out
View File

@ -1,9 +1,15 @@
%Warning-COVERIGN: t/t_fsmmulti_same_bad.v:33:5: Ignoring unsupported: FSM coverage on multiple supported case statements found in the same always block. Only the first candidate will be instrumented.
33 | case (state)
%Warning-COVERIGN: t/t_fsmmulti_same_bad.v:34:5: Ignoring unsupported: FSM coverage on multiple supported case statements found in the same always block. Only the first candidate will be instrumented.
34 | case (state)
| ^~~~
t/t_fsmmulti_same_bad.v:28:7: ... Location of first supported candidate for 't.state'
28 | case (state)
t/t_fsmmulti_same_bad.v:29:7: ... Location of first supported candidate for 't.state'
29 | case (state)
| ^~~~
... For warning description see https://verilator.org/warn/COVERIGN?v=latest
... Use "/* verilator lint_off COVERIGN */" and lint_on around source to disable this message.
%Warning-COVERIGN: t/t_fsmmulti_same_bad.v:44:5: Ignoring unsupported: FSM coverage on multiple supported transition candidates found in the same always block. Only the first candidate will be instrumented.
44 | if (state_if == S1) state_if <= S2;
| ^~
t/t_fsmmulti_same_bad.v:41:5: ... Location of first supported candidate for 't.state_if'
41 | if (state_if == S0) state_if <= S1;
| ^~
%Error: Exiting due to

9
test_regress/t/t_fsmmulti_same_bad.v
View File

@ -16,6 +16,7 @@ module t (
} state_t;
state_t state;
state_t state_if;
// This is intentionally non-idiomatic RTL. The detector sees one supported
// candidate in the reset-if else branch and a second supported top-level
@ -36,4 +37,12 @@ module t (
endcase
end
always_ff @(posedge clk) begin
if (state_if == S0) state_if <= S1;
else if (state_if == S1) state_if <= S0;
if (state_if == S1) state_if <= S2;
else if (state_if == S2) state_if <= S1;
end
endmodule

14
test_regress/t/t_fsmmulti_warn_bad.out
View File

@ -1,9 +1,15 @@
%Warning-FSMMULTI: t/t_fsmmulti_warn_bad.v:29:5: FSM coverage: multiple enum-typed case statements found in the same always block. Only the first candidate will be instrumented.
29 | case (state_b)
%Warning-FSMMULTI: t/t_fsmmulti_warn_bad.v:41:5: FSM coverage: multiple enum-typed case statements found in the same always block. Only the first candidate will be instrumented.
41 | case (state_b)
| ^~~~
t/t_fsmmulti_warn_bad.v:25:5: ... Location of first supported candidate for 't.state_a'
25 | case (state_a)
t/t_fsmmulti_warn_bad.v:37:5: ... Location of first supported candidate for 't.state_a'
37 | case (state_a)
| ^~~~
... For warning description see https://verilator.org/warn/FSMMULTI?v=latest
... Use "/* verilator lint_off FSMMULTI */" and lint_on around source to disable this message.
%Warning-FSMMULTI: t/t_fsmmulti_warn_bad.v:51:5: FSM coverage: multiple enum-typed transition candidates found in the same always block. Only the first candidate will be instrumented.
51 | if (state_d == D0) state_d <= D1;
| ^~
t/t_fsmmulti_warn_bad.v:48:5: ... Location of first supported candidate for 't.state_c'
48 | if (state_c == C0) state_c <= C1;
| ^~
%Error: Exiting due to

20
test_regress/t/t_fsmmulti_warn_bad.v
View File

@ -18,8 +18,20 @@ module t (
B1
} b_state_t;
typedef enum logic [1:0] {
C0,
C1
} c_state_t;
typedef enum logic [1:0] {
D0,
D1
} d_state_t;
a_state_t state_a;
b_state_t state_b;
c_state_t state_c;
d_state_t state_d;
always_ff @(posedge clk) begin
case (state_a)
@ -32,4 +44,12 @@ module t (
endcase
end
always_ff @(posedge clk) begin
if (state_c == C0) state_c <= C1;
else if (state_c == C1) state_c <= C0;
if (state_d == D0) state_d <= D1;
else if (state_d == D1) state_d <= D0;
end
endmodule