Move tiny-arm interfaces

Author: febyeji

instrs-user.sail

@@ -114,13 +114,22 @@ function clause execute ExclusiveOr(d, n, m) = {
 }
 
 /* Data Barrier */
-union clause ast = DataMemoryBarrier : MBReqTypes
-union clause ast = DataSynchronizationBarrier : MBReqTypes
+union clause ast = DataMemoryBarrier : (MBReqDomain, MBReqTypes)
+union clause ast = DataSynchronizationBarrier : (MBReqDomain, MBReqTypes)
 union clause ast = InstructionSynchronizationBarrier : unit
 
 val decodeDataBarrier : (bits(4), bool) -> option(ast)
 
 function decodeDataBarrier(CRm, is_sync) = {
+  let domain : MBReqDomain =
+    match CRm[3..2] {
+      0b11 => MBReqDomain_FullSystem,
+      0b10 => MBReqDomain_InnerShareable,
+      0b01 => MBReqDomain_Nonshareable,
+      0b00 => MBReqDomain_OuterShareable,
+      _ => return None()
+    };
+
   let types : MBReqTypes =
     match CRm[1..0] {
       0b01 => MBReqTypes_Reads,
@@ -130,33 +139,33 @@ function decodeDataBarrier(CRm, is_sync) = {
     };
 
   if is_sync then
-    Some(DataSynchronizationBarrier(types))
+    Some(DataSynchronizationBarrier(domain, types))
   else
-    Some(DataMemoryBarrier(types))
+    Some(DataMemoryBarrier(domain, types))
 }
 
 /* DMB */
 function clause decode (0b1101010100@0b0@0b00@0b011@0b0011@(CRm : bits(4))@0b1@0b01@0b11111) = {
   decodeDataBarrier(CRm, false)
 }
 
-function clause execute DataMemoryBarrier(types) = {
+function clause execute DataMemoryBarrier(domain, types) = {
   // Update the PC
   _PC = _PC + 4;
   // Then perform the barrier
-  dataMemoryBarrier(types);
+  dataMemoryBarrier(domain, types);
 }
 
 /* DSB */
 function clause decode (0b11010101000000110011@(CRm:bits(4))@0b100@0b11111) = {
   decodeDataBarrier(CRm, true)
 }
 
-function clause execute DataSynchronizationBarrier(types) = {
+function clause execute DataSynchronizationBarrier(domain, types) = {
   // Update the PC
   _PC = _PC + 4;
   // Then perform the barrier
-  dataSynchronizationBarrer(types)
+  dataSynchronizationBarrer(domain, types)
 }
 
 /* ISB */
@@ -205,6 +214,3 @@ function clause execute CompareAndBranch(t, offset) = {
   }
   else _PC = _PC + 4;
 }
-
-// This catch-all clause MUST be the last clause for the `decode` function.
-function clause decode(_) = { None() }

interface.sail

@@ -4,6 +4,17 @@ $include <concurrency_interface/exception.sail>
 $include <concurrency_interface/cache_op.sail>
 $include <concurrency_interface/translation.sail>
 
+scattered union ast
+
+val decode : bits(32) -> option(ast)
+scattered function decode
+
+val execute : ast -> unit
+scattered function execute
+
+// Simple top level fetch and execute loop.
+val fetch_and_execute : unit -> unit
+
 $ifdef SYSTEM_TINY_ARM
 type addr_size : Int = 56
 let addr_size' : int(56) = 56
@@ -299,8 +310,8 @@ val iFetch : (bits(addr_size), AccessDescriptor) -> bits(32)
 val rMem : (bits(addr_size), AccessDescriptor) -> bits(64)
 val wMem_Addr : bits(addr_size) -> unit
 val wMem : (bits(addr_size), bits(64), AccessDescriptor) -> unit
-val dataMemoryBarrier : MBReqTypes -> unit
-val dataSynchronizationBarrer : MBReqTypes -> unit
+val dataMemoryBarrier : (MBReqDomain, MBReqTypes) -> unit
+val dataSynchronizationBarrer : (MBReqDomain, MBReqTypes) -> unit
 val instructionSynchronizationBarrier : unit -> unit
 
 val translate_address : (bits(64), AccessDescriptor) -> option(bits(addr_size))
@@ -346,15 +357,15 @@ function wMem(addr, value, accdesc) = {
 instantiation sail_barrier with
   'barrier = Barrier
 
-function dataMemoryBarrier(types) = sail_barrier(
+function dataMemoryBarrier(domain, types) = sail_barrier(
   Barrier_DMB(struct{
-    domain = MBReqDomain_InnerShareable,
+    domain = domain,
     types = types,
     nXS = false}))
 
-function dataSynchronizationBarrer(types) = sail_barrier(
+function dataSynchronizationBarrer(domain, types) = sail_barrier(
   Barrier_DSB(struct{
-    domain = MBReqDomain_InnerShareable,
+    domain = domain,
     types = types,
     nXS = false}))
 

sail_files

@@ -3,6 +3,6 @@ interface_types.sail
 registers.sail
 interface.sail
 translation.sail
-tiny-arm.sail
-instrs-sys.sail
 instrs-user.sail
+instrs-sys.sail
+tiny-arm.sail

tiny-arm.sail

@@ -1,13 +1,6 @@
-scattered union ast
+// This catch-all clause MUST be the last clause for the `decode` function.
+function clause decode(_) = { None() }
 
-val decode : bits(32) -> option(ast)
-scattered function decode
-
-val execute : ast -> unit
-scattered function execute
-
-// Simple top level fetch and execute loop.
-val fetch_and_execute : unit -> unit
 
 function fetch_and_execute () = {
   let accdesc = create_iFetchAccessDescriptor();