add amocas operation

riscv · Jul 22, 2023 · 3b50cea · 3b50cea
1 parent 74275c9
commit 3b50cea
Showing 1 changed file with 33 additions and 20 deletions.
diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
@@ -375,20 +375,14 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
                     match (mval_high) {
                       MemException(e)  => { handle_mem_exception(addr, e); RETIRE_FAIL },
                       MemValue(loaded_high) => {
-                        let result_high : xlenbits =
-                          match (width, sizeof(xlen), op) {
-                            (AMO_DOUBLE, 32, AMOCAS) => if (loaded_high == rd_plus_one_val) then rs2_plus_one_val else loaded_high,
-                            (AMO_QUAD, 64, AMOCAS) => if (loaded_high == rd_plus_one_val) then rs2_plus_one_val else loaded_high,
-                            _ => zeros()
-                          };
                         let result : xlenbits =
                           match op {
                             AMOSWAP => rs2_val,
                             AMOADD  => rs2_val + loaded,
                             AMOXOR  => rs2_val ^ loaded,
                             AMOAND  => rs2_val & loaded,
                             AMOOR   => rs2_val | loaded,
-                            AMOCAS  => if ( loaded == rd_val & loaded_high == rd_plus_one_val ) then rs2_val else loaded,
+                            AMOCAS  => rs2_val,
 
                             /* These operations convert bitvectors to integer values using [un]signed,
                              * and back using to_bits().
@@ -398,32 +392,51 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
                             AMOMINU => to_bits(sizeof(xlen), min(unsigned(rs2_val), unsigned(loaded))),
                             AMOMAXU => to_bits(sizeof(xlen), max(unsigned(rs2_val), unsigned(loaded)))
                           };
+                        let result_high : xlenbits =
+                          match op {
+                            AMOCAS  => rs2_plus_one_val,
+                            _       => zeros(),
+                          };
+                        let cas_result : bool =
+                          match (op, sizeof(xlen), width) {
+                            (AMOCAS, 32, AMO_WORD)   => if ( loaded == rd_val ) then true else false,
+                            (AMOCAS, 32, AMO_DOUBLE) => if ( loaded == rd_val & loaded_high == rd_plus_one_val ) then true else false,
+                            (AMOCAS, 64, AMO_WORD)   => if ( loaded == rd_val ) then true else false,
+                            (AMOCAS, 64, AMO_DOUBLE) => if ( loaded == rd_val ) then true else false,
+                            (AMOCAS, 64, AMO_QUAD)   => if ( loaded == rd_val & loaded_high == rd_plus_one_val ) then true else false,
+                            (_,      _, _)           => true
+                          };
                         let rval : xlenbits = match width {
                           AMO_BYTE   => EXTS(loaded[7..0]),
                           AMO_HALF   => EXTS(loaded[15..0]),
                           AMO_WORD   => EXTS(loaded[31..0]),
                           AMO_DOUBLE => loaded,
                           AMO_QUAD   => loaded
                         };
-                        let wval : MemoryOpResult(bool) = match (width, sizeof(xlen)) {
-                          (AMO_BYTE, _)    => mem_write_value(addr, 1, result[7..0],  aq & rl, rl, true),
-                          (AMO_HALF, _)    => mem_write_value(addr, 2, result[15..0], aq & rl, rl, true),
-                          (AMO_WORD, _)    => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true),
-                          (AMO_DOUBLE, 64) => mem_write_value(addr, 8, result,        aq & rl, rl, true),
-                          (AMO_DOUBLE, 32) => mem_write_value(addr, 4, result,        aq & rl, rl, true),
-                          (AMO_QUAD,   64) => mem_write_value(addr, 8, result,        aq & rl, rl, true),
-                          _                => internal_error(__FILE__, __LINE__, "Unexpected AMO width")
+                        let rval_high : xlenbits = match width {
+                          AMO_DOUBLE => loaded_high,
+                          AMO_QUAD   => loaded_high,
+                          _          => zeros()
+                        };
+                        let wval : MemoryOpResult(bool) = match (width, sizeof(xlen), cas_result) {
+                          (AMO_BYTE,    _, true)  => mem_write_value(addr, 1, result[7..0],  aq & rl, rl, true),
+                          (AMO_HALF,    _, true)  => mem_write_value(addr, 2, result[15..0], aq & rl, rl, true),
+                          (AMO_WORD,    _, true)  => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true),
+                          (AMO_DOUBLE, 32, true)  => mem_write_value(addr, 4, result,        aq & rl, rl, true),
+                          (AMO_DOUBLE, 64, true)  => mem_write_value(addr, 8, result,        aq & rl, rl, true),
+                          (AMO_QUAD,   64, true)  => mem_write_value(addr, 8, result,        aq & rl, rl, true),
+                          _                       => MemValue(true)
                         };
                         match (wval) {
                           MemValue(true)  => {
                             let wval_high : MemoryOpResult(bool) =
-                              match (width, sizeof(xlen)) {
-                                (AMO_DOUBLE, 32) => mem_write_value(addr+4, 4, result_high, aq & rl, rl, true),
-                                (AMO_QUAD, 64)   => mem_write_value(addr+8, 8, result_high, aq & rl, rl, true),
-                                _                => MemValue(true)
+                              match (width, sizeof(xlen), cas_result) {
+                                (AMO_DOUBLE, 32, true) => mem_write_value(addr+4, 4, result_high, aq & rl, rl, true),
+                                (AMO_QUAD,   64, true) => mem_write_value(addr+8, 8, result_high, aq & rl, rl, true),
+                                _                      => MemValue(true)
                               };
                             match (wval_high) {
-                              MemValue(true)  => { X(rd) = rval; X(rd_plus_one) = loaded_high; RETIRE_SUCCESS},
+                              MemValue(true)  => { X(rd) = rval; X(rd_plus_one) = rval_high; RETIRE_SUCCESS},
                               MemValue(false) => { internal_error(__FILE__, __LINE__, "AMO got false from mem_write_value") },
                               MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }
                             }