From 75d50c12ee220fecf955b1626c78b78636cbca92 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 1 Sep 2015 16:44:29 +0200 Subject: Added the gcc builtin prefetch. This commit implements the gcc __builtin_prefetch in a form with all arguments for the powerpc architecture. The resulting instructions are the dcbt and dcbtst instructions in Server Category. --- powerpc/Asm.v | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'powerpc/Asm.v') 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 _ _ -- cgit