diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index 599c0a7a4..ae1969b22 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -199,6 +199,25 @@ mapping itype_mnemonic : iop <-> string = {
 mapping clause assembly = ITYPE(imm, rs1, rd, op)
   <-> itype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_signed_12(imm)
 
+/* ****************************************************************** */
+union clause ast = LA : (regidx, bits(32))
+
+mapping clause assembly = LA(rd, imm)
+  <-> "la" ^ spc() ^ reg_name(rd) ^sep() ^ hex_bits_32(imm)
+
+function clause pseudo_of(LA(rd, imm)) = [|
+  "auipc" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_signed_20(imm[31..12]),
+  "addi" ^ spc() ^ reg_name(rd) ^ sep()  ^"x0" ^ sep() ^ hex_bits_signed_12(imm[11..0])
+|]
+
+function clause execute LA(rd, imm) = {
+  if execute(UTYPE(imm[31..12],rd,RISCV_AUIPC)) == RETIRE_SUCCESS &
+     execute(ITYPE(imm[11..0],reg_name("x0"),rd,RISCV_ADDI)) == RETIRE_SUCCESS then
+      RETIRE_SUCCESS
+  else
+      RETIRE_FAIL
+}
+
 /* ****************************************************************** */
 union clause ast = SHIFTIOP : (bits(6), regidx, regidx, sop)
 
diff --git a/model/riscv_insts_begin.sail b/model/riscv_insts_begin.sail
index 4287535c0..5162e4200 100644
--- a/model/riscv_insts_begin.sail
+++ b/model/riscv_insts_begin.sail
@@ -26,6 +26,9 @@ scattered mapping encdec
 val encdec_compressed : ast <-> bits(16)
 scattered mapping encdec_compressed
 
+val pseudo_of : ast -> list(string)
+scattered function pseudo_of
+
 /*
  * We declare the ILLEGAL/C_ILLEGAL ast clauses here instead of in
  * riscv_insts_end, so that model extensions can make use of them.
diff --git a/model/riscv_insts_end.sail b/model/riscv_insts_end.sail
index 728c21e43..d361f9d41 100644
--- a/model/riscv_insts_end.sail
+++ b/model/riscv_insts_end.sail
@@ -9,6 +9,7 @@
 /* Put the illegal instructions last to use their wildcard match. */
 
 /* ****************************************************************** */
+function clause pseudo_of(s) = [|"illegal"|]
 
 mapping clause encdec = ILLEGAL(s) <-> s
 
@@ -27,6 +28,7 @@ mapping clause assembly = C_ILLEGAL(s) <-> "c.illegal" ^ spc() ^ hex_bits_16(s)
 /* ****************************************************************** */
 
 /* End definitions */
+end pseudo_of
 end extension
 end extensionEnabled
 end ast
diff --git a/model/riscv_insts_vext_arith.sail b/model/riscv_insts_vext_arith.sail
index b351b01bb..d36c7b8c3 100644
--- a/model/riscv_insts_vext_arith.sail
+++ b/model/riscv_insts_vext_arith.sail
@@ -517,6 +517,21 @@ mapping vxtype_mnemonic : vxfunct6 <-> string = {
 mapping clause assembly = VXTYPE(funct6, vm, vs2, rs1, vd)
   <-> vxtype_mnemonic(funct6) ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ reg_name(rs1) ^ maybe_vmask(vm)
 
+/* ******************************************************************************* */
+union clause ast = VNEG : (regidx, regidx)
+
+mapping clause assembly = VNEG(vs, vd)
+  <-> "vneg.v" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs)
+
+function clause pseudo_of(VNEG(vs, vd)) = [|
+  "vrsub.vx" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs) ^ sep() ^ "x0"
+|]
+
+function clause execute VNEG(vs, vd) = {
+  /* execute(VXTYPE(VX_VRSUB, maybe_vmask(""), vs, reg_name("x0"), vd)) */
+  RETIRE_FAIL
+}
+
 /* ************************** OPIVX (WXTYPE Narrowing) *************************** */
 /* ************** Vector Narrowing Integer Right Shift Instructions ************** */
 union clause ast = NXSTYPE : (nxsfunct6, bits(1), regidx, regidx, regidx)