add warp formal checks

Author: coderkalyan

.gitignore

@@ -1,5 +1,5 @@
 a.out
-warp/
+./warp/
 warp_bmc/
 warp_cover/
 env

formal/riscv-formal/cores/warp/.gitignore

@@ -0,0 +1,15 @@
+/cover/
+/complete/
+/honest/
+/checks/
+/testbug[0-9][0-9][0-9].cfg
+/testbug[0-9][0-9][0-9]/
+/testbugs.mk
+/cexdata-[0-9][0-9][0-9][0-9][0-9][0-9][0-9][0-9]
+/cexdata-[0-9][0-9][0-9][0-9][0-9][0-9][0-9][0-9].zip
+/picorv32.v
+/disasm.s
+/disasm.o
+*.v
+warp_formal.sv
+warp_hart_tb.sv

formal/riscv-formal/cores/warp/Makefile

@@ -0,0 +1,12 @@
+discrete.v:
+	cp -ra ../../../../rtl/{*.v,*.sv} .
+
+checks: discrete.v
+	python3 ../../checks/genchecks.py
+	$(MAKE) -C checks
+
+check: checks
+
+clean:
+	rm -f *.v *.sv
+	rm -rf checks

formal/riscv-formal/cores/warp/checks.cfg

@@ -0,0 +1,76 @@
+[options]
+isa rv64i
+nret 2
+
+[depth]
+# arithmetic instructions retire on ch0
+insn_add_ch0    20
+insn_slt_ch0    20
+insn_sltu_ch0   20
+insn_addi_ch0   20
+insn_slti_ch0   20
+insn_sltiu_ch0  20
+insn_lui_ch0    20
+insn_auipc_ch0  20
+insn_addw_ch0   20
+insn_subw_ch0   20
+insn_addiw_ch0  20
+
+# logical instructions retire on ch1
+insn_or_ch1     20
+insn_and_ch1    20
+insn_xor_ch1    20
+insn_ori_ch1    20
+insn_andi_ch1   20
+insn_xori_ch1   20
+
+# reg       15   25
+# reg       1 3
+# 25
+#pc_fwd    10    30
+#pc_bwd    10    30
+# liveness  1  10 30
+# unique    1  10 30
+# causal    10    30
+# cover     1     15
+
+# csrw            15
+# csr_ill         15
+# csrc_inc   1    15
+# csrc_upcnt 1    15
+
+[sort]
+reg_ch0
+
+# [csrs]
+# mcycle          inc upcnt
+# minstret        inc upcnt
+
+# [illegal_csrs]
+# c00     u       w
+# c80     u       w
+# c02     u       w
+# c82     u       w
+
+[defines]
+`define RISCV_FORMAL_ALIGNED_MEM
+# `define RISCV_FORMAL_ALTOPS
+`define RISCV_FORMAL_UMODE
+# `define PICORV32_TESTBUG_NONE
+# `define DEBUGNETS
+
+# [defines liveness]
+# `define PICORV32_FAIRNESS
+
+[verilog-files]
+@basedir@/cores/@core@/wrapper.sv
+@basedir@/cores/@core@/warp_defines.v
+@basedir@/cores/@core@/warp_util.v
+@basedir@/cores/@core@/warp_fetch.v
+@basedir@/cores/@core@/warp_decode.v
+@basedir@/cores/@core@/warp_issue.v
+@basedir@/cores/@core@/warp_integer.v
+@basedir@/cores/@core@/warp_hart.v
+
+# [cover]
+# always @* if (!reset) cover (channel[0].cnt_insns == 2);

formal/riscv-formal/cores/warp/wrapper.sv

@@ -0,0 +1,25 @@
+module rvfi_wrapper (
+    input wire clock,
+    input wire reset,
+    `RVFI_OUTPUTS
+);
+    
+    (* keep *) wire [31:0] imem_addr;
+    (* keep *) wire [31:0] imem_rdata;
+    (* keep *) wire [31:0] dmem_addr;
+    (* keep *) wire [31:0] dmem_wdata;
+    (* keep *) wire [31:0] dmem_rdata;
+
+    warp_hart dut (
+        .i_clk(clock),
+        .i_rst_n(!reset),
+
+        // .o_imem_addr(imem_addr),
+        // .i_imem_rdata(imem_rdata),
+        // .o_dmem_addr(dmem_addr),
+        // .o_dmem_wdata(dmem_wdata),
+        // .i_dmem_rdata(dmem_rdata),
+
+        `RVFI_CONN
+    );
+endmodule