diff options
Diffstat (limited to 'powerpc/Asm.v')
| -rw-r--r-- | powerpc/Asm.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index dbb819d1..43ddc1ed 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -168,7 +168,8 @@ Inductive instruction : Type := | Pdcbf: ireg -> ireg -> instruction (**r data cache flush *) | Pdcbi: ireg -> ireg -> instruction (**r data cache invalidate *) | Pdcbt: int -> ireg -> instruction (**r data cache block touch *) - | Pdcbtst: int -> ireg -> instruction (**r data cache block touch *) + | Pdcbtst: int -> ireg -> instruction (**r data cache block touch *) + | Pdcbtls: int -> ireg -> instruction (**r data cache block touch and lock set *) | Pdivw: ireg -> ireg -> ireg -> instruction (**r signed division *) | Pdivwu: ireg -> ireg -> ireg -> instruction (**r unsigned division *) | Peieio: instruction (**r EIEIO barrier *) @@ -874,6 +875,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pdcbi _ _ | Pdcbt _ _ | Pdcbtst _ _ + | Pdcbtls _ _ | Peieio | Pfctiw _ _ | Pfctiwz _ _ |