From d4fc0ac3ced52d28a1046b6fdfc45d7c8c0afd56 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 3 Feb 2020 19:11:37 +0000
Subject: Add an __instr_announce builtin in regfp.sail

Allows keeping track of which instructions actually get executed in a trace
---
 lib/regfp.sail | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'lib')

diff --git a/lib/regfp.sail b/lib/regfp.sail
index 231ccf6e..86b3cf17 100644
--- a/lib/regfp.sail
+++ b/lib/regfp.sail
@@ -170,6 +170,11 @@ val __cache_maintenance
   : forall (constant 'addrsize : Int), 'addrsize in {32, 64}.
   (cache_op_kind, int('addrsize), bits('addrsize)) -> unit
 
+val __instr_announce
+  = { ocaml: "Platform.instr_announce", c: "platform_instr_announce", _: "instr_announce" }
+  : forall 'n, 'n > 0.
+  bits('n) -> unit
+
 /*
 val __write : forall 'n, 'n > 0. (write_kind, bits(64), int('n), bits(8 * 'n)) -> bool effect {eamem,wmv}
 function __write (wk, addr, len, value) = {
-- 
cgit v1.2.3