Serv

cores/serv/.gitignore

@@ -0,0 +1,3 @@
+/checks
+/cover
+/serv-src

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
+```

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

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

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"

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

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