From 8163278174362fb8269804a7958f6e9e7878a511 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 3 May 2019 03:33:58 +0200 Subject: getting stuck need to move offsets --- mppa_k1c/Asm.v | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'mppa_k1c/Asm.v') diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index d73d00c7..8b1c9a81 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -122,7 +122,9 @@ Inductive instruction : Type := | Psd (rs: ireg) (ra: ireg) (ofs: addressing) (**r store int64 *) | Psd_a (rs: ireg) (ra: ireg) (ofs: addressing) (**r store any64 *) | Pfss (rs: freg) (ra: ireg) (ofs: addressing) (**r store float *) - | Pfsd (rd: freg) (ra: ireg) (ofs: addressing) (**r store 64-bit float *) + | Pfsd (rs: freg) (ra: ireg) (ofs: addressing) (**r store 64-bit float *) + + | Psq (rs: gpreg_q) (ra: ireg) (ofs: addressing) (**r store 64-bit float *) (** Arith RR *) | Pmv (rd rs: ireg) (**r register move *) @@ -484,6 +486,7 @@ Definition basic_to_instruction (b: basic) := | PStoreRRRXS Asmvliw.Pfss rd ra ro => Pfss rd ra (ARegXS ro) | PStoreRRRXS Asmvliw.Pfsd rd ra ro => Pfsd rd ra (ARegXS ro) + | PStoreQRRO qrs ra ofs => Psq qrs ra (AOff ofs) end. Section RELSEM. -- cgit