Unexpected behavior in Stmt sequence when using par

[arjenroodselaar]

I am using the StmtFSM package to implement a protocol handler. A minimized example would be as follows:

import StmtFSM::*;

module mkParBehavior (Empty);
    Reg#(Bit#(3)) control <- mkReg(0);
    PulseWire ready <- mkPulseWire();

    mkAutoFSM(seq
        control <= 1;
        par
            control <= 2;
            await(ready);
        endpar
        control <= 0;
    endseq);
endmodule

What I expect to happen here is that the FSM sets control to 1 in the first action, then executes the par block where it sets control to 2 and waits for the ready flag to be set, before it continues to the final action where it sets control back to 0. When compiling this however I get the following warnings:

Warning: "../hdl/ParBehavior.bsv", line 3, column 8: (G0036)
  Rule "action_l8c17" will appear to fire before "action_l10c21" when both
  fire in the same clock cycle, affecting:
    calls to control.write vs. control.write
Warning: "../hdl/ParBehavior.bsv", line 3, column 8: (G0036)
  Rule "action_l13c17" will appear to fire before "action_l10c21" when both
  fire in the same clock cycle, affecting:
    calls to control.write vs. control.write
Warning: "../hdl/ParBehavior.bsv", line 3, column 8: (G0117)
  Rule `action_l10c21' shadows the effects of `action_l8c17' when they execute
  in the same clock cycle. Affected method calls:
    control.write
  To silence this warning, use the `-no-warn-action-shadowing' flag.
Warning: "../hdl/ParBehavior.bsv", line 3, column 8: (G0117)
  Rule `action_l10c21' shadows the effects of `action_l13c17' when they
  execute in the same clock cycle. Affected method calls:
    control.write
  To silence this warning, use the `-no-warn-action-shadowing' flag.

Removing the par statements, changing the sequence to

    mkAutoFSM(seq
      control <= 1;
      // par
          control <= 2;
          // await(ready);
      // endpar
      control <= 0;
  endseq);

results in expected behavior where bsc appropriately determines the rules are mutually exclusive.

Is my understanding of par incorrect? I tried wrapping the three phases in seq endseq blocks to try and force the schedule/sequence, but any time I introduce a par it looks like bsc schedules all rules in the sequence in parallel, resulting in conflicts.

The example above was tested to reproduce on the just released version 2024.01.

[rsnikhil]

Your understanding of par is probably fine.

I think these warnings are an artefact of how the bsc compiler translates StmtFSM into rules and introduces state registers to sequence actions in the FSM, after which it cannot reconstruct some properties that were clear in the original StmtFSM.

The attached code shows a "hand-translation" of the above StmtFSM into rules, using a particular choice of state variables to control the seq/par sequencing. When you compile it, it produces similar compiler warnings, the first of which is:

Warning: "src_BSV/Top.bsv", line 29, column 8: (G0010)
  Rule "rl_seq_1" was treated as more urgent than
  "rl_seq_2_endpar". Conflicts:
    "rl_seq_1" cannot fire before "rl_seq_2_endpar":
      calls to
        rg_state_par_A.write vs. rg_state_par_A.read
        rg_state_par_B.write vs. rg_state_par_B.read
    "rl_seq_2_endpar" cannot fire before "rl_seq_1":
      calls to rg_state_seq.write vs. rg_state_seq.read

This warning is unnecessary if we recognize either of the following properties, which make the rules mutually exclusive. Both properties are clear from the original StmtFSM structure, but perhaps not so obvious from the rules:

(rg_state_par_A == 2)    implies    (rg_state_seq == 2)
(rg_state_par_B == 2)    implies    (rg_state_seq == 2)

Foo.tar.gz

[quark17]

It's quite possible that the StmtFSM behavior (much of which is implemented in a the library StmtFSM.bs) could be improved to generate code that doesn't have this warning. Feel free to explore the implementation and submit PRs with improvements.

For example, in hand-written code, it's possible to silence the warning by telling BSC that you know two rules will never be enabled at the same time, using rJoinMutuallyExclusive. Another option could be to write the conditions of the rules so they explicitly expose the mutual exclusivity.