diff --git a/cores/serv/.gitignore b/cores/serv/.gitignore new file mode 100644 index 0000000..4ce7579 --- /dev/null +++ b/cores/serv/.gitignore @@ -0,0 +1,3 @@ +/checks +/cover +/serv-src diff --git a/cores/serv/README.md b/cores/serv/README.md new file mode 100644 index 0000000..c05adc6 --- /dev/null +++ b/cores/serv/README.md @@ -0,0 +1,25 @@ +riscv-formal proofs for SErial RiscV (SERV) +=========================================== + +Quickstart guide: + +First install Yosys, SymbiYosys, and the solvers. See +[here](http://symbiyosys.readthedocs.io/en/latest/quickstart.html#installing) +for instructions. Then build the version of SERV with RVFI support and +rsicv-tools, and generate the formal checks: + +``` +bash generate.sh +``` + +Then run the formal checks: + +``` +make -C checks -j$(nproc) +``` + +And running the cover check: + +``` +sby -f cover.sby +``` diff --git a/cores/serv/checks.cfg b/cores/serv/checks.cfg new file mode 100644 index 0000000..44d5cc0 --- /dev/null +++ b/cores/serv/checks.cfg @@ -0,0 +1,32 @@ +[options] +isa rv32i +nret 1 + +[depth] +insn 150 +reg 1 150 +pc_fwd 1 150 +pc_bwd 1 150 +liveness 1 75 150 +unique 1 75 150 +causal 1 150 + +[defines] +`define RISCV_FORMAL_ALIGNED_MEM + +[script-sources] +read_verilog -sv @basedir@/cores/@core@/wrapper.sv +read_verilog -sv -defer @basedir@/cores/@core@/sbram.sv +read_verilog -sv -defer @basedir@/cores/@core@/serv-src/rtl/camd_ram.v +read_verilog -sv -defer @basedir@/cores/@core@/serv-src/rtl/ser_add.v +read_verilog -sv -defer @basedir@/cores/@core@/serv-src/rtl/ser_eq.v +read_verilog -sv -defer @basedir@/cores/@core@/serv-src/rtl/ser_lt.v +read_verilog -sv -defer @basedir@/cores/@core@/serv-src/rtl/ser_shift.v +read_verilog -sv -defer @basedir@/cores/@core@/serv-src/rtl/serv_alu.v +read_verilog -sv -defer @basedir@/cores/@core@/serv-src/rtl/serv_ctrl.v +read_verilog -sv -defer @basedir@/cores/@core@/serv-src/rtl/serv_decode.v +read_verilog -sv -defer @basedir@/cores/@core@/serv-src/rtl/serv_mem_if.v +read_verilog -sv -defer @basedir@/cores/@core@/serv-src/rtl/serv_params.vh +read_verilog -sv -defer @basedir@/cores/@core@/serv-src/rtl/serv_regfile.v +read_verilog -sv -defer @basedir@/cores/@core@/serv-src/rtl/serv_top.v +read_verilog -sv -defer @basedir@/cores/@core@/serv-src/rtl/shift_reg.v diff --git a/cores/serv/cover.gtkw b/cores/serv/cover.gtkw new file mode 100644 index 0000000..af772ec --- /dev/null +++ b/cores/serv/cover.gtkw @@ -0,0 +1,80 @@ +[*] +[*] GTKWave Analyzer v3.3.89 (w)1999-2018 BSI +[*] Thu Nov 1 11:25:45 2018 +[*] +[dumpfile] "/home/clifford/Work/riscv-formal/cores/serv/cover/engine_0/trace0.vcd" +[dumpfile_mtime] "Thu Nov 1 11:24:51 2018" +[dumpfile_size] 121959 +[savefile] "/home/clifford/Work/riscv-formal/cores/serv/cover.gtkw" +[timestart] 0 +[size] 1394 830 +[pos] -1 -1 +*-5.990967 5 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 +[treeopen] testbench. +[treeopen] testbench.wrapper. +[sst_width] 225 +[signals_width] 310 +[sst_expanded] 1 +[sst_vpaned_height] 241 +@24 +testbench.cycle[31:0] +testbench.wrapper.icnt[31:0] +@25 +testbench.wrapper.dcnt[31:0] +@200 +- +@28 +testbench.wrapper.clock +testbench.wrapper.reset +@200 +- +-I-MEM +@28 +testbench.wrapper.o_i_ca_vld +testbench.wrapper.i_i_ca_rdy +@22 +testbench.wrapper.o_i_ca_adr[31:0] +@200 +- +@28 +testbench.wrapper.i_i_rd_vld +testbench.wrapper.o_i_rd_rdy +@22 +testbench.wrapper.i_i_rd_dat[31:0] +@200 +- +-D-MEM +@28 +testbench.wrapper.o_d_ca_vld +testbench.wrapper.i_d_ca_rdy +testbench.wrapper.o_d_ca_cmd +@22 +testbench.wrapper.o_d_ca_adr[31:0] +@200 +- +@28 +testbench.wrapper.o_d_dm_vld +testbench.wrapper.i_d_dm_rdy +@22 +testbench.wrapper.o_d_dm_dat[31:0] +testbench.wrapper.o_d_dm_msk[3:0] +@200 +- +@28 +testbench.wrapper.i_d_rd_vld +testbench.wrapper.o_d_rd_rdy +@22 +testbench.wrapper.i_d_rd_dat[31:0] +@200 +- +-RVFI +@28 +testbench.wrapper.rvfi_valid +@22 +testbench.wrapper.rvfi_insn[31:0] +testbench.wrapper.rvfi_pc_rdata[31:0] +@200 +- +- +[pattern_trace] 1 +[pattern_trace] 0 diff --git a/cores/serv/cover.sby b/cores/serv/cover.sby new file mode 100644 index 0000000..873b046 --- /dev/null +++ b/cores/serv/cover.sby @@ -0,0 +1,61 @@ +[options] +mode cover +append 0 +tbtop wrapper.uut +depth 150 + +[engines] +smtbmc boolector + +[script] +read_verilog -sv defines.sv +read_verilog -sv cover.sv +read_verilog -sv wrapper.sv +read_verilog -sv -defer sbram.sv +read_verilog -sv -defer camd_ram.v +read_verilog -sv -defer ser_add.v +read_verilog -sv -defer ser_eq.v +read_verilog -sv -defer ser_lt.v +read_verilog -sv -defer ser_shift.v +read_verilog -sv -defer serv_alu.v +read_verilog -sv -defer serv_ctrl.v +read_verilog -sv -defer serv_decode.v +read_verilog -sv -defer serv_mem_if.v +read_verilog -sv -defer serv_params.vh +read_verilog -sv -defer serv_regfile.v +read_verilog -sv -defer serv_top.v +read_verilog -sv -defer shift_reg.v +prep -flatten -nordff -top testbench + +[files] +cover.sv +wrapper.sv +sbram.sv +serv-src/rtl/camd_ram.v +serv-src/rtl/ser_add.v +serv-src/rtl/ser_eq.v +serv-src/rtl/ser_lt.v +serv-src/rtl/ser_shift.v +serv-src/rtl/serv_alu.v +serv-src/rtl/serv_ctrl.v +serv-src/rtl/serv_decode.v +serv-src/rtl/serv_mem_if.v +serv-src/rtl/serv_params.vh +serv-src/rtl/serv_regfile.v +serv-src/rtl/serv_top.v +serv-src/rtl/shift_reg.v +../../checks/rvfi_macros.vh + +[file defines.sv] +`define RISCV_FORMAL +`define RISCV_FORMAL_NRET 1 +`define RISCV_FORMAL_XLEN 32 +`define RISCV_FORMAL_ILEN 32 +`define RISCV_FORMAL_RESET_CYCLES 1 +`define RISCV_FORMAL_CHECK_CYCLE 20 +`define RISCV_FORMAL_CHANNEL_IDX 0 +`define RISCV_FORMAL_CHECKER rvfi_insn_check +`define RISCV_FORMAL_INSN_MODEL rvfi_insn_add +`define RISCV_FORMAL_ALIGNED_MEM +`define MEMIO_FAIRNESS +`include "rvfi_macros.vh" diff --git a/cores/serv/cover.sv b/cores/serv/cover.sv new file mode 100644 index 0000000..64f70a3 --- /dev/null +++ b/cores/serv/cover.sv @@ -0,0 +1,19 @@ +module testbench ( + input clock, + input reset, + `RVFI_OUTPUTS +); + rvfi_wrapper wrapper ( + .clock(clock), + .reset(reset), + `RVFI_CONN + ); + + integer cycle = 0; + always @(posedge clock) cycle <= cycle + 1; + + always @(posedge clock) begin + assume (reset == (cycle == 0)); + cover (rvfi_valid); + end +endmodule diff --git a/cores/serv/generate.sh b/cores/serv/generate.sh new file mode 100644 index 0000000..07c62e6 --- /dev/null +++ b/cores/serv/generate.sh @@ -0,0 +1,6 @@ +#!/bin/bash +set -ex +rm -rf serv-src +git clone git@github.com:olofk/serv.git serv-src +sed -i -e '/define RISCV_FORMAL/ d;' serv-src/rtl/serv_top.v +python3 ../../checks/genchecks.py diff --git a/cores/serv/sbram.sv b/cores/serv/sbram.sv new file mode 100644 index 0000000..592d8dc --- /dev/null +++ b/cores/serv/sbram.sv @@ -0,0 +1,350 @@ +// SiliconBlue RAM Cells + +module SB_RAM40_4K ( + output [15:0] RDATA, + input RCLK, RCLKE, RE, + input [10:0] RADDR, + input WCLK, WCLKE, WE, + input [10:0] WADDR, + input [15:0] MASK, WDATA +); + // MODE 0: 256 x 16 + // MODE 1: 512 x 8 + // MODE 2: 1024 x 4 + // MODE 3: 2048 x 2 + parameter WRITE_MODE = 0; + parameter READ_MODE = 0; + + parameter INIT_0 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_1 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_2 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_3 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_4 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_5 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_6 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_7 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_8 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_9 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_A = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_B = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_C = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_D = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_E = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_F = 256'h0000000000000000000000000000000000000000000000000000000000000000; + +`ifndef BLACKBOX + wire [15:0] WMASK_I; + wire [15:0] RMASK_I; + + reg [15:0] RDATA_I; + wire [15:0] WDATA_I; + + generate + case (WRITE_MODE) + 0: assign WMASK_I = MASK; + + 1: assign WMASK_I = WADDR[ 8] == 0 ? 16'b 1010_1010_1010_1010 : + WADDR[ 8] == 1 ? 16'b 0101_0101_0101_0101 : 16'bx; + + 2: assign WMASK_I = WADDR[ 9:8] == 0 ? 16'b 1110_1110_1110_1110 : + WADDR[ 9:8] == 1 ? 16'b 1101_1101_1101_1101 : + WADDR[ 9:8] == 2 ? 16'b 1011_1011_1011_1011 : + WADDR[ 9:8] == 3 ? 16'b 0111_0111_0111_0111 : 16'bx; + + 3: assign WMASK_I = WADDR[10:8] == 0 ? 16'b 1111_1110_1111_1110 : + WADDR[10:8] == 1 ? 16'b 1111_1101_1111_1101 : + WADDR[10:8] == 2 ? 16'b 1111_1011_1111_1011 : + WADDR[10:8] == 3 ? 16'b 1111_0111_1111_0111 : + WADDR[10:8] == 4 ? 16'b 1110_1111_1110_1111 : + WADDR[10:8] == 5 ? 16'b 1101_1111_1101_1111 : + WADDR[10:8] == 6 ? 16'b 1011_1111_1011_1111 : + WADDR[10:8] == 7 ? 16'b 0111_1111_0111_1111 : 16'bx; + endcase + + case (READ_MODE) + 0: assign RMASK_I = 16'b 0000_0000_0000_0000; + + 1: assign RMASK_I = RADDR[ 8] == 0 ? 16'b 1010_1010_1010_1010 : + RADDR[ 8] == 1 ? 16'b 0101_0101_0101_0101 : 16'bx; + + 2: assign RMASK_I = RADDR[ 9:8] == 0 ? 16'b 1110_1110_1110_1110 : + RADDR[ 9:8] == 1 ? 16'b 1101_1101_1101_1101 : + RADDR[ 9:8] == 2 ? 16'b 1011_1011_1011_1011 : + RADDR[ 9:8] == 3 ? 16'b 0111_0111_0111_0111 : 16'bx; + + 3: assign RMASK_I = RADDR[10:8] == 0 ? 16'b 1111_1110_1111_1110 : + RADDR[10:8] == 1 ? 16'b 1111_1101_1111_1101 : + RADDR[10:8] == 2 ? 16'b 1111_1011_1111_1011 : + RADDR[10:8] == 3 ? 16'b 1111_0111_1111_0111 : + RADDR[10:8] == 4 ? 16'b 1110_1111_1110_1111 : + RADDR[10:8] == 5 ? 16'b 1101_1111_1101_1111 : + RADDR[10:8] == 6 ? 16'b 1011_1111_1011_1111 : + RADDR[10:8] == 7 ? 16'b 0111_1111_0111_1111 : 16'bx; + endcase + + case (WRITE_MODE) + 0: assign WDATA_I = WDATA; + + 1: assign WDATA_I = {WDATA[14], WDATA[14], WDATA[12], WDATA[12], + WDATA[10], WDATA[10], WDATA[ 8], WDATA[ 8], + WDATA[ 6], WDATA[ 6], WDATA[ 4], WDATA[ 4], + WDATA[ 2], WDATA[ 2], WDATA[ 0], WDATA[ 0]}; + + 2: assign WDATA_I = {WDATA[13], WDATA[13], WDATA[13], WDATA[13], + WDATA[ 9], WDATA[ 9], WDATA[ 9], WDATA[ 9], + WDATA[ 5], WDATA[ 5], WDATA[ 5], WDATA[ 5], + WDATA[ 1], WDATA[ 1], WDATA[ 1], WDATA[ 1]}; + + 3: assign WDATA_I = {WDATA[11], WDATA[11], WDATA[11], WDATA[11], + WDATA[11], WDATA[11], WDATA[11], WDATA[11], + WDATA[ 3], WDATA[ 3], WDATA[ 3], WDATA[ 3], + WDATA[ 3], WDATA[ 3], WDATA[ 3], WDATA[ 3]}; + endcase + + case (READ_MODE) + 0: assign RDATA = RDATA_I; + 1: assign RDATA = {1'b0, |RDATA_I[15:14], 1'b0, |RDATA_I[13:12], 1'b0, |RDATA_I[11:10], 1'b0, |RDATA_I[ 9: 8], + 1'b0, |RDATA_I[ 7: 6], 1'b0, |RDATA_I[ 5: 4], 1'b0, |RDATA_I[ 3: 2], 1'b0, |RDATA_I[ 1: 0]}; + 2: assign RDATA = {2'b0, |RDATA_I[15:12], 3'b0, |RDATA_I[11: 8], 3'b0, |RDATA_I[ 7: 4], 3'b0, |RDATA_I[ 3: 0], 1'b0}; + 3: assign RDATA = {4'b0, |RDATA_I[15: 8], 7'b0, |RDATA_I[ 7: 0], 3'b0}; + endcase + endgenerate + + integer i; + reg [15:0] memory [0:255]; + + initial begin + for (i=0; i<16; i=i+1) begin + memory[ 0*16 + i] <= INIT_0[16*i +: 16]; + memory[ 1*16 + i] <= INIT_1[16*i +: 16]; + memory[ 2*16 + i] <= INIT_2[16*i +: 16]; + memory[ 3*16 + i] <= INIT_3[16*i +: 16]; + memory[ 4*16 + i] <= INIT_4[16*i +: 16]; + memory[ 5*16 + i] <= INIT_5[16*i +: 16]; + memory[ 6*16 + i] <= INIT_6[16*i +: 16]; + memory[ 7*16 + i] <= INIT_7[16*i +: 16]; + memory[ 8*16 + i] <= INIT_8[16*i +: 16]; + memory[ 9*16 + i] <= INIT_9[16*i +: 16]; + memory[10*16 + i] <= INIT_A[16*i +: 16]; + memory[11*16 + i] <= INIT_B[16*i +: 16]; + memory[12*16 + i] <= INIT_C[16*i +: 16]; + memory[13*16 + i] <= INIT_D[16*i +: 16]; + memory[14*16 + i] <= INIT_E[16*i +: 16]; + memory[15*16 + i] <= INIT_F[16*i +: 16]; + end + end + + always @(posedge WCLK) begin + if (WE && WCLKE) begin + if (!WMASK_I[ 0]) memory[WADDR[7:0]][ 0] <= WDATA_I[ 0]; + if (!WMASK_I[ 1]) memory[WADDR[7:0]][ 1] <= WDATA_I[ 1]; + if (!WMASK_I[ 2]) memory[WADDR[7:0]][ 2] <= WDATA_I[ 2]; + if (!WMASK_I[ 3]) memory[WADDR[7:0]][ 3] <= WDATA_I[ 3]; + if (!WMASK_I[ 4]) memory[WADDR[7:0]][ 4] <= WDATA_I[ 4]; + if (!WMASK_I[ 5]) memory[WADDR[7:0]][ 5] <= WDATA_I[ 5]; + if (!WMASK_I[ 6]) memory[WADDR[7:0]][ 6] <= WDATA_I[ 6]; + if (!WMASK_I[ 7]) memory[WADDR[7:0]][ 7] <= WDATA_I[ 7]; + if (!WMASK_I[ 8]) memory[WADDR[7:0]][ 8] <= WDATA_I[ 8]; + if (!WMASK_I[ 9]) memory[WADDR[7:0]][ 9] <= WDATA_I[ 9]; + if (!WMASK_I[10]) memory[WADDR[7:0]][10] <= WDATA_I[10]; + if (!WMASK_I[11]) memory[WADDR[7:0]][11] <= WDATA_I[11]; + if (!WMASK_I[12]) memory[WADDR[7:0]][12] <= WDATA_I[12]; + if (!WMASK_I[13]) memory[WADDR[7:0]][13] <= WDATA_I[13]; + if (!WMASK_I[14]) memory[WADDR[7:0]][14] <= WDATA_I[14]; + if (!WMASK_I[15]) memory[WADDR[7:0]][15] <= WDATA_I[15]; + end + end + + always @(posedge RCLK) begin + if (RE && RCLKE) begin + RDATA_I <= memory[RADDR[7:0]] & ~RMASK_I; + end + end +`endif +endmodule + +module SB_RAM40_4KNR ( + output [15:0] RDATA, + input RCLKN, RCLKE, RE, + input [10:0] RADDR, + input WCLK, WCLKE, WE, + input [10:0] WADDR, + input [15:0] MASK, WDATA +); + parameter WRITE_MODE = 0; + parameter READ_MODE = 0; + + parameter INIT_0 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_1 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_2 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_3 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_4 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_5 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_6 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_7 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_8 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_9 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_A = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_B = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_C = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_D = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_E = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_F = 256'h0000000000000000000000000000000000000000000000000000000000000000; + + SB_RAM40_4K #( + .WRITE_MODE(WRITE_MODE), + .READ_MODE (READ_MODE ), + .INIT_0 (INIT_0 ), + .INIT_1 (INIT_1 ), + .INIT_2 (INIT_2 ), + .INIT_3 (INIT_3 ), + .INIT_4 (INIT_4 ), + .INIT_5 (INIT_5 ), + .INIT_6 (INIT_6 ), + .INIT_7 (INIT_7 ), + .INIT_8 (INIT_8 ), + .INIT_9 (INIT_9 ), + .INIT_A (INIT_A ), + .INIT_B (INIT_B ), + .INIT_C (INIT_C ), + .INIT_D (INIT_D ), + .INIT_E (INIT_E ), + .INIT_F (INIT_F ) + ) RAM ( + .RDATA(RDATA), + .RCLK (~RCLKN), + .RCLKE(RCLKE), + .RE (RE ), + .RADDR(RADDR), + .WCLK (WCLK ), + .WCLKE(WCLKE), + .WE (WE ), + .WADDR(WADDR), + .MASK (MASK ), + .WDATA(WDATA) + ); +endmodule + +module SB_RAM40_4KNW ( + output [15:0] RDATA, + input RCLK, RCLKE, RE, + input [10:0] RADDR, + input WCLKN, WCLKE, WE, + input [10:0] WADDR, + input [15:0] MASK, WDATA +); + parameter WRITE_MODE = 0; + parameter READ_MODE = 0; + + parameter INIT_0 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_1 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_2 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_3 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_4 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_5 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_6 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_7 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_8 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_9 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_A = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_B = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_C = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_D = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_E = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_F = 256'h0000000000000000000000000000000000000000000000000000000000000000; + + SB_RAM40_4K #( + .WRITE_MODE(WRITE_MODE), + .READ_MODE (READ_MODE ), + .INIT_0 (INIT_0 ), + .INIT_1 (INIT_1 ), + .INIT_2 (INIT_2 ), + .INIT_3 (INIT_3 ), + .INIT_4 (INIT_4 ), + .INIT_5 (INIT_5 ), + .INIT_6 (INIT_6 ), + .INIT_7 (INIT_7 ), + .INIT_8 (INIT_8 ), + .INIT_9 (INIT_9 ), + .INIT_A (INIT_A ), + .INIT_B (INIT_B ), + .INIT_C (INIT_C ), + .INIT_D (INIT_D ), + .INIT_E (INIT_E ), + .INIT_F (INIT_F ) + ) RAM ( + .RDATA(RDATA), + .RCLK (RCLK ), + .RCLKE(RCLKE), + .RE (RE ), + .RADDR(RADDR), + .WCLK (~WCLKN), + .WCLKE(WCLKE), + .WE (WE ), + .WADDR(WADDR), + .MASK (MASK ), + .WDATA(WDATA) + ); +endmodule + +module SB_RAM40_4KNRNW ( + output [15:0] RDATA, + input RCLKN, RCLKE, RE, + input [10:0] RADDR, + input WCLKN, WCLKE, WE, + input [10:0] WADDR, + input [15:0] MASK, WDATA +); + parameter WRITE_MODE = 0; + parameter READ_MODE = 0; + + parameter INIT_0 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_1 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_2 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_3 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_4 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_5 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_6 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_7 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_8 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_9 = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_A = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_B = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_C = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_D = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_E = 256'h0000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_F = 256'h0000000000000000000000000000000000000000000000000000000000000000; + + SB_RAM40_4K #( + .WRITE_MODE(WRITE_MODE), + .READ_MODE (READ_MODE ), + .INIT_0 (INIT_0 ), + .INIT_1 (INIT_1 ), + .INIT_2 (INIT_2 ), + .INIT_3 (INIT_3 ), + .INIT_4 (INIT_4 ), + .INIT_5 (INIT_5 ), + .INIT_6 (INIT_6 ), + .INIT_7 (INIT_7 ), + .INIT_8 (INIT_8 ), + .INIT_9 (INIT_9 ), + .INIT_A (INIT_A ), + .INIT_B (INIT_B ), + .INIT_C (INIT_C ), + .INIT_D (INIT_D ), + .INIT_E (INIT_E ), + .INIT_F (INIT_F ) + ) RAM ( + .RDATA(RDATA), + .RCLK (~RCLKN), + .RCLKE(RCLKE), + .RE (RE ), + .RADDR(RADDR), + .WCLK (~WCLKN), + .WCLKE(WCLKE), + .WE (WE ), + .WADDR(WADDR), + .MASK (MASK ), + .WDATA(WDATA) + ); +endmodule diff --git a/cores/serv/wrapper.sv b/cores/serv/wrapper.sv new file mode 100644 index 0000000..d9883a6 --- /dev/null +++ b/cores/serv/wrapper.sv @@ -0,0 +1,144 @@ +module rvfi_wrapper ( + input clock, + input reset, + `RVFI_OUTPUTS +); + // I-MEM + (* keep *) wire [31:0] o_i_ca_adr; + (* keep *) wire o_i_ca_vld; + (* keep *) rand reg i_i_ca_rdy; + + (* keep *) rand reg [31:0] i_i_rd_dat; + (* keep *) rand reg i_i_rd_vld; + (* keep *) wire o_i_rd_rdy; + + // D-MEM + (* keep *) wire o_d_ca_cmd; + (* keep *) wire [31:0] o_d_ca_adr; + (* keep *) wire o_d_ca_vld; + (* keep *) rand reg i_d_ca_rdy; + + (* keep *) wire [31:0] o_d_dm_dat; + (* keep *) wire [3:0] o_d_dm_msk; + (* keep *) wire o_d_dm_vld; + (* keep *) rand reg i_d_dm_rdy; + + (* keep *) rand reg [31:0] i_d_rd_dat; + (* keep *) rand reg i_d_rd_vld; + (* keep *) wire o_d_rd_rdy; + + serv_top uut ( + .clk(clock), + `RVFI_CONN, + + .o_i_ca_adr (o_i_ca_adr), + .o_i_ca_vld (o_i_ca_vld), + .i_i_ca_rdy (i_i_ca_rdy), + + .i_i_rd_dat (i_i_rd_dat), + .i_i_rd_vld (i_i_rd_vld), + .o_i_rd_rdy (o_i_rd_rdy), + + .o_d_ca_cmd (o_d_ca_cmd), + .o_d_ca_adr (o_d_ca_adr), + .o_d_ca_vld (o_d_ca_vld), + .i_d_ca_rdy (i_d_ca_rdy), + + .o_d_dm_dat (o_d_dm_dat), + .o_d_dm_msk (o_d_dm_msk), + .o_d_dm_vld (o_d_dm_vld), + .i_d_dm_rdy (i_d_dm_rdy), + + .i_d_rd_dat (i_d_rd_dat), + .i_d_rd_vld (i_d_rd_vld), + .o_d_rd_rdy (o_d_rd_rdy) + ); + + integer icnt = 0; + integer dcnt = 0; + + // I-MEM + always @(posedge clock) begin + if (reset) begin + assume (i_i_ca_rdy == 0); + assume (i_i_rd_vld == 0); + end + + // do not "take back" rdy + if ($past(i_i_ca_rdy) && !$past(o_i_ca_vld)) begin + assume (i_i_ca_rdy); + end + + // do not send data without active request + if (icnt == 0 && !(i_i_ca_rdy && o_i_ca_vld)) begin + assume (!i_i_rd_vld); + end + + // count number of active requests + icnt <= icnt + (i_i_ca_rdy && o_i_ca_vld) - (i_i_rd_vld && o_i_rd_rdy); + end + + // D-MEM + always @(posedge clock) begin + if (reset) begin + assume (i_d_ca_rdy == 0); + assume (i_d_dm_rdy == 0); + assume (i_d_rd_vld == 0); + end + + // do not "take back" rdy on ca channel + if ($past(i_d_ca_rdy) && !$past(o_d_ca_vld)) begin + assume (i_d_ca_rdy); + end + + // do not "take back" rdy on dm channel + if ($past(i_d_dm_rdy) && !$past(o_d_dm_vld)) begin + assume (i_d_dm_rdy); + end + + // do not send data without active read request + if (dcnt == 0 && !(i_d_ca_rdy && o_d_ca_vld && !o_d_ca_cmd)) begin + assume (!i_d_rd_vld); + end + + // count number of active read requests + dcnt <= dcnt + (i_d_ca_rdy && o_d_ca_vld && !o_d_ca_cmd) - (i_d_rd_vld && o_d_rd_rdy); + end + +`ifdef MEMIO_FAIRNESS + reg [1:0] timeout_i_ca = 0; + reg [1:0] timeout_i_rd = 0; + reg [1:0] timeout_d_ca = 0; + reg [1:0] timeout_d_dm = 0; + reg [1:0] timeout_d_rd = 0; + + always @(posedge clock) begin + timeout_i_ca <= 0; + timeout_i_rd <= 0; + timeout_d_ca <= 0; + timeout_d_dm <= 0; + timeout_d_rd <= 0; + + if (o_i_ca_vld && !i_i_ca_rdy) + timeout_i_ca <= timeout_i_ca + 1; + + if (icnt && !i_i_rd_vld) + timeout_i_rd <= timeout_i_rd + 1; + + if (o_d_ca_vld && !i_d_ca_rdy) + timeout_d_ca <= timeout_d_ca + 1; + + if (o_d_dm_vld && !i_d_dm_rdy) + timeout_d_dm <= timeout_d_dm + 1; + + if (dcnt && !i_d_rd_vld) + timeout_d_rd <= timeout_d_rd + 1; + + assume (timeout_i_ca != 3); + assume (timeout_i_rd != 3); + assume (timeout_d_ca != 3); + assume (timeout_d_dm != 3); + assume (timeout_d_rd != 3); + end +`endif +endmodule