Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix some syntax errors #45

Open
wants to merge 3 commits into
base: master
from
Open
Changes from all commits
Commits
File filter...
Filter file types
Jump to…
Jump to file
Failed to load files.

Always

Just for now

@@ -16,8 +16,8 @@ module rvfi_causal_check (
input clock, reset, check,
`RVFI_INPUTS
);
`rvformal_const_rand_reg [63:0] insn_order;
`rvformal_const_rand_reg [4:0] register_index;
`rvformal_rand_const_reg [63:0] insn_order;
`rvformal_rand_const_reg [4:0] register_index;
reg found_non_causal = 0;

integer channel_idx;
@@ -53,10 +53,10 @@ module rvfi_csrw_check (
`endif
);

wire [63:0] csr_insn_rmask_full = `csrget(`RISCV_FORMAL_CSRW_NAME, rmask);
wire [63:0] csr_insn_wmask_full = `csrget(`RISCV_FORMAL_CSRW_NAME, wmask);
wire [63:0] csr_insn_rdata_full = `csrget(`RISCV_FORMAL_CSRW_NAME, rdata);
wire [63:0] csr_insn_wdata_full = `csrget(`RISCV_FORMAL_CSRW_NAME, wdata);
wire [63:0] csr_insn_rmask_full = `csrget(`RISCV_FORMAL_CSRW_NAME,rmask);
wire [63:0] csr_insn_wmask_full = `csrget(`RISCV_FORMAL_CSRW_NAME,wmask);
wire [63:0] csr_insn_rdata_full = `csrget(`RISCV_FORMAL_CSRW_NAME,rdata);
wire [63:0] csr_insn_wdata_full = `csrget(`RISCV_FORMAL_CSRW_NAME,wdata);

wire [63:0] csr_insn_changed_full = csr_insn_wmask_full & (~csr_insn_rmask_full | (csr_insn_rmask_full & (csr_insn_rdata_full ^ csr_insn_wdata_full)));

@@ -65,10 +65,10 @@ module rvfi_csrw_check (
wire [`RISCV_FORMAL_XLEN-1:0] csr_insn_rdata = (csr_hi ? csr_insn_rdata_full >> 32 : csr_insn_rdata_full) & (rvfi.ixl == 1 ? 'h FFFF_FFFF : -1);
wire [`RISCV_FORMAL_XLEN-1:0] csr_insn_wdata = (csr_hi ? csr_insn_wdata_full >> 32 : csr_insn_wdata_full) & (rvfi.ixl == 1 ? 'h FFFF_FFFF : -1);
`else
wire [`RISCV_FORMAL_XLEN-1:0] csr_insn_rmask = `csrget(`RISCV_FORMAL_CSRW_NAME, rmask);
wire [`RISCV_FORMAL_XLEN-1:0] csr_insn_wmask = `csrget(`RISCV_FORMAL_CSRW_NAME, wmask);
wire [`RISCV_FORMAL_XLEN-1:0] csr_insn_rdata = `csrget(`RISCV_FORMAL_CSRW_NAME, rdata);
wire [`RISCV_FORMAL_XLEN-1:0] csr_insn_wdata = `csrget(`RISCV_FORMAL_CSRW_NAME, wdata);
wire [`RISCV_FORMAL_XLEN-1:0] csr_insn_rmask = `csrget(`RISCV_FORMAL_CSRW_NAME,rmask);
wire [`RISCV_FORMAL_XLEN-1:0] csr_insn_wmask = `csrget(`RISCV_FORMAL_CSRW_NAME,wmask);
wire [`RISCV_FORMAL_XLEN-1:0] csr_insn_rdata = `csrget(`RISCV_FORMAL_CSRW_NAME,rdata);
wire [`RISCV_FORMAL_XLEN-1:0] csr_insn_wdata = `csrget(`RISCV_FORMAL_CSRW_NAME,wdata);
`endif

wire [`RISCV_FORMAL_XLEN-1:0] csr_insn_smask =
@@ -17,7 +17,7 @@ module rvfi_dmem_check (
output [`RISCV_FORMAL_XLEN-1:0] dmem_addr,
`RVFI_INPUTS
);
`rvformal_const_rand_reg [`RISCV_FORMAL_XLEN-1:0] dmem_addr_randval;
`rvformal_rand_const_reg [`RISCV_FORMAL_XLEN-1:0] dmem_addr_randval;
assign dmem_addr = dmem_addr_randval;

reg [`RISCV_FORMAL_XLEN-1:0] dmem_shadow;
@@ -18,8 +18,8 @@ module rvfi_imem_check (
output [15:0] imem_data,
`RVFI_INPUTS
);
`rvformal_const_rand_reg [`RISCV_FORMAL_XLEN-1:0] imem_addr_randval;
`rvformal_const_rand_reg [15:0] imem_data_randval;
`rvformal_rand_const_reg [`RISCV_FORMAL_XLEN-1:0] imem_addr_randval;
`rvformal_rand_const_reg [15:0] imem_data_randval;
assign imem_addr = imem_addr_randval;
assign imem_data = imem_data_randval;

@@ -16,7 +16,7 @@ module rvfi_liveness_check (
input clock, reset, trig, check,
`RVFI_INPUTS
);
`rvformal_const_rand_reg [63:0] insn_order;
`rvformal_rand_const_reg [63:0] insn_order;
reg found_next_insn = 0;

integer channel_idx;
@@ -18,14 +18,14 @@
print("")
print("`ifdef YOSYS")
print("`define rvformal_rand_reg rand reg")
print("`define rvformal_const_rand_reg const rand reg")
print("`define rvformal_rand_const_reg rand const reg")
print("`else")
print("`ifdef SIMULATION")
print("`define rvformal_rand_reg reg")
print("`define rvformal_const_rand_reg reg")
print("`define rvformal_rand_const_reg reg")
print("`else")
print("`define rvformal_rand_reg wire")
print("`define rvformal_const_rand_reg reg")
print("`define rvformal_rand_const_reg reg")
print("`endif")
print("`endif")
print("")
@@ -2,14 +2,14 @@

`ifdef YOSYS
`define rvformal_rand_reg rand reg
`define rvformal_const_rand_reg const rand reg
`define rvformal_rand_const_reg rand const reg
`else
`ifdef SIMULATION
`define rvformal_rand_reg reg
`define rvformal_const_rand_reg reg
`define rvformal_rand_const_reg reg
`else
`define rvformal_rand_reg wire
`define rvformal_const_rand_reg reg
`define rvformal_rand_const_reg reg
`endif
`endif

@@ -16,7 +16,7 @@ module rvfi_pc_bwd_check (
input clock, reset, check,
`RVFI_INPUTS
);
`rvformal_const_rand_reg [63:0] insn_order;
`rvformal_rand_const_reg [63:0] insn_order;
reg [`RISCV_FORMAL_XLEN-1:0] expect_pc;
reg expect_pc_valid = 0;

@@ -16,7 +16,7 @@ module rvfi_pc_fwd_check (
input clock, reset, check,
`RVFI_INPUTS
);
`rvformal_const_rand_reg [63:0] insn_order;
`rvformal_rand_const_reg [63:0] insn_order;
reg [`RISCV_FORMAL_XLEN-1:0] expect_pc;
reg expect_pc_valid = 0;

@@ -16,8 +16,8 @@ module rvfi_reg_check (
input clock, reset, check,
`RVFI_INPUTS
);
`rvformal_const_rand_reg [63:0] insn_order;
`rvformal_const_rand_reg [4:0] register_index;
`rvformal_rand_const_reg [63:0] insn_order;
`rvformal_rand_const_reg [4:0] register_index;
reg [`RISCV_FORMAL_XLEN-1:0] register_shadow = 0;
reg register_written = 0;

@@ -16,7 +16,7 @@ module rvfi_unique_check (
input clock, reset, trig, check,
`RVFI_INPUTS
);
`rvformal_const_rand_reg [63:0] insn_order;
`rvformal_rand_const_reg [63:0] insn_order;
reg found_other_insn = 0;

integer channel_idx;
@@ -126,22 +126,22 @@ Macros to declare wires, output ports, or input ports for all `rvfi_*` signals.
macro is for creating the proper connections on module instances. This macros can be
useful for routing the `rvfi_*` signals through the design hierarchy.

rvformal_rand_reg and rvformal_const_rand_reg
rvformal_rand_reg and rvformal_rand_const_reg
---------------------------------------------

Macros for defining unconstrained signals (`rvformal_rand_reg`) or constant signals with
an unconstrained initial value (`rvformal_const_rand_reg`).
an unconstrained initial value (`rvformal_rand_const_reg`).

Usage example:

`rvformal_rand_reg [7:0] anyseq;
`rvformal_const_rand_reg [7:0] anyconst;
`rvformal_rand_const_reg [7:0] anyconst;

For formal verification with Yosys (i.e. when `YOSYS` is defined), this will be
converted to the following code:

rand reg [7:0] anyseq;
const rand reg [7:0] anyconst;
rand const reg [7:0] anyconst;

For simulation (i.e. when `SIMULATION` is defined), this will be converted to:

ProTip! Use n and p to navigate between commits in a pull request.