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
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
|
// Based on the benchmark from 2016 Yosys-SMTBMC presentation, which in turn is
// based on the tracecmp2 test from this directory.
module testbench (
input clk,
input [31:0] mem_rdata_in,
input pcpi_wr,
input [31:0] pcpi_rd,
input pcpi_wait,
input pcpi_ready
);
reg resetn = 0;
always @(posedge clk)
resetn <= 1;
wire cpu0_trap;
wire cpu0_mem_valid;
wire cpu0_mem_instr;
wire cpu0_mem_ready;
wire [31:0] cpu0_mem_addr;
wire [31:0] cpu0_mem_wdata;
wire [3:0] cpu0_mem_wstrb;
wire [31:0] cpu0_mem_rdata;
wire cpu0_trace_valid;
wire [35:0] cpu0_trace_data;
wire cpu1_trap;
wire cpu1_mem_valid;
wire cpu1_mem_instr;
wire cpu1_mem_ready;
wire [31:0] cpu1_mem_addr;
wire [31:0] cpu1_mem_wdata;
wire [3:0] cpu1_mem_wstrb;
wire [31:0] cpu1_mem_rdata;
wire cpu1_trace_valid;
wire [35:0] cpu1_trace_data;
wire mem_ready;
wire [31:0] mem_rdata;
assign mem_ready = cpu0_mem_valid && cpu1_mem_valid;
assign mem_rdata = mem_rdata_in;
assign cpu0_mem_ready = mem_ready;
assign cpu0_mem_rdata = mem_rdata;
assign cpu1_mem_ready = mem_ready;
assign cpu1_mem_rdata = mem_rdata;
reg [ 2:0] trace_balance = 3'b010;
reg [35:0] trace_buffer_cpu0 = 0, trace_buffer_cpu1 = 0;
always @(posedge clk) begin
if (resetn) begin
if (cpu0_trace_valid)
trace_buffer_cpu0 <= cpu0_trace_data;
if (cpu1_trace_valid)
trace_buffer_cpu1 <= cpu1_trace_data;
if (cpu0_trace_valid && !cpu1_trace_valid)
trace_balance <= trace_balance << 1;
if (!cpu0_trace_valid && cpu1_trace_valid)
trace_balance <= trace_balance >> 1;
end
end
always @* begin
if (resetn && cpu0_mem_ready) begin
assert(cpu0_mem_addr == cpu1_mem_addr);
assert(cpu0_mem_wstrb == cpu1_mem_wstrb);
if (cpu0_mem_wstrb[3]) assert(cpu0_mem_wdata[31:24] == cpu1_mem_wdata[31:24]);
if (cpu0_mem_wstrb[2]) assert(cpu0_mem_wdata[23:16] == cpu1_mem_wdata[23:16]);
if (cpu0_mem_wstrb[1]) assert(cpu0_mem_wdata[15: 8] == cpu1_mem_wdata[15: 8]);
if (cpu0_mem_wstrb[0]) assert(cpu0_mem_wdata[ 7: 0] == cpu1_mem_wdata[ 7: 0]);
end
if (trace_balance == 3'b010) begin
assert(trace_buffer_cpu0 == trace_buffer_cpu1);
end
end
picorv32 #(
.ENABLE_COUNTERS(0),
.REGS_INIT_ZERO(1),
.COMPRESSED_ISA(1),
.ENABLE_TRACE(1),
.TWO_STAGE_SHIFT(0),
.ENABLE_PCPI(1)
) cpu0 (
.clk (clk ),
.resetn (resetn ),
.trap (cpu0_trap ),
.mem_valid (cpu0_mem_valid ),
.mem_instr (cpu0_mem_instr ),
.mem_ready (cpu0_mem_ready ),
.mem_addr (cpu0_mem_addr ),
.mem_wdata (cpu0_mem_wdata ),
.mem_wstrb (cpu0_mem_wstrb ),
.mem_rdata (cpu0_mem_rdata ),
.pcpi_wr (pcpi_wr ),
.pcpi_rd (pcpi_rd ),
.pcpi_wait (pcpi_wait ),
.pcpi_ready (pcpi_ready ),
.trace_valid (cpu0_trace_valid),
.trace_data (cpu0_trace_data )
);
picorv32 #(
.ENABLE_COUNTERS(0),
.REGS_INIT_ZERO(1),
.COMPRESSED_ISA(1),
.ENABLE_TRACE(1),
.TWO_STAGE_SHIFT(1),
.TWO_CYCLE_COMPARE(1),
.TWO_CYCLE_ALU(1)
) cpu1 (
.clk (clk ),
.resetn (resetn ),
.trap (cpu1_trap ),
.mem_valid (cpu1_mem_valid ),
.mem_instr (cpu1_mem_instr ),
.mem_ready (cpu1_mem_ready ),
.mem_addr (cpu1_mem_addr ),
.mem_wdata (cpu1_mem_wdata ),
.mem_wstrb (cpu1_mem_wstrb ),
.mem_rdata (cpu1_mem_rdata ),
.trace_valid (cpu1_trace_valid),
.trace_data (cpu1_trace_data )
);
endmodule
|
