From 96ddaa0e0167ad10b4953ed39b123eed26f52ea0 Mon Sep 17 00:00:00 2001 From: Leon Schoorl Date: Tue, 26 Jan 2021 16:46:52 +0100 Subject: [PATCH 1/3] Switch "const" and "rand" modifier order The current Yosys only accepts the order: rand const The other way round results in: ERROR: syntax error, unexpected TOK_RAND And "rand const" is also the way they show it in their README: https://github.com/YosysHQ/yosys/blob/master/README.md#non-standard-or-systemverilog-features-for-formal-verification --- checks/rvfi_macros.py | 2 +- checks/rvfi_macros.vh | 2 +- docs/config.md | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/checks/rvfi_macros.py b/checks/rvfi_macros.py index 2b5fcdb..3647868 100644 --- a/checks/rvfi_macros.py +++ b/checks/rvfi_macros.py @@ -18,7 +18,7 @@ print("") print("`ifdef YOSYS") print("`define rvformal_rand_reg rand reg") -print("`define rvformal_const_rand_reg const rand reg") +print("`define rvformal_const_rand_reg rand const reg") print("`else") print("`ifdef SIMULATION") print("`define rvformal_rand_reg reg") diff --git a/checks/rvfi_macros.vh b/checks/rvfi_macros.vh index 3ffcde4..28e95e2 100644 --- a/checks/rvfi_macros.vh +++ b/checks/rvfi_macros.vh @@ -2,7 +2,7 @@ `ifdef YOSYS `define rvformal_rand_reg rand reg -`define rvformal_const_rand_reg const rand reg +`define rvformal_const_rand_reg rand const reg `else `ifdef SIMULATION `define rvformal_rand_reg reg diff --git a/docs/config.md b/docs/config.md index 1ac6fe0..35e621b 100644 --- a/docs/config.md +++ b/docs/config.md @@ -141,7 +141,7 @@ 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: From 0a295312075b4e1d8f2f2040b0cd53fe6d83222c Mon Sep 17 00:00:00 2001 From: Leon Schoorl Date: Tue, 26 Jan 2021 16:48:47 +0100 Subject: [PATCH 2/3] Rename macro rvformal_const_rand_reg to rvformal_rand_const_reg So it matches the new order of the modifiers --- checks/rvfi_causal_check.sv | 4 ++-- checks/rvfi_dmem_check.sv | 2 +- checks/rvfi_imem_check.sv | 4 ++-- checks/rvfi_liveness_check.sv | 2 +- checks/rvfi_macros.py | 6 +++--- checks/rvfi_macros.vh | 6 +++--- checks/rvfi_pc_bwd_check.sv | 2 +- checks/rvfi_pc_fwd_check.sv | 2 +- checks/rvfi_reg_check.sv | 4 ++-- checks/rvfi_unique_check.sv | 2 +- docs/config.md | 6 +++--- 11 files changed, 20 insertions(+), 20 deletions(-) diff --git a/checks/rvfi_causal_check.sv b/checks/rvfi_causal_check.sv index c6fdebd..14962f6 100644 --- a/checks/rvfi_causal_check.sv +++ b/checks/rvfi_causal_check.sv @@ -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; diff --git a/checks/rvfi_dmem_check.sv b/checks/rvfi_dmem_check.sv index c0e2147..e713800 100644 --- a/checks/rvfi_dmem_check.sv +++ b/checks/rvfi_dmem_check.sv @@ -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; diff --git a/checks/rvfi_imem_check.sv b/checks/rvfi_imem_check.sv index 445612e..0ad019d 100644 --- a/checks/rvfi_imem_check.sv +++ b/checks/rvfi_imem_check.sv @@ -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; diff --git a/checks/rvfi_liveness_check.sv b/checks/rvfi_liveness_check.sv index 589ad06..66046f1 100644 --- a/checks/rvfi_liveness_check.sv +++ b/checks/rvfi_liveness_check.sv @@ -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; diff --git a/checks/rvfi_macros.py b/checks/rvfi_macros.py index 3647868..08152b4 100644 --- a/checks/rvfi_macros.py +++ b/checks/rvfi_macros.py @@ -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("") diff --git a/checks/rvfi_macros.vh b/checks/rvfi_macros.vh index 28e95e2..52a635c 100644 --- a/checks/rvfi_macros.vh +++ b/checks/rvfi_macros.vh @@ -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 diff --git a/checks/rvfi_pc_bwd_check.sv b/checks/rvfi_pc_bwd_check.sv index 3788016..1a44f74 100644 --- a/checks/rvfi_pc_bwd_check.sv +++ b/checks/rvfi_pc_bwd_check.sv @@ -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; diff --git a/checks/rvfi_pc_fwd_check.sv b/checks/rvfi_pc_fwd_check.sv index 78026b9..b1e1740 100644 --- a/checks/rvfi_pc_fwd_check.sv +++ b/checks/rvfi_pc_fwd_check.sv @@ -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; diff --git a/checks/rvfi_reg_check.sv b/checks/rvfi_reg_check.sv index 9b3d055..62d014c 100644 --- a/checks/rvfi_reg_check.sv +++ b/checks/rvfi_reg_check.sv @@ -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; diff --git a/checks/rvfi_unique_check.sv b/checks/rvfi_unique_check.sv index 3a67308..9e8d0ee 100644 --- a/checks/rvfi_unique_check.sv +++ b/checks/rvfi_unique_check.sv @@ -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; diff --git a/docs/config.md b/docs/config.md index 35e621b..3f48898 100644 --- a/docs/config.md +++ b/docs/config.md @@ -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: From e0fd8ce5e9e33d26903671c8fb9e46766c4e85d4 Mon Sep 17 00:00:00 2001 From: Leon Schoorl Date: Tue, 26 Jan 2021 17:46:09 +0100 Subject: [PATCH 3/3] Fix syntax errors in rvfi_csrw_check.sv `csrget(`RISCV_FORMAL_CSRW_NAME, rmask) Got expanded into: rvfi.csr_mcycle_ rmask Because of the extra space, this resulted in: [csrw_mcycle_ch0] base: rvfi_csrw_check.sv:56: ERROR: syntax error, unexpected TOK_ID --- checks/rvfi_csrw_check.sv | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/checks/rvfi_csrw_check.sv b/checks/rvfi_csrw_check.sv index f798704..a866102 100644 --- a/checks/rvfi_csrw_check.sv +++ b/checks/rvfi_csrw_check.sv @@ -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 =