proc_dff: process sync rules in reverse input order

[widlarizer]

What are the reasons/motivation for this change?

It's assumed that sync rules are in some kind of priority ordering. See here

Explain how this is achieved.

Since there is no "insertion ordered map" in STL, I provide a minimal one of my own

If applicable, please suggest to reviewers how they can test the change.

The tests now pass including dfflibmap.ys even when our hash function is modified as in #4559 and #4524. More investigation is needed about proc_dff and into this particular test and its correctness

[whitequark]

I wonder if this should be clarified in the RTLIL guide in the manual.

[widlarizer]

I think so, I checked docs/source/yosys_internals/formats/rtlil_rep.rst and it's not described there. I'd describe it if I had sufficient faith in my mental model.

Also as @georgerennie pointed out the reverse order would be the correct one, the CI only confirms this

[georgerennie]

I discussed this with @widlarizer by dm, but I think this solution doesn't fully capture the priority for the sync rules. As the syncrules are still being aggregated by the assign expression for their condition, later syncrules automatically get the same priority as earlier syncrules that assign the same value, rather than their correct priority. I assume this is meant to be an optimization to merge together conditions leading to the same value being loaded, but some more care needs to be taken to preserve priorities.

Consider the following example

read_verilog <<EOT
module dffsr(input CLK, D, A, B, C, output reg Q);

always @(posedge CLK, posedge A, posedge B, posedge C)
	if (A)      Q <= '0;
	else if (B) Q <= '1;
	else if (C) Q <= '0;
	else        Q <= D;
endmodule
EOT

proc -noopt

opt -mux_bool
write_verilog -noattr

This produces

assign _0_ = | { C, A };
assign _1_ = _0_ ? 1'h0 : B;
always @(posedge CLK, posedge _1_, posedge _0_)
  if (_0_) Q <= 1'b0;
  else if (_1_) Q <= 1'b1;
  else Q <= D;

The 0 case has taken the trigger |{C, A}, whereas really it should be something like |{A, C && !B). This means that if the inputs A = 0, B = 1, C = 1 are applied, in the first circuit Q = 1 whereas in the processed version Q = 0

I think a possible solution is to process the sync rules one by one in the order they appear from proc_arst, guarding each condition with all the previous sync rule conditions, and taking the disjunction of conditions that lead to the same value.

With this, you would therefore get for each sync rule A -> Q <= '0, B && !A -> Q <= '1, C && !B && !A -> Q <= '0. You can then merge the conditions leading to zero, so you get |{A, C && !B && !A} -> Q <= '0 and B && !A -> Q <= '1.

[widlarizer]

Superseded by #4569