🐛 Synthesis of right shift does not generate correct gate sequence

[TooMuchDakka]

Environment information

• OS: Windows
• C++ Compiler: clang 17.0.3
• MQT-Core: 3.0.2
• MQT-Syrec: Main branch commit 2ba6873

Description

A shift expression using the right shift operation is currently synthesized as a sequence of CNOT gates while ignoring the defined shift amount of the operation. A simulation of the following SyReC program:

module main(in a(4), out b(4)) 
b ^= ~(a >> 2) 

with the input state a=1 (0001), b=0 leads to the result a=1, b=14 (1110)

Expected behavior

For the given input state a=1, b=0 the expected output state is a=1, b=15 (1111).

How to Reproduce

1. Install mqt.syrec version 1.21.1 via pip install mqt.syrec==1.21.1
2. Launch the syrec-editor python application and copy the SyReC circuit from the bug description into the code editor
3. Select either the cost or line aware synthesis radio button and then press the 'Build' button

[Geremia]

I noticed some gate sequence issues when simulating a ~2 million line circuit (which included the >> operation) prior to #252. I don't know if it had to do with the >>, the large number of lines, or both. About 0.5% of the gates were wrongly sequenced.

[TooMuchDakka]

A second potential issue that we have identified for the synthesis of both the left and right shift operation is a shift of an expression by more positions than the bitwidth of said expression. An example for this case is the following SyReC program:

module main(in a(4), out b(4)) 
b ^= (a >> 5)

Currently this assignment statement cannot be synthesized because of the previously mentioned issue in the shift expression. However, we think that the shift expression should evaluate to 0 and when stored in ancillary qubits be synthesizable.

[TooMuchDakka]

I noticed some gate sequence issues when simulating a ~2 million line circuit (which included the >> operation) prior to #252. I don't know if it had to do with the >>, the large number of lines, or both. About 0.5% of the gates were wrongly sequenced.

Since it is currently not documented which gates are generated for every supported SyReC entity, a gate sequence could be identified by the user as "wrong" due to the user not considering any applied optimizations or assuming another ordering of the generated gates while both the generated and expected gate sequences are functionally equivalent.

I am not entirely sure whether your description of "About 0.5% of the gates were wrongly sequenced" is referring to an actual synthesis error or rather the previously described "sequencing" issue (with the expected gate sequence being functionally equivalent to the created one). Could you determine a set of inputs for your circuit where the simulated outputs did not match your expected ones?

[Geremia]

@TooMuchDakka

I am not entirely sure whether your description of "About 0.5% of the gates were wrongly sequenced" is referring to

I ran the simulation forward and then backward (cf. #231) and compared the output of the backward run to the original input. About 99.5% of the reversed output matched the original input, which is a problem; it should be 100%. So it seems there is some gate sequencing issue somewhere.

You can try it yourself. The last for loop below is where the reversibility/gate-sequence problems crop up:

sha256.src

module ror32(out o, in shift, in word)
  if (shift = 1) then
    o ^= ((word >> 1) | (word << 30))
  else
  if (shift = 2) then
    o ^= ((word >> 2) | (word << 29))
  else
  if (shift = 3) then
    o ^= ((word >> 3) | (word << 28))
  else
  if (shift = 4) then
    o ^= ((word >> 4) | (word << 27))
  else
  if (shift = 5) then
    o ^= ((word >> 5) | (word << 26))
  else
  if (shift = 6) then
    o ^= ((word >> 6) | (word << 25))
  else
  if (shift = 7) then
    o ^= ((word >> 7) | (word << 24))
  else
  if (shift = 8) then
    o ^= ((word >> 8) | (word << 23))
  else
  if (shift = 9) then
    o ^= ((word >> 9) | (word << 22))
  else
  if (shift = 10) then
    o ^= ((word >> 10) | (word << 21))
  else
  if (shift = 11) then
    o ^= ((word >> 11) | (word << 20))
  else
  if (shift = 12) then
    o ^= ((word >> 12) | (word << 19))
  else
  if (shift = 13) then
    o ^= ((word >> 13) | (word << 18))
  else
  if (shift = 14) then
    o ^= ((word >> 14) | (word << 17))
  else
  if (shift = 15) then
    o ^= ((word >> 15) | (word << 16))
  else
  if (shift = 16) then
    o ^= ((word >> 16) | (word << 15))
  else
  if (shift = 17) then
    o ^= ((word >> 17) | (word << 14))
  else
  if (shift = 18) then
    o ^= ((word >> 18) | (word << 13))
  else
  if (shift = 19) then
    o ^= ((word >> 19) | (word << 12))
  else
  if (shift = 20) then
    o ^= ((word >> 20) | (word << 11))
  else
  if (shift = 21) then
    o ^= ((word >> 21) | (word << 10))
  else
  if (shift = 22) then
    o ^= ((word >> 22) | (word << 9))
  else
  if (shift = 23) then
    o ^= ((word >> 23) | (word << 8))
  else
  if (shift = 24) then
    o ^= ((word >> 24) | (word << 7))
  else
  if (shift = 25) then
    o ^= ((word >> 25) | (word << 6))
  else
  if (shift = 26) then
    o ^= ((word >> 26) | (word << 5))
  else
  if (shift = 27) then
    o ^= ((word >> 27) | (word << 4))
  else
  if (shift = 28) then
    o ^= ((word >> 28) | (word << 3))
  else
  if (shift = 29) then
    o ^= ((word >> 29) | (word << 2))
  else
  if (shift = 30) then
    o ^= ((word >> 30) | (word << 1))
  else
  if (shift = 31) then
    o ^= (word >> 31)
  else
    o ^= word
  fi (shift = 31)
  fi (shift = 30)
  fi (shift = 29)
  fi (shift = 28)
  fi (shift = 27)
  fi (shift = 26)
  fi (shift = 25)
  fi (shift = 24)
  fi (shift = 23)
  fi (shift = 22)
  fi (shift = 21)
  fi (shift = 20)
  fi (shift = 19)
  fi (shift = 18)
  fi (shift = 17)
  fi (shift = 16)
  fi (shift = 15)
  fi (shift = 14)
  fi (shift = 13)
  fi (shift = 12)
  fi (shift = 11)
  fi (shift = 10)
  fi (shift = 9)
  fi (shift = 8)
  fi (shift = 7)
  fi (shift = 6)
  fi (shift = 5)
  fi (shift = 4)
  fi (shift = 3)
  fi (shift = 2)
  fi (shift = 1)

module Ch(out o, in x, in y, in z)
  o ^= (z ^ (x & (y ^ z)))

module Maj(out o, in x, in y, in z)
  o ^= ((x & y) | (z & (x | y)))

module e0(out o, in x)
  wire a, b, c, s1, s2, s3
  s1 ^= 2 ; call ror32(a, x, s1);
  s2 ^= 13; call ror32(b, x, s2);
  s3 ^= 22; call ror32(c, x, s3);
  o ^= (a ^ (b ^ c))

module e1(out o, in x)
  wire a, b, c, s1, s2
  s1 ^= 7 ; call ror32(a, x, s1);
  s2 ^= 18; call ror32(b, x, s2);
  o ^= (a ^ (b ^ c))

module s0(out o, in x)
  wire a, b, s1, s2
  s1 ^= 7 ; call ror32(a, x, s1);
  s2 ^= 18; call ror32(b, x, s2);
  o ^= (a ^ (b ^ (x >> 3)))

module s1(out o, in x)
  wire a, b, s1, s2
  s1 ^= 17; call ror32(a, x, s1);
  s2 ^= 19; call ror32(b, x, s2);
  o ^= (a ^ (b ^ (x >> 10)))

module main(inout s[8], in i[16])
  wire i1, i2, i3, i4, s1o, s0o, wi1, wi3  // ← for blend loop
  wire a, b, c, d, e, f, g, h, t1, t2
  wire W[64], K[64]
  wire e1o, Cho, e0o, Majo
  wire zero
  K[0]  ^= 1116352408;  K[16] ^= 3835390401;  K[32] ^=  666307205;  K[48] ^=  430227734;
  K[1]  ^= 1899447441;  K[17] ^= 4022224774;  K[33] ^=  773529912;  K[49] ^=  506948616;
  K[2]  ^= 3049323471;  K[18] ^=  264347078;  K[34] ^= 1294757372;  K[50] ^=  659060556;
  K[3]  ^= 3921009573;  K[19] ^=  604807628;  K[35] ^= 1396182291;  K[51] ^=  883997877;
  K[4]  ^=  961987163;  K[20] ^=  770255983;  K[36] ^= 1695183700;  K[52] ^=  958139571;
  K[5]  ^= 1508970993;  K[21] ^= 1249150122;  K[37] ^= 1986661051;  K[53] ^= 1322822218;
  K[6]  ^= 2453635748;  K[22] ^= 1555081692;  K[38] ^= 2177026350;  K[54] ^= 1537002063;
  K[7]  ^= 2870763221;  K[23] ^= 1996064986;  K[39] ^= 2456956037;  K[55] ^= 1747873779;
  K[8]  ^= 3624381080;  K[24] ^= 2554220882;  K[40] ^= 2730485921;  K[56] ^= 1955562222;
  K[9]  ^=  310598401;  K[25] ^= 2821834349;  K[41] ^= 2820302411;  K[57] ^= 2024104815;
  K[10] ^=  607225278;  K[26] ^= 2952996808;  K[42] ^= 3259730800;  K[58] ^= 2227730452;
  K[11] ^= 1426881987;  K[27] ^= 3210313671;  K[43] ^= 3345764771;  K[59] ^= 2361852424;
  K[12] ^= 1925078388;  K[28] ^= 3336571891;  K[44] ^= 3516065817;  K[60] ^= 2428436474;
  K[13] ^= 2162078206;  K[29] ^= 3584528711;  K[45] ^= 3600352804;  K[61] ^= 2756734187;
  K[14] ^= 2614888103;  K[30] ^=  113926993;  K[46] ^= 4094571909;  K[62] ^= 3204031479;
  K[15] ^= 3248222580;  K[31] ^=  338241895;  K[47] ^=  275423344;  K[63] ^= 3329325298;

  // load init state
  for $i = 0 to 7 do
    s[$i] <=> zero
  rof;
  s[0] ^= 1779033703;  s[1] ^= 3144134277;  s[2] ^= 1013904242;  s[3] ^= 2773480762;
  s[4] ^= 1359893119;  s[5] ^= 2600822924;  s[6] ^=  528734635;  s[7] ^= 1541459225;

  // load the input
  for $i = 0 to 15 do
    W[$i] ^= i[$i]
  rof;

  // now blend
  for $i = 16 to 63 do
    i1 <=> zero; i1 ^= ($i - 2);
    i2 <=> zero; i2 ^= ($i - 7);
    i3 <=> zero; i3 ^= ($i - 15);
    i4 <=> zero; i4 ^= ($i - 16);
    wi1 <=> zero; wi1 ^= W[i1]; s1o <=> zero; call s1(s1o, wi1);
    wi3 <=> zero; wi3 ^= W[i3]; s0o <=> zero; call s0(s0o, wi3); 
    W[$i] ^= ((s1o + W[i2]) + (s0o + W[i4]))
  rof;

  // load the state i into our registers
  a ^= s[0];  b ^= s[1];  c ^= s[2];  d ^= s[3];
  e ^= s[4];  f ^= s[5];  g ^= s[6];  h ^= s[7];

  // now iterate
  // This loop creates reversibility problems somehow:
  for $i = 0 to 63 do
    e1o <=> zero; call e1(e1o, e);
    Cho <=> zero; call Ch(Cho, e, f, g);
    e0o <=> zero; call e0(e0o, a);
    Majo <=> zero; call Maj(Majo, a, b, c);
    t1 <=> zero; t1 ^= (((h + e1o) + Cho) + (K[$i] + W[$i]));
    t2 <=> zero; t2 ^= (e0o + Majo);
    h <=> zero; h ^= g;
    g <=> zero; g ^= f;
    f <=> zero; f ^= e;
    e <=> zero; e ^= (d + t1);
    d <=> zero; d ^= c;
    c <=> zero; c ^= b;
    b <=> zero; b ^= a;
    a <=> zero; a ^= (t1 + t2)
  rof;

  s[0] += a;  s[1] += b;  s[2] += c;  s[3] += d;
  s[4] += e;  s[5] += f;  s[6] += g;  s[7] += h

[TooMuchDakka]

@TooMuchDakka

I am not entirely sure whether your description of "About 0.5% of the gates were wrongly sequenced" is referring to

I ran the simulation forward and then backward (cf. #231) and compared the output of the backward run to the original input. About 99.5% of the reversed output matched the original input, which is a problem; it should be 100%. So it seems there is some gate sequencing issue somewhere.

You can try it yourself. The last for loop below is where the reversibility/gate-sequence problems crop up:
sha256.src

Thank you for providing the implementation of the circuit. As you might have seen in the source code, the current verification tests for the correct synthesis of the supported SyReC operations are rather rudimentary as of now and finding the issue in your provided complex circuit might take some time. A first version of a fix for the issue in the synthesis of the right shift operation should be available in the next view days and might solve the error in your circuit (assuming that no further errors in the synthesis are found) but I will keep you informed here if more information is available.

[Geremia]

@TooMuchDakka

finding the issue in your provided complex circuit might take some time

The call stack isn't shallow for that .src code (modules call other modules which call yet others). I'm wondering if that's where the issue could stem from.
I tested the (non-main) modules separately and there were no issues.

[TooMuchDakka]

Trying to synthesize sha256.src using the latest commit of the main branch result in an error in the synthesizer due to duplicate qubit labels being created during the inline of called modules (see related issue #278).

[Geremia]

@TooMuchDakka cf. #279 for a problem synthesizing that sha256.src.

[TooMuchDakka]

A second potential issue that we have identified for the synthesis of both the left and right shift operation is a shift of an expression by more positions than the bitwidth of said expression. An example for this case is the following SyReC program:

module main(in a(4), out b(4)) 
b ^= (a >> 5)

Currently this assignment statement cannot be synthesized because of the previously mentioned issue in the shift expression. However, we think that the shift expression should evaluate to 0 and when stored in ancillary qubits be synthesizable.

While the consideration of the shift amount in the SyrecSynthesis::rightShift was added with PR #259 , the issue with shift expressions in which the shift amount is larger than the to be shifted expression still remains in both the SyrecSynthesis::leftShift and SyrecSynthesis::rightShift operation. While the SyReC parser will transform the shift expression above to the integer constant 0 and thus allow for the assignment to be synthesized, shift expressions like the following cannot be synthesized:

module alu(out x0(2), inout x1(2), inout x2(2))
for $i = 3 to 5 step 1 do 
    x0 += (x1 << $i);
    x0 += (x1 >> $i)
rof

@burgholzer Additionally, the following potential issues were identified in the current synthesis tests:

• While the parser validates the semantics of a SyReC program when read from a string or file using the syrec::Program::read and syrec::Program::readFromString, the synthesis implementations CostAwareSynthesis and LineAwareSynthesis do not perform such checks (i.e. for assignments to read only variables) and can be invoked by the user in both the python as well as C++ library with semantically incorrect SyReC programs (passed in their IR representation).
• The synthesis tests all use the syrec::Program interface to provide the input SyReC program to the test and never an IR representation.

Two options for how these issues could be covered are:

• Duplicate the existing synthesis tests to use the IR representation instead of the "stringified" SyReC program as input.
• And/Or add additional test to only cover the error cases for semantically incorrect IR representations passed to the synthesis algorithms.

[burgholzer]

I am fine with either of these solutions, which ever one is more maintainable for future additions.