John Hauser
2024 Sep 16

In this file, the behaviors proposed for many Base P instructions are
documented, either as Sail code or by other means.

The Sail code in this file has not been tested and may contain mistakes.
(If you see misuses of Sail, let me know, so I can correct my understanding
of the language.)  Because the Base P extension is still in development,
it is also possible that behaviors for some of these instructions will
ultimately be changed from what is specified here.

The purpose of this file is only to describe what each proposed instruction
does, to inform the creation of proper P extension documentation and an
official RISC-V Sail model.  I expect the official Sail model will encode
these same instruction behaviors differently.  In particular, there is a lot
of redundancy among the instructions that the Sail model could factor into
subfunctions.

Instructions that perform multiplications are currently missing.  The
intention is to add them in a subsequent version.

In its current version, the code in this file never sets an overflow flag.
The P-extension task group has yet to discuss whether the Base P extension
will include such a flag.  If it is decided that it will, a later version of
this file will add updates to the overflow flag.

Much of the Sail code here should be readable even without much familiarity
with Sail.  Note these Sail conventions (according to my understanding):

  - An at sign (@) denotes concatenation of bits.

  - "bits(<N>)" is the type of a "bitvector" of <N> bits.

  - Integers and bitvectors are different types.  Built-in functions
    "signed" and "unsigned" convert a bitvector to an integer.

In the Sail model for RISC-V, the X registers are XLEN-size bitvectors,
accessed as "X(<N>)" for 5-bit number <N> in the range 0 to 31.  The value
of "X(0)" is always zero, of course.

The existing RISC-V Sail model defines some other functions and operators
that are used in the Sail code in this file:

   to_bits       - convert an integer to a bitvector; first argument is size
   zero_extend   - zero-extend a bitvector; first argument is new size
   sign_extend   - sign-extend a bitvector; first argument is new size
   <<            - shift a bitvector left, inserting zero bits
   >>            - shift a bitvector right, inserting zero bits
   <_s           - signed less-than comparison of two bitvectors
   <=_s          - signed less-than-or-equal comparison of two bitvectors
   >_s           - signed greater-than comparison of two bitvectors
   >=_s          - signed greater-than-or-equal comparison of two bitvectors
   <_u           - unsigned less-than comparison of two bitvectors
   >_u           - unsigned greater-than comparison of two bitvectors

For signed shifts right ("arithmetic" shifts) of a bitvector, the code in
this file first sign-extends to a larger size, then uses the >> operator.

The following uses of names 'xlen' and 'xlen_bytes' also appear:

   bits(xlen)          - the type of a bitvector of XLEN bits
   sizeof(xlen)        - an integer with the value XLEN
   sizeof(xlen_bytes)  - an integer with the value XLEN/8
   log2(sizeof(xlen))  - 5 when XLEN = 32; 6 when XLEN = 64

A few named values in the Sail code come from instruction subfields.  "rs1",
"rs2", and "rd" are the familiar 5-bit register operand fields for RISC-V
instructions.  "rs1_p", "rs2_p", and "rd_p" are 4-bit fields specifying
even-odd register pair operands.  Field "w_uimm" is 7 bits and contains
an immediate value in the lower 3, 4, 5, or 6 bits, depending on the
instruction.

For many double-wide Base P instructions for RV32, instead of Sail code, the
instruction's function is described as being equivalent to two single-wide
instructions.  In these descriptions, if rd, rs1, or rs2 is an even-numbered
X register other than x0, then the corresponding notation "rd+", "rs1+", or
"rs2+" denotes the next higher-numbered (odd) register.  When rd, rs1, or
rs2 is x0, then the corresponding "rd+", "rs1+", or "rs2+" is also x0, never
x1.

------------------------------------------------------------------------------

PADD.B.B0:

    let s1 = X(rs1);
    let s2_b0 = X(rs2)[7..0];
    var d : bits(xlen);
    foreach (i from 0 to sizeof(xlen_bytes) - 1) {
        let s1_b = s1[(i*8+7)..(i*8)];
        d[(i*8+7)..(i*8)] = s1_b + s2_b0;
    }
    X(rd) = d;

PDIF.B:

    let s1 = X(rs1);
    let s2 = X(rs2);
    var d : bits(xlen);
    foreach (i from 0 to sizeof(xlen_bytes) - 1) {
        let s1_b = s1[(i*8+7)..(i*8)];
        let s2_b = s2[(i*8+7)..(i*8)];
        d[(i*8+7)..(i*8)] =
            if (s1_b <_s s2_b) then s2_b - s1_b else s1_b - s2_b;
    }
    X(rd) = d;

PDIFU.B:

    let s1 = X(rs1);
    let s2 = X(rs2);
    var d : bits(xlen);
    foreach (i from 0 to sizeof(xlen_bytes) - 1) {
        let s1_b = s1[(i*8+7)..(i*8)];
        let s2_b = s2[(i*8+7)..(i*8)];
        d[(i*8+7)..(i*8)] =
            if (s1_b <_u s2_b) then s2_b - s1_b else s1_b - s2_b;
    }
    X(rd) = d;

PREDSUM.B:

    let s1 = X(rs1);
    var sum : bits(xlen) = X(rs2);
    foreach (i from 0 to sizeof(xlen_bytes) - 1) {
        let s1_b = s1[(i*8+7)..(i*8)];
        sum = sum + sign_extend(sizeof(xlen), s1_b);
    }
    X(rd) = sum;

PREDSUMU.B:

    let s1 = X(rs1);
    var sum : bits(xlen) = X(rs2);
    foreach (i from 0 to sizeof(xlen_bytes) - 1) {
        let s1_b = s1[(i*8+7)..(i*8)];
        sum = sum + zero_extend(sizeof(xlen), s1_b);
    }
    X(rd) = sum;

PADD.H.H0:

    let s1 = X(rs1);
    let s2_h0 = X(rs2)[15..0];
    var d : bits(xlen);
    foreach (i from 0 to sizeof(xlen_bytes)/2 - 1) {
        let s1_h = s1[(i*16+15)..(i*16)];
        d[(i*16+15)..(i*16)] = s1_h + s2_h0;
    }
    X(rd) = d;

PSH1ADD.H:

    let s1 = X(rs1);
    let s2 = X(rs2);
    var d : bits(xlen);
    foreach (i from 0 to sizeof(xlen_bytes)/2 - 1) {
        let s1_h = s1[(i*16+15)..(i*16)];
        let s2_h = s2[(i*16+15)..(i*16)];
        d[(i*16+15)..(i*16)] = (s1_h << 1) + s2_h;
    }
    X(rd) = d;

PSSH1SADD.H:

    let s1 = X(rs1);
    let s2 = X(rs2);
    var d : bits(xlen);
    foreach (i from 0 to sizeof(xlen_bytes)/2 - 1) {
        let s1_h = s1[(i*16+15)..(i*16)];
        let s2_h = s2[(i*16+15)..(i*16)];
        let ssh1_s1_h : bits(16) =
            if (s1_h <_s 0xC000) then 0x8000
                else if (s1_h >=_s 0x4000) then 0x7FFF else s1_h << 1;
        let xadd_ssh1 = to_bits(20, signed(ssh1_s1_h) + signed(s2_h));
        d[(i*16+15)..(i*16)] =
            if (xadd_ssh1 <_s 0xF8000) then 0x8000
                else if (xadd_ssh1 >_s 0x07FFF) then 0x7FFF
                    else xadd_ssh1[15..0];
    }
    X(rd) = d;

PDIF.H:

    let s1 = X(rs1);
    let s2 = X(rs2);
    var d : bits(xlen);
    foreach (i from 0 to sizeof(xlen_bytes)/2 - 1) {
        let s1_h = s1[(i*16+15)..(i*16)];
        let s2_h = s2[(i*16+15)..(i*16)];
        d[(i*16+15)..(i*16)] =
            if (s1_h <_s s2_h) then s2_h - s1_h else s1_h - s2_h;
    }
    X(rd) = d;

PDIFU.H:

    let s1 = X(rs1);
    let s2 = X(rs2);
    var d : bits(xlen);
    foreach (i from 0 to sizeof(xlen_bytes)/2 - 1) {
        let s1_h = s1[(i*16+15)..(i*16)];
        let s2_h = s2[(i*16+15)..(i*16)];
        d[(i*16+15)..(i*16)] =
            if (s1_h <_u s2_h) then s2_h - s1_h else s1_h - s2_h;
    }
    X(rd) = d;

PREDSUM.H:

    let s1 = X(rs1);
    var sum : bits(xlen) = X(rs2);
    foreach (i from 0 to sizeof(xlen_bytes)/2 - 1) {
        let s1_h = s1[(i*16+15)..(i*16)];
        sum = sum + sign_extend(sizeof(xlen), s1_h);
    }
    X(rd) = sum;

PREDSUMU.H:

    let s1 = X(rs1);
    var sum : bits(xlen) = X(rs2);
    foreach (i from 0 to sizeof(xlen_bytes)/2 - 1) {
        let s1_h = s1[(i*16+15)..(i*16)];
        sum = sum + zero_extend(sizeof(xlen), s1_h);
    }
    X(rd) = sum;

RV32 SSH1SADD:

    let s1 = X(rs1);
    let s2 = X(rs2);
    let ssh1_s1 : bits(32) =
        if (s1 <_s 0xC0000000) then 0x80000000
            else if (s1 >=_s 0x40000000) then 0x7FFFFFFF else s1 << 1;
    let xadd_ssh1 = to_bits(36, signed(ssh1_s1) + signed(s2));
    X(rd) =
        if (xadd_ssh1 <_s 0xF80000000) then 0x80000000
            else if (xadd_ssh1 >_s 0x07FFFFFFF) then 0x7FFFFFFF
                else xadd_ssh1[31..0];

RV64 PADD.W.W0:

    let s1 = X(rs1);
    let s2_w0 = X(rs2)[31..0];
    var d : bits(64);
    d[31..0]  = s1[31..0]  + s2_w0;
    d[63..32] = s1[63..32] + s2_w0;
    X(rd) = d;

RV64 PSH1ADD.W:

    let s1 = X(rs1);
    let s2 = X(rs2);
    var d : bits(64);
    d[31..0]  = (s1[31..0]  << 1) + s2[31..0];
    d[63..32] = (s1[63..32] << 1) + s2[63..32];
    X(rd) = d;

RV64 PSSH1SADD.W:

    let s1 = X(rs1);
    let s2 = X(rs2);
    var d : bits(64);
    foreach (i from 0 to 1) {
        let s1_w = s1[(i*32+31)..(i*32)];
        let s2_w = s2[(i*32+31)..(i*32)];
        let ssh1_s1_w : bits(32) =
            if (s1_w <_s 0xC0000000) then 0x80000000
                else if (s1_w >=_s 0x40000000) then 0x7FFFFFFF else s1_w << 1;
        let xadd_ssh1 = to_bits(36, signed(ssh1_s1_w) + signed(s2_w));
        d[(i*32+31)..(i*32)] =
            if (xadd_ssh1 <_s 0xF80000000) then 0x80000000
                else if (xadd_ssh1 >_s 0x07FFFFFFF) then 0x7FFFFFFF
                    else xadd_ssh1[31..0];
    }
    X(rd) = d;

RV64 PREDSUM.W:

    let s1 = X(rs1);
    X(rd) = X(rs2) + sign_extend(64, s1[31..0]) + sign_extend(64, s1[63..32]);

RV64 PREDSUMU.W:

    let s1 = X(rs1);
    X(rd) = X(rs2) + zero_extend(64, s1[31..0]) + zero_extend(64, s1[63..32]);

------------------------------------------------------------------------------

PSSHA.H.H0:

    let s1 = X(rs1);
    let shamt = X(rs2)[7..0];
    let sshamt = signed(shamt);
    var d : bits(xlen);
    foreach (i from 0 to sizeof(xlen_bytes)/2 - 1) {
        let s1_h = s1[(i*16+15)..(i*16)];
        let s1_xh = sign_extend(32, s1_h);
        d[(i*16+15)..(i*16)] =
            if (sshamt < 0) then {
                if (sshamt <= -16) then s1_xh[31..16]
                    else (s1_xh >> (0x00 - shamt)[3..0])[15..0]
            } else {
                let shx : bits(32) =
                    if (sshamt >= 16) then s1_h @ 0x0000
                        else s1_xh << shamt[3..0];
                if (shx <_s 0xFFFF8000) then 0x8000
                    else if (shx >_s 0x00007FFF) then 0x7FFF else shx[15..0]
            };
    }
    X(rd) = d;

PSSHAR.H.H0:

    let s1 = X(rs1);
    let shamt = X(rs2)[7..0];
    let sshamt = signed(shamt);
    var d : bits(xlen);
    foreach (i from 0 to sizeof(xlen_bytes)/2 - 1) {
        let s1_h = s1[(i*16+15)..(i*16)];
        d[(i*16+15)..(i*16)] =
            if (sshamt < 0) then {
                let s1_xh : bits(33) = sign_extend(32, s1_h) @ 0b0;
                let shx : bits(17) =
                    if (sshamt <= -16) then s1_xh[32..16]
                        else (s1_xh >> (0x00 - shamt)[3..0])[16..0];
                (shx + 1)[16..1]
            } else {
                let shx : bits(32) =
                    if (sshamt >= 16) then s1_h @ 0x0000
                        else sign_extend(32, s1_h) << shamt[3..0];
                if (shx <_s 0xFFFF8000) then 0x8000
                    else if (shx >_s 0x00007FFF) then 0x7FFF else shx[15..0]
            };
    }
    X(rd) = d;

RV32 SSHA:

    let s1 = X(rs1);
    let shamt = X(rs2)[7..0];
    let sshamt = signed(shamt);
    let xs1 = sign_extend(64, s1);
    X(rd) =
        if (sshamt < 0) then {
            if (sshamt <= -32) then xs1[63..32]
                else (xs1 >> (0x00 - shamt)[4..0])[31..0]
        } else {
            let shx : bits(64) =
                if (sshamt >= 32) then s1 @ 0x00000000 else xs1 << shamt[4..0];
            if (shx <_s 0xFFFFFFFF80000000) then 0x80000000
                else if (shx >_s 0x000000007FFFFFFF) then 0x7FFFFFFF
                    else shx[31..0]
        };

RV32 SSHAR:

    let s1 = X(rs1);
    let shamt = X(rs2)[7..0];
    let sshamt = signed(shamt);
    X(rd) =
        if (sshamt < 0) then {
            let xs1 : bits(65) = sign_extend(64, s1) @ 0b0;
            let shx : bits(33) =
                if (sshamt <= -32) then xs1[64..32]
                    else (xs1 >> (0x00 - shamt)[4..0])[32..0]
            (shx + 1)[32..1]
        } else {
            let shx : bits(64) =
                if (sshamt >= 32) then s1 @ 0x00000000
                    else sign_extend(64, s1) << shamt[4..0];
            if (shx <_s 0xFFFFFFFF80000000) then 0x80000000
                else if (shx >_s 0x000000007FFFFFFF) then 0x7FFFFFFF
                    else shx[31..0]
        };

RV32 MSEQ:

    X(rd) = if (X(rs1) == X(rs2)) then 0xFFFFFFFF else 0x00000000;

RV32 MSLT:

    X(rd) = if (X(rs1) <_s X(rs2)) then 0xFFFFFFFF else 0x00000000;

RV32 MSLTU:

    X(rd) = if (X(rs1) <_u X(rs2)) then 0xFFFFFFFF else 0x00000000;

RV64 PSEXTB.W:

    let s1 = X(rs1);
    X(rd) = sign_extend(32, s1[39..32]) @ sign_extend(32, s1[7..0]);

RV64 PSEXTH.W:

    let s1 = X(rs1);
    X(rd) = sign_extend(32, s1[47..32]) @ sign_extend(32, s1[15..0]);

RV64 PSSHA.W.W0:

    let s1 = X(rs1);
    let shamt = X(rs2)[7..0];
    let sshamt = signed(shamt);
    var d : bits(64);
    foreach (i from 0 to 1) {
        let s1_w = s1[(i*32+31)..(i*32)];
        let s1_xw = sign_extend(64, s1_w);
        d[(i*32+31)..(i*32)] =
            if (sshamt < 0) then {
                if (sshamt <= -32) then s1_xw[63..32]
                    else (s1_xw >> (0x00 - shamt)[4..0])[31..0]
            } else {
                let shx : bits(64) =
                    if (sshamt >= 32) then s1_w @ 0x00000000
                        else s1_xw << shamt[4..0];
                if (shx <_s 0xFFFFFFFF80000000) then 0x80000000
                    else if (shx >_s 0x000000007FFFFFFF) then 0x7FFFFFFF
                        else shx[31..0]
            };
    }
    X(rd) = d;

RV64 PSSHAR.W.W0:

    let s1 = X(rs1);
    let shamt = X(rs2)[7..0];
    let sshamt = signed(shamt);
    var d : bits(64);
    foreach (i from 0 to 1) {
        let s1_w = s1[(i*32+31)..(i*32)];
        d[(i*32+31)..(i*32)] =
            if (sshamt < 0) then {
                let s1_xw : bits(65) = sign_extend(64, s1_w) @ 0b0;
                let shx : bits(33) =
                    if (sshamt <= -32) then s1_xw[64..32]
                        else (s1_xw >> (0x00 - shamt)[4..0])[32..0];
                (shx + 1)[32..1]
            } else {
                let shx : bits(64) =
                    if (sshamt >= 32) then s1_w @ 0x00000000
                        else sign_extend(64, s1_w) << shamt[4..0];
                if (shx <_s 0xFFFFFFFF80000000) then 0x80000000
                    else if (shx >_s 0x000000007FFFFFFF) then 0x7FFFFFFF
                        else shx[31..0]
            };
    }
    X(rd) = d;

RV64 PMSEQ.W:

    let s1 = X(rs1);
    let s2 = X(rs2);
    var d : bits(64);
    foreach (i from 0 to 1) {
        let s1_w = s1[(i*32+31)..(i*32)];
        let s2_w = s2[(i*32+31)..(i*32)];
        d[(i*32+31)..(i*32)] =
            if (s1_w == s2_w) then 0xFFFFFFFF else 0x00000000;
    }
    X(rd) = d;

RV64 PMSLT.W:

    let s1 = X(rs1);
    let s2 = X(rs2);
    var d : bits(64);
    foreach (i from 0 to 1) {
        let s1_w = s1[(i*32+31)..(i*32)];
        let s2_w = s2[(i*32+31)..(i*32)];
        d[(i*32+31)..(i*32)] =
            if (s1_w <_s s2_w) then 0xFFFFFFFF else 0x00000000;
    }
    X(rd) = d;

RV64 PMSLTU.W:

    let s1 = X(rs1);
    let s2 = X(rs2);
    var d : bits(64);
    foreach (i from 0 to 1) {
        let s1_w = s1[(i*32+31)..(i*32)];
        let s2_w = s2[(i*32+31)..(i*32)];
        d[(i*32+31)..(i*32)] =
            if (s1_w <_u s2_w) then 0xFFFFFFFF else 0x00000000;
    }
    X(rd) = d;

RV64 SATI:

    let s1 = X(rs1);
    let n = w_uimm[5..0];
    let minval : bits(64) = 0xFFFFFFFFFFFFFFFF << n;
    let maxval = ~minval;
    X(rd) =
        if (s1 <_s minval) then minval
            else if (s1 >_s maxval) then maxval else s1;

RV64 USATI:

    let s1 = X(rs1);
    let n = w_uimm[5..0];
    let maxval : bits(64) = ~(0xFFFFFFFFFFFFFFFF << n);
    X(rd) =
        if (s1 <_s 0x0000000000000000) then 0x0000000000000000
            else if (s1 >_s maxval) then maxval else s1;

RV64 SHA:

    let s1 = X(rs1);
    let shamt = X(rs2)[7..0];
    let sshamt = signed(shamt);
    X(rd) =
        if (sshamt < 0) then {
            let xs1 = sign_extend(128, s1);
            if (sshamt <= -64) then xs1[127..64]
                else (xs1 >> (0x00 - shamt)[5..0])[63..0]
        } else {
            if (sshamt >= 32) then 0x0000000000000000 else s1 << shamt[5..0]
        };

RV64 SHAR:

    let s1 = X(rs1);
    let shamt = X(rs2)[7..0];
    let sshamt = signed(shamt);
    X(rd) =
        if (sshamt < 0) then {
            let xs1 : bits(129) = sign_extend(128, s1) @ 0b0;
            let shx : bits(65) =
                if (sshamt <= -64) then xs1[128..64]
                    else (xs1 >> (0x00 - shamt)[5..0])[64..0];
            (shx + 1)[64..1]
        } else {
            if (sshamt >= 32) then 0x0000000000000000 else s1 << shamt[5..0]
        };

------------------------------------------------------------------------------

PPACK.H:

    let s1 = X(rs1);
    let s2 = X(rs2);
    var d : bits(xlen);
    foreach (i from 0 to sizeof(xlen_bytes)/2 - 1) {
        let s1_h = s1[(i*16+15)..(i*16)];
        let s2_h = s2[(i*16+15)..(i*16)];
        d[(i*16+15)..(i*16)] = s2_h[7..0] @ s1_h[7..0];
    }
    X(rd) = d;

PPACKBT.H:

    let s1 = X(rs1);
    let s2 = X(rs2);
    var d : bits(xlen);
    foreach (i from 0 to sizeof(xlen_bytes)/2 - 1) {
        let s1_h = s1[(i*16+15)..(i*16)];
        let s2_h = s2[(i*16+15)..(i*16)];
        d[(i*16+15)..(i*16)] = s2_h[15..8] @ s1_h[7..0];
    }
    X(rd) = d;

PPACKTB.H:

    let s1 = X(rs1);
    let s2 = X(rs2);
    var d : bits(xlen);
    foreach (i from 0 to sizeof(xlen_bytes)/2 - 1) {
        let s1_h = s1[(i*16+15)..(i*16)];
        let s2_h = s2[(i*16+15)..(i*16)];
        d[(i*16+15)..(i*16)] = s2_h[7..0] @ s1_h[15..8];
    }
    X(rd) = d;

PPACKT.H:

    let s1 = X(rs1);
    let s2 = X(rs2);
    var d : bits(xlen);
    foreach (i from 0 to sizeof(xlen_bytes)/2 - 1) {
        let s1_h = s1[(i*16+15)..(i*16)];
        let s2_h = s2[(i*16+15)..(i*16)];
        d[(i*16+15)..(i*16)] = s2_h[15..8] @ s1_h[15..8];
    }
    X(rd) = d;

------------------------------------------------------------------------------

RV64 REV16:

    let s1 = X(rs1);
    X(rd) = s1[15..0] @ s1[31..16] @ s1[47..32] @ s1[63..48];

RV64 ZIP8P:

    let s1 = X(rs1);
    let s2 = X(rs2);
    X(rd) =
        s2[31..24] @ s1[31..24] @ s2[23..16] @ s1[23..16]
            @ s2[15..8] @ s1[15..8] @ s2[7..0] @ s1[7..0];

RV64 ZIP8HP:

    let s1 = X(rs1);
    let s2 = X(rs2);
    X(rd) =
        s2[63..56] @ s1[63..56] @ s2[55..48] @ s1[55..48]
            @ s2[47..40] @ s1[47..40] @ s2[39..32] @ s1[39..32];

RV64 UNZIP8P:

    let s1 = X(rs1);
    let s2 = X(rs2);
    X(rd) =
        s2[55..48] @ s2[39..32] @ s2[23..16] @ s2[7..0]
            @ s1[55..48] @ s1[39..32] @ s1[23..16] @ s1[7..0];

RV64 UNZIP8HP:

    let s1 = X(rs1);
    let s2 = X(rs2);
    X(rd) =
        s2[63..56] @ s2[47..40] @ s2[31..24] @ s2[15..8]
            @ s1[63..56] @ s1[47..40] @ s1[31..24] @ s1[15..8];

RV64 ZIP16P:

    let s1 = X(rs1);
    let s2 = X(rs2);
    X(rd) = s2[31..16] @ s1[31..16] @ s2[15..0] @ s1[15..0];

RV64 ZIP16HP:

    let s1 = X(rs1);
    let s2 = X(rs2);
    X(rd) = s2[63..48] @ s1[63..48] @ s2[47..32] @ s1[47..32];

RV64 UNZIP16P:

    let s1 = X(rs1);
    let s2 = X(rs2);
    X(rd) = s2[47..32] @ s2[15..0] @ s1[47..32] @ s1[15..0];

RV64 UNZIP16HP:

    let s1 = X(rs1);
    let s2 = X(rs2);
    X(rd) = s2[63..48] @ s2[31..16] @ s1[63..48] @ s1[31..16];

------------------------------------------------------------------------------

ABS:

    let s1 = X(rs1);
    X(rd) = if (signed(s1) < 0) then 0 - s1 else s1;

CLS:

    var v : bits(xlen) = X(rs1);
    let lo_bound = to_bits(sizeof(xlen), -(2^(sizeof(xlen) - 2)));
    let hi_bound = ~lowbound;
    var c : int = 0;
    while (c < sizeof(xlen)) & (v >=_s lo_bound) & (v <=_s hi_bound) do {
        c = c + 1;
        v = v << 1;
    }
    X(rd) = to_bits(sizeof(xlen), c);

SLX:

    let shamt = X(rs2)[(log2(sizeof(xlen))-1)..0];
    X(rd) = ((X(rd) @ X(rs1)) << shamt)[(sizeof(xlen)*2-1)..sizeof(xlen)];

SRX:

    let shamt = X(rs2)[(log2(sizeof(xlen))-1)..0];
    X(rd) = ((X(rs1) @ X(rd)) >> shamt)[(sizeof(xlen)-1)..0];

MVM:

    let s2 = X(rs2);
    X(rd) = (~s2 & X(rd)) | (s2 & X(rs1));

MVMN:

    let s2 = X(rs2);
    X(rd) = (~s2 & X(rs1)) | (s2 & X(rd));

MERGE:

    let d = X(rd);
    X(rd) = (~d & X(rs1)) | (d & X(rs2));

RV64 ABSW:

    let s1_w = X(rs1)[31..0];
    X(rd) =
        sign_extend(
            64, if (signed(s1_w) <_s 0) then 0x00000000 - s1_w else s1_w);

RV64 CLSW:

    var w : bits(32) = X(rs1)[31..0];
    var c : int = 0;
    while (c < 32) & (w >=_s 0xC0000000) & (w <=_s 0x3FFFFFFF) do {
        c = c + 1;
        w = w << 1;
    }
    X(rd) = to_bits(sizeof(xlen), c);

------------------------------------------------------------------------------

RV32 PWADD.B:

    if (rd_p != 0x0) {
        let s1 = X(rs1);
        let s2 = X(rs2);
        var vd_h : vector(4, bits(16));
        foreach (i from 0 to 3) {
            let s1_b = s1[(i*8+7)..(i*8)];
            let s2_b = s2[(i*8+7)..(i*8)];
            vd_h[i] = to_bits(16, signed(s1_b) + signed(s2_b));
        };
        X(rd_p*2)   = vd_h[1] @ vd_h[0];
        X(rd_p*2+1) = vd_h[3] @ vd_h[2];
    }

RV32 PWADDA.B:

    if (rd_p != 0x0) {
        let s1 = X(rs1);
        let s2 = X(rs2);
        let d = X(rd_p*2+1) @ X(rd_p*2);
        var vd_h : vector(4, bits(16));
        foreach (i from 0 to 3) {
            let s1_b = s1[(i*8+7)..(i*8)];
            let s2_b = s2[(i*8+7)..(i*8)];
            let d_h = d[(i*16+15)..(i*16)];
            vd_h[i] = to_bits(16, signed(d_h) + signed(s1_b) + signed(s2_b));
        };
        X(rd_p*2)   = vd_h[1] @ vd_h[0];
        X(rd_p*2+1) = vd_h[3] @ vd_h[2];
    }

RV32 PWADDU.B:

    if (rd_p != 0x0) {
        let s1 = X(rs1);
        let s2 = X(rs2);
        var vd_h : vector(4, bits(16));
        foreach (i from 0 to 3) {
            let s1_b = s1[(i*8+7)..(i*8)];
            let s2_b = s2[(i*8+7)..(i*8)];
            vd_h[i] = to_bits(16, unsigned(s1_b) + unsigned(s2_b));
        };
        X(rd_p*2)   = vd_h[1] @ vd_h[0];
        X(rd_p*2+1) = vd_h[3] @ vd_h[2];
    }

RV32 PWADDAU.B:

    if (rd_p != 0x0) {
        let s1 = X(rs1);
        let s2 = X(rs2);
        let d = X(rd_p*2+1) @ X(rd_p*2);
        var vd_h : vector(4, bits(16));
        foreach (i from 0 to 3) {
            let s1_b = s1[(i*8+7)..(i*8)];
            let s2_b = s2[(i*8+7)..(i*8)];
            let d_h = d[(i*16+15)..(i*16)];
            vd_h[i] =
                to_bits(16, unsigned(d_h) + unsigned(s1_b) + unsigned(s2_b));
        };
        X(rd_p*2)   = vd_h[1] @ vd_h[0];
        X(rd_p*2+1) = vd_h[3] @ vd_h[2];
    }

RV32 PWSUB.B:

    if (rd_p != 0x0) {
        let s1 = X(rs1);
        let s2 = X(rs2);
        var vd_h : vector(4, bits(16));
        foreach (i from 0 to 3) {
            let s1_b = s1[(i*8+7)..(i*8)];
            let s2_b = s2[(i*8+7)..(i*8)];
            vd_h[i] = to_bits(16, signed(s1_b) - signed(s2_b));
        };
        X(rd_p*2)   = vd_h[1] @ vd_h[0];
        X(rd_p*2+1) = vd_h[3] @ vd_h[2];
    }

RV32 PWSUBA.B:

    if (rd_p != 0x0) {
        let s1 = X(rs1);
        let s2 = X(rs2);
        let d = X(rd_p*2+1) @ X(rd_p*2);
        var vd_h : vector(4, bits(16));
        foreach (i from 0 to 3) {
            let s1_b = s1[(i*8+7)..(i*8)];
            let s2_b = s2[(i*8+7)..(i*8)];
            let d_h = d[(i*16+15)..(i*16)];
            vd_h[i] = to_bits(16, signed(d_h) + signed(s1_b) - signed(s2_b));
        };
        X(rd_p*2)   = vd_h[1] @ vd_h[0];
        X(rd_p*2+1) = vd_h[3] @ vd_h[2];
    }

RV32 PWSUBU.B:

    if (rd_p != 0x0) {
        let s1 = X(rs1);
        let s2 = X(rs2);
        var vd_h : vector(4, bits(16));
        foreach (i from 0 to 3) {
            let s1_b = s1[(i*8+7)..(i*8)];
            let s2_b = s2[(i*8+7)..(i*8)];
            vd_h[i] = to_bits(16, unsigned(s1_b) - unsigned(s2_b));
        };
        X(rd_p*2)   = vd_h[1] @ vd_h[0];
        X(rd_p*2+1) = vd_h[3] @ vd_h[2];
    }

RV32 PWSUBAU.B:

    if (rd_p != 0x0) {
        let s1 = X(rs1);
        let s2 = X(rs2);
        let d = X(rd_p*2+1) @ X(rd_p*2);
        var vd_h : vector(4, bits(16));
        foreach (i from 0 to 3) {
            let s1_b = s1[(i*8+7)..(i*8)];
            let s2_b = s2[(i*8+7)..(i*8)];
            let d_h = d[(i*16+15)..(i*16)];
            vd_h[i] =
                to_bits(16, unsigned(d_h) + unsigned(s1_b) - unsigned(s2_b));
        };
        X(rd_p*2)   = vd_h[1] @ vd_h[0];
        X(rd_p*2+1) = vd_h[3] @ vd_h[2];
    }

RV32 PWSLLI.B:

    if (rd_p != 0x0) {
        let s1 = X(rs1);
        let shamt = w_uimm[3..0];
        var vd_h : vector(4, bits(16));
        foreach (i from 0 to 3) {
            let s1_b = s1[(i*8+7)..(i*8)];
            vd_h[i] = zero_extend(16, s1_b) << shamt;
        };
        X(rd_p*2)   = vd_h[1] @ vd_h[0];
        X(rd_p*2+1) = vd_h[3] @ vd_h[2];
    }

RV32 PWSLL.B.B0:

    if (rd_p != 0x0) {
        let s1 = X(rs1);
        let shamt = X(rs2)[3..0];
        var vd_h : vector(4, bits(16));
        foreach (i from 0 to 3) {
            let s1_b = s1[(i*8+7)..(i*8)];
            vd_h[i] = zero_extend(16, s1_b) << shamt;
        };
        X(rd_p*2)   = vd_h[1] @ vd_h[0];
        X(rd_p*2+1) = vd_h[3] @ vd_h[2];
    }

RV32 PWSLAI.B:

    if (rd_p != 0x0) {
        let s1 = X(rs1);
        let shamt = w_uimm[3..0];
        var vd_h : vector(4, bits(16));
        foreach (i from 0 to 3) {
            let s1_b = s1[(i*8+7)..(i*8)];
            vd_h[i] = sign_extend(16, s1_b) << shamt;
        };
        X(rd_p*2)   = vd_h[1] @ vd_h[0];
        X(rd_p*2+1) = vd_h[3] @ vd_h[2];
    }

RV32 PWSLA.B.B0:

    if (rd_p != 0x0) {
        let s1 = X(rs1);
        let shamt = X(rs2)[3..0];
        var vd_h : vector(4, bits(16));
        foreach (i from 0 to 3) {
            let s1_b = s1[(i*8+7)..(i*8)];
            vd_h[i] = sign_extend(16, s1_b) << shamt;
        };
        X(rd_p*2)   = vd_h[1] @ vd_h[0];
        X(rd_p*2+1) = vd_h[3] @ vd_h[2];
    }

RV32 PWADD.H:

    if (rd_p != 0x0) {
        let s1 = X(rs1);
        let s2 = X(rs2);
        X(rd_p*2)   = to_bits(32, signed(s1[15..0])  + signed(s2[15..0] ));
        X(rd_p*2+1) = to_bits(32, signed(s1[31..16]) + signed(s2[31..16]));
    }

RV32 PWADDA.H:

    if (rd_p != 0x0) {
        let s1 = X(rs1);
        let s2 = X(rs2);
        X(rd_p*2) =
            to_bits(
                32, signed(X(rd_p*2)) + signed(s1[15..0]) + signed(s2[15..0]));
        X(rd_p*2+1) =
            to_bits(
                32,
                signed(X(rd_p*2+1)) + signed(s1[31..16]) + signed(s2[31..16])
            );
    }

RV32 PWADDU.H:

    if (rd_p != 0x0) {
        let s1 = X(rs1);
        let s2 = X(rs2);
        X(rd_p*2)   = to_bits(32, unsigned(s1[15..0])  + unsigned(s2[15..0] ));
        X(rd_p*2+1) = to_bits(32, unsigned(s1[31..16]) + unsigned(s2[31..16]));
    }

RV32 PWADDAU.H:

    if (rd_p != 0x0) {
        let s1 = X(rs1);
        let s2 = X(rs2);
        X(rd_p*2) =
            to_bits(
                32,
                unsigned(X(rd_p*2)) + unsigned(s1[15..0]) + unsigned(s2[15..0])
            );
        X(rd_p*2+1) =
            to_bits(
                32,
                unsigned(X(rd_p*2+1))
                    + unsigned(s1[31..16]) + unsigned(s2[31..16])
            );
    }

RV32 PWSUB.H:

    if (rd_p != 0x0) {
        let s1 = X(rs1);
        let s2 = X(rs2);
        X(rd_p*2)   = to_bits(32, signed(s1[15..0])  - signed(s2[15..0] ));
        X(rd_p*2+1) = to_bits(32, signed(s1[31..16]) - signed(s2[31..16]));
    }

RV32 PWSUBA.H:

    if (rd_p != 0x0) {
        let s1 = X(rs1);
        let s2 = X(rs2);
        X(rd_p*2) =
            to_bits(
                32, signed(X(rd_p*2)) + signed(s1[15..0]) - signed(s2[15..0]));
        X(rd_p*2+1) =
            to_bits(
                32,
                signed(X(rd_p*2+1)) + signed(s1[31..16]) - signed(s2[31..16])
            );
    }

RV32 PWSUBU.H:

    if (rd_p != 0x0) {
        let s1 = X(rs1);
        let s2 = X(rs2);
        X(rd_p*2)   = to_bits(32, unsigned(s1[15..0])  - unsigned(s2[15..0] ));
        X(rd_p*2+1) = to_bits(32, unsigned(s1[31..16]) - unsigned(s2[31..16]));
    }

RV32 PWSUBAU.H:

    if (rd_p != 0x0) {
        let s1 = X(rs1);
        let s2 = X(rs2);
        X(rd_p*2) =
            to_bits(
                32,
                unsigned(X(rd_p*2)) + unsigned(s1[15..0]) - unsigned(s2[15..0])
            );
        X(rd_p*2+1) =
            to_bits(
                32,
                unsigned(X(rd_p*2+1))
                    + unsigned(s1[31..16]) - unsigned(s2[31..16])
            );
    }

RV32 PWSLLI.H:

    if (rd_p != 0x0) {
        let s1 = X(rs1);
        let shamt = w_uimm[4..0];
        X(rd_p*2)   = zero_extend(32, s1[15..0] ) << shamt;
        X(rd_p*2+1) = zero_extend(32, s1[31..16]) << shamt;
    }

RV32 PWSLL.H.H0:

    if (rd_p != 0x0) {
        let s1 = X(rs1);
        let shamt = X(rs2)[4..0];
        X(rd_p*2)   = zero_extend(32, s1[15..0] ) << shamt;
        X(rd_p*2+1) = zero_extend(32, s1[31..16]) << shamt;
    }

RV32 PWSLAI.H:

    if (rd_p != 0x0) {
        let s1 = X(rs1);
        let shamt = w_uimm[4..0];
        X(rd_p*2)   = sign_extend(32, s1[15..0] ) << shamt;
        X(rd_p*2+1) = sign_extend(32, s1[31..16]) << shamt;
    }

RV32 PWSLA.H.H0:

    if (rd_p != 0x0) {
        let s1 = X(rs1);
        let shamt = X(rs2)[4..0];
        X(rd_p*2)   = sign_extend(32, s1[15..0] ) << shamt;
        X(rd_p*2+1) = sign_extend(32, s1[31..16]) << shamt;
    }

RV32 WADD:

    if (rd_p != 0x0) {
        let d = to_bits(64, signed(X(rs1)) + signed(X(rs2)));
        X(rd_p*2)   = d[31..0];
        X(rd_p*2+1) = d[63..32];
    }

RV32 WADDA:

    if (rd_p != 0x0) {
        var d = X(rd_p*2+1) @ X(rd_p*2);
        d = to_bits(64, signed(d) + signed(X(rs1)) + signed(X(rs2)));
        X(rd_p*2)   = d[31..0];
        X(rd_p*2+1) = d[63..32];
    }

RV32 WADDU:

    if (rd_p != 0x0) {
        let d = to_bits(64, unsigned(X(rs1)) + unsigned(X(rs2)));
        X(rd_p*2)   = d[31..0];
        X(rd_p*2+1) = d[63..32];
    }

RV32 WADDAU:

    if (rd_p != 0x0) {
        var d = X(rd_p*2+1) @ X(rd_p*2);
        d = to_bits(64, unsigned(d) + unsigned(X(rs1)) + unsigned(X(rs2)));
        X(rd_p*2)   = d[31..0];
        X(rd_p*2+1) = d[63..32];
    }

RV32 WSUB:

    if (rd_p != 0x0) {
        let d = to_bits(64, signed(X(rs1)) - signed(X(rs2)));
        X(rd_p*2)   = d[31..0];
        X(rd_p*2+1) = d[63..32];
    }

RV32 WSUBA:

    if (rd_p != 0x0) {
        var d = X(rd_p*2+1) @ X(rd_p*2);
        d = to_bits(64, signed(d) + signed(X(rs1)) - signed(X(rs2)));
        X(rd_p*2)   = d[31..0];
        X(rd_p*2+1) = d[63..32];
    }

RV32 WSUBU:

    if (rd_p != 0x0) {
        let d = to_bits(64, unsigned(X(rs1)) - unsigned(X(rs2)));
        X(rd_p*2)   = d[31..0];
        X(rd_p*2+1) = d[63..32];
    }

RV32 WSUBAU:

    if (rd_p != 0x0) {
        var d = X(rd_p*2+1) @ X(rd_p*2);
        d = to_bits(64, unsigned(d) + unsigned(X(rs1)) - unsigned(X(rs2)));
        X(rd_p*2)   = d[31..0];
        X(rd_p*2+1) = d[63..32];
    }

RV32 WSLLI:

    if (rd_p != 0x0) {
        let shamt = w_uimm[5..0];
        let d = zero_extend(64, X(rs1)) << shamt;
        X(rd_p*2)   = d[31..0];
        X(rd_p*2+1) = d[63..32];
    }

RV32 WSLL:

    if (rd_p != 0x0) {
        let shamt = X(rs2)[5..0];
        let d = zero_extend(64, X(rs1)) << shamt;
        X(rd_p*2)   = d[31..0];
        X(rd_p*2+1) = d[63..32];
    }

RV32 WSLAI:

    if (rd_p != 0x0) {
        let shamt = w_uimm[5..0];
        let d = sign_extend(64, X(rs1)) << shamt;
        X(rd_p*2)   = d[31..0];
        X(rd_p*2+1) = d[63..32];
    }

RV32 WSLA:

    if (rd_p != 0x0) {
        let shamt = X(rs2)[5..0];
        let d = sign_extend(64, X(rs1)) << shamt;
        X(rd_p*2)   = d[31..0];
        X(rd_p*2+1) = d[63..32];
    }

------------------------------------------------------------------------------

RV32 WZIP8P:

    if (rd_p != 0x0) {
        let s1 = X(rs1);
        let s2 = X(rs2);
        X(rd_p*2)   = s2[15..8]  @ s1[15..8]  @ s2[7..0]   @ s1[7..0];
        X(rd_p*2+1) = s2[31..24] @ s1[31..24] @ s2[23..16] @ s1[23..16];
    }

RV32 WZIP16P:

    if (rd_p != 0x0) {
        let s1 = X(rs1);
        let s2 = X(rs2);
        X(rd_p*2)   = s2[15..0]  @ s1[15..0];
        X(rd_p*2+1) = s2[31..16] @ s1[31..16];
    }

------------------------------------------------------------------------------

RV32 PLI.DB, PLI.DH, PLUI.DH:

    For these instructions, the function of

        P<op>.D<s> rd,imm    // only even destination register number allowed

    is the same as two instructions:

        P<op>.<s> rd,imm     // the even destination register
        P<op>.<s> rd+,imm    // the odd destination register

    See the introduction for the precise meaning of "rd+".

RV32 PADD.DB, PSUB.DB, PSADD.DB, PSADDU.DB, PSSUB.DB, PSSUBU.DB, PAADD.DB,
 PAADDU.DB, PASUB.DB, PASUBU.DB, PDIF.DB, PDIFU.DB, PADD.DH, PSUB.DH,
 PSADD.DH, PSADDU.DH, PSSUB.DH, PSSUBU.DH, PAADD.DH, PAADDU.DH, PASUB.DH,
 PASUBU.DH, PSH1ADD.DH, PSSH1SADD.DH, PDIF.DH, PDIFU.DH:

    For these instructions, the function of

        P<op>.D<s> rd,rs1,rs2     // only even register numbers allowed

    is the same as two instructions:

        P<op>.<s> rd,rs1,rs2      // the even registers
        P<op>.<s> rd+,rs1+,rs2+   // the odd registers

    See the introduction for the precise meaning of "rd+", "rs1+", and
    "rs2+".

RV32 PAS.DHX, PSA.DHX, PSAS.DHX, PSSA.DHX, PAAS.DHX, PASA.DHX:

    For these instructions, the function of

        P<op>.DHX rd,rs1,rs2      // only even register numbers allowed

    is the same as two instructions:

        P<op>.HX rd,rs1,rs2       // the even registers
        P<op>.HX rd+,rs1+,rs2+    // the odd registers

    See the introduction for the precise meaning of "rd+", "rs1+", and
    "rs2+".

RV32 PSABS.DB, PSABS.DH:

    For these instructions, the function of

        PSABS.D<s> rd,rs1         // only even register numbers allowed

    is the same as two instructions:

        PSABS.<s> rd,rs1          // the even registers
        PSABS.<s> rd+,rs1+        // the odd registers

    See the introduction for the precise meaning of "rd+" and "rs1+".

RV32 PADD.DW, PSUB.DW, PSADD.DW, PSADDU.DW, PSSUB.DW, PSSUBU.DW, PAADD.DW,
 PAADDU.DW, PASUB.DW, PASUBU.DW, PSH1ADD.DW, PSSH1SADD.DW:

    For these instructions, the function of

        P<op>.DW rd,rs1,rs2       // only even register numbers allowed

    is the same as two instructions:

        <op> rd,rs1,rs2           // the even registers
        <op> rd+,rs1+,rs2+        // the odd registers

    See the introduction for the precise meaning of "rd+", "rs1+", and
    "rs2+".

------------------------------------------------------------------------------

RV32 PREDSUM.DB:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    X(rd) =
        to_bits(
            32,
            signed(X(rs2)) + signed(s1[7..0]) + signed(s1[15..8])
                + signed(s1[23..16]) + signed(s1[31..24])
                + signed(s1[39..32]) + signed(s1[47..40])
                + signed(s1[55..48]) + signed(s1[63..56])
        );

RV32 PREDSUMU.DB:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    X(rd) =
        to_bits(
            32,
            unsigned(X(rs2)) + unsigned(s1[7..0]) + unsigned(s1[15..8])
                + unsigned(s1[23..16]) + unsigned(s1[31..24])
                + unsigned(s1[39..32]) + unsigned(s1[47..40])
                + unsigned(s1[55..48]) + unsigned(s1[63..56])
        );

RV32 PREDSUM.DH:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    X(rd) =
        to_bits(
            32,
            signed(X(rs2)) + signed(s1[15..0]) + signed(s1[31..16])
                + signed(s1[47..32]) + signed(s1[63..48])
        );

RV32 PREDSUMU.DH:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    X(rd) =
        to_bits(
            32,
            unsigned(X(rs2)) + unsigned(s1[15..0]) + unsigned(s1[31..16])
                + unsigned(s1[47..32]) + unsigned(s1[63..48])
        );

------------------------------------------------------------------------------

RV32 PSLLI.DB, PSRLI.DB, PSRAI.DB, PSATI.DH, PUSATI.DH, PSLLI.DH, PSRLI.DH,
 PSRAI.DH, PSSLAI.DH, PSRARI.DH:

    For these instructions, the function of

        P<op>.D<s> rd,rs1,imm     // only even register numbers allowed

    is the same as two instructions:

        P<op>.<s> rd,rs1,imm      // the even registers
        P<op>.<s> rd+,rs1+,imm    // the odd registers

    See the introduction for the precise meaning of "rd+" and "rs1+".

RV32 PMIN.DB, PMINU.DB, PMAX.DB, PMAXU.DB, PMSEQ.DB, PMSLT.DB, PMSLTU.DB,
 PMIN.DH, PMINU.DH, PMAX.DH, PMAXU.DH, PMSEQ.DH, PMSLT.DH, PMSLTU.DH:

    For these instructions, the function of

        P<op>.D<s> rd,rs1,rs2     // only even register numbers allowed

    is the same as two instructions:

        P<op>.<s> rd,rs1,rs2      // the even registers
        P<op>.<s> rd+,rs1+,rs2+   // the odd registers

    See the introduction for the precise meaning of "rd+", "rs1+", and
    "rs2+".

RV32 PSEXTB.DH:

    The function of

        PSEXTB.DH rd,rs1          // only even register numbers allowed

    is the same as two instructions:

        PSEXTB.H rd,rs1           // the even registers
        PSEXTB.H rd+,rs1+         // the odd registers

    See the introduction for the precise meaning of "rd+" and "rs1+".

RV32 PSEXTB.DW, PSEXTH.DW:

    For these instructions, the function of

        PSEXT<s>.DW rd,rs1        // only even register numbers allowed

    is the same as two instructions:

        SEXT.<s> rd,rs1           // the even registers
        SEXT.<s> rd+,rs1+         // the odd registers

    See the introduction for the precise meaning of "rd+" and "rs1+".

RV32 PSATI.DW, PUSATI.DW, PSLLI.DW, PSRLI.DW, PSRAI.DW, PSSLAI.DW, PSRARI.DW:

    For these instructions, the function of

        P<op>.DW rd,rs1,imm       // only even register numbers allowed

    is the same as two instructions:

        <op> rd,rs1,imm           // the even registers
        <op> rd+,rs1+,imm         // the odd registers

    See the introduction for the precise meaning of "rd+" and "rs1+".

RV32 PMIN.DW, PMINU.DW, PMAX.DW, PMAXU.DW, PMSEQ.DW, PMSLT.DW, PMSLTU.DW:

    For these instructions, the function of

        P<op>.DW rd,rs1,rs2       // only even register numbers allowed

    is the same as two instructions:

        <op> rd,rs1,rs2           // the even registers
        <op> rd+,rs1+,rs2+        // the odd registers

    See the introduction for the precise meaning of "rd+", "rs1+", and
    "rs2+".

------------------------------------------------------------------------------

RV32 PADD.DB.B0, PSLL.DB.B0, PSRL.DB.B0, PSRA.DB.B0, PADD.DH.H0, PSLL.DH.H0,
 PSRL.DH.H0, PSRA.DH.H0, PSSHA.DH.H0, PSSHAR.DH.H0:

    For these instructions, the function of

        P<op>.D<s>.<s>0 rd,rs1,rs2    // only even register numbers allowed
                                      //  for rd and rs1

    is the same as two instructions:

        P<op>.<s>.<s>0 rd,rs1,rs2     // the even registers for rd and rs1
        P<op>.<s>.<s>0 rd+,rs1+,rs2   // the odd registers for rd and rs1

    See the introduction for the precise meaning of "rd+" and "rs1+".

RV32 PADD.DW.W, PSLL.DW.W, PSRL.DW.W, PSRA.DW.W, PSSHA.DW.W, PSSHAR.DW.W:

    For these instructions, the function of

        P<op>.DW.W rd,rs1,rs2     // only even register numbers allowed for
                                  //  rd and rs1

    is the same as two instructions:

        <op> rd,rs1,rs2           // the even registers for rd and rs1
        <op> rd+,rs1+,rs2         // the odd registers for rd and rs1

    See the introduction for the precise meaning of "rd+" and "rs1+".

------------------------------------------------------------------------------

RV32 PPACK.DH, PPACKBT.DH, PPACKTB.DH, PPACKT.DH:

    For these instructions, the function of

        P<op>.DH rd,rs1,rs2       // only even register numbers allowed

    is the same as two instructions:

        P<op>.H rd,rs1,rs2        // the even registers
        P<op>.H rd+,rs1+,rs2+     // the odd registers

    See the introduction for the precise meaning of "rd+", "rs1+", and
    "rs2+".

RV32 PPACK.DW, PPACKBT.DW, PPACKTB.DW, PPACKT.DW:

    For these instructions, the function of

        P<op>.DW rd,rs1,rs2       // only even register numbers allowed

    is the same as two instructions:

        <op> rd,rs1,rs2           // the even registers
        <op> rd+,rs1+,rs2+        // the odd registers

    See the introduction for the precise meaning of "rd+", "rs1+", and
    "rs2+".

------------------------------------------------------------------------------

RV32 PNSRLI.B:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = w_uimm[3..0];
    var d : bits(32);
    foreach (i from 0 to 3) {
        let s1_h = s1[(i*16+15)..(i*16)];
        d[(i*8+7)..(i*8)] = (s1_h >> shamt)[7..0];
    }
    X(rd) = d;

RV32 PNSRL.B.B0:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = X(rs2)[3..0];
    var d : bits(32);
    foreach (i from 0 to 3) {
        let s1_h = s1[(i*16+15)..(i*16)];
        d[(i*8+7)..(i*8)] = (s1_h >> shamt)[7..0];
    }
    X(rd) = d;

RV32 PNSRAI.B:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = w_uimm[3..0];
    var d : bits(32);
    foreach (i from 0 to 3) {
        let s1_h = s1[(i*16+15)..(i*16)];
        d[(i*8+7)..(i*8)] = (sign_extend(24, s1_h) >> shamt)[7..0];
    }
    X(rd) = d;

RV32 PNSRA.B.B0:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = X(rs2)[3..0];
    var d : bits(32);
    foreach (i from 0 to 3) {
        let s1_h = s1[(i*16+15)..(i*16)];
        d[(i*8+7)..(i*8)] = (sign_extend(24, s1_h) >> shamt)[7..0];
    }
    X(rd) = d;

RV32 PNSRARI.B:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = w_uimm[3..0];
    var d : bits(32);
    foreach (i from 0 to 3) {
        let s1_h = s1[(i*16+15)..(i*16)];
        let shx : bits(9) = ((sign_extend(24, s1_h) @ 0b0) >> shamt)[8..0];
        d[(i*8+7)..(i*8)] = (shx + 1)[8..1];
    }
    X(rd) = d;

RV32 PNSRAR.B.B0:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = X(rs2)[3..0];
    var d : bits(32);
    foreach (i from 0 to 3) {
        let s1_h = s1[(i*16+15)..(i*16)];
        let shx : bits(9) = ((sign_extend(24, s1_h) @ 0b0) >> shamt)[8..0];
        d[(i*8+7)..(i*8)] = (shx + 1)[8..1];
    }
    X(rd) = d;

RV32 PNCLIPI.B:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = w_uimm[3..0];
    var d : bits(32);
    foreach (i from 0 to 3) {
        let s1_h = s1[(i*16+15)..(i*16)];
        let shx : bits(16) = (sign_extend(32, s1_h) >> shamt)[15..0];
        d[(i*8+7)..(i*8)] =
            if (shx <_s 0xFF80) then 0x80
                else if (shx >_s 0x007F) then 0x7F else shx[7..0];
    }
    X(rd) = d;

RV32 PNCLIP.B.B0:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = X(rs2)[3..0];
    var d : bits(32);
    foreach (i from 0 to 3) {
        let s1_h = s1[(i*16+15)..(i*16)];
        let shx : bits(16) = (sign_extend(32, s1_h) >> shamt)[15..0];
        d[(i*8+7)..(i*8)] =
            if (shx <_s 0xFF80) then 0x80
                else if (shx >_s 0x007F) then 0x7F else shx[7..0];
    }
    X(rd) = d;

RV32 PNCLIPRI.B:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = w_uimm[3..0];
    var d : bits(32);
    foreach (i from 0 to 3) {
        let s1_h = s1[(i*16+15)..(i*16)];
        let shx : bits(17) = ((sign_extend(32, s1_h) @ 0b0) >> shamt)[16..0];
        let round_shx : bits(16) = (shx + 1)[16..1];
        d[(i*8+7)..(i*8)] =
            if (round_shx <_s 0xFF80) then 0x80
                else if (round_shx >_s 0x007F) then 0x7F else round_shx[7..0];
    }
    X(rd) = d;

RV32 PNCLIPR.B.B0:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = X(rs2)[3..0];
    var d : bits(32);
    foreach (i from 0 to 3) {
        let s1_h = s1[(i*16+15)..(i*16)];
        let shx : bits(17) = ((sign_extend(32, s1_h) @ 0b0) >> shamt)[16..0];
        let round_shx : bits(16) = (shx + 1)[16..1];
        d[(i*8+7)..(i*8)] =
            if (round_shx <_s 0xFF80) then 0x80
                else if (round_shx >_s 0x007F) then 0x7F else round_shx[7..0];
    }
    X(rd) = d;

RV32 PNCLIPIU.B:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = w_uimm[3..0];
    var d : bits(32);
    foreach (i from 0 to 3) {
        let s1_h = s1[(i*16+15)..(i*16)];
        let shx = s1_h >> shamt;
        d[(i*8+7)..(i*8)] = if (shx >_u 0x00FF) then 0xFF else shx[7..0];
    }
    X(rd) = d;

RV32 PNCLIPU.B.B0:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = X(rs2)[3..0];
    var d : bits(32);
    foreach (i from 0 to 3) {
        let s1_h = s1[(i*16+15)..(i*16)];
        let shx = s1_h >> shamt;
        d[(i*8+7)..(i*8)] = if (shx >_u 0x00FF) then 0xFF else shx[7..0];
    }
    X(rd) = d;

RV32 PNCLIPRIU.B:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = w_uimm[3..0];
    var d : bits(32);
    foreach (i from 0 to 3) {
        let s1_h = s1[(i*16+15)..(i*16)];
        let shx : bits(17) = (s1_h @ 0b0) >> shamt;
        let round_shx : bits(16) = (shx + 1)[16..1];
        d[(i*8+7)..(i*8)] =
            if (round_shx >_u 0x00FF) then 0xFF else round_shx[7..0];
    }
    X(rd) = d;

RV32 PNCLIPRU.B.B0:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = X(rs2)[3..0];
    var d : bits(32);
    foreach (i from 0 to 3) {
        let s1_h = s1[(i*16+15)..(i*16)];
        let shx : bits(17) = (s1_h @ 0b0) >> shamt;
        let round_shx : bits(16) = (shx + 1)[16..1];
        d[(i*8+7)..(i*8)] =
            if (round_shx >_u 0x00FF) then 0xFF else round_shx[7..0];
    }
    X(rd) = d;

RV32 PNSRLI.H:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = w_uimm[4..0];
    var d : bits(32);
    d[15..0]  = (s1[31..0]  >> shamt)[15..0];
    d[31..16] = (s1[63..32] >> shamt)[15..0];
    X(rd) = d;

RV32 PNSRL.H.H0:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = X(rs2)[4..0];
    var d : bits(32);
    d[15..0]  = (s1[31..0]  >> shamt)[15..0];
    d[31..16] = (s1[63..32] >> shamt)[15..0];
    X(rd) = d;

RV32 PNSRAI.H:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = w_uimm[4..0];
    var d : bits(32);
    d[15..0]  = (sign_extend(48, s1[31..0]))  >> shamt)[15..0];
    d[31..16] = (sign_extend(48, s1[63..32])) >> shamt)[15..0];
    X(rd) = d;

RV32 PNSRA.H.H0:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = X(rs2)[4..0];
    var d : bits(32);
    d[15..0]  = (sign_extend(48, s1[31..0]))  >> shamt)[15..0];
    d[31..16] = (sign_extend(48, s1[63..32])) >> shamt)[15..0];
    X(rd) = d;

RV32 PNSRARI.H:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = w_uimm[4..0];
    var d : bits(32);
    foreach (i from 0 to 1) {
        let s1_w = s1[(i*32+31)..(i*32)];
        let shx : bits(17) = ((sign_extend(48, s1_w) @ 0b0) >> shamt)[16..0];
        d[(i*16+15)..(i*16)] = (shx + 1)[17..1];
    }
    X(rd) = d;

RV32 PNSRAR.H.H0:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = X(rs2)[4..0];
    var d : bits(32);
    foreach (i from 0 to 1) {
        let s1_w = s1[(i*32+31)..(i*32)];
        let shx : bits(17) = ((sign_extend(48, s1_w) @ 0b0) >> shamt)[16..0];
        d[(i*16+15)..(i*16)] = (shx + 1)[17..1];
    }
    X(rd) = d;

RV32 PNCLIPI.H:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = w_uimm[4..0];
    var d : bits(32);
    foreach (i from 0 to 1) {
        let s1_w = s1[(i*32+31)..(i*32)];
        let shx : bits(32) = (sign_extend(64, s1_w) >> shamt)[31..0];
        d[(i*16+15)..(i*16)] =
            if (shx <_s 0xFFFF8000) then 0x8000
                else if (shx >_s 0x00007FFF) then 0x7FFF else shx[15..0];
    }
    X(rd) = d;

RV32 PNCLIP.H.H0:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = X(rs2)[4..0];
    var d : bits(32);
    foreach (i from 0 to 1) {
        let s1_w = s1[(i*32+31)..(i*32)];
        let shx : bits(32) = (sign_extend(64, s1_w) >> shamt)[31..0];
        d[(i*16+15)..(i*16)] =
            if (shx <_s 0xFFFF8000) then 0x8000
                else if (shx >_s 0x00007FFF) then 0x7FFF else shx[15..0];
    }
    X(rd) = d;

RV32 PNCLIPRI.H:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = w_uimm[4..0];
    var d : bits(32);
    foreach (i from 0 to 1) {
        let s1_w = s1[(i*32+31)..(i*32)];
        let shx : bits(33) = ((sign_extend(64, s1_w) @ 0b0) >> shamt)[32..0];
        let round_shx : bits(32) = (shx + 1)[32..1];
        d[(i*16+15)..(i*16)] =
            if (round_shx <_s 0xFFFF8000) then 0x8000
                else if (round_shx >_s 0x00007FFF) then 0x7FFF
                    else round_shx[15..0];
    }
    X(rd) = d;

RV32 PNCLIPR.H.H0:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = X(rs2)[4..0];
    var d : bits(32);
    foreach (i from 0 to 1) {
        let s1_w = s1[(i*32+31)..(i*32)];
        let shx : bits(33) = ((sign_extend(64, s1_w) @ 0b0) >> shamt)[32..0];
        let round_shx : bits(32) = (shx + 1)[32..1];
        d[(i*16+15)..(i*16)] =
            if (round_shx <_s 0xFFFF8000) then 0x8000
                else if (round_shx >_s 0x00007FFF) then 0x7FFF
                    else round_shx[15..0];
    }
    X(rd) = d;

RV32 PNCLIPIU.H:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = w_uimm[4..0];
    var d : bits(32);
    foreach (i from 0 to 1) {
        let s1_w = s1[(i*32+31)..(i*32)];
        let shx = s1_w >> shamt;
        d[(i*16+15)..(i*16)] =
            if (shx >_u 0x0000FFFF) then 0xFFFF else shx[15..0];
    }
    X(rd) = d;

RV32 PNCLIPU.H.H0:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = X(rs2)[4..0];
    var d : bits(32);
    foreach (i from 0 to 1) {
        let s1_w = s1[(i*32+31)..(i*32)];
        let shx = s1_w >> shamt;
        d[(i*16+15)..(i*16)] =
            if (shx >_u 0x0000FFFF) then 0xFFFF else shx[15..0];
    }
    X(rd) = d;

RV32 PNCLIPRIU.H:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = w_uimm[4..0];
    var d : bits(32);
    foreach (i from 0 to 1) {
        let s1_w = s1[(i*32+31)..(i*32)];
        let shx : bits(33) = (s1_w @ 0b0) >> shamt;
        let round_shx : bits(32) = (shx + 1)[32..1];
        d[(i*16+15)..(i*16)] =
            if (round_shx >_u 0x0000FFFF) then 0xFFFF else round_shx[15..0];
    }
    X(rd) = d;

RV32 PNCLIPRU.H.H0:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = X(rs2)[4..0];
    var d : bits(32);
    foreach (i from 0 to 1) {
        let s1_w = s1[(i*32+31)..(i*32)];
        let shx : bits(33) = (s1_w @ 0b0) >> shamt;
        let round_shx : bits(32) = (shx + 1)[32..1];
        d[(i*16+15)..(i*16)] =
            if (round_shx >_u 0x0000FFFF) then 0xFFFF else round_shx[15..0];
    }
    X(rd) = d;

RV32 NSRLI:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = w_uimm[5..0];
    X(rd) = (s1 >> shamt)[31..0];

RV32 NSRL:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = X(rs2)[5..0];
    X(rd) = (s1 >> shamt)[31..0];

RV32 NSRAI:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = w_uimm[5..0];
    X(rd) = (sign_extend(96, s1) >> shamt)[31..0];

RV32 NSRA:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = X(rs2)[5..0];
    X(rd) = (sign_extend(96, s1) >> shamt)[31..0];

RV32 NSRARI:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = w_uimm[5..0];
    let shx : bits(33) = ((sign_extend(96, s1) @ 0b0) >> shamt)[32..0];
    X(rd) = (shx + 1)[32..1];

RV32 NSRAR:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = X(rs2)[5..0];
    let shx : bits(33) = ((sign_extend(96, s1) @ 0b0) >> shamt)[32..0];
    X(rd) = (shx + 1)[32..1];

RV32 NCLIPI:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = w_uimm[5..0];
    let shx : bits(64) = (sign_extend(128, s1) >> shamt)[63..0];
    X(rd) =
        if (shx <_s 0xFFFFFFFF80000000) then 0x80000000
            else if (shx >_s 0x000000007FFFFFFF) then 0x7FFFFFFF
                else shx[31..0];

RV32 NCLIP:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = X(rs2)[5..0];
    let shx : bits(64) = (sign_extend(128, s1) >> shamt)[63..0];
    X(rd) =
        if (shx <_s 0xFFFFFFFF80000000) then 0x80000000
            else if (shx >_s 0x000000007FFFFFFF) then 0x7FFFFFFF
                else shx[31..0];

RV32 NCLIPRI:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = w_uimm[5..0];
    let shx : bits(65) = ((sign_extend(128, s1) @ 0b0) >> shamt)[64..0];
    let round_shx : bits(64) = (shx + 1)[64..1];
    X(rd) =
        if (round_shx <_s 0xFFFFFFFF80000000) then 0x80000000
            else if (round_shx >_s 0x000000007FFFFFFF) then 0x7FFFFFFF
                else round_shx[31..0];

RV32 NCLIPR:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = X(rs2)[5..0];
    let shx : bits(65) = ((sign_extend(128, s1) @ 0b0) >> shamt)[64..0];
    let round_shx : bits(64) = (shx + 1)[64..1];
    X(rd) =
        if (round_shx <_s 0xFFFFFFFF80000000) then 0x80000000
            else if (round_shx >_s 0x000000007FFFFFFF) then 0x7FFFFFFF
                else round_shx[31..0];

RV32 NCLIPIU:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = w_uimm[5..0];
    let shx = s1 >> shamt;
    X(rd) = if (shx >_u 0x00000000FFFFFFFF) then 0xFFFFFFFF else shx[31..0];

RV32 NCLIPU:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = X(rs2)[5..0];
    let shx = s1 >> shamt;
    X(rd) = if (shx >_u 0x00000000FFFFFFFF) then 0xFFFFFFFF else shx[31..0];

RV32 NCLIPRIU:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = w_uimm[5..0];
    let shx : bits(65) = (s1 @ 0b0) >> shamt;
    let round_shx : bits(64) = (shx + 1)[64..1];
    X(rd) =
        if (round_shx >_u 0x00000000FFFFFFFF) then 0xFFFFFFFF
            else round_shx[31..0];

RV32 NCLIPRU:

    let s1 : bits(64) =
        if (rs1_p == 0x0) then zeros() else X(rs1_p*2+1) @ X(rs1_p*2);
    let shamt = X(rs2)[5..0];
    let shx : bits(65) = (s1 @ 0b0) >> shamt;
    let round_shx : bits(64) = (shx + 1)[64..1];
    X(rd) =
        if (round_shx >_u 0x00000000FFFFFFFF) then 0xFFFFFFFF
            else round_shx[31..0];

------------------------------------------------------------------------------