Skip to content

Commit

Permalink
Zalrsc at 100% coverage for RV32 and RV64 with improved coverpoints
Browse files Browse the repository at this point in the history
  • Loading branch information
davidharrishmc committed Feb 23, 2025
1 parent 48a184d commit 8a4b19e
Show file tree
Hide file tree
Showing 6 changed files with 208 additions and 5 deletions.
11 changes: 11 additions & 0 deletions templates/coverage/cp_custom_lr.txt
Original file line number Diff line number Diff line change
Expand Up @@ -2,3 +2,14 @@
// Combinations of acquire and release
ignore_bins rl_noaq = {2'b01};
}
cp_custom_rd_corners : coverpoint ins.current.rd_val iff (ins.trap == 0) {
`ifdef XLEN32
bins zero = {0};
bins one = {32'b00000000000000000000000000000001};
bins max = {32'b11111111111111111111111111111111};
`else // XLEN64
bins zero = {0};
bins one = {64'b0000000000000000000000000000000000000000000000000000000000000001};
bins max = {64'b1111111111111111111111111111111111111111111111111111111111111111};
`endif
}
18 changes: 16 additions & 2 deletions templates/coverage/cp_custom_sc.txt
Original file line number Diff line number Diff line change
@@ -1,7 +1,10 @@
// Custom coverpoints for Store Conditional

cp_prev_lr : coverpoint (ins.prev.inst_name == "lr.w" | ins.prev.inst_name == "lr.d") {
// previous instruction was load reserved
cp_prev_lr : coverpoint ({ins.prev.inst_name == "lr.w", ins.prev.inst_name == "lr.d"}) {
bins lr_w = {2'b10}; // previous instruction was load reserved
`ifdef XLEN64
bins lr_d = {2'b01};
`endif
}

cp_sc_fail : coverpoint (ins.current.rd_val) {
Expand Down Expand Up @@ -30,6 +33,17 @@
`endif
wildcard ignore_bins badbin = {3'b1??};
}
cp_custom_sc_after_load : coverpoint (ins.prev.insn[14:12]) iff (ins.prev.insn[6:0] == 7'b0000011) {
// previous instruction was a store
bins lb = {3'b000};
bins lh = {3'b001};
bins lhu = {3'b101};
bins lw = {3'b010};
`ifdef XLEN64
bins lwu = {3'b110};
bins ld = {3'b011};
`endif
}
cp_custom_sc_lrsc : cross cp_prev_lr, cp_sc_fail;
cp_custom_sc_addresses : cross cp_prev_lr, cp_address_difference;

16 changes: 15 additions & 1 deletion templates/testgen/lr.d.S
Original file line number Diff line number Diff line change
Expand Up @@ -10,5 +10,19 @@
lr.d.aq t2, (t0)
lr.d.aqrl t3, (t0)


# cp_custom_rd_corners
li t4, 0x0
sd t4, 0(t0)
lr.d t1, (t0) # lr t1 = 0

li t4, 0x1
sd t4, 0(t0)
lr.d t1, (t0) # lr t1 = 1

li t4, 0x00000000FFFFFFFF
sd t4, 0(t0)
lr.d t1, (t0) # lr t1 = 00000000FFFFFFFF

li t4, 0xFFFFFFFFFFFFFFFF
sd t4, 0(t0)
lr.d t1, (t0) # lr t1 = FFFFFFFFFFFFFFFF
14 changes: 13 additions & 1 deletion templates/testgen/lr.w.S
Original file line number Diff line number Diff line change
Expand Up @@ -10,5 +10,17 @@
lr.w.aq t2, (t0)
lr.w.aqrl t3, (t0)


# cp_custom_rd_corners
li t4, 0x0
sw t4, 0(t0)
sw zero, 4(t0)
lr.w t1, (t0) # lr t1 = 0

li t4, 0x1
sw t4, 0(t0)
lr.w t1, (t0) # lr t1 = 1

li t4, 0xFFFFFFFF
sw t4, 0(t0)
lr.w t1, (t0) # lr t1 = FFFFFFFF (sign-extended in RV64)

78 changes: 77 additions & 1 deletion templates/testgen/sc.d.S
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,17 @@
lr.d t1, (t0) # load from reservation set
sc.d t1, t3, (t5) # try store conditional, should succeed if in same set
sc.d t1, t3, (t5) # try again, and it should fail this time

# for RV64, also check different size lr vs. sc
#ifdef __riscv_xlen
#if __riscv_xlen == 64
lr.w t1, (t0)
sc.d t1, t3, (t5)
#endif
#else
ERROR: __riscv_xlen not defined
#endif

addi t6, t6, 8 # increment offset
slti t5, t6, 129 # offset <= 128
bnez t5, 1b # repeat until done
Expand All @@ -60,4 +71,69 @@
lr.d t1, (t0)
sd t3, 0(t0) # store double
sc.d t5, t4, (t0) # succeeds


# cp_custom_sc_after_load
# should not care about intervening loads

lr.w t1, (t0)
lb t3, 3(t0) # load byte
sc.d t5, t4, (t0) # succeeds

lr.w t1, (t0)
lb t3, 128(t0) # load byte
sc.d t5, t4, (t0) # succeeds

lr.w t1, (t0)
lbu t3, 2(t0) # load byte unsigned
sc.d t5, t4, (t0) # succeeds

lr.w t1, (t0)
lbu t3, 128(t0) # load byte unsigned
sc.d t5, t4, (t0) # succeeds

lr.w t1, (t0)
lh t3, 2(t0) # load half
sc.d t5, t4, (t0) # succeeds

lr.w t1, (t0)
lh t3, 128(t0) # load half
sc.d t5, t4, (t0) # succeeds

lr.w t1, (t0)
lhu t3, 0(t0) # load half unsigned
sc.d t5, t4, (t0) # succeeds

lr.w t1, (t0)
lhu t3, 128(t0) # load half unsigned
sc.d t5, t4, (t0) # succeeds

lr.w t1, (t0)
lw t3, 0(t0) # load word
sc.d t5, t4, (t0) # succeeds

lr.w t1, (t0)
lw t3, 128(t0) # load word
sc.d t5, t4, (t0) # succeeds

#ifdef __riscv_xlen
#if __riscv_xlen == 64
lr.w t1, (t0)
lwu t3, 0(t0) # load word unsigned
sc.d t5, t4, (t0) # succeeds

lr.w t1, (t0)
lwu t3, 128(t0) # load word unsigned
sc.d t5, t4, (t0) # succeeds

lr.w t1, (t0)
ld t3, 0(t0) # load double
sc.d t5, t4, (t0) # succeeds

lr.w t1, (t0)
ld t3, 128(t0) # load double
sc.d t5, t4, (t0) # succeeds

#endif
#else
ERROR: __riscv_xlen not defined
#endif
76 changes: 76 additions & 0 deletions templates/testgen/sc.w.S
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,17 @@
lr.w t1, (t0) # load from reservation set
sc.w t1, t3, (t5) # try store conditional, should succeed if in same set
sc.w t1, t3, (t5) # try again, and it should fail this time

# for RV64, also check different size lr vs. sc
#ifdef __riscv_xlen
#if __riscv_xlen == 64
lr.d t1, (t0)
sc.w t1, t3, (t5)
#endif
#else
ERROR: __riscv_xlen not defined
#endif

addi t6, t6, 4 # increment offset
slti t5, t6, 129 # offset <= 128
bnez t5, 1b # repeat until done
Expand Down Expand Up @@ -58,3 +69,68 @@
ERROR: __riscv_xlen not defined
#endif

# cp_custom_sc_after_load
# should not care about intervening loads

lr.w t1, (t0)
lb t3, 3(t0) # load byte
sc.w t5, t4, (t0) # succeeds

lr.w t1, (t0)
lb t3, 128(t0) # load byte
sc.w t5, t4, (t0) # succeeds

lr.w t1, (t0)
lbu t3, 2(t0) # load byte unsigned
sc.w t5, t4, (t0) # succeeds

lr.w t1, (t0)
lbu t3, 128(t0) # load byte unsigned
sc.w t5, t4, (t0) # succeeds

lr.w t1, (t0)
lh t3, 2(t0) # load half
sc.w t5, t4, (t0) # succeeds

lr.w t1, (t0)
lh t3, 128(t0) # load half
sc.w t5, t4, (t0) # succeeds

lr.w t1, (t0)
lhu t3, 0(t0) # load half unsigned
sc.w t5, t4, (t0) # succeeds

lr.w t1, (t0)
lhu t3, 128(t0) # load half unsigned
sc.w t5, t4, (t0) # succeeds

lr.w t1, (t0)
lw t3, 0(t0) # load word
sc.w t5, t4, (t0) # succeeds

lr.w t1, (t0)
lw t3, 128(t0) # load word
sc.w t5, t4, (t0) # succeeds

#ifdef __riscv_xlen
#if __riscv_xlen == 64
lr.w t1, (t0)
lwu t3, 0(t0) # load word unsigned
sc.w t5, t4, (t0) # succeeds

lr.w t1, (t0)
lwu t3, 128(t0) # load word unsigned
sc.w t5, t4, (t0) # succeeds

lr.w t1, (t0)
ld t3, 0(t0) # load double
sc.w t5, t4, (t0) # succeeds

lr.w t1, (t0)
ld t3, 128(t0) # load double
sc.w t5, t4, (t0) # succeeds

#endif
#else
ERROR: __riscv_xlen not defined
#endif

0 comments on commit 8a4b19e

Please sign in to comment.