diff options
Diffstat (limited to 'powerpc/Asm.v')
| -rw-r--r-- | powerpc/Asm.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 589d66fe..dbb819d1 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -167,6 +167,8 @@ Inductive instruction : Type := | Pcrxor: crbit -> crbit -> crbit -> instruction (**r xor between condition bits *) | 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 *) | Pdivw: ireg -> ireg -> ireg -> instruction (**r signed division *) | Pdivwu: ireg -> ireg -> ireg -> instruction (**r unsigned division *) | Peieio: instruction (**r EIEIO barrier *) @@ -870,6 +872,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pcrxor _ _ _ | Pdcbf _ _ | Pdcbi _ _ + | Pdcbt _ _ + | Pdcbtst _ _ | Peieio | Pfctiw _ _ | Pfctiwz _ _ |