mirror of
https://github.com/retroSoC/retroSoC.git
synced 2026-11-04 22:32:36 +00:00
maksyuki
3aa3d937e1
- Updated filelist to include new timer peripheral files. - Enhanced formal file generation script to support timer target. - Created timer formal design and properties for formal verification. - Modified formal makefile to include timer targets and source files. - Added timer-related source files to software makefile. - Updated core and management wrappers to include debug halted signal. - Implemented timer testbench for RTL simulation. - Added regression tests for timer functionality in Python. - Introduced timer helper functions in C tests for validation.
74 lines
2.1 KiB
Systemverilog
74 lines
2.1 KiB
Systemverilog
// Copyright (c) 2026 Yuchi Miao <miaoyuchi@ict.ac.cn>
|
|
// retroSoC is licensed under Mulan PSL v2.
|
|
|
|
module timer_formal;
|
|
|
|
(* anyseq *) (* gclk *)reg clk_i;
|
|
wire rst_n_i;
|
|
wire f_past_valid;
|
|
wire rib_valid;
|
|
wire [31:0] rib_addr;
|
|
wire [31:0] rib_wdata;
|
|
wire [ 3:0] rib_wstrb;
|
|
wire rib_ready;
|
|
wire rib_resp_err;
|
|
wire debug_halted;
|
|
wire active;
|
|
wire debug_frozen;
|
|
wire [31:0] value;
|
|
wire start;
|
|
wire stop;
|
|
wire load_now;
|
|
wire timeout_event;
|
|
wire compare0_event;
|
|
wire compare1_event;
|
|
wire one_shot_done;
|
|
wire [ 2:0] intr_state;
|
|
wire [ 2:0] intr_enable;
|
|
wire irq;
|
|
|
|
timer_formal_design u_design (.*);
|
|
|
|
always @(posedge clk_i) begin
|
|
if (f_past_valid && $past(rst_n_i && rib_valid && !rib_ready)) begin
|
|
assume (rib_valid);
|
|
assume (rib_addr == $past(rib_addr));
|
|
assume (rib_wdata == $past(rib_wdata));
|
|
assume (rib_wstrb == $past(rib_wstrb));
|
|
end
|
|
|
|
if (rst_n_i) begin
|
|
assert (irq == |(intr_state & intr_enable));
|
|
if (f_past_valid && $past(rst_n_i && rib_valid && !rib_ready)) begin
|
|
assert (rib_ready);
|
|
end
|
|
if (f_past_valid && $past(rst_n_i && !active && !load_now)) begin
|
|
assert (value == $past(value));
|
|
end
|
|
if (f_past_valid && $past(rst_n_i && debug_frozen && !load_now && !stop)) begin
|
|
assert (value == $past(value));
|
|
end
|
|
if (f_past_valid && $past(rst_n_i && timeout_event)) begin
|
|
assert (intr_state[0]);
|
|
end
|
|
if (f_past_valid && $past(rst_n_i && compare0_event)) begin
|
|
assert (intr_state[1]);
|
|
end
|
|
if (f_past_valid && $past(rst_n_i && compare1_event)) begin
|
|
assert (intr_state[2]);
|
|
end
|
|
if (f_past_valid && $past(rst_n_i && one_shot_done)) begin
|
|
assert (!active);
|
|
end
|
|
|
|
cover (start);
|
|
cover (debug_frozen && debug_halted);
|
|
cover (timeout_event);
|
|
cover (compare0_event && compare1_event);
|
|
cover (irq);
|
|
cover (rib_ready && rib_resp_err);
|
|
end
|
|
end
|
|
|
|
endmodule
|