diff options
Diffstat (limited to 'verilog/Asm.v')
| -rw-r--r-- | verilog/Asm.v | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/verilog/Asm.v b/verilog/Asm.v index 64ae1c32..64a835e1 100644 --- a/verilog/Asm.v +++ b/verilog/Asm.v @@ -279,6 +279,7 @@ Inductive instruction: Type := | Pmaxsd (rd: freg) (r2: freg) | Pminsd (rd: freg) (r2: freg) | Pmovb_rm (rd: ireg) (a: addrmode) + | Pmovq_rf (rd: ireg) (r1: freg) | Pmovsq_mr (a: addrmode) (rs: freg) | Pmovsq_rm (rd: freg) (a: addrmode) | Pmovsb @@ -311,6 +312,7 @@ Module Pregmap := EMap(PregEq). Definition regset := Pregmap.t val. Definition genv := Genv.t fundef unit. +Declare Scope asm. Notation "a # b" := (a b) (at level 1, only parsing) : asm. Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm. @@ -876,6 +878,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (compare_floats (rs r1) (rs r2) rs)) m | Pxorpd_f rd => Next (nextinstr_nf (rs#rd <- (Vfloat Float.zero))) m + | Pmaxsd rd r1 => + Next (nextinstr (rs#rd <- (Op.maxf rs#rd rs#r1))) m + | Pminsd rd r1 => + Next (nextinstr (rs#rd <- (Op.minf rs#rd rs#r1))) m (** Arithmetic operations over single-precision floats *) | Padds_ff rd r1 => Next (nextinstr (rs#rd <- (Val.addfs rs#rd rs#r1))) m @@ -995,9 +1001,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pfnmsub132 _ _ _ | Pfnmsub213 _ _ _ | Pfnmsub231 _ _ _ - | Pmaxsd _ _ - | Pminsd _ _ | Pmovb_rm _ _ + | Pmovq_rf _ _ | Pmovsq_rm _ _ | Pmovsq_mr _ _ | Pmovsb |