diff options
Diffstat (limited to 'model')
| -rw-r--r-- | model/riscv_analysis.sail | 22 | ||||
| -rw-r--r-- | model/riscv_insts_base.sail | 22 |
2 files changed, 22 insertions, 22 deletions
diff --git a/model/riscv_analysis.sail b/model/riscv_analysis.sail index 34572f8..1f0f59b 100644 --- a/model/riscv_analysis.sail +++ b/model/riscv_analysis.sail @@ -112,15 +112,15 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst FENCE(pred, succ) => { ik = match (pred, succ) { - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_rw_rw), - (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_r_rw), - (_ : bits(2) @ 0b10, _ : bits(2) @ 0b10) => IK_barrier (Barrier_RISCV_r_r), - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b01) => IK_barrier (Barrier_RISCV_rw_w), - (_ : bits(2) @ 0b01, _ : bits(2) @ 0b01) => IK_barrier (Barrier_RISCV_w_w), - (_ : bits(2) @ 0b01, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_w_rw), - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b10) => IK_barrier (Barrier_RISCV_rw_r), - (_ : bits(2) @ 0b10, _ : bits(2) @ 0b01) => IK_barrier (Barrier_RISCV_r_w), - (_ : bits(2) @ 0b01, _ : bits(2) @ 0b10) => IK_barrier (Barrier_RISCV_w_r), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_rw_rw ()), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_r_rw ()), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b10) => IK_barrier (Barrier_RISCV_r_r ()), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b01) => IK_barrier (Barrier_RISCV_rw_w ()), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b01) => IK_barrier (Barrier_RISCV_w_w ()), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_w_rw ()), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b10) => IK_barrier (Barrier_RISCV_rw_r ()), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b01) => IK_barrier (Barrier_RISCV_r_w ()), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b10) => IK_barrier (Barrier_RISCV_w_r ()), (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => IK_simple (), @@ -131,12 +131,12 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst FENCE_TSO(pred, succ) => { ik = match (pred, succ) { - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_tso), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_tso ()), _ => internal_error("barrier type not implemented in initial_analysis") }; }, FENCEI() => { - ik = IK_simple (); // for RMEM, should morally be Barrier_RISCV_i + ik = IK_simple (); // for RMEM, should morally be (Barrier_RISCV_i ()) }, LOADRES(aq, rl, rs1, width, rd) => { if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR; diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index 14a626e..eab4bfc 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -566,15 +566,15 @@ mapping clause encdec = FENCE(pred, succ) function clause execute (FENCE(pred, succ)) = { match (pred, succ) { - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_rw_rw), - (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_r_rw), - (_ : bits(2) @ 0b10, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_r_r), - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_rw_w), - (_ : bits(2) @ 0b01, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_w_w), - (_ : bits(2) @ 0b01, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_w_rw), - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_rw_r), - (_ : bits(2) @ 0b10, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_r_w), - (_ : bits(2) @ 0b01, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_w_r), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_rw_rw ()), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_r_rw ()), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_r_r ()), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_rw_w ()), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_w_w ()), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_w_rw ()), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_rw_r ()), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_r_w ()), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_w_r ()), (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => (), @@ -619,7 +619,7 @@ mapping clause encdec = FENCE_TSO(pred, succ) function clause execute (FENCE_TSO(pred, succ)) = { match (pred, succ) { - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_tso), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_tso ()), (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => (), _ => { print("FIXME: unsupported fence"); @@ -638,7 +638,7 @@ mapping clause encdec = FENCEI() <-> 0b000000000000 @ 0b00000 @ 0b001 @ 0b00000 @ 0b0001111 /* fence.i is a nop for the memory model */ -function clause execute FENCEI() = { /* __barrier(Barrier_RISCV_i); */ RETIRE_SUCCESS } +function clause execute FENCEI() = { /* __barrier(Barrier_RISCV_i ()); */ RETIRE_SUCCESS } mapping clause assembly = FENCEI() <-> "fence.i" |