FSM encoding, safety and state coverage

hdl/wash_ctrl.sv

// A washing-machine controller. Start checks the door: open is a fault, closed starts the cycle of fill, wash,
// drain, rinse and spin, which ends waiting for the door to open. Timers and sensors outside it say when the drum is
// full or empty and when a wash, a rinse or a spin is done. Every state makes one two-way choice, written as an if
// with an else, and the state register has a block of its own with an active-high reset, the forms that the FSM
// coverage of the simulator reads. The names take the codes 0 to 8 in order; with -DGRAY each step of the cycle
// changes one bit; with -DKEEP_CODES synthesis keeps the codes as written.
module wash_ctrl (
  input  logic clk_i,
  input  logic rst_i,          // active high
  input  logic start_i,
  input  logic door_closed_i,
  input  logic full_i,
  input  logic empty_i,
  input  logic done_i,         // this wash, rinse or spin has run long enough
  input  logic clear_i,        // the fault has been seen
  output logic lock_o,         // the door is locked
  output logic valve_o,
  output logic motor_o,
  output logic pump_o,
  output logic fault_o
);
`ifdef GRAY
  typedef enum logic [3:0] {IDLE = 4'b0000, CHECK = 4'b0001, FILL = 4'b0011, WASH = 4'b0010, DRAIN = 4'b0110,
                            RINSE = 4'b0111, SPIN = 4'b0101, DONE = 4'b0100, FAULT = 4'b1000} state_t;
`else
  typedef enum logic [3:0] {IDLE, CHECK, FILL, WASH, DRAIN, RINSE, SPIN, DONE, FAULT} state_t;
`endif

`ifdef KEEP_CODES
  (* fsm_encoding = "none" *)
`endif
  state_t state_q /*verilator fsm_arc_include_cond*/;
  state_t state_d;

  always_comb begin
    state_d = state_q;
    unique case (state_q)
      IDLE:  if (start_i)       state_d = CHECK; else state_d = IDLE;
      CHECK: if (door_closed_i) state_d = FILL;  else state_d = FAULT;
      FILL:  if (full_i)        state_d = WASH;  else state_d = FILL;
      WASH:  if (done_i)        state_d = DRAIN; else state_d = WASH;
      DRAIN: if (empty_i)       state_d = RINSE; else state_d = DRAIN;
      RINSE: if (done_i)        state_d = SPIN;  else state_d = RINSE;
      SPIN:  if (done_i)        state_d = DONE;  else state_d = SPIN;
      DONE:  if (door_closed_i) state_d = DONE;  else state_d = IDLE;
      FAULT: if (clear_i)       state_d = IDLE;  else state_d = FAULT;
      default:                  state_d = IDLE;    // a code that names no state
    endcase
  end

  always_ff @(posedge clk_i or posedge rst_i)
    if (rst_i) state_q <= IDLE;
    else       state_q <= state_d;

`ifndef SYNTHESIS
  // The state diagram as assertions, which synthesis leaves out: the register holds only codes that name a state,
  // and each state either stays or moves to the state its choice names.
  a_known: assert property (@(posedge clk_i) disable iff (rst_i)
                            state_q inside {IDLE, CHECK, FILL, WASH, DRAIN, RINSE, SPIN, DONE, FAULT})
           else $error("state code %0d names no state", state_q);
  a_idle:  assert property (@(posedge clk_i) disable iff (rst_i) state_q == IDLE  |=> state_q inside {IDLE, CHECK});
  a_check: assert property (@(posedge clk_i) disable iff (rst_i) state_q == CHECK |=> state_q inside {FILL, FAULT});
  a_fill:  assert property (@(posedge clk_i) disable iff (rst_i) state_q == FILL  |=> state_q inside {FILL, WASH});
  a_wash:  assert property (@(posedge clk_i) disable iff (rst_i) state_q == WASH  |=> state_q inside {WASH, DRAIN});
  a_drain: assert property (@(posedge clk_i) disable iff (rst_i) state_q == DRAIN |=> state_q inside {DRAIN, RINSE});
  a_rinse: assert property (@(posedge clk_i) disable iff (rst_i) state_q == RINSE |=> state_q inside {RINSE, SPIN});
  a_spin:  assert property (@(posedge clk_i) disable iff (rst_i) state_q == SPIN  |=> state_q inside {SPIN, DONE});
  a_done:  assert property (@(posedge clk_i) disable iff (rst_i) state_q == DONE  |=> state_q inside {DONE, IDLE});
  a_fault: assert property (@(posedge clk_i) disable iff (rst_i) state_q == FAULT |=> state_q inside {FAULT, IDLE});
`endif

  assign lock_o  = (state_q == CHECK) || (state_q == FILL) || (state_q == WASH) || (state_q == DRAIN) ||
                   (state_q == RINSE) || (state_q == SPIN);
  assign valve_o = (state_q == FILL) || (state_q == RINSE);
  assign motor_o = (state_q == WASH) || (state_q == RINSE) || (state_q == SPIN);
  assign pump_o  = (state_q == DRAIN) || (state_q == SPIN);
  assign fault_o = (state_q == FAULT);
endmodule

Commands · hdl/encodings_session.py

from session import run

# What Yosys makes of the washer's states, and how many transitions the table it extracted holds; then the washer
# synthesised for an iCE40 UP5K three ways and placed and routed with seed 1. grep keeps the flip-flops and look-up
# tables of each, and the last clock report of each run.
run("""
yosys -q -p "read_verilog -sv wash_ctrl.sv; proc; opt -nodffe -nosdff; tee -q -o fsm.txt fsm -nomap"
grep -E "Found FSM|encoding to|state bits" fsm.txt
grep -c "transition:" fsm.txt
yosys -q -p "read_verilog -sv -DKEEP_CODES wash_ctrl.sv; synth_ice40 -top wash_ctrl -json binary.json; tee -q -o binary.txt stat"
yosys -q -p "read_verilog -sv -DKEEP_CODES -DGRAY wash_ctrl.sv; synth_ice40 -top wash_ctrl -json gray.json; tee -q -o gray.txt stat"
yosys -q -p "read_verilog -sv wash_ctrl.sv; synth_ice40 -top wash_ctrl -json onehot.json; tee -q -o onehot.txt stat"
grep -H -E "SB_(DFF|LUT4)" binary.txt gray.txt onehot.txt
nextpnr-ice40 --up5k --package sg48 --seed 1 --json binary.json 2>&1 | grep "Max frequency" | tail -n 1
nextpnr-ice40 --up5k --package sg48 --seed 1 --json gray.json 2>&1 | grep "Max frequency" | tail -n 1
nextpnr-ice40 --up5k --package sg48 --seed 1 --json onehot.json 2>&1 | grep "Max frequency" | tail -n 1
""")

# Yosys 0.69 · nextpnr-ice40 0.11.1
$ yosys -q -p "read_verilog -sv wash_ctrl.sv; proc; opt -nodffe -nosdff; tee -q -o fsm.txt fsm -nomap"
$ grep -E "Found FSM|encoding to|state bits" fsm.txt
Found FSM state register wash_ctrl.state_q.
  mapping auto encoding to `one-hot` for this FSM.
  Number of state bits:       9
$ grep -c "transition:" fsm.txt
18
$ yosys -q -p "read_verilog -sv -DKEEP_CODES wash_ctrl.sv; synth_ice40 -top wash_ctrl -json binary.json; tee -q -o binary.txt stat"
$ yosys -q -p "read_verilog -sv -DKEEP_CODES -DGRAY wash_ctrl.sv; synth_ice40 -top wash_ctrl -json gray.json; tee -q -o gray.txt stat"
$ yosys -q -p "read_verilog -sv wash_ctrl.sv; synth_ice40 -top wash_ctrl -json onehot.json; tee -q -o onehot.txt stat"
$ grep -H -E "SB_(DFF|LUT4)" binary.txt gray.txt onehot.txt
binary.txt:        4   SB_DFFR
binary.txt:       25   SB_LUT4
gray.txt:        4   SB_DFFR
gray.txt:       21   SB_LUT4
onehot.txt:        8   SB_DFFR
onehot.txt:        1   SB_DFFS
onehot.txt:       14   SB_LUT4
$ nextpnr-ice40 --up5k --package sg48 --seed 1 --json binary.json 2>&1 | grep "Max frequency" | tail -n 1
Info: Max frequency for clock 'clk_i$SB_IO_IN_$glb_clk': 96.68 MHz (PASS at 12.00 MHz)
$ nextpnr-ice40 --up5k --package sg48 --seed 1 --json gray.json 2>&1 | grep "Max frequency" | tail -n 1
Info: Max frequency for clock 'clk_i$SB_IO_IN_$glb_clk': 100.14 MHz (PASS at 12.00 MHz)
$ nextpnr-ice40 --up5k --package sg48 --seed 1 --json onehot.json 2>&1 | grep "Max frequency" | tail -n 1
Info: Max frequency for clock 'clk_i$SB_IO_IN_$glb_clk': 144.07 MHz (PASS at 12.00 MHz)

hdl/tb_upset.sv

// One upset, three builds of wash_ctrl.sv side by side: the RTL; wash_kept, the netlist synthesised with its codes
// kept (fsm_encoding "none"); and wash_hot, the netlist synthesised with the defaults, in which Yosys re-encoded the
// states as one-hot. During the wash one flip-flop of each state register flips: bit 3 of the binary code 0011, which
// makes code 11, and the one set bit of the one-hot code, which leaves none set. Then the door opens and start is
// pressed, to see which builds still answer.
module tb_upset;
  logic clk = 1'b0, rst = 1'b1, start = 1'b0, door_closed = 1'b1, full = 1'b1, empty = 1'b0, done = 1'b0,
        clear = 1'b0;
  logic [4:0] o_rtl, o_kept, o_hot;            // lock, valve, motor, pump, fault of each build

  wash_ctrl u_rtl  (.clk_i(clk), .rst_i(rst), .start_i(start), .door_closed_i(door_closed), .full_i(full),
                    .empty_i(empty), .done_i(done), .clear_i(clear), .lock_o(o_rtl[4]), .valve_o(o_rtl[3]),
                    .motor_o(o_rtl[2]), .pump_o(o_rtl[1]), .fault_o(o_rtl[0]));
  wash_kept u_kept (.clk_i(clk), .rst_i(rst), .start_i(start), .door_closed_i(door_closed), .full_i(full),
                    .empty_i(empty), .done_i(done), .clear_i(clear), .lock_o(o_kept[4]), .valve_o(o_kept[3]),
                    .motor_o(o_kept[2]), .pump_o(o_kept[1]), .fault_o(o_kept[0]));
  wash_hot  u_hot  (.clk_i(clk), .rst_i(rst), .start_i(start), .door_closed_i(door_closed), .full_i(full),
                    .empty_i(empty), .done_i(done), .clear_i(clear), .lock_o(o_hot[4]), .valve_o(o_hot[3]),
                    .motor_o(o_hot[2]), .pump_o(o_hot[1]), .fault_o(o_hot[0]));

  always #5 clk = ~clk;

  task automatic show(input string what);
    $display("RTL %b code %2d | kept %b code %2d | one-hot %b code %b | %s", o_rtl, u_rtl.state_q,
             o_kept, u_kept.state_q, o_hot, u_hot.state_q, what);
  endtask

  initial begin
    logic [3:0] rtl_code, kept_code;
    $display("outputs: lock, valve, motor, pump, fault");
    @(negedge clk) rst = 1'b0;
    @(negedge clk) start = 1'b1;
    @(negedge clk) start = 1'b0;               // CHECK, then FILL, which is full at once, then WASH
    repeat (3) @(negedge clk);
    show("washing");
    rtl_code  = u_rtl.state_q ^ 4'b1000;      // the codes with bit 3 flipped
    kept_code = u_kept.state_q ^ 4'b1000;
    force u_rtl.state_q  = type(u_rtl.state_q)'(rtl_code);
    force u_kept.state_q = kept_code;
    force u_hot.state_q  = '0;
    #1;
    release u_rtl.state_q;
    release u_kept.state_q;
    release u_hot.state_q;
    show("the upset");
    repeat (2) begin
      @(negedge clk);
      show("one edge on");
    end
    door_closed = 1'b0;
    @(negedge clk);
    door_closed = 1'b1;
    start = 1'b1;
    @(negedge clk) start = 1'b0;
    @(negedge clk);
    show("start again");
    $finish;
  end
endmodule

Commands · hdl/safety_session.py

from session import run

# Two netlists of the washer, one with its codes kept and one re-encoded by Yosys, beside the RTL, with one upset in
# each. The testbench's force and release write the state registers, so Verilator's MULTIDRIVEN warning is off, and
# the error limit lets the run go on past the assertions of the RTL.
run("""
yosys -q -p "read_verilog -sv -DKEEP_CODES wash_ctrl.sv; synth -top wash_ctrl; rename wash_ctrl wash_kept; write_verilog -noattr wash_kept.v"
yosys -q -p "read_verilog -sv wash_ctrl.sv; synth -top wash_ctrl; rename wash_ctrl wash_hot; write_verilog -noattr wash_hot.v"
verilator --binary -j 0 --quiet -Wno-MULTIDRIVEN --top-module tb_upset tb_upset.sv wash_ctrl.sv wash_kept.v wash_hot.v
obj_dir/Vtb_upset +verilator+quiet +verilator+error+limit+10
""")

# Yosys 0.69 · Verilator 5.052
$ yosys -q -p "read_verilog -sv -DKEEP_CODES wash_ctrl.sv; synth -top wash_ctrl; rename wash_ctrl wash_kept; write_verilog -noattr wash_kept.v"
$ yosys -q -p "read_verilog -sv wash_ctrl.sv; synth -top wash_ctrl; rename wash_ctrl wash_hot; write_verilog -noattr wash_hot.v"
$ verilator --binary -j 0 --quiet -Wno-MULTIDRIVEN --top-module tb_upset tb_upset.sv wash_ctrl.sv wash_kept.v wash_hot.v
$ obj_dir/Vtb_upset +verilator+quiet +verilator+error+limit+10
outputs: lock, valve, motor, pump, fault
RTL 10100 code  3 | kept 10100 code  3 | one-hot 10100 code 010000000 | washing
RTL 00000 code 11 | kept 00000 code 11 | one-hot 00000 code 000000000 | the upset
[65] %Error: wash_ctrl.sv:60: Assertion failed in tb_upset.u_rtl.a_known: state code 11 names no state
-Info: wash_ctrl.sv:60: Verilog $stop, ignored due to +verilator+error+limit
[65] %Error: wash_ctrl.sv:64: Assertion failed in tb_upset.u_rtl.a_wash: 'assert' failed.
RTL 00000 code  0 | kept 00000 code  0 | one-hot 00000 code 000000000 | one edge on
RTL 00000 code  0 | kept 00000 code  0 | one-hot 00000 code 000000000 | one edge on
RTL 11000 code  2 | kept 11000 code  2 | one-hot 00000 code 000000000 | start again
- tb_upset.sv:57: Verilog $finish

hdl/door_lock.sv

// A keypad door lock. The four digits of Code unlock it for OpenTicks cycles. A wrong code is still read to its
// fourth digit, so the keypad never shows which digit was wrong, and the third wrong code in a row locks the keypad
// for LockTicks cycles. Two-process style: the next state and the Mealy output in always_comb, the registers in
// always_ff, then the output logic.
module door_lock #(
  parameter logic [15:0] Code              = 16'h5913,  // one digit per four bits, the first digit on top
  parameter logic [3:0]  OpenTicks         = 4'd3,
  parameter logic [3:0]  LockTicks         = 4'd8,
  parameter bit          RegisteredOutputs = 1'b0       // 1: every output from a flip-flop
) (
  input  logic       clk_i,
  input  logic       rst_ni,
  input  logic       key_valid_i,  // a key press, for one cycle
  input  logic [3:0] key_i,        // its digit, 0 to 9
  output logic       accept_o,     // Mealy: the key of this cycle is taken
  output logic       unlock_o,     // Moore: the door is unlocked
  output logic       lockout_o     // Moore: keys are ignored for now
);
  typedef enum logic [3:0] {IDLE, OK1, OK2, OK3, BAD1, BAD2, BAD3, OPEN, LOCKOUT} state_t;

  state_t     state_q, state_d;
  logic [1:0] fails_q, fails_d;    // wrong codes in a row
  logic [3:0] timer_q, timer_d;    // cycles left in OPEN or LOCKOUT
  logic       accept_d;            // the key of this cycle is taken
  logic       wrong;               // the fourth digit of a wrong code is being taken

  // Next-state logic: start from "stay", then let the present state's branch decide.
  always_comb begin
    state_d  = state_q;
    fails_d  = fails_q;
    timer_d  = timer_q;
    accept_d = 1'b0;
    wrong    = 1'b0;
    unique case (state_q)
      IDLE: if (key_valid_i) begin
        accept_d = 1'b1;
        if (key_i == Code[15:12]) state_d = OK1;
        else                      state_d = BAD1;
      end
      OK1: if (key_valid_i) begin
        accept_d = 1'b1;
        if (key_i == Code[11:8]) state_d = OK2;
        else                     state_d = BAD2;
      end
      OK2: if (key_valid_i) begin
        accept_d = 1'b1;
        if (key_i == Code[7:4]) state_d = OK3;
        else                    state_d = BAD3;
      end
      OK3: if (key_valid_i) begin
        accept_d = 1'b1;
        if (key_i == Code[3:0]) begin
          state_d = OPEN;
          fails_d = '0;
          timer_d = OpenTicks - 4'd1;
        end else begin
          wrong = 1'b1;
        end
      end
      BAD1: if (key_valid_i) begin
        accept_d = 1'b1;
        state_d  = BAD2;
      end
      BAD2: if (key_valid_i) begin
        accept_d = 1'b1;
        state_d  = BAD3;
      end
      BAD3: if (key_valid_i) begin
        accept_d = 1'b1;
        wrong    = 1'b1;
      end
      OPEN, LOCKOUT: begin         // keys are ignored until the timer runs out
        if (timer_q == '0) state_d = IDLE;
        else               timer_d = timer_q - 4'd1;
      end
`ifndef NO_RECOVERY
      default: state_d = IDLE;     // codes 9 to 15 name no state: back to IDLE
`endif
    endcase
    if (wrong) begin
      if (fails_q == 2'd2) begin   // the third wrong code in a row
        state_d = LOCKOUT;
        fails_d = '0;
        timer_d = LockTicks - 4'd1;
      end else begin
        state_d = IDLE;
        fails_d = fails_q + 2'd1;
      end
    end
  end

  // The registers: reset values, then the values the next-state logic chose.
  always_ff @(posedge clk_i or negedge rst_ni) begin
    if (!rst_ni) begin
      state_q <= IDLE;
      fails_q <= '0;
      timer_q <= '0;
    end else begin
      state_q <= state_d;
      fails_q <= fails_d;
      timer_q <= timer_d;
    end
  end

  // Output logic: the Moore outputs decoded from the state and the Mealy output passed on, or, with
  // RegisteredOutputs, all three loaded into flip-flops from the next-state logic's values.
  if (!RegisteredOutputs) begin : g_decoded
    assign unlock_o  = (state_q == OPEN);
    assign lockout_o = (state_q == LOCKOUT);
    assign accept_o  = accept_d;
  end else begin : g_registered
    logic unlock_q, lockout_q, accept_q;
    always_ff @(posedge clk_i or negedge rst_ni) begin
      if (!rst_ni) begin
        unlock_q  <= 1'b0;
        lockout_q <= 1'b0;
        accept_q  <= 1'b0;
      end else begin
        unlock_q  <= (state_d == OPEN);     // from the next state: no cycle lost
        lockout_q <= (state_d == LOCKOUT);
        accept_q  <= accept_d;              // a Mealy output: one cycle later
      end
    end
    assign unlock_o  = unlock_q;
    assign lockout_o = lockout_q;
    assign accept_o  = accept_q;
  end
endmodule

Commands · hdl/lock_coverage_session.py

from session import run

# Every kind of coverage on the lock of the first lesson of this module, keyed with its right code.
run("""
verilator --binary -j 0 --quiet --coverage --top-module tb_moore_mealy tb_moore_mealy.sv door_lock.sv
obj_dir/Vtb_moore_mealy +verilator+quiet +verilator+coverage+file+lock.dat > lock.log
verilator_coverage lock.dat
""")

# Verilator 5.052
$ verilator --binary -j 0 --quiet --coverage --top-module tb_moore_mealy tb_moore_mealy.sv door_lock.sv
$ obj_dir/Vtb_moore_mealy +verilator+quiet +verilator+coverage+file+lock.dat > lock.log
$ verilator_coverage lock.dat
Coverage Summary:
  line      : 80.0% (16/20)
  toggle    : 71.4% (60/84)
  branch    : 75.0% (24/32)
  expr      : 100.0% ( 4/ 4)
  fsm_state : 0.0% ( 0/ 0)
  fsm_arc   : 0.0% ( 0/ 0)

hdl/tb_wash.sv

// Directed tests of wash_ctrl.sv, picked with +test=: "cycle" runs one whole wash with the door closed and opens the
// door two cycles after the end; "fault" presses start with the door open, then clears the fault; "powerup" runs with
// no reset at all, so the state register keeps whatever it powered up with (random under Verilator's
// +verilator+rand+reset+2), and shows it at the start and one edge later. The testbench models what the controller
// drives: the drum fills by one level a cycle while the valve is open and empties while the pump runs, and a timer
// that restarts whenever the outputs change gives done_i after 4 cycles of the motor.
module tb_wash;
  logic       clk = 1'b0, rst, start = 1'b0, door_closed = 1'b1, clear = 1'b0;
  logic       lock, valve, motor, pump, fault, full, empty, done;
  logic [2:0] outs, outs_q = '0;
  int         level = 0, run_for = 0;

  wash_ctrl u_wash (.clk_i(clk), .rst_i(rst), .start_i(start), .door_closed_i(door_closed), .full_i(full),
                    .empty_i(empty), .done_i(done), .clear_i(clear), .lock_o(lock), .valve_o(valve),
                    .motor_o(motor), .pump_o(pump), .fault_o(fault));

  always #5 clk = ~clk;
  assign full  = (level == 4);
  assign empty = (level == 0);
  assign outs  = {valve, motor, pump};
  assign done  = motor && outs == outs_q && run_for >= 3;
  always @(posedge clk) begin
    if (valve && level < 4) level <= level + 1;
    if (pump && level > 0) level <= level - 1;
    run_for <= (outs == outs_q) ? run_for + 1 : 1;
    outs_q  <= outs;
  end

  task automatic press_start();
    @(negedge clk) start = 1'b1;
    @(negedge clk) start = 1'b0;
  endtask

  task automatic press_clear();
    @(negedge clk) clear = 1'b1;
    @(negedge clk) clear = 1'b0;
  endtask

  initial begin
    string test;
    if (!$value$plusargs("test=%s", test)) test = "cycle";
    rst = (test != "powerup");
    if (test == "powerup") begin               // no reset: the register keeps what it powered up with
      $display("powerup: the state register starts at code %0d", u_wash.state_q);
      @(negedge clk);
      $display("powerup: one edge later, code %0d", u_wash.state_q);
      $finish;
    end
    @(negedge clk) rst = 1'b0;
    if (test == "cycle") begin
      press_start();
      wait (lock);
      wait (!lock);                            // the cycle is over: DONE unlocks the door
      repeat (2) @(negedge clk);
      door_closed = 1'b0;
      @(negedge clk);
      $display("cycle: washed, then the door opened; locked %b", lock);
    end else if (test == "fault") begin
      door_closed = 1'b0;
      press_start();
      @(negedge clk);
      $display("fault: started with the door open, fault %b", fault);
      press_clear();
      $display("fault: cleared, fault %b", fault);
    end
    $finish;
  end
endmodule

Commands · hdl/coverage_session.py

from session import run

# FSM coverage of the washer on Verilator: its three tests, merged one by one. The annotation lists the arcs, with how
# often the first test took each.
run("""
verilator --binary -j 0 --quiet --coverage-fsm --top-module tb_wash tb_wash.sv wash_ctrl.sv
obj_dir/Vtb_wash +verilator+quiet +test=cycle +verilator+coverage+file+cycle.dat
verilator_coverage cycle.dat
verilator_coverage --annotate ann cycle.dat > ann.log
grep -E "fsm_arc|DEFAULT" ann/wash_ctrl.sv | grep -v -E "reset|include_cond"
obj_dir/Vtb_wash +verilator+quiet +test=fault +verilator+coverage+file+fault.dat
verilator_coverage cycle.dat fault.dat
obj_dir/Vtb_wash +verilator+quiet +test=powerup +verilator+rand+reset+2 +verilator+seed+1 +verilator+error+limit+10 +verilator+coverage+file+powerup.dat
verilator_coverage cycle.dat fault.dat powerup.dat
""")

# Verilator 5.052
$ verilator --binary -j 0 --quiet --coverage-fsm --top-module tb_wash tb_wash.sv wash_ctrl.sv
$ obj_dir/Vtb_wash +verilator+quiet +test=cycle +verilator+coverage+file+cycle.dat
cycle: washed, then the door opened; locked 0
- tb_wash.sv:66: Verilog $finish
$ verilator_coverage cycle.dat
Coverage Summary:
  line      : 0.0% ( 0/ 0)
  toggle    : 0.0% ( 0/ 0)
  branch    : 0.0% ( 0/ 0)
  expr      : 0.0% ( 0/ 0)
  fsm_state : 88.9% ( 8/ 9)
  fsm_arc   : 80.0% (16/20)
$ verilator_coverage --annotate ann cycle.dat > ann.log
$ grep -E "fsm_arc|DEFAULT" ann/wash_ctrl.sv | grep -v -E "reset|include_cond"
%000000        // [fsm_arc tb_wash.u_wash.state_q::CHECK->FAULT]
%000001        // [fsm_arc tb_wash.u_wash.state_q::CHECK->FILL]
%000001        // [fsm_arc tb_wash.u_wash.state_q::DONE->DONE]
%000001        // [fsm_arc tb_wash.u_wash.state_q::DONE->IDLE]
%000004        // [fsm_arc tb_wash.u_wash.state_q::DRAIN->DRAIN]
%000001        // [fsm_arc tb_wash.u_wash.state_q::DRAIN->RINSE]
%000000        // [fsm_arc tb_wash.u_wash.state_q::FAULT->FAULT]
%000000        // [fsm_arc tb_wash.u_wash.state_q::FAULT->IDLE]
%000004        // [fsm_arc tb_wash.u_wash.state_q::FILL->FILL]
%000001        // [fsm_arc tb_wash.u_wash.state_q::FILL->WASH]
%000001        // [fsm_arc tb_wash.u_wash.state_q::IDLE->CHECK]
%000003        // [fsm_arc tb_wash.u_wash.state_q::IDLE->IDLE]
%000003        // [fsm_arc tb_wash.u_wash.state_q::RINSE->RINSE]
%000001        // [fsm_arc tb_wash.u_wash.state_q::RINSE->SPIN]
%000001        // [fsm_arc tb_wash.u_wash.state_q::SPIN->DONE]
%000003        // [fsm_arc tb_wash.u_wash.state_q::SPIN->SPIN]
%000001        // [fsm_arc tb_wash.u_wash.state_q::WASH->DRAIN]
%000003        // [fsm_arc tb_wash.u_wash.state_q::WASH->WASH]
%000000        // [SYNTHETIC DEFAULT ARC: tb_wash.u_wash.state_q::default->IDLE]
$ obj_dir/Vtb_wash +verilator+quiet +test=fault +verilator+coverage+file+fault.dat
fault: started with the door open, fault 1
fault: cleared, fault 0
- tb_wash.sv:66: Verilog $finish
$ verilator_coverage cycle.dat fault.dat
Coverage Summary:
  line      : 0.0% ( 0/ 0)
  toggle    : 0.0% ( 0/ 0)
  branch    : 0.0% ( 0/ 0)
  expr      : 0.0% ( 0/ 0)
  fsm_state : 100.0% ( 9/ 9)
  fsm_arc   : 95.0% (19/20)
$ obj_dir/Vtb_wash +verilator+quiet +test=powerup +verilator+rand+reset+2 +verilator+seed+1 +verilator+error+limit+10 +verilator+coverage+file+powerup.dat
powerup: the state register starts at code 12
[5] %Error: wash_ctrl.sv:60: Assertion failed in tb_wash.u_wash.a_known: state code 12 names no state
-Info: wash_ctrl.sv:60: Verilog $stop, ignored due to +verilator+error+limit
powerup: one edge later, code 0
- tb_wash.sv:47: Verilog $finish
$ verilator_coverage cycle.dat fault.dat powerup.dat
Coverage Summary:
  line      : 0.0% ( 0/ 0)
  toggle    : 0.0% ( 0/ 0)
  branch    : 0.0% ( 0/ 0)
  expr      : 0.0% ( 0/ 0)
  fsm_state : 100.0% ( 9/ 9)
  fsm_arc   : 100.0% (20/20)