diff options
Diffstat (limited to 'etc')
| -rw-r--r-- | etc/power_header | 31 | ||||
| -rw-r--r-- | etc/regfp.sail | 24 |
2 files changed, 52 insertions, 3 deletions
diff --git a/etc/power_header b/etc/power_header new file mode 100644 index 00000000..eb01510e --- /dev/null +++ b/etc/power_header @@ -0,0 +1,31 @@ + +Copyright (c) 2015-2017 Gabriel Kerneis, Susmit Sarkar, Kathyrn Gray +Copyright (c) 2015-2017 Peter Sewell +All rights reserved. + +This software was developed by the University of Cambridge Computer +Laboratory as part of the Rigorous Engineering of Mainstream Systems +(REMS) project, funded by EPSRC grant EP/K008528/1. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions +are met: +1. Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. +2. Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in + the documentation and/or other materials provided with the + distribution. + +THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' +AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED +TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A +PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR +CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF +USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND +ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, +OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT +OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF +SUCH DAMAGE. diff --git a/etc/regfp.sail b/etc/regfp.sail index fb15310a..cc057f2e 100644 --- a/etc/regfp.sail +++ b/etc/regfp.sail @@ -32,21 +32,31 @@ typedef diafp = const union { typedef read_kind = enumerate { Read_plain; - Read_tag; Read_reserve; Read_acquire; Read_exclusive; Read_exclusive_acquire; - Read_stream + Read_stream; + Read_RISCV_acquire; + Read_RISCV_strong_acquire; + Read_RISCV_reserved; + Read_RISCV_reserved_acquire; + Read_RISCV_reserved_strong_acquire; + Read_X86_locked; } typedef write_kind = enumerate { Write_plain; - Write_tag; Write_conditional; Write_release; Write_exclusive; Write_exclusive_release; + Write_RISCV_release; + Write_RISCV_strong_release; + Write_RISCV_conditional; + Write_RISCV_conditional_release; + Write_RISCV_conditional_strong_release; + Write_X86_locked; } typedef barrier_kind = enumerate { @@ -62,6 +72,13 @@ typedef barrier_kind = enumerate { Barrier_DSB_LD; Barrier_ISB; Barrier_MIPS_SYNC; + Barrier_RISCV_rw_rw; + Barrier_RISCV_r_rw; + Barrier_RISCV_r_r; + Barrier_RISCV_rw_w; + Barrier_RISCV_w_w; + Barrier_RISCV_i; + Barrier_x86_MFENCE; } typedef trans_kind = enumerate { @@ -72,6 +89,7 @@ typedef instruction_kind = const union { (barrier_kind) IK_barrier; (read_kind) IK_mem_read; (write_kind) IK_mem_write; + (read_kind, write_kind) IK_mem_rmw; IK_cond_branch; (trans_kind) IK_trans; IK_simple |