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 1 commit
Commits
File filter...
Filter file types
Jump to…
Jump to file
Failed to load files.

Always

Just for now

Rename macro rvformal_const_rand_reg to rvformal_rand_const_reg

So it matches the new order of the modifiers
  • Loading branch information
leonschoorl committed Jan 26, 2021
commit 0a295312075b4e1d8f2f2040b0cd53fe6d83222c
@@ -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;
@@ -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 rand const 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 rand const 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,16 +126,16 @@ 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:
ProTip! Use n and p to navigate between commits in a pull request.