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
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions checks/rvfi_causal_check.sv
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
16 changes: 8 additions & 8 deletions checks/rvfi_csrw_check.sv
Original file line number Diff line number Diff line change
Expand Up @@ -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)));

Expand All @@ -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 =
Expand Down
2 changes: 1 addition & 1 deletion checks/rvfi_dmem_check.sv
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
4 changes: 2 additions & 2 deletions checks/rvfi_imem_check.sv
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand Down
2 changes: 1 addition & 1 deletion checks/rvfi_liveness_check.sv
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
6 changes: 3 additions & 3 deletions checks/rvfi_macros.py
Original file line number Diff line number Diff line change
Expand Up @@ -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("")
Expand Down
6 changes: 3 additions & 3 deletions checks/rvfi_macros.vh
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion checks/rvfi_pc_bwd_check.sv
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand Down
2 changes: 1 addition & 1 deletion checks/rvfi_pc_fwd_check.sv
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand Down
4 changes: 2 additions & 2 deletions checks/rvfi_reg_check.sv
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand Down
2 changes: 1 addition & 1 deletion checks/rvfi_unique_check.sv
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
8 changes: 4 additions & 4 deletions docs/config.md
Original file line number Diff line number Diff line change
Expand Up @@ -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:

Expand Down