Skip to content

Commit

Permalink
Switching rocket code to Yosys Verific front-end
Browse files Browse the repository at this point in the history 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
  • Loading branch information
@cliffordwolf
cliffordwolf committed Nov 15, 2018
1 parent dbb2d9b commit a52eb8f
Show file tree
Hide file tree
Showing 5 changed files with 218 additions and 231 deletions.
25 changes: 25 additions & 0 deletions checks/rvfi_macros.py
View file
Expand Up @@ -129,6 +129,21 @@
print("`define rvformal_csr_%s_conn" % csr)
print("`endif")

print("")
print("`ifdef RISCV_FORMAL_EXTAMO")
print("`define rvformal_extamo_wires (* keep *) wire [`RISCV_FORMAL_NRET-1:0] rvfi_mem_extamo;")
print("`define rvformal_extamo_outputs , output [`RISCV_FORMAL_NRET-1:0] rvfi_mem_extamo")
print("`define rvformal_extamo_inputs , input [`RISCV_FORMAL_NRET-1:0] rvfi_mem_extamo")
print("`define rvformal_extamo_channel(_idx) wire mem_extamo = rvfi_mem_extamo [_idx];")
print("`define rvformal_extamo_conn , .rvfi_mem_extamo(rvfi_mem_extamo)")
print("`else")
print("`define rvformal_extamo_wires")
print("`define rvformal_extamo_outputs")
print("`define rvformal_extamo_inputs")
print("`define rvformal_extamo_channel(_idx)")
print("`define rvformal_extamo_conn")
print("`endif")

print("")
print("`define RVFI_WIRES \\")
print("(* keep *) wire [`RISCV_FORMAL_NRET - 1 : 0] rvfi_valid; \\")
Expand All @@ -137,6 +152,7 @@
print("(* keep *) wire [`RISCV_FORMAL_NRET - 1 : 0] rvfi_trap; \\")
print("(* keep *) wire [`RISCV_FORMAL_NRET - 1 : 0] rvfi_halt; \\")
print("(* keep *) wire [`RISCV_FORMAL_NRET - 1 : 0] rvfi_intr; \\")
print("(* keep *) wire [`RISCV_FORMAL_NRET * 2 - 1 : 0] rvfi_mode; \\")
print("(* keep *) wire [`RISCV_FORMAL_NRET * 5 - 1 : 0] rvfi_rs1_addr; \\")
print("(* keep *) wire [`RISCV_FORMAL_NRET * 5 - 1 : 0] rvfi_rs2_addr; \\")
print("(* keep *) wire [`RISCV_FORMAL_NRET * `RISCV_FORMAL_XLEN - 1 : 0] rvfi_rs1_rdata; \\")
Expand All @@ -150,6 +166,7 @@
print("(* keep *) wire [`RISCV_FORMAL_NRET * `RISCV_FORMAL_XLEN/8 - 1 : 0] rvfi_mem_wmask; \\")
print("(* keep *) wire [`RISCV_FORMAL_NRET * `RISCV_FORMAL_XLEN - 1 : 0] rvfi_mem_rdata; \\")
print("(* keep *) wire [`RISCV_FORMAL_NRET * `RISCV_FORMAL_XLEN - 1 : 0] rvfi_mem_wdata; \\")
print("`rvformal_extamo_wires \\")
for csr in all_csrs:
print("`rvformal_csr_%s_wires%s" % (csr, "" if csr == all_csrs[-1] else " \\"))

Expand All @@ -161,6 +178,7 @@
print("output [`RISCV_FORMAL_NRET - 1 : 0] rvfi_trap, \\")
print("output [`RISCV_FORMAL_NRET - 1 : 0] rvfi_halt, \\")
print("output [`RISCV_FORMAL_NRET - 1 : 0] rvfi_intr, \\")
print("output [`RISCV_FORMAL_NRET * 2 - 1 : 0] rvfi_mode, \\")
print("output [`RISCV_FORMAL_NRET * 5 - 1 : 0] rvfi_rs1_addr, \\")
print("output [`RISCV_FORMAL_NRET * 5 - 1 : 0] rvfi_rs2_addr, \\")
print("output [`RISCV_FORMAL_NRET * `RISCV_FORMAL_XLEN - 1 : 0] rvfi_rs1_rdata, \\")
Expand All @@ -174,6 +192,7 @@
print("output [`RISCV_FORMAL_NRET * `RISCV_FORMAL_XLEN/8 - 1 : 0] rvfi_mem_wmask, \\")
print("output [`RISCV_FORMAL_NRET * `RISCV_FORMAL_XLEN - 1 : 0] rvfi_mem_rdata, \\")
print("output [`RISCV_FORMAL_NRET * `RISCV_FORMAL_XLEN - 1 : 0] rvfi_mem_wdata \\")
print("`rvformal_extamo_outputs \\")
for csr in all_csrs:
print("`rvformal_csr_%s_outputs%s" % (csr, "" if csr == all_csrs[-1] else " \\"))

Expand All @@ -185,6 +204,7 @@
print("input [`RISCV_FORMAL_NRET - 1 : 0] rvfi_trap, \\")
print("input [`RISCV_FORMAL_NRET - 1 : 0] rvfi_halt, \\")
print("input [`RISCV_FORMAL_NRET - 1 : 0] rvfi_intr, \\")
print("input [`RISCV_FORMAL_NRET * 2 - 1 : 0] rvfi_mode, \\")
print("input [`RISCV_FORMAL_NRET * 5 - 1 : 0] rvfi_rs1_addr, \\")
print("input [`RISCV_FORMAL_NRET * 5 - 1 : 0] rvfi_rs2_addr, \\")
print("input [`RISCV_FORMAL_NRET * `RISCV_FORMAL_XLEN - 1 : 0] rvfi_rs1_rdata, \\")
Expand All @@ -198,6 +218,7 @@
print("input [`RISCV_FORMAL_NRET * `RISCV_FORMAL_XLEN/8 - 1 : 0] rvfi_mem_wmask, \\")
print("input [`RISCV_FORMAL_NRET * `RISCV_FORMAL_XLEN - 1 : 0] rvfi_mem_rdata, \\")
print("input [`RISCV_FORMAL_NRET * `RISCV_FORMAL_XLEN - 1 : 0] rvfi_mem_wdata \\")
print("`rvformal_extamo_inputs \\")
for csr in all_csrs:
print("`rvformal_csr_%s_inputs%s" % (csr, "" if csr == all_csrs[-1] else " \\"))

Expand All @@ -210,6 +231,7 @@
print("wire [ 1 - 1 : 0] trap = rvfi_trap [(_idx)*( 1 ) +: 1 ]; \\")
print("wire [ 1 - 1 : 0] halt = rvfi_halt [(_idx)*( 1 ) +: 1 ]; \\")
print("wire [ 1 - 1 : 0] intr = rvfi_intr [(_idx)*( 1 ) +: 1 ]; \\")
print("wire [ 2 - 1 : 0] mode = rvfi_mode [(_idx)*( 2 ) +: 2 ]; \\")
print("wire [ 5 - 1 : 0] rs1_addr = rvfi_rs1_addr [(_idx)*( 5 ) +: 5 ]; \\")
print("wire [ 5 - 1 : 0] rs2_addr = rvfi_rs2_addr [(_idx)*( 5 ) +: 5 ]; \\")
print("wire [`RISCV_FORMAL_XLEN - 1 : 0] rs1_rdata = rvfi_rs1_rdata [(_idx)*(`RISCV_FORMAL_XLEN ) +: `RISCV_FORMAL_XLEN ]; \\")
Expand All @@ -223,6 +245,7 @@
print("wire [`RISCV_FORMAL_XLEN/8 - 1 : 0] mem_wmask = rvfi_mem_wmask [(_idx)*(`RISCV_FORMAL_XLEN/8) +: `RISCV_FORMAL_XLEN/8]; \\")
print("wire [`RISCV_FORMAL_XLEN - 1 : 0] mem_rdata = rvfi_mem_rdata [(_idx)*(`RISCV_FORMAL_XLEN ) +: `RISCV_FORMAL_XLEN ]; \\")
print("wire [`RISCV_FORMAL_XLEN - 1 : 0] mem_wdata = rvfi_mem_wdata [(_idx)*(`RISCV_FORMAL_XLEN ) +: `RISCV_FORMAL_XLEN ]; \\")
print("`rvformal_extamo_channel(_idx) \\")
for csr in all_csrs:
print("`rvformal_csr_%s_channel(_idx) \\" % csr)
print("end endgenerate")
Expand All @@ -235,6 +258,7 @@
print(".rvfi_trap (rvfi_trap ), \\")
print(".rvfi_halt (rvfi_halt ), \\")
print(".rvfi_intr (rvfi_intr ), \\")
print(".rvfi_mode (rvfi_mode ), \\")
print(".rvfi_rs1_addr (rvfi_rs1_addr ), \\")
print(".rvfi_rs2_addr (rvfi_rs2_addr ), \\")
print(".rvfi_rs1_rdata (rvfi_rs1_rdata), \\")
Expand All @@ -248,5 +272,6 @@
print(".rvfi_mem_wmask (rvfi_mem_wmask), \\")
print(".rvfi_mem_rdata (rvfi_mem_rdata), \\")
print(".rvfi_mem_wdata (rvfi_mem_wdata) \\")
print("`rvformal_extamo_conn \\")
for csr in all_csrs:
print("`rvformal_csr_%s_conn%s" % (csr, "" if csr == all_csrs[-1] else " \\"))
24 changes: 24 additions & 0 deletions checks/rvfi_macros.vh
View file
Expand Up @@ -258,13 +258,28 @@ wire [64 - 1 : 0] csr_minstret_wdata = rvfi_csr_minstret_wdata [(_idx)*64 +: 6
`define rvformal_csr_minstret_conn
`endif

`ifdef RISCV_FORMAL_EXTAMO
`define rvformal_extamo_wires (* keep *) wire [`RISCV_FORMAL_NRET-1:0] rvfi_mem_extamo;
`define rvformal_extamo_outputs , output [`RISCV_FORMAL_NRET-1:0] rvfi_mem_extamo
`define rvformal_extamo_inputs , input [`RISCV_FORMAL_NRET-1:0] rvfi_mem_extamo
`define rvformal_extamo_channel(_idx) wire mem_extamo = rvfi_mem_extamo [_idx];
`define rvformal_extamo_conn , .rvfi_mem_extamo(rvfi_mem_extamo)
`else
`define rvformal_extamo_wires
`define rvformal_extamo_outputs
`define rvformal_extamo_inputs
`define rvformal_extamo_channel(_idx)
`define rvformal_extamo_conn
`endif

`define RVFI_WIRES \
(* keep *) wire [`RISCV_FORMAL_NRET - 1 : 0] rvfi_valid; \
(* keep *) wire [`RISCV_FORMAL_NRET * 64 - 1 : 0] rvfi_order; \
(* keep *) wire [`RISCV_FORMAL_NRET * `RISCV_FORMAL_ILEN - 1 : 0] rvfi_insn; \
(* keep *) wire [`RISCV_FORMAL_NRET - 1 : 0] rvfi_trap; \
(* keep *) wire [`RISCV_FORMAL_NRET - 1 : 0] rvfi_halt; \
(* keep *) wire [`RISCV_FORMAL_NRET - 1 : 0] rvfi_intr; \
(* keep *) wire [`RISCV_FORMAL_NRET * 2 - 1 : 0] rvfi_mode; \
(* keep *) wire [`RISCV_FORMAL_NRET * 5 - 1 : 0] rvfi_rs1_addr; \
(* keep *) wire [`RISCV_FORMAL_NRET * 5 - 1 : 0] rvfi_rs2_addr; \
(* keep *) wire [`RISCV_FORMAL_NRET * `RISCV_FORMAL_XLEN - 1 : 0] rvfi_rs1_rdata; \
Expand All @@ -278,6 +293,7 @@ wire [64 - 1 : 0] csr_minstret_wdata = rvfi_csr_minstret_wdata [(_idx)*64 +: 6
(* keep *) wire [`RISCV_FORMAL_NRET * `RISCV_FORMAL_XLEN/8 - 1 : 0] rvfi_mem_wmask; \
(* keep *) wire [`RISCV_FORMAL_NRET * `RISCV_FORMAL_XLEN - 1 : 0] rvfi_mem_rdata; \
(* keep *) wire [`RISCV_FORMAL_NRET * `RISCV_FORMAL_XLEN - 1 : 0] rvfi_mem_wdata; \
`rvformal_extamo_wires \
`rvformal_csr_fflags_wires \
`rvformal_csr_frm_wires \
`rvformal_csr_fcsr_wires \
Expand All @@ -293,6 +309,7 @@ output [`RISCV_FORMAL_NRET * `RISCV_FORMAL_ILEN - 1 : 0] rvfi_insn, \
output [`RISCV_FORMAL_NRET - 1 : 0] rvfi_trap, \
output [`RISCV_FORMAL_NRET - 1 : 0] rvfi_halt, \
output [`RISCV_FORMAL_NRET - 1 : 0] rvfi_intr, \
output [`RISCV_FORMAL_NRET * 2 - 1 : 0] rvfi_mode, \
output [`RISCV_FORMAL_NRET * 5 - 1 : 0] rvfi_rs1_addr, \
output [`RISCV_FORMAL_NRET * 5 - 1 : 0] rvfi_rs2_addr, \
output [`RISCV_FORMAL_NRET * `RISCV_FORMAL_XLEN - 1 : 0] rvfi_rs1_rdata, \
Expand All @@ -306,6 +323,7 @@ output [`RISCV_FORMAL_NRET * `RISCV_FORMAL_XLEN/8 - 1 : 0] rvfi_mem_rmask, \
output [`RISCV_FORMAL_NRET * `RISCV_FORMAL_XLEN/8 - 1 : 0] rvfi_mem_wmask, \
output [`RISCV_FORMAL_NRET * `RISCV_FORMAL_XLEN - 1 : 0] rvfi_mem_rdata, \
output [`RISCV_FORMAL_NRET * `RISCV_FORMAL_XLEN - 1 : 0] rvfi_mem_wdata \
`rvformal_extamo_outputs \
`rvformal_csr_fflags_outputs \
`rvformal_csr_frm_outputs \
`rvformal_csr_fcsr_outputs \
Expand All @@ -321,6 +339,7 @@ input [`RISCV_FORMAL_NRET * `RISCV_FORMAL_ILEN - 1 : 0] rvfi_insn, \
input [`RISCV_FORMAL_NRET - 1 : 0] rvfi_trap, \
input [`RISCV_FORMAL_NRET - 1 : 0] rvfi_halt, \
input [`RISCV_FORMAL_NRET - 1 : 0] rvfi_intr, \
input [`RISCV_FORMAL_NRET * 2 - 1 : 0] rvfi_mode, \
input [`RISCV_FORMAL_NRET * 5 - 1 : 0] rvfi_rs1_addr, \
input [`RISCV_FORMAL_NRET * 5 - 1 : 0] rvfi_rs2_addr, \
input [`RISCV_FORMAL_NRET * `RISCV_FORMAL_XLEN - 1 : 0] rvfi_rs1_rdata, \
Expand All @@ -334,6 +353,7 @@ input [`RISCV_FORMAL_NRET * `RISCV_FORMAL_XLEN/8 - 1 : 0] rvfi_mem_rmask, \
input [`RISCV_FORMAL_NRET * `RISCV_FORMAL_XLEN/8 - 1 : 0] rvfi_mem_wmask, \
input [`RISCV_FORMAL_NRET * `RISCV_FORMAL_XLEN - 1 : 0] rvfi_mem_rdata, \
input [`RISCV_FORMAL_NRET * `RISCV_FORMAL_XLEN - 1 : 0] rvfi_mem_wdata \
`rvformal_extamo_inputs \
`rvformal_csr_fflags_inputs \
`rvformal_csr_frm_inputs \
`rvformal_csr_fcsr_inputs \
Expand All @@ -350,6 +370,7 @@ wire [`RISCV_FORMAL_ILEN - 1 : 0] insn = rvfi_insn [(_idx)*(`RISCV
wire [ 1 - 1 : 0] trap = rvfi_trap [(_idx)*( 1 ) +: 1 ]; \
wire [ 1 - 1 : 0] halt = rvfi_halt [(_idx)*( 1 ) +: 1 ]; \
wire [ 1 - 1 : 0] intr = rvfi_intr [(_idx)*( 1 ) +: 1 ]; \
wire [ 2 - 1 : 0] mode = rvfi_mode [(_idx)*( 2 ) +: 2 ]; \
wire [ 5 - 1 : 0] rs1_addr = rvfi_rs1_addr [(_idx)*( 5 ) +: 5 ]; \
wire [ 5 - 1 : 0] rs2_addr = rvfi_rs2_addr [(_idx)*( 5 ) +: 5 ]; \
wire [`RISCV_FORMAL_XLEN - 1 : 0] rs1_rdata = rvfi_rs1_rdata [(_idx)*(`RISCV_FORMAL_XLEN ) +: `RISCV_FORMAL_XLEN ]; \
Expand All @@ -363,6 +384,7 @@ wire [`RISCV_FORMAL_XLEN/8 - 1 : 0] mem_rmask = rvfi_mem_rmask [(_idx)*(`RISCV
wire [`RISCV_FORMAL_XLEN/8 - 1 : 0] mem_wmask = rvfi_mem_wmask [(_idx)*(`RISCV_FORMAL_XLEN/8) +: `RISCV_FORMAL_XLEN/8]; \
wire [`RISCV_FORMAL_XLEN - 1 : 0] mem_rdata = rvfi_mem_rdata [(_idx)*(`RISCV_FORMAL_XLEN ) +: `RISCV_FORMAL_XLEN ]; \
wire [`RISCV_FORMAL_XLEN - 1 : 0] mem_wdata = rvfi_mem_wdata [(_idx)*(`RISCV_FORMAL_XLEN ) +: `RISCV_FORMAL_XLEN ]; \
`rvformal_extamo_channel(_idx) \
`rvformal_csr_fflags_channel(_idx) \
`rvformal_csr_frm_channel(_idx) \
`rvformal_csr_fcsr_channel(_idx) \
Expand All @@ -379,6 +401,7 @@ end endgenerate
.rvfi_trap (rvfi_trap ), \
.rvfi_halt (rvfi_halt ), \
.rvfi_intr (rvfi_intr ), \
.rvfi_mode (rvfi_mode ), \
.rvfi_rs1_addr (rvfi_rs1_addr ), \
.rvfi_rs2_addr (rvfi_rs2_addr ), \
.rvfi_rs1_rdata (rvfi_rs1_rdata), \
Expand All @@ -392,6 +415,7 @@ end endgenerate
.rvfi_mem_wmask (rvfi_mem_wmask), \
.rvfi_mem_rdata (rvfi_mem_rdata), \
.rvfi_mem_wdata (rvfi_mem_wdata) \
`rvformal_extamo_conn \
`rvformal_csr_fflags_conn \
`rvformal_csr_frm_conn \
`rvformal_csr_fcsr_conn \
Expand Down

0 comments on commit a52eb8f

Please sign in to comment.