-
Notifications
You must be signed in to change notification settings - Fork 52
/
complete.sv
107 lines (94 loc) · 3.04 KB
/
complete.sv
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
`include "defines.sv"
module testbench (
input clock
);
logic reset = 1;
always_ff @(posedge clock) begin
reset <= 0;
end
`RVFI_WIRES
(* keep *) logic [31:2] ibus_adr;
(* keep *) logic [31:0] ibus_dat_w;
(* keep *) `rvformal_rand_reg [31:0] ibus_dat_r;
(* keep *) logic [3:0] ibus_sel;
(* keep *) logic ibus_cyc;
(* keep *) logic ibus_stb;
(* keep *) logic ibus_we;
(* keep *) `rvformal_rand_reg ibus_ack;
(* keep *) `rvformal_rand_reg ibus_err;
(* keep *) logic [31:2] dbus_adr;
(* keep *) logic [31:0] dbus_dat_w;
(* keep *) `rvformal_rand_reg [31:0] dbus_dat_r;
(* keep *) logic [3:0] dbus_sel;
(* keep *) logic dbus_cyc;
(* keep *) logic dbus_stb;
(* keep *) logic dbus_we;
(* keep *) `rvformal_rand_reg dbus_ack;
(* keep *) `rvformal_rand_reg dbus_err;
\icicle.cpu.CPU #(
.rvfi(1),
`ifdef RISCV_FORMAL_BLACKBOX_ALU
.rvfi_blackbox_alu(1),
`endif
`ifdef RISCV_FORMAL_BLACKBOX_REGS
.rvfi_blackbox_regs(1),
`endif
) uut (
.clk(clock),
.rst(reset),
.ibus__adr(ibus_adr),
.ibus__dat_w(ibus_dat_w),
.ibus__dat_r(ibus_dat_r),
.ibus__sel(ibus_sel),
.ibus__cyc(ibus_cyc),
.ibus__stb(ibus_stb),
.ibus__we(ibus_we),
.ibus__ack(ibus_ack),
.ibus__err(ibus_err),
.dbus__adr(dbus_adr),
.dbus__dat_w(dbus_dat_w),
.dbus__dat_r(dbus_dat_r),
.dbus__sel(dbus_sel),
.dbus__cyc(dbus_cyc),
.dbus__stb(dbus_stb),
.dbus__we(dbus_we),
.dbus__ack(dbus_ack),
.dbus__err(ibus_err),
`RVFI_CONN
);
(* keep *) logic spec_valid;
(* keep *) logic spec_trap;
(* keep *) logic [4:0] spec_rs1_addr;
(* keep *) logic [4:0] spec_rs2_addr;
(* keep *) logic [4:0] spec_rd_addr;
(* keep *) logic [`RISCV_FORMAL_XLEN-1:0] spec_rd_wdata;
(* keep *) logic [`RISCV_FORMAL_XLEN-1:0] spec_pc_wdata;
(* keep *) logic [`RISCV_FORMAL_XLEN-1:0] spec_mem_addr;
(* keep *) logic [`RISCV_FORMAL_XLEN/8-1:0] spec_mem_rmask;
(* keep *) logic [`RISCV_FORMAL_XLEN/8-1:0] spec_mem_wmask;
(* keep *) logic [`RISCV_FORMAL_XLEN-1:0] spec_mem_wdata;
rvfi_isa_rv32i isa_spec (
.rvfi_valid(rvfi_valid),
.rvfi_insn(rvfi_insn),
.rvfi_pc_rdata(rvfi_pc_rdata),
.rvfi_rs1_rdata(rvfi_rs1_rdata),
.rvfi_rs2_rdata(rvfi_rs2_rdata),
.rvfi_mem_rdata(rvfi_mem_rdata),
.spec_valid(spec_valid),
.spec_trap(spec_trap),
.spec_rs1_addr(spec_rs1_addr),
.spec_rs2_addr(spec_rs2_addr),
.spec_rd_addr(spec_rd_addr),
.spec_rd_wdata(spec_rd_wdata),
.spec_pc_wdata(spec_pc_wdata),
.spec_mem_addr(spec_mem_addr),
.spec_mem_rmask(spec_mem_rmask),
.spec_mem_wmask(spec_mem_wmask),
.spec_mem_wdata(spec_mem_wdata)
);
always_comb begin
if (~reset && rvfi_valid && ~rvfi_trap & rvfi_insn[6:0] != 7'b0001111) begin
assert (spec_valid && ~spec_trap);
end
end
endmodule