diff --git a/model/riscv_insts_zba.sail b/model/riscv_insts_zba.sail index 2e474defd..980f911b1 100644 --- a/model/riscv_insts_zba.sail +++ b/model/riscv_insts_zba.sail @@ -71,8 +71,8 @@ /* ****************************************************************** */ union clause ast = RISCV_SLLIUW : (bits(6), regidx, regidx) -mapping clause encdec = RISCV_SLLIUW(shamt, rs1, rd) if haveZba() & sizeof(xlen) == 64 - <-> 0b000010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0011011 if haveZba() & sizeof(xlen) == 64 +mapping clause encdec = RISCV_SLLIUW(shamt, rs1, rd) if (haveZba() | haveBExt()) & sizeof(xlen) == 64 + <-> 0b000010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0011011 if (haveZba() | haveBExt()) & sizeof(xlen) == 64 mapping clause assembly = RISCV_SLLIUW(shamt, rs1, rd) <-> "slli.uw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_6(shamt) @@ -87,17 +87,17 @@ function clause execute (RISCV_SLLIUW(shamt, rs1, rd)) = { /* ****************************************************************** */ union clause ast = ZBA_RTYPEUW : (regidx, regidx, regidx, bropw_zba) -mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_ADDUW) if haveZba() & sizeof(xlen) == 64 - <-> 0b0000100 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011 if haveZba() & sizeof(xlen) == 64 +mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_ADDUW) if (haveZba() | haveBExt()) & sizeof(xlen) == 64 + <-> 0b0000100 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011 if (haveZba() | haveBExt()) & sizeof(xlen) == 64 -mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_SH1ADDUW) if haveZba() & sizeof(xlen) == 64 - <-> 0b0010000 @ rs2 @ rs1 @ 0b010 @ rd @ 0b0111011 if haveZba() & sizeof(xlen) == 64 +mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_SH1ADDUW) if (haveZba() | haveBExt()) & sizeof(xlen) == 64 + <-> 0b0010000 @ rs2 @ rs1 @ 0b010 @ rd @ 0b0111011 if (haveZba() | haveBExt()) & sizeof(xlen) == 64 -mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_SH2ADDUW) if haveZba() & sizeof(xlen) == 64 - <-> 0b0010000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0111011 if haveZba() & sizeof(xlen) == 64 +mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_SH2ADDUW) if (haveZba() | haveBExt()) & sizeof(xlen) == 64 + <-> 0b0010000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0111011 if (haveZba() | haveBExt()) & sizeof(xlen) == 64 -mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_SH3ADDUW) if haveZba() & sizeof(xlen) == 64 - <-> 0b0010000 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0111011 if haveZba() & sizeof(xlen) == 64 +mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_SH3ADDUW) if (haveZba() | haveBExt()) & sizeof(xlen) == 64 + <-> 0b0010000 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0111011 if (haveZba() | haveBExt()) & sizeof(xlen) == 64 mapping zba_rtypeuw_mnemonic : bropw_zba <-> string = { RISCV_ADDUW <-> "add.uw", @@ -126,12 +126,12 @@ function clause execute (ZBA_RTYPEUW(rs2, rs1, rd, op)) = { /* ****************************************************************** */ union clause ast = ZBA_RTYPE : (regidx, regidx, regidx, brop_zba) -mapping clause encdec = ZBA_RTYPE(rs2, rs1, rd, RISCV_SH1ADD) if haveZba() - <-> 0b0010000 @ rs2 @ rs1 @ 0b010 @ rd @ 0b0110011 if haveZba() -mapping clause encdec = ZBA_RTYPE(rs2, rs1, rd, RISCV_SH2ADD) if haveZba() - <-> 0b0010000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if haveZba() -mapping clause encdec = ZBA_RTYPE(rs2, rs1, rd, RISCV_SH3ADD) if haveZba() - <-> 0b0010000 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0110011 if haveZba() +mapping clause encdec = ZBA_RTYPE(rs2, rs1, rd, RISCV_SH1ADD) if haveZba() | haveBExt() + <-> 0b0010000 @ rs2 @ rs1 @ 0b010 @ rd @ 0b0110011 if haveZba() | haveBExt() +mapping clause encdec = ZBA_RTYPE(rs2, rs1, rd, RISCV_SH2ADD) if haveZba() | haveBExt() + <-> 0b0010000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if haveZba() | haveBExt() +mapping clause encdec = ZBA_RTYPE(rs2, rs1, rd, RISCV_SH3ADD) if haveZba() | haveBExt() + <-> 0b0010000 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0110011 if haveZba() | haveBExt() mapping zba_rtype_mnemonic : brop_zba <-> string = { RISCV_SH1ADD <-> "sh1add", diff --git a/model/riscv_insts_zbb.sail b/model/riscv_insts_zbb.sail index 62e456764..4c09d92f8 100644 --- a/model/riscv_insts_zbb.sail +++ b/model/riscv_insts_zbb.sail @@ -71,8 +71,8 @@ /* ****************************************************************** */ union clause ast = RISCV_RORIW : (bits(5), regidx, regidx) -mapping clause encdec = RISCV_RORIW(shamt, rs1, rd) if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64 - <-> 0b0110000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64 +mapping clause encdec = RISCV_RORIW(shamt, rs1, rd) if (haveZbb() | haveBExt() | haveZbkb()) & sizeof(xlen) == 64 + <-> 0b0110000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 if (haveZbb() | haveBExt() | haveZbkb()) & sizeof(xlen) == 64 mapping clause assembly = RISCV_RORIW(shamt, rs1, rd) <-> "roriw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_5(shamt) @@ -87,8 +87,8 @@ function clause execute (RISCV_RORIW(shamt, rs1, rd)) = { /* ****************************************************************** */ union clause ast = RISCV_RORI : (bits(6), regidx, regidx) -mapping clause encdec = RISCV_RORI(shamt, rs1, rd) if (haveZbb() | haveZbkb()) & (sizeof(xlen) == 64 | shamt[5] == bitzero) - <-> 0b011000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if (haveZbb() | haveZbkb()) & (sizeof(xlen) == 64 | shamt[5] == bitzero) +mapping clause encdec = RISCV_RORI(shamt, rs1, rd) if (haveZbb() | haveBExt() | haveZbkb()) & (sizeof(xlen) == 64 | shamt[5] == bitzero) + <-> 0b011000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if (haveZbb() | haveBExt() | haveZbkb()) & (sizeof(xlen) == 64 | shamt[5] == bitzero) mapping clause assembly = RISCV_RORI(shamt, rs1, rd) <-> "rori" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_6(shamt) @@ -105,11 +105,11 @@ function clause execute (RISCV_RORI(shamt, rs1, rd)) = { /* ****************************************************************** */ union clause ast = ZBB_RTYPEW : (regidx, regidx, regidx, bropw_zbb) -mapping clause encdec = ZBB_RTYPEW(rs2, rs1, rd, RISCV_ROLW) if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64 - <-> 0b0110000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0111011 if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64 +mapping clause encdec = ZBB_RTYPEW(rs2, rs1, rd, RISCV_ROLW) if (haveZbb() | haveBExt() | haveZbkb()) & sizeof(xlen) == 64 + <-> 0b0110000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0111011 if (haveZbb() | haveBExt() | haveZbkb()) & sizeof(xlen) == 64 -mapping clause encdec = ZBB_RTYPEW(rs2, rs1, rd, RISCV_RORW) if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64 - <-> 0b0110000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011 if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64 +mapping clause encdec = ZBB_RTYPEW(rs2, rs1, rd, RISCV_RORW) if (haveZbb() | haveBExt() | haveZbkb()) & sizeof(xlen) == 64 + <-> 0b0110000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011 if (haveZbb() | haveBExt() | haveZbkb()) & sizeof(xlen) == 64 mapping zbb_rtypew_mnemonic : bropw_zbb <-> string = { RISCV_ROLW <-> "rolw", @@ -133,32 +133,32 @@ function clause execute (ZBB_RTYPEW(rs2, rs1, rd, op)) = { /* ****************************************************************** */ union clause ast = ZBB_RTYPE : (regidx, regidx, regidx, brop_zbb) -mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ANDN) if haveZbb() | haveZbkb() - <-> 0b0100000 @ rs2 @ rs1 @ 0b111 @ rd @ 0b0110011 if haveZbb() | haveZbkb() +mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ANDN) if haveZbb() | haveBExt() | haveZbkb() + <-> 0b0100000 @ rs2 @ rs1 @ 0b111 @ rd @ 0b0110011 if haveZbb() | haveBExt() | haveZbkb() -mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ORN) if haveZbb() | haveZbkb() - <-> 0b0100000 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0110011 if haveZbb() | haveZbkb() +mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ORN) if haveZbb() | haveBExt() | haveZbkb() + <-> 0b0100000 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0110011 if haveZbb() | haveBExt() | haveZbkb() -mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_XNOR) if haveZbb() | haveZbkb() - <-> 0b0100000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if haveZbb() | haveZbkb() +mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_XNOR) if haveZbb() | haveBExt() | haveZbkb() + <-> 0b0100000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if haveZbb() | haveBExt() | haveZbkb() -mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_MAX) if haveZbb() - <-> 0b0000101 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0110011 if haveZbb() +mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_MAX) if haveZbb() | haveBExt() + <-> 0b0000101 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0110011 if haveZbb() | haveBExt() -mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_MAXU) if haveZbb() - <-> 0b0000101 @ rs2 @ rs1 @ 0b111 @ rd @ 0b0110011 if haveZbb() +mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_MAXU) if haveZbb() | haveBExt() + <-> 0b0000101 @ rs2 @ rs1 @ 0b111 @ rd @ 0b0110011 if haveZbb() | haveBExt() -mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_MIN) if haveZbb() - <-> 0b0000101 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if haveZbb() +mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_MIN) if haveZbb() | haveBExt() + <-> 0b0000101 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if haveZbb() | haveBExt() -mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_MINU) if haveZbb() - <-> 0b0000101 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011 if haveZbb() +mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_MINU) if haveZbb() | haveBExt() + <-> 0b0000101 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011 if haveZbb() | haveBExt() -mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ROL) if haveZbb() | haveZbkb() - <-> 0b0110000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if haveZbb() | haveZbkb() +mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ROL) if haveZbb() | haveBExt() | haveZbkb() + <-> 0b0110000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if haveZbb() | haveBExt() | haveZbkb() -mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ROR) if haveZbb() | haveZbkb() - <-> 0b0110000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011 if haveZbb() | haveZbkb() +mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ROR) if haveZbb() | haveBExt() | haveZbkb() + <-> 0b0110000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011 if haveZbb() | haveBExt() | haveZbkb() mapping zbb_rtype_mnemonic : brop_zbb <-> string = { RISCV_ANDN <-> "andn", @@ -200,17 +200,17 @@ function clause execute (ZBB_RTYPE(rs2, rs1, rd, op)) = { /* ****************************************************************** */ union clause ast = ZBB_EXTOP : (regidx, regidx, extop_zbb) -mapping clause encdec = ZBB_EXTOP(rs1, rd, RISCV_SEXTB) if haveZbb() - <-> 0b0110000 @ 0b00100 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbb() +mapping clause encdec = ZBB_EXTOP(rs1, rd, RISCV_SEXTB) if haveZbb() | haveBExt() + <-> 0b0110000 @ 0b00100 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbb() | haveBExt() -mapping clause encdec = ZBB_EXTOP(rs1, rd, RISCV_SEXTH) if haveZbb() - <-> 0b0110000 @ 0b00101 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbb() +mapping clause encdec = ZBB_EXTOP(rs1, rd, RISCV_SEXTH) if haveZbb() | haveBExt() + <-> 0b0110000 @ 0b00101 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbb() | haveBExt() -mapping clause encdec = ZBB_EXTOP(rs1, rd, RISCV_ZEXTH) if haveZbb() & sizeof(xlen) == 32 - <-> 0b0000100 @ 0b00000 @ rs1 @ 0b100 @ rd @ 0b0110011 if haveZbb() & sizeof(xlen) == 32 +mapping clause encdec = ZBB_EXTOP(rs1, rd, RISCV_ZEXTH) if (haveZbb() | haveBExt()) & sizeof(xlen) == 32 + <-> 0b0000100 @ 0b00000 @ rs1 @ 0b100 @ rd @ 0b0110011 if (haveZbb() | haveBExt()) & sizeof(xlen) == 32 -mapping clause encdec = ZBB_EXTOP(rs1, rd, RISCV_ZEXTH) if haveZbb() & sizeof(xlen) == 64 - <-> 0b0000100 @ 0b00000 @ rs1 @ 0b100 @ rd @ 0b0111011 if haveZbb() & sizeof(xlen) == 64 +mapping clause encdec = ZBB_EXTOP(rs1, rd, RISCV_ZEXTH) if (haveZbb() | haveBExt()) & sizeof(xlen) == 64 + <-> 0b0000100 @ 0b00000 @ rs1 @ 0b100 @ rd @ 0b0111011 if (haveZbb() | haveBExt()) & sizeof(xlen) == 64 mapping zbb_extop_mnemonic : extop_zbb <-> string = { RISCV_SEXTB <-> "sext.b", @@ -235,11 +235,11 @@ function clause execute (ZBB_EXTOP(rs1, rd, op)) = { /* ****************************************************************** */ union clause ast = RISCV_REV8 : (regidx, regidx) -mapping clause encdec = RISCV_REV8(rs1, rd) if (haveZbb() | haveZbkb()) & sizeof(xlen) == 32 - <-> 0b011010011000 @ rs1 @ 0b101 @ rd @ 0b0010011 if (haveZbb() | haveZbkb()) & sizeof(xlen) == 32 +mapping clause encdec = RISCV_REV8(rs1, rd) if (haveZbb() | haveBExt() | haveZbkb()) & sizeof(xlen) == 32 + <-> 0b011010011000 @ rs1 @ 0b101 @ rd @ 0b0010011 if (haveZbb() | haveBExt() | haveZbkb()) & sizeof(xlen) == 32 -mapping clause encdec = RISCV_REV8(rs1, rd) if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64 - <-> 0b011010111000 @ rs1 @ 0b101 @ rd @ 0b0010011 if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64 +mapping clause encdec = RISCV_REV8(rs1, rd) if (haveZbb() | haveBExt() | haveZbkb()) & sizeof(xlen) == 64 + <-> 0b011010111000 @ rs1 @ 0b101 @ rd @ 0b0010011 if (haveZbb() | haveBExt() | haveZbkb()) & sizeof(xlen) == 64 mapping clause assembly = RISCV_REV8(rs1, rd) <-> "rev8" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) @@ -256,8 +256,8 @@ function clause execute (RISCV_REV8(rs1, rd)) = { /* ****************************************************************** */ union clause ast = RISCV_ORCB : (regidx, regidx) -mapping clause encdec = RISCV_ORCB(rs1, rd) if haveZbb() - <-> 0b001010000111 @ rs1 @ 0b101 @ rd @ 0b0010011 if haveZbb() +mapping clause encdec = RISCV_ORCB(rs1, rd) if haveZbb() | haveBExt() + <-> 0b001010000111 @ rs1 @ 0b101 @ rd @ 0b0010011 if haveZbb() | haveBExt() mapping clause assembly = RISCV_ORCB(rs1, rd) <-> "orc.b" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) @@ -276,8 +276,8 @@ function clause execute (RISCV_ORCB(rs1, rd)) = { /* ****************************************************************** */ union clause ast = RISCV_CPOP : (regidx, regidx) -mapping clause encdec = RISCV_CPOP(rs1, rd) if haveZbb() - <-> 0b011000000010 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbb() +mapping clause encdec = RISCV_CPOP(rs1, rd) if haveZbb() | haveBExt() + <-> 0b011000000010 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbb() | haveBExt() mapping clause assembly = RISCV_CPOP(rs1, rd) <-> "cpop" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) @@ -294,8 +294,8 @@ function clause execute (RISCV_CPOP(rs1, rd)) = { /* ****************************************************************** */ union clause ast = RISCV_CPOPW : (regidx, regidx) -mapping clause encdec = RISCV_CPOPW(rs1, rd) if haveZbb() & sizeof(xlen) == 64 - <-> 0b011000000010 @ rs1 @ 0b001 @ rd @ 0b0011011 if haveZbb() & sizeof(xlen) == 64 +mapping clause encdec = RISCV_CPOPW(rs1, rd) if (haveZbb() | haveBExt()) & sizeof(xlen) == 64 + <-> 0b011000000010 @ rs1 @ 0b001 @ rd @ 0b0011011 if (haveZbb() | haveBExt()) & sizeof(xlen) == 64 mapping clause assembly = RISCV_CPOPW(rs1, rd) <-> "cpopw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) @@ -312,8 +312,8 @@ function clause execute (RISCV_CPOPW(rs1, rd)) = { /* ****************************************************************** */ union clause ast = RISCV_CLZ : (regidx, regidx) -mapping clause encdec = RISCV_CLZ(rs1, rd) if haveZbb() - <-> 0b011000000000 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbb() +mapping clause encdec = RISCV_CLZ(rs1, rd) if haveZbb() | haveBExt() + <-> 0b011000000000 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbb() | haveBExt() mapping clause assembly = RISCV_CLZ(rs1, rd) <-> "clz" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) @@ -333,8 +333,8 @@ function clause execute (RISCV_CLZ(rs1, rd)) = { /* ****************************************************************** */ union clause ast = RISCV_CLZW : (regidx, regidx) -mapping clause encdec = RISCV_CLZW(rs1, rd) if haveZbb() & sizeof(xlen) == 64 - <-> 0b011000000000 @ rs1 @ 0b001 @ rd @ 0b0011011 if haveZbb() & sizeof(xlen) == 64 +mapping clause encdec = RISCV_CLZW(rs1, rd) if (haveZbb() | haveBExt()) & sizeof(xlen) == 64 + <-> 0b011000000000 @ rs1 @ 0b001 @ rd @ 0b0011011 if (haveZbb() | haveBExt()) & sizeof(xlen) == 64 mapping clause assembly = RISCV_CLZW(rs1, rd) <-> "clzw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) @@ -354,8 +354,8 @@ function clause execute (RISCV_CLZW(rs1, rd)) = { /* ****************************************************************** */ union clause ast = RISCV_CTZ : (regidx, regidx) -mapping clause encdec = RISCV_CTZ(rs1, rd) if haveZbb() - <-> 0b011000000001 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbb() +mapping clause encdec = RISCV_CTZ(rs1, rd) if haveZbb() | haveBExt() + <-> 0b011000000001 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbb() | haveBExt() mapping clause assembly = RISCV_CTZ(rs1, rd) <-> "ctz" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) @@ -375,8 +375,8 @@ function clause execute (RISCV_CTZ(rs1, rd)) = { /* ****************************************************************** */ union clause ast = RISCV_CTZW : (regidx, regidx) -mapping clause encdec = RISCV_CTZW(rs1, rd) if haveZbb() & sizeof(xlen) == 64 - <-> 0b011000000001 @ rs1 @ 0b001 @ rd @ 0b0011011 if haveZbb() & sizeof(xlen) == 64 +mapping clause encdec = RISCV_CTZW(rs1, rd) if (haveZbb() | haveBExt()) & sizeof(xlen) == 64 + <-> 0b011000000001 @ rs1 @ 0b001 @ rd @ 0b0011011 if (haveZbb() | haveBExt()) & sizeof(xlen) == 64 mapping clause assembly = RISCV_CTZW(rs1, rd) <-> "ctzw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) diff --git a/model/riscv_insts_zbs.sail b/model/riscv_insts_zbs.sail index 75a12b3c5..117f599b3 100644 --- a/model/riscv_insts_zbs.sail +++ b/model/riscv_insts_zbs.sail @@ -71,17 +71,17 @@ /* ****************************************************************** */ union clause ast = ZBS_IOP : (bits(6), regidx, regidx, biop_zbs) -mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BCLRI) if haveZbs() & (sizeof(xlen) == 64 | shamt[5] == bitzero) - <-> 0b010010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbs() & (sizeof(xlen) == 64 | shamt[5] == bitzero) +mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BCLRI) if (haveZbs() | haveBExt()) & (sizeof(xlen) == 64 | shamt[5] == bitzero) + <-> 0b010010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if (haveZbs() | haveBExt()) & (sizeof(xlen) == 64 | shamt[5] == bitzero) -mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BEXTI) if haveZbs() & (sizeof(xlen) == 64 | shamt[5] == bitzero) - <-> 0b010010 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if haveZbs() & (sizeof(xlen) == 64 | shamt[5] == bitzero) +mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BEXTI) if (haveZbs() | haveBExt()) & (sizeof(xlen) == 64 | shamt[5] == bitzero) + <-> 0b010010 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if (haveZbs() | haveBExt()) & (sizeof(xlen) == 64 | shamt[5] == bitzero) -mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BINVI) if haveZbs() & (sizeof(xlen) == 64 | shamt[5] == bitzero) - <-> 0b011010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbs() & (sizeof(xlen) == 64 | shamt[5] == bitzero) +mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BINVI) if (haveZbs() | haveBExt()) & (sizeof(xlen) == 64 | shamt[5] == bitzero) + <-> 0b011010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if (haveZbs() | haveBExt()) & (sizeof(xlen) == 64 | shamt[5] == bitzero) -mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BSETI) if haveZbs() & (sizeof(xlen) == 64 | shamt[5] == bitzero) - <-> 0b001010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbs() & (sizeof(xlen) == 64 | shamt[5] == bitzero) +mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BSETI) if (haveZbs() | haveBExt()) & (sizeof(xlen) == 64 | shamt[5] == bitzero) + <-> 0b001010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if (haveZbs() | haveBExt()) & (sizeof(xlen) == 64 | shamt[5] == bitzero) mapping zbs_iop_mnemonic : biop_zbs <-> string = { RISCV_BCLRI <-> "bclri", @@ -111,17 +111,17 @@ function clause execute (ZBS_IOP(shamt, rs1, rd, op)) = { /* ****************************************************************** */ union clause ast = ZBS_RTYPE : (regidx, regidx, regidx, brop_zbs) -mapping clause encdec = ZBS_RTYPE(rs2, rs1, rd, RISCV_BCLR) if haveZbs() - <-> 0b0100100 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if haveZbs() +mapping clause encdec = ZBS_RTYPE(rs2, rs1, rd, RISCV_BCLR) if haveZbs() | haveBExt() + <-> 0b0100100 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if haveZbs() | haveBExt() -mapping clause encdec = ZBS_RTYPE(rs2, rs1, rd, RISCV_BEXT) if haveZbs() - <-> 0b0100100 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011 if haveZbs() +mapping clause encdec = ZBS_RTYPE(rs2, rs1, rd, RISCV_BEXT) if haveZbs() | haveBExt() + <-> 0b0100100 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011 if haveZbs() | haveBExt() -mapping clause encdec = ZBS_RTYPE(rs2, rs1, rd, RISCV_BINV) if haveZbs() - <-> 0b0110100 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if haveZbs() +mapping clause encdec = ZBS_RTYPE(rs2, rs1, rd, RISCV_BINV) if haveZbs() | haveBExt() + <-> 0b0110100 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if haveZbs() | haveBExt() -mapping clause encdec = ZBS_RTYPE(rs2, rs1, rd, RISCV_BSET) if haveZbs() - <-> 0b0010100 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if haveZbs() +mapping clause encdec = ZBS_RTYPE(rs2, rs1, rd, RISCV_BSET) if haveZbs() | haveBExt() + <-> 0b0010100 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if haveZbs() | haveBExt() mapping zbs_rtype_mnemonic : brop_zbs <-> string = { RISCV_BCLR <-> "bclr", diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 3830725d1..232796d54 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -557,6 +557,7 @@ function init_sys() -> unit = { misa->MXL() = arch_to_bits(if sizeof(xlen) == 32 then RV32 else RV64); misa->A() = 0b1; /* atomics */ + misa->B() = 0b1; /* Bit-manipulation */ misa->C() = bool_to_bits(sys_enable_rvc()); /* RVC */ misa->I() = 0b1; /* base integer ISA */ misa->M() = 0b1; /* integer multiply/divide */ diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 84f708e2f..4af215c0c 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -179,6 +179,7 @@ function legalize_misa(m : Misa, v : xlenbits) -> Misa = { /* helpers to check support for various extensions. */ /* we currently don't model 'E', so always assume 'I'. */ function haveAtomics() -> bool = misa.A() == 0b1 +function haveBExt() -> bool = misa.B() == 0b1 function haveRVC() -> bool = misa.C() == 0b1 function haveMulDiv() -> bool = misa.M() == 0b1 function haveSupMode() -> bool = misa.S() == 0b1