Consider the following Verilog code fragment, and a corresponding (incorrect) Bluespec model.
reg [31:0] burst_count, dest_burst_size ;
Incorrect Bluespec model:
At first inspection the Bluespec code may look equivalent, but the scheduler sees the cross correlation between the rules. That is, Rule burst_counting reads burst_in_progress and updates register burst_count. Rule burst_in_progress reads burst_count and sets burst_in_progress.
For the scheduler to allow the rules to happen in parallel, they must be able to occur in any order and still give the same result. If Rule burst_counting happens first, then register burst_count can be updated such that rule burst_counting become disabled; a similar argument happens in the other directions.
A corrected model is below, which combines the two rules into one rule which only occurs when burst_in_progress is True. Note that the two actions in the rule can be listed in either order, since all actions in one rule occur concurrently.