Skip to content

Commit 4958b35

Browse files
mndstrmrmarnovandermaas
mndstrmr
authored and
marnovandermaas
committed
[dv/formal] Cleanup RTL for use by yosys-slang
Yosys-slang is a SystemVerilog frontend to yosys, which will be used in upcoming formal work. It takes issue with some parts of the formal flow. This commit cleans things up so that it may consume the RTL happily.
1 parent 9a50001 commit 4958b35

File tree

6 files changed

+82
-26
lines changed

6 files changed

+82
-26
lines changed

‎dv/formal/check/peek/follower.sv‎

Lines changed: 57 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -25,16 +25,16 @@ assign ex_err = `IDC.exc_req_d;
2525
assign ex_kill = `ID.wb_exception | ~`ID.controller_run;
2626
// Note that this only kills instructions because e.g. of a jump ahead of it or an exception
2727

28-
assign exc_finishing = `IDC.ctrl_fsm_cs == `ID.controller_i.FLUSH;
29-
assign wbexc_handling_irq = `IDC.ctrl_fsm_cs == `ID.controller_i.IRQ_TAKEN;
28+
assign exc_finishing = `IDC.ctrl_fsm_cs == FLUSH;
29+
assign wbexc_handling_irq = `IDC.ctrl_fsm_cs == IRQ_TAKEN;
3030

3131
assign wb_finishing = wbexc_is_wfi? wfi_will_finish:`CR.instr_done_wb;
3232

33-
assign wfi_will_finish = `IDC.ctrl_fsm_cs == `ID.controller_i.FLUSH;
33+
assign wfi_will_finish = `IDC.ctrl_fsm_cs == FLUSH;
3434

3535
assign wbexc_err = wbexc_ex_err |
3636
`IDC.wb_exception_o |
37-
((`IDC.ctrl_fsm_cs == `ID.controller_i.FLUSH) & ~wbexc_csr_pipe_flush);
37+
((`IDC.ctrl_fsm_cs == FLUSH) & ~wbexc_csr_pipe_flush);
3838
// CSR pipe flushes don't count as exceptions
3939

4040
assign wbexc_finishing =
@@ -51,7 +51,7 @@ always_comb begin
5151

5252
ex_has_branched_d = (ex_has_branched_d | `IF.branch_req) &&
5353
~ex_kill &&
54-
(`IDC.ctrl_fsm_cs == `IDC.DECODE);
54+
(`IDC.ctrl_fsm_cs == DECODE);
5555
end
5656

5757
always @(posedge clk_i or negedge rst_ni) begin
@@ -60,6 +60,58 @@ always @(posedge clk_i or negedge rst_ni) begin
6060
ex_has_compressed_instr <= 1'b0;
6161
ex_has_branched_q <= 1'b0;
6262
wbexc_csr_pipe_flush <= 1'b0;
63+
64+
// Zero initialise everything to avoid warnings
65+
wbexc_post_wX <= 32'b0;
66+
wbexc_post_wX_addr <= 5'b0;
67+
wbexc_post_wX_en <= 1'b0;
68+
wbexc_instr <= 32'b0;
69+
wbexc_decompressed_instr <= 32'b0;
70+
wbexc_compressed_illegal <= 1'b0;
71+
wbexc_ex_err <= 1'b0;
72+
wbexc_fetch_err <= 1'b0;
73+
wbexc_post_int_err <= 1'b0;
74+
wbexc_illegal <= 1'b0;
75+
wbexc_pc <= 32'b0;
76+
wbexc_is_checkable_csr <= 1'b0;
77+
wbexc_spec_mem_read_fst_rdata <= 32'b0;
78+
wbexc_spec_mem_read_snd_rdata <= 32'b0;
79+
wbexc_mem_had_snd_req <= 1'b0;
80+
ex_compressed_instr <= 32'b0;
81+
wbexc_post_pc <= 32'h0;
82+
wbexc_post_priv <= Machine;
83+
wbexc_post_mstatus <= 32'h0;
84+
wbexc_post_mie <= 32'h0;
85+
wbexc_post_mcause <= 32'h0;
86+
wbexc_post_mtval <= 32'h0;
87+
wbexc_post_mtvec <= 32'h0;
88+
wbexc_post_mscratch <= 32'h0;
89+
wbexc_post_mepc <= 32'h0;
90+
wbexc_post_mcycle <= 32'h0;
91+
wbexc_post_mshwmb <= 32'h0;
92+
wbexc_post_mshwm <= 32'h0;
93+
wbexc_post_mcounteren <= 32'h0;
94+
wbexc_post_mseccfg <= 32'h0;
95+
wbexc_dut_post_pc <= 32'h0;
96+
wbexc_dut_post_priv <= Machine;
97+
wbexc_dut_post_mstatus <= 32'h0;
98+
wbexc_dut_post_mie <= 32'h0;
99+
wbexc_dut_post_mcause <= 32'h0;
100+
wbexc_dut_post_mtval <= 32'h0;
101+
wbexc_dut_post_mtvec <= 32'h0;
102+
wbexc_dut_post_mscratch <= 32'h0;
103+
wbexc_dut_post_mepc <= 32'h0;
104+
wbexc_dut_post_mcycle <= 32'h0;
105+
wbexc_dut_post_mshwmb <= 32'h0;
106+
wbexc_dut_post_mshwm <= 32'h0;
107+
wbexc_dut_post_mcounteren <= 32'h0;
108+
wbexc_dut_post_mseccfg <= 32'h0;
109+
for (integer i = 0; i < PMPNumRegions; i++) begin
110+
wbexc_post_pmp_cfg[i] <= 32'h0;
111+
wbexc_post_pmp_addr[i] <= 32'h0;
112+
wbexc_dut_post_pmp_cfg[i] <= 32'h0;
113+
wbexc_dut_post_pmp_addr[i] <= 32'h0;
114+
end
63115
end else begin
64116
if (wbexc_finishing) begin
65117
wbexc_exists <= 1'b0;

‎dv/formal/check/peek/mem.sv‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -60,7 +60,10 @@ assign mem_req_fst_d = data_req_o & ~mem_gnt_fst_q;
6060
assign mem_req_snd_d = data_req_o & mem_gnt_fst_q;
6161

6262
always @(posedge clk_i or negedge rst_ni) begin
63-
if (~rst_ni | instr_will_progress) begin
63+
if (~rst_ni) begin
64+
mem_gnt_fst_q <= 1'b0;
65+
mem_gnt_snd_q <= 1'b0;
66+
end else if (instr_will_progress) begin
6467
mem_gnt_fst_q <= 1'b0;
6568
mem_gnt_snd_q <= 1'b0;
6669
end else begin

‎dv/formal/spec/spec_api.sv‎

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -57,8 +57,6 @@ module spec_api #(
5757
output mstatus_t mstatus_o,
5858
input logic [31:0] mcause_i,
5959
output logic [31:0] mcause_o,
60-
input logic [63:0] mcycle_i,
61-
output logic [63:0] mcycle_o,
6260
input logic [31:0] mtval_i,
6361
output logic [31:0] mtval_o,
6462
input logic [31:0] mtvec_i,
@@ -67,10 +65,6 @@ module spec_api #(
6765
output logic [31:0] mscratch_o,
6866
input logic [31:0] mepc_i,
6967
output logic [31:0] mepc_o,
70-
input logic [31:0] mshwmb_i,
71-
output logic [31:0] mshwmb_o,
72-
input logic [31:0] mshwm_i,
73-
output logic [31:0] mshwm_o,
7468
input logic [31:0] mcounteren_i,
7569
output logic [31:0] mcounteren_o,
7670

@@ -166,7 +160,12 @@ end
166160
t_Mseccfg_ent mseccfg_out;
167161
assign mseccfg_o = mseccfg_out.bits;
168162

163+
logic sail_reached_unreachable;
164+
logic [31:0] sail_reached_unreachable_loc;
165+
169166
sail_ibexspec spec_i(
167+
.sail_reached_unreachable,
168+
.sail_reached_unreachable_loc,
170169
.cur_inst_in(insn_bits),
171170
.cur_inst_out(),
172171
.cur_privilege_in(priv_i),
@@ -345,7 +344,7 @@ sail_ibexspec spec_i(
345344
.mode(main_mode)
346345
);
347346

348-
assign int_err_o = spec_i.sail_reached_unreachable |
347+
assign int_err_o = sail_reached_unreachable |
349348
spec_i.sail_have_exception |
350349
(main_result != MAINRES_OK);
351350

‎dv/formal/spec/stub.sv‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,8 @@
44
// Original author: Louis-Emile Ploix
55
// SPDX-License-Identifier: Apache-2.0
66

7+
`include "sail.sv"
8+
79
/*
810
Provides stubs (mostly) for the native functions the Sail expects to see, mostly
911
handling config stuff.

‎dv/formal/thm/ibex.proof‎

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@ lemma ibex
3939
NonCompressedMatch: have (wbexc_finishing && wbexc_instr[1:0] == 2'b11 |-> wbexc_instr == wbexc_decompressed_instr)
4040
CompressedMatch: have (ex_has_compressed_instr |-> ex_compressed_instr[15:0] == `CR.instr_rdata_c_id)
4141

42-
PostFlushNoInstr: have (`IDC.ctrl_fsm_cs == `IDC.FLUSH |=> ~`CR.instr_valid_id)
42+
PostFlushNoInstr: have (`IDC.ctrl_fsm_cs == FLUSH |=> ~`CR.instr_valid_id)
4343

4444
DecompressionIllegalIdEx: have (ex_has_compressed_instr |-> decompressed_instr_illegal == `CR.illegal_c_insn_id)
4545
DecompressionMatchIdEx: have (ex_has_compressed_instr & ~`CR.illegal_insn_id & ~`CR.illegal_c_insn_id |-> decompressed_instr == `CR.instr_rdata_id)
@@ -69,13 +69,13 @@ lemma ibex
6969

7070
RfWriteWb: have (`CR.rf_write_wb & wbexc_finishing |-> `WB.rf_we_wb_o)
7171

72-
CtrlWbexc: have (wbexc_exists |-> `IDC.ctrl_fsm_cs == `IDC.DECODE || `IDC.ctrl_fsm_cs == `IDC.FLUSH)
73-
ProgressDecode: have (instr_will_progress |-> `IDC.ctrl_fsm_cs == `IDC.DECODE)
72+
CtrlWbexc: have (wbexc_exists |-> `IDC.ctrl_fsm_cs == DECODE || `IDC.ctrl_fsm_cs == FLUSH)
73+
ProgressDecode: have (instr_will_progress |-> `IDC.ctrl_fsm_cs == DECODE)
7474

7575
BranchedProg: have (ex_has_branched_d & ~instr_will_progress |=> ex_has_branched_d | `IDC.wb_exception_o)
7676

77-
IDCFsmAny: have (`IDC.ctrl_fsm_cs inside {`IDC.RESET, `IDC.BOOT_SET, `IDC.WAIT_SLEEP, `IDC.SLEEP, `IDC.FIRST_FETCH, `IDC.DECODE, `IDC.IRQ_TAKEN, `IDC.FLUSH})
78-
IDCFsmNotBoot: have (##3 ~(`IDC.ctrl_fsm_cs inside {`IDC.RESET, `IDC.BOOT_SET}))
77+
IDCFsmAny: have (`IDC.ctrl_fsm_cs inside {RESET, BOOT_SET, WAIT_SLEEP, SLEEP, FIRST_FETCH, DECODE, IRQ_TAKEN, FLUSH})
78+
IDCFsmNotBoot: have (##3 ~(`IDC.ctrl_fsm_cs inside {RESET, BOOT_SET}))
7979

8080
MemInstrEx: have (`LSU.ls_fsm_cs != `LSU.IDLE |-> ex_is_mem_instr)
8181
MemInstrWbLoad: have (`WB.outstanding_load_wb_o |-> wbexc_is_load_instr)
@@ -207,13 +207,13 @@ lemma ibex
207207
StallNoChangeA: have (`LSU.ls_fsm_cs != `LSU.IDLE && ($past(`LSU.ls_fsm_cs) != `LSU.IDLE || $past(`LSU.lsu_req_i)) |-> $stable(`ID.rf_rdata_a_fwd))
208208
StallNoChangeB: have (data_we_o && `LSU.ls_fsm_cs != `LSU.IDLE && ($past(`LSU.ls_fsm_cs) != `LSU.IDLE || $past(`LSU.lsu_req_i)) |-> $stable(`ID.rf_rdata_b_fwd))
209209

210-
BecameDecodeIsInstrStart: have (`IDC.ctrl_fsm_cs == `IDC.DECODE && !$stable(`IDC.ctrl_fsm_cs) |-> ~`ID.instr_valid_i | `CR.instr_new_id)
211-
BecameDecodeIsEmptyWbexc: have (`IDC.ctrl_fsm_cs == `IDC.DECODE && !$stable(`IDC.ctrl_fsm_cs) |-> ~wbexc_exists)
210+
BecameDecodeIsInstrStart: have (`IDC.ctrl_fsm_cs == DECODE && !$stable(`IDC.ctrl_fsm_cs) |-> ~`ID.instr_valid_i | `CR.instr_new_id)
211+
BecameDecodeIsEmptyWbexc: have (`IDC.ctrl_fsm_cs == DECODE && !$stable(`IDC.ctrl_fsm_cs) |-> ~wbexc_exists)
212212
FetchErrIsErr: have (wbexc_fetch_err & wbexc_exists |-> wbexc_err & `IDC.instr_fetch_err)
213213

214214
# If control FSM is in `FIRST_FETCH`, then there shouldn't be an instruction that is already fetched by IF but not consumed by ID.
215215
# This helps to prove FetchErrRoot.
216-
FirstFetchNoInstr: have (`IDC.ctrl_fsm_ns == `IDC.FIRST_FETCH |-> ~`IF.instr_valid_id_q)
216+
FirstFetchNoInstr: have (`IDC.ctrl_fsm_ns == FIRST_FETCH |-> ~`IF.instr_valid_id_q)
217217

218218
MemOpRequiresValid: have (`LSU.ls_fsm_cs != `LSU.IDLE || `CR.lsu_req |-> `ID.instr_valid_i)
219219

@@ -253,7 +253,7 @@ lemma ibex
253253
SpecStableStoreData: have (ex_is_store_instr && `LSU.ls_fsm_cs != `LSU.IDLE && ($past(`LSU.ls_fsm_cs) != `LSU.IDLE || $past(`LSU.lsu_req_i)) |-> $stable(spec_mem_write_fst_wdata))
254254
SpecStableStoreSndData: have (ex_is_store_instr && `LSU.ls_fsm_cs != `LSU.IDLE && ($past(`LSU.ls_fsm_cs) != `LSU.IDLE || $past(`LSU.lsu_req_i)) |-> $stable(spec_mem_write_snd_wdata))
255255

256-
FetchErrRoot: have (`ID.instr_valid_i && (`IDC.ctrl_fsm_cs == `IDC.FLUSH -> ~$past(`IDC.csr_pipe_flush)) |-> spec_fetch_err == `ID.instr_fetch_err_i)
256+
FetchErrRoot: have (`ID.instr_valid_i && (`IDC.ctrl_fsm_cs == FLUSH -> ~$past(`IDC.csr_pipe_flush)) |-> spec_fetch_err == `ID.instr_fetch_err_i)
257257

258258
LoadNotSpecWrite: have (`ID.instr_valid_i & ex_is_load_instr |-> ~spec_mem_write)
259259
StoreNotSpecRead: have (`ID.instr_valid_i & ex_is_store_instr |-> ~spec_mem_read)
@@ -301,9 +301,9 @@ lemma live
301301
DivMiddle: have (`MULT.div_counter_q == 5'd31 && `MULT.md_state_q == `MULT.MD_COMP |-> ##30 `MULT.div_counter_q == 5'd1 && `MULT.md_state_q == `MULT.MD_COMP)
302302
DivEnd: have (`MULT.div_counter_q == 5'd1 && `MULT.md_state_q == `MULT.MD_COMP |-> ##3 instr_will_progress)
303303

304-
WFIStart: have (instr_will_progress & ex_is_wfi & ~ex_err |-> ##[0:5] `IDC.ctrl_fsm_cs == `IDC.SLEEP)
305-
WFIMiddle: have (`IDC.ctrl_fsm_cs == `IDC.SLEEP |-> ##[0:20] `IDC.ctrl_fsm_cs == `IDC.SLEEP && `IDC.ctrl_fsm_ns == `IDC.FIRST_FETCH)
306-
WFIEnd: have (`IDC.ctrl_fsm_cs == `IDC.SLEEP && `IDC.ctrl_fsm_ns == `IDC.FIRST_FETCH |-> ##[0:5] `IF.id_in_ready_i)
304+
WFIStart: have (instr_will_progress & ex_is_wfi & ~ex_err |-> ##[0:5] `IDC.ctrl_fsm_cs == SLEEP)
305+
WFIMiddle: have (`IDC.ctrl_fsm_cs == SLEEP |-> ##[0:20] `IDC.ctrl_fsm_cs == SLEEP && `IDC.ctrl_fsm_ns == FIRST_FETCH)
306+
WFIEnd: have (`IDC.ctrl_fsm_cs == SLEEP && `IDC.ctrl_fsm_ns == FIRST_FETCH |-> ##[0:5] `IF.id_in_ready_i)
307307

308308
NewProgNormal: have (`CR.instr_new_id & `CR.instr_valid_id & ~ex_is_div & ~ex_is_mem_instr |-> ##[0:5] (instr_will_progress | (ex_kill & `CR.instr_valid_id)))
309309
NewProgMem: have (`CR.instr_new_id & `CR.instr_valid_id & ex_is_mem_instr |-> ##[0:10] (instr_will_progress | (ex_kill & `CR.instr_valid_id)))

‎dv/formal/thm/riscv.proof‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -153,7 +153,7 @@ lemma riscv
153153
Pmp_cfg:(pmp_cfg) Pmp_addr:(pmp_addr) Mseccfg:(mseccfg)
154154
have (spec_past_``X == pre_``X)
155155

156-
SleepSpecPastPC: have (has_spec_past & (`IDC.ctrl_fsm_cs == `IDC.WAIT_SLEEP || `IDC.ctrl_fsm_cs == `IDC.SLEEP) |-> spec_past_pc == `CR.pc_if)
156+
SleepSpecPastPC: have (has_spec_past & (`IDC.ctrl_fsm_cs == WAIT_SLEEP || `IDC.ctrl_fsm_cs == SLEEP) |-> spec_past_pc == `CR.pc_if)
157157

158158
/
159159

0 commit comments

Comments
 (0)