Skip to content

Commit 9c452b6

Browse files
author
Aditya Amol Kuchekar
authored
Merge branch 'act4' into fix/dry-run-and-build-plan-fixes
2 parents 578e1e6 + e664687 commit 9c452b6

112 files changed

Lines changed: 135343 additions & 107628 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

coverpoints/coverage/RISCV_instruction_sample.svh

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5952,7 +5952,7 @@
59525952
ins.add_rs2(2);
59535953
end
59545954
"amocas.d" : begin
5955-
ins.add_rd(0);
5955+
ins.add_rd_pair(0);
59565956
ins.add_rs2(1);
59575957
ins.add_rs1(2);
59585958
end
@@ -6101,7 +6101,7 @@
61016101
ins.add_rs1(2);
61026102
end
61036103
"amocas.q" : begin
6104-
ins.add_rd(0);
6104+
ins.add_rd_pair(0);
61056105
ins.add_rs2(1);
61066106
ins.add_rs1(2);
61076107
end

coverpoints/norm/Zacas.yaml

Lines changed: 27 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -3,40 +3,55 @@
33

44
normative_rule_definitions:
55
- name: Zacas_rv32_amocas-w_op
6-
coverpoint: [""]
6+
coverpoint:
7+
[
8+
"Zacas_amocas_w_cg/{cp_asm_count, cp_rs1, cp_rs2, cp_rd, cmp_rd_rs1_val_eq, cmp_rd_rs1_val_lsb, cmp_rd_rs1_val_hw}",
9+
]
710

811
- name: Zacas_rv32_amocas-d_op
9-
coverpoint: [""]
12+
coverpoint:
13+
[
14+
"Zacas_amocas_d_cg/{cp_asm_count, cp_rs1, cp_rs2, cp_rd, cmp_rd_rs1_val_eq, cmp_rd_rs1_val_lsb, cmp_rd_rs1_val_hw, cmp_rd_rs1_val_w, cmp_rd_rs1_pair_partial_val}",
15+
]
1016

1117
- name: Zacas_rv32_amocas-d_frst_pair_entry_reg_even
12-
coverpoint: [""]
18+
coverpoint: ["Zacas_amocas_d_cg/{cp_rs2_pair, cp_rd_pair}"]
1319

1420
- name: Zacas_rv32_amocas-d_rs2_frst_reg_x0
15-
coverpoint: [""]
21+
coverpoint: ["Zacas_amocas_d_cg/{cp_rs2}"]
1622

1723
- name: Zacas_rv32_amocas-d_rd_frst_reg_x0
18-
coverpoint: [""]
24+
coverpoint: ["Zacas_amocas_d_cg/{cp_rd}"]
1925

2026
- name: Zacas_rv64_amocas-w_op
21-
coverpoint: [""]
27+
coverpoint:
28+
[
29+
"Zacas_amocas_w_cg/{cp_asm_count, cp_rs1, cp_rs2, cp_rd, cmp_rd_rs1_val_eq, cmp_rd_rs1_val_lsb, cmp_rd_rs1_val_hw, cmp_rd_sign_ext}",
30+
]
2231

2332
- name: Zacas_rv64_amocas-d_op
24-
coverpoint: [""]
33+
coverpoint:
34+
[
35+
"Zacas_amocas_d_cg/{cp_asm_count, cp_rs1, cp_rs2, cp_rd, cmp_rd_rs1_val_eq, cmp_rd_rs1_val_lsb, cmp_rd_rs1_val_hw, cmp_rd_rs1_val_w}",
36+
]
2537

2638
- name: Zacas_rv64_amocas-q_op
27-
coverpoint: [""]
39+
coverpoint:
40+
[
41+
"Zacas_amocas_q_cg/{cp_asm_count, cp_rs1, cp_rs2, cp_rd, cmp_rd_rs1_val_eq, cmp_rd_rs1_val_lsb, cmp_rd_rs1_val_hw, cmp_rd_rs1_val_w, cmp_rd_rs1_pair_partial_val}",
42+
]
2843

2944
- name: Zacas_rv64_amocas-q_frst_pair_entry_reg_even
30-
coverpoint: [""]
45+
coverpoint: ["Zacas_amocas_q_cg/{cp_rs2_pair, cp_rd_pair}"]
3146

3247
- name: Zacas_rv64_amocas-q_rs2_frst_reg_x0
33-
coverpoint: [""]
48+
coverpoint: ["Zacas_amocas_q_cg/{cp_rs2}"]
3449

3550
- name: Zacas_rv64_amocas-q_rd_frst_reg_x0
36-
coverpoint: [""]
51+
coverpoint: ["Zacas_amocas_q_cg/{cp_rd}"]
3752

3853
- name: Zacas_amocas_rs1_addr_alignment
39-
coverpoint: [""]
54+
coverpoint: ["ExceptionsZaamo_cg/{cp_amo_address_misaligned}"]
4055

4156
- name: Zacas_amocas_mem_op_success_aq_rl
4257
coverpoint: [""]

coverpoints/norm/Zimop.yaml

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,13 +2,12 @@
22

33
normative_rule_definitions:
44
- name: mop_r_op
5-
# mop.r.n writes the value zero to rd. rs1 is ignored architecturally.
6-
coverpoint: ["Zimop_mop_r_cg/{cp_asm_count, cp_rs1, cp_rd, cp_rs1_edges}"]
5+
coverpoint:
6+
["Zimop_mop_r_cg/{cp_asm_count, cp_rs1, cp_rd, cp_rs1_edges, cmp_rd_rs1}"]
77
- name: mop_rr_op
8-
# mop.rr.n writes the value zero to rd. rs1 and rs2 are ignored architecturally.
98
coverpoint:
109
[
11-
"Zimop_mop_rr_cg/{cp_asm_count, cp_rs1, cp_rs2, cp_rd, cp_rs1_edges, cp_rs2_edges, cr_rs1_rs2_edges}",
10+
"Zimop_mop_rr_cg/{cp_asm_count, cp_rs1, cp_rs2, cp_rd, cp_rs1_edges, cp_rs2_edges, cmp_rd_rs1, cmp_rd_rs2, cmp_rd_rs1_rs2}",
1211
]
1312

1413
- name: Zimop_mop-r_enc

coverpoints/priv/ExceptionsZaamo_coverage.svh

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,8 @@ covergroup ExceptionsZaamo_cg with function sample(ins_t ins);
2525
wildcard bins amomaxu_w = {AMOMAXU_W};
2626
wildcard bins amomin_w = {AMOMIN_W};
2727
wildcard bins amominu_w = {AMOMINU_W};
28+
wildcard bins amocas_w = {AMOCAS_W};
29+
wildcard bins amocas_d = {AMOCAS_D};
2830
`ifdef UDB_MXLEN_64
2931
wildcard bins amoswap_d = {AMOSWAP_D};
3032
wildcard bins amoadd_d = {AMOADD_D};
@@ -35,6 +37,7 @@ covergroup ExceptionsZaamo_cg with function sample(ins_t ins);
3537
wildcard bins amomaxu_d = {AMOMAXU_D};
3638
wildcard bins amomin_d = {AMOMIN_D};
3739
wildcard bins amominu_d = {AMOMINU_D};
40+
wildcard bins amocas_q = {AMOCAS_Q};
3841
`endif
3942
`ifdef ZABHA_SUPPORTED
4043
wildcard bins amoswap_h = {AMOSWAP_H};

coverpoints/unpriv/Zacas_coverage.svh

Lines changed: 117 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,10 +24,32 @@ covergroup Zacas_amocas_w_cg with function sample(ins_t ins);
2424
ignore_bins x0 = {x0};
2525
}
2626

27+
cmp_rd_rs1_val_eq : coverpoint (ins.current.rd_val == ins.prev.rd_val) iff (ins.trap == 0) {
28+
// Compare rd current to rd previous value (which is the same as rs1 value for the current instruction)
29+
}
30+
31+
cmp_rd_rs1_val_hw : coverpoint (ins.current.rd_val[15:0] == ins.prev.rd_val[15:0]) iff (ins.trap == 0) {
32+
// Compare the lowest 16 bits of current rd value to
33+
// lowest 16 bits of previous rd value (which is the same as rs1 value for the current instruction)
34+
bins rd_equal_val_hw_rs1 = {1}; // Cases where the lowest 16 bits of rd and rs1 are equal
35+
bins rd_not_equal_val_hw_rs1 = {0}; // Cases where the lowest 16 bits of rd and rs1 are not equal
36+
}
37+
38+
cmp_rd_rs1_val_lsb : coverpoint (ins.current.rd_val[7:0] == ins.prev.rd_val[7:0]) iff (ins.trap == 0) {
39+
// Compare the least significant byte of current rd value to the
40+
// least significant byte of previous rd value (which is the same as rs1 value for the current instruction)
41+
bins rd_equal_val_lsb_rs1 = {1}; // Cases where the least significant byte of rd and rs1 are equal
42+
bins rd_not_equal_val_lsb_rs1 = {0}; // Cases where the least significant byte of rd and rs1 are not equal
43+
}
44+
2745
cmp_rd_rs2 : coverpoint ins.get_gpr_reg(ins.current.rd) iff (ins.current.rd == ins.current.rs2 & ins.trap == 0 ) {
2846
// Compare assignments of all registers
2947
}
3048

49+
cmp_rd_sign_ext : coverpoint ins.current.rd_val[31] iff (ins.trap == 0) {
50+
51+
}
52+
3153
cmp_rs1_rs2_nx0 : coverpoint ins.get_gpr_reg(ins.current.rs1) iff (ins.current.rs1 == ins.current.rs2 & ins.trap == 0 ) {
3254
// Compare assignments of all 31 registers excluding x0
3355
ignore_bins x0 = {x0};
@@ -99,12 +121,47 @@ covergroup Zacas_amocas_d_cg with function sample(ins_t ins);
99121
bins reg_pair[] = {[$:$]} with (item % 2 == 0);
100122
}
101123

124+
cmp_rd_rs1_pair_partial_val : coverpoint (
125+
(ins.current.rd_val == ins.prev.rd_val) ^
126+
(ins.current.rd_next_val == ins.prev.rd_next_val)
127+
) iff (ins.trap == 0)
128+
{
129+
// Cases where rd and rs1 have matching high or low halves but not both
130+
bins rd_pair_partial_equal_val_rs1 = {1};
131+
bins rd_pair_partial_not_equal_val_rs1 = {0};
132+
}
133+
102134
cmp_rd_rs1_rs2_nx0_pair : coverpoint ins.get_gpr_reg(ins.current.rd) iff (ins.current.rd == ins.current.rs1 & ins.current.rd == ins.current.rs2 & ins.trap == 0 ) {
103135
// Compare assignments of all even registers excluding x0
104136
ignore_bins x0 = {x0};
105137
bins reg_pair[] = {[$:$]} with (item % 2 == 0);
106138
}
107139

140+
cmp_rd_rs1_val_eq : coverpoint (ins.current.rd_val == ins.prev.rd_val) iff (ins.trap == 0) {
141+
// Compare rd current to rd previous value (which is the same as rs1 value for the current instruction)
142+
}
143+
144+
cmp_rd_rs1_val_hw : coverpoint (ins.current.rd_val[15:0] == ins.prev.rd_val[15:0]) iff (ins.trap == 0) {
145+
// Compare the lowest 16 bits of current rd value to
146+
// lowest 16 bits of previous rd value (which is the same as rs1 value for the current instruction)
147+
bins rd_equal_val_hw_rs1 = {1}; // Cases where the lowest 16 bits of rd and rs1 are equal
148+
bins rd_not_equal_val_hw_rs1 = {0}; // Cases where the lowest 16 bits of rd and rs1 are not equal
149+
}
150+
151+
cmp_rd_rs1_val_lsb : coverpoint (ins.current.rd_val[7:0] == ins.prev.rd_val[7:0]) iff (ins.trap == 0) {
152+
// Compare the least significant byte of current rd value to the
153+
// least significant byte of previous rd value (which is the same as rs1 value for the current instruction)
154+
bins rd_equal_val_lsb_rs1 = {1}; // Cases where the least significant byte of rd and rs1 are equal
155+
bins rd_not_equal_val_lsb_rs1 = {0}; // Cases where the least significant byte of rd and rs1 are not equal
156+
}
157+
158+
cmp_rd_rs1_val_w : coverpoint (ins.current.rd_val[31:0] == ins.prev.rd_val[31:0]) iff (ins.trap == 0) {
159+
// Compare the lowest 32 bits of current rd value to the
160+
// lowest 32 bits of previous rd value (which is the same as rs1 value for the current instruction)
161+
bins rd_equal_val_w_rs1 = {1}; // Cases where the lowest 32 bits of rd and rs1 are equal
162+
bins rd_not_equal_val_w_rs1 = {0}; // Cases where the lowest 32 bits of rd and rs1 are not equal
163+
}
164+
108165
cmp_rd_rs2_pair : coverpoint ins.get_gpr_reg(ins.current.rd) iff (ins.current.rd == ins.current.rs2 & ins.trap == 0 ) {
109166
// Compare assignments of all even registers
110167
bins reg_pair[] = {[$:$]} with (item % 2 == 0);
@@ -186,6 +243,31 @@ covergroup Zacas_amocas_d_cg with function sample(ins_t ins);
186243
ignore_bins x0 = {x0};
187244
}
188245

246+
cmp_rd_rs1_val_eq : coverpoint (ins.current.rd_val == ins.prev.rd_val) iff (ins.trap == 0) {
247+
// Compare rd current to rd previous value (which is the same as rs1 value for the current instruction)
248+
}
249+
250+
cmp_rd_rs1_val_hw : coverpoint (ins.current.rd_val[15:0] == ins.prev.rd_val[15:0]) iff (ins.trap == 0) {
251+
// Compare the lowest 16 bits of current rd value to
252+
// lowest 16 bits of previous rd value (which is the same as rs1 value for the current instruction)
253+
bins rd_equal_val_hw_rs1 = {1}; // Cases where the lowest 16 bits of rd and rs1 are equal
254+
bins rd_not_equal_val_hw_rs1 = {0}; // Cases where the lowest 16 bits of rd and rs1 are not equal
255+
}
256+
257+
cmp_rd_rs1_val_lsb : coverpoint (ins.current.rd_val[7:0] == ins.prev.rd_val[7:0]) iff (ins.trap == 0) {
258+
// Compare the least significant byte of current rd value to the
259+
// least significant byte of previous rd value (which is the same as rs1 value for the current instruction)
260+
bins rd_equal_val_lsb_rs1 = {1}; // Cases where the least significant byte of rd and rs1 are equal
261+
bins rd_not_equal_val_lsb_rs1 = {0}; // Cases where the least significant byte of rd and rs1 are not equal
262+
}
263+
264+
cmp_rd_rs1_val_w : coverpoint (ins.current.rd_val[31:0] == ins.prev.rd_val[31:0]) iff (ins.trap == 0) {
265+
// Compare the lowest 32 bits of current rd value to the
266+
// lowest 32 bits of previous rd value (which is the same as rs1 value for the current instruction)
267+
bins rd_equal_val_w_rs1 = {1}; // Cases where the lowest 32 bits of rd and rs1 are equal
268+
bins rd_not_equal_val_w_rs1 = {0}; // Cases where the lowest 32 bits of rd and rs1 are not equal
269+
}
270+
189271
cmp_rd_rs2 : coverpoint ins.get_gpr_reg(ins.current.rd) iff (ins.current.rd == ins.current.rs2 & ins.trap == 0 ) {
190272
// Compare assignments of all registers
191273
}
@@ -257,12 +339,47 @@ covergroup Zacas_amocas_q_cg with function sample(ins_t ins);
257339
bins reg_pair[] = {[$:$]} with (item % 2 == 0);
258340
}
259341

342+
cmp_rd_rs1_pair_partial_val : coverpoint (
343+
(ins.current.rd_val == ins.prev.rd_val) ^
344+
(ins.current.rd_next_val == ins.prev.rd_next_val)
345+
) iff (ins.trap == 0)
346+
{
347+
// Cases where rd and rs1 have matching high or low halves but not both
348+
bins rd_pair_partial_equal_val_rs1 = {1};
349+
bins rd_pair_partial_not_equal_val_rs1 = {0};
350+
}
351+
260352
cmp_rd_rs1_rs2_nx0_pair : coverpoint ins.get_gpr_reg(ins.current.rd) iff (ins.current.rd == ins.current.rs1 & ins.current.rd == ins.current.rs2 & ins.trap == 0 ) {
261353
// Compare assignments of all even registers excluding x0
262354
ignore_bins x0 = {x0};
263355
bins reg_pair[] = {[$:$]} with (item % 2 == 0);
264356
}
265357

358+
cmp_rd_rs1_val_eq : coverpoint (ins.current.rd_val == ins.prev.rd_val) iff (ins.trap == 0) {
359+
// Compare rd current to rd previous value (which is the same as rs1 value for the current instruction)
360+
}
361+
362+
cmp_rd_rs1_val_hw : coverpoint (ins.current.rd_val[15:0] == ins.prev.rd_val[15:0]) iff (ins.trap == 0) {
363+
// Compare the lowest 16 bits of current rd value to
364+
// lowest 16 bits of previous rd value (which is the same as rs1 value for the current instruction)
365+
bins rd_equal_val_hw_rs1 = {1}; // Cases where the lowest 16 bits of rd and rs1 are equal
366+
bins rd_not_equal_val_hw_rs1 = {0}; // Cases where the lowest 16 bits of rd and rs1 are not equal
367+
}
368+
369+
cmp_rd_rs1_val_lsb : coverpoint (ins.current.rd_val[7:0] == ins.prev.rd_val[7:0]) iff (ins.trap == 0) {
370+
// Compare the least significant byte of current rd value to the
371+
// least significant byte of previous rd value (which is the same as rs1 value for the current instruction)
372+
bins rd_equal_val_lsb_rs1 = {1}; // Cases where the least significant byte of rd and rs1 are equal
373+
bins rd_not_equal_val_lsb_rs1 = {0}; // Cases where the least significant byte of rd and rs1 are not equal
374+
}
375+
376+
cmp_rd_rs1_val_w : coverpoint (ins.current.rd_val[31:0] == ins.prev.rd_val[31:0]) iff (ins.trap == 0) {
377+
// Compare the lowest 32 bits of current rd value to the
378+
// lowest 32 bits of previous rd value (which is the same as rs1 value for the current instruction)
379+
bins rd_equal_val_w_rs1 = {1}; // Cases where the lowest 32 bits of rd and rs1 are equal
380+
bins rd_not_equal_val_w_rs1 = {0}; // Cases where the lowest 32 bits of rd and rs1 are not equal
381+
}
382+
266383
cmp_rd_rs2_pair : coverpoint ins.get_gpr_reg(ins.current.rd) iff (ins.current.rd == ins.current.rs2 & ins.trap == 0 ) {
267384
// Compare assignments of all even registers
268385
bins reg_pair[] = {[$:$]} with (item % 2 == 0);

0 commit comments

Comments
 (0)