def setupSimonRound(self, stp_file, x_in, y_in, x_out, y_out, and_out, b, c,
                        abits, w, tmpWeight, sbits, pbits, wordsize):
        """
        Model for linear behaviour of one round SIMON.
        y[i+1] = x[i]
        x[i+1] = (x[i] <<< 1) & (x[i] <<< 8) ^ y[i] ^ (x[i] << 2)

        This is a loop unrolled version of the model presented in
        http://eprint.iacr.org/2015/145
        """
        command = ""

        deltarot = self.rot_alpha - self.rot_beta
        lout = y_in
        lin = "BVXOR(BVXOR({}, {}), {})".format(x_in, rotr(lout, self.rot_gamma, wordsize), y_out)
        #lin = "BVXOR({}, {})".format(x_in, rotr(lout, self.rot_gamma, wordsize))

        #Assert(y_out = x_in)
        command += "ASSERT({} = {});\n".format(x_out, y_in)

        #Assert for AND linear approximation
        tmp = "BVXOR(({0} | {1}), {2}) & {2}".format(
            rotr(lout, self.rot_alpha, wordsize),
            rotr(lout, self.rot_beta, wordsize),
            lin)

        command += "ASSERT({} = 0x{});\n".format(tmp, "0"*(wordsize // 4))

        #Assert for y_out
        # command += "ASSERT({0} = BVXOR({1}, BVXOR({2}, BVXOR({3}, {4}))));\n".format(
        #     y_out, x_in, rotr(lout, self.rot_alpha, wordsize), rotr(lout, self.rot_beta, wordsize),
        #     rotr(x_out, self.rot_gamma, wordsize))
        command += "ASSERT({0} = BVXOR({1}, BVXOR({2}, {3})));\n".format(
            y_out, x_in, rotr(x_out, self.rot_gamma, wordsize), lin)

        #For weight computation
        #Compute abits
        loutRotated = rotr(lout, deltarot, wordsize)

        command += "ASSERT({} = ({} & {}));\n".format(tmpWeight[0], lout, loutRotated)

        for i in range(1, wordsize):
            command += "ASSERT({} = ({} & {}));\n".format(
                tmpWeight[i], lout, rotr(tmpWeight[i - 1], deltarot, wordsize))

        abits = "BVXOR({}, {})".format(lout, tmpWeight[0])
        for i in range(1, wordsize):
            abits = "BVXOR({}, {})".format(tmpWeight[i], abits)

        #abits = y_in #only use weight

        #Weight computation
        #command += "ASSERT({0} = (IF {1} = 0x{3} THEN BVSUB({4},0x{3},0x{5}1) \
        #          ELSE {2} ENDIF));\n".format(
        #            w, y_in, abits, "f"*(wordsize / 4),
        #            wordsize, "0"*((wordsize / 4) - 1))

        command += "ASSERT({} = {});\n".format(w, abits)

        #Parity Checks
        command += "ASSERT({} = {});\n".format(
            sbits[0], rotr("({} & ~{} & ~{})".format(
                rotr(lout, deltarot, wordsize), lout, rotr(abits, deltarot, wordsize)),
                1, wordsize))

        command += "ASSERT({} = {});\n".format(
            pbits[0], rotl("({} & {})".format(sbits[0], lin), 2*deltarot, wordsize))

        for i in range(1, wordsize):
            command += "ASSERT({} = {});\n".format(
                sbits[i], rotl("({} & {})".format(
                    rotl(sbits[i - 1], deltarot, wordsize),
                    rotr(sbits[i-1], self.rot_beta, wordsize)),
                    deltarot, wordsize)
                )
            command += "ASSERT({} = {});\n".format(
                pbits[i], rotl("BVXOR({}, {} & {})".format(
                    pbits[i - 1], sbits[i], lin), 2*deltarot, wordsize)
                )

        command += "ASSERT({} = 0x{});\n".format(pbits[wordsize - 1], "0"*(wordsize // 4))

        stp_file.write(command)
        return
dataset/ETHPy150Open kste/cryptosmt/ciphers/simonlinear.py/SimonLinearCipher.setupSimonRound/original