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

add RTL LINT scripts. #931

Merged
merged 4 commits into from
Feb 15, 2024
Merged
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
2 changes: 1 addition & 1 deletion .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -18,9 +18,9 @@ TAGS
/build
/Bender.lock
/Bender.local
golden_reference_design
golden.src
revised.src
cadence_conformal
golden_reference_design
synopsys_formality
questa_autocheck
28 changes: 28 additions & 0 deletions scripts/lint/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
# RTL source Lint

This folder contains LINT scripts that runs using SiemensEDA Questa AutoCheck tool. It requires SiemensEDA QuestaSim to first compile the design.

Those scripts allow to check RTL coding quality using common guidelines and rules. It can find syntax errors or issues leading to bad/incorrect synthesis (like latches in combinational process).
Common practice is to launch LINT check prior to committing RTL sources to git repository.

As cv32e40p\_top has 5 parameters and to be able to check different parameters values, a new top level module (cv32e40p\_wrapper) has been created together with some predefined configuration packages (in config\_?p\_?f\_?z\_?lat\_??c directories).

Configuration directory naming style is:
- \_?p : PULP enabled or not (0 or 1)
- \_?f : FPU enabled or not (0 or 1)
- \_?z : ZFINX enabled or not (0 or 1)
- \_?lat : FPU instructions latency (0, 1 or 2)
- \_?c : PULP\_CLUSTER enabled or not (0 or 1)

### Running the script

From a shell, please execute:

```
./lint.sh 1p_0f_0z_0lat_0c
```

The script uses `../../rtl` as design sources to check.

Intermediate logs are visible in `questa_autocheck/config_?p_?f_?z_?lat_?c` and `questa_autocheck/config_?p_?f_?z_?lat_?c/formal_lint_out` and final lint report in `questa_autocheck/config_?p_?f_?z_?lat_?c/formal_lint.rpt`

14 changes: 14 additions & 0 deletions scripts/lint/autocheck_common_rules.do
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
autocheck enable
autocheck disable -type ARITH_OVERFLOW_SUB
autocheck disable -type ARITH_OVERFLOW_VAL
autocheck disable -type CASE_DEFAULT
autocheck disable -type DECLARATION_UNUSED_UNDRIVEN
autocheck disable -type FUNCTION_INCOMPLETE_ASSIGN
autocheck disable -type INDEX_UNREACHABLE
autocheck disable -type INIT_X_OPTIMISM
autocheck disable -type INIT_X_PESSIMISM
autocheck disable -type INIT_X_UNRESOLVED
autocheck disable -type INIT_X_UNRESOLVED_MEM
autocheck disable -type REG_RACE
autocheck disable -type REG_STUCK_AT
configure message severity fatal -id elaboration-835
19 changes: 19 additions & 0 deletions scripts/lint/config_0p_0f_0z_0lat_0c/cv32e40p_config_pkg.sv
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
`ifndef CV32E40P_CONFIG_PKG
`define CV32E40P_CONFIG_PKG

package cv32e40p_config_pkg;

parameter bit COREV_PULP = 0;
parameter bit COREV_CLUSTER = 0;
parameter bit FPU = 0;
parameter int FPU_ADDMUL_LAT = 0;
parameter int FPU_OTHERS_LAT = 0;
parameter bit ZFINX = 0;
parameter int INSTR_ADDR_MEM_WIDTH = 13;
parameter int DATA_ADDR_MEM_WIDTH = 13;

endpackage

`endif


19 changes: 19 additions & 0 deletions scripts/lint/config_1p_0f_0z_0lat_0c/cv32e40p_config_pkg.sv
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
`ifndef CV32E40P_CONFIG_PKG
`define CV32E40P_CONFIG_PKG

package cv32e40p_config_pkg;

parameter bit COREV_PULP = 1;
parameter bit COREV_CLUSTER = 0;
parameter bit FPU = 0;
parameter int FPU_ADDMUL_LAT = 0;
parameter int FPU_OTHERS_LAT = 0;
parameter bit ZFINX = 0;
parameter int INSTR_ADDR_MEM_WIDTH = 13;
parameter int DATA_ADDR_MEM_WIDTH = 13;

endpackage

`endif


19 changes: 19 additions & 0 deletions scripts/lint/config_1p_1f_0z_0lat_0c/cv32e40p_config_pkg.sv
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
`ifndef CV32E40P_CONFIG_PKG
`define CV32E40P_CONFIG_PKG

package cv32e40p_config_pkg;

parameter bit COREV_PULP = 1;
parameter bit COREV_CLUSTER = 0;
parameter bit FPU = 1;
parameter int FPU_ADDMUL_LAT = 0;
parameter int FPU_OTHERS_LAT = 0;
parameter bit ZFINX = 0;
parameter int INSTR_ADDR_MEM_WIDTH = 13;
parameter int DATA_ADDR_MEM_WIDTH = 13;

endpackage

`endif


19 changes: 19 additions & 0 deletions scripts/lint/config_1p_1f_0z_1lat_0c/cv32e40p_config_pkg.sv
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
`ifndef CV32E40P_CONFIG_PKG
`define CV32E40P_CONFIG_PKG

package cv32e40p_config_pkg;

parameter bit COREV_PULP = 1;
parameter bit COREV_CLUSTER = 0;
parameter bit FPU = 1;
parameter int FPU_ADDMUL_LAT = 1;
parameter int FPU_OTHERS_LAT = 1;
parameter bit ZFINX = 0;
parameter int INSTR_ADDR_MEM_WIDTH = 13;
parameter int DATA_ADDR_MEM_WIDTH = 13;

endpackage

`endif


19 changes: 19 additions & 0 deletions scripts/lint/config_1p_1f_0z_2lat_0c/cv32e40p_config_pkg.sv
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
`ifndef CV32E40P_CONFIG_PKG
`define CV32E40P_CONFIG_PKG

package cv32e40p_config_pkg;

parameter bit COREV_PULP = 1;
parameter bit COREV_CLUSTER = 0;
parameter bit FPU = 1;
parameter int FPU_ADDMUL_LAT = 2;
parameter int FPU_OTHERS_LAT = 2;
parameter bit ZFINX = 0;
parameter int INSTR_ADDR_MEM_WIDTH = 13;
parameter int DATA_ADDR_MEM_WIDTH = 13;

endpackage

`endif


19 changes: 19 additions & 0 deletions scripts/lint/config_1p_1f_1z_0lat_0c/cv32e40p_config_pkg.sv
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
`ifndef CV32E40P_CONFIG_PKG
`define CV32E40P_CONFIG_PKG

package cv32e40p_config_pkg;

parameter bit COREV_PULP = 1;
parameter bit COREV_CLUSTER = 0;
parameter bit FPU = 1;
parameter int FPU_ADDMUL_LAT = 0;
parameter int FPU_OTHERS_LAT = 0;
parameter bit ZFINX = 1;
parameter int INSTR_ADDR_MEM_WIDTH = 13;
parameter int DATA_ADDR_MEM_WIDTH = 13;

endpackage

`endif


19 changes: 19 additions & 0 deletions scripts/lint/config_1p_1f_1z_1lat_0c/cv32e40p_config_pkg.sv
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
`ifndef CV32E40P_CONFIG_PKG
`define CV32E40P_CONFIG_PKG

package cv32e40p_config_pkg;

parameter bit COREV_PULP = 1;
parameter bit COREV_CLUSTER = 0;
parameter bit FPU = 1;
parameter int FPU_ADDMUL_LAT = 1;
parameter int FPU_OTHERS_LAT = 1;
parameter bit ZFINX = 1;
parameter int INSTR_ADDR_MEM_WIDTH = 13;
parameter int DATA_ADDR_MEM_WIDTH = 13;

endpackage

`endif


19 changes: 19 additions & 0 deletions scripts/lint/config_1p_1f_1z_2lat_0c/cv32e40p_config_pkg.sv
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
`ifndef CV32E40P_CONFIG_PKG
`define CV32E40P_CONFIG_PKG

package cv32e40p_config_pkg;

parameter bit COREV_PULP = 1;
parameter bit COREV_CLUSTER = 0;
parameter bit FPU = 1;
parameter int FPU_ADDMUL_LAT = 2;
parameter int FPU_OTHERS_LAT = 2;
parameter bit ZFINX = 1;
parameter int INSTR_ADDR_MEM_WIDTH = 13;
parameter int DATA_ADDR_MEM_WIDTH = 13;

endpackage

`endif


19 changes: 19 additions & 0 deletions scripts/lint/config_1p_1f_1z_2lat_1c/cv32e40p_config_pkg.sv
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
`ifndef CV32E40P_CONFIG_PKG
`define CV32E40P_CONFIG_PKG

package cv32e40p_config_pkg;

parameter bit COREV_PULP = 1;
parameter bit COREV_CLUSTER = 1;
parameter bit FPU = 1;
parameter int FPU_ADDMUL_LAT = 2;
parameter int FPU_OTHERS_LAT = 2;
parameter bit ZFINX = 1;
parameter int INSTR_ADDR_MEM_WIDTH = 13;
parameter int DATA_ADDR_MEM_WIDTH = 13;

endpackage

`endif


123 changes: 123 additions & 0 deletions scripts/lint/cv32e40p_wrapper.sv
Original file line number Diff line number Diff line change
@@ -0,0 +1,123 @@
// Copyright 2024 OpenHW Group and Dolphin Design
//
// Licensed under the Solderpad Hardware Licence, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// https://solderpad.org/licenses/
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
//
// SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1

// Contributor(s): Pascal Gouedo, Dolphin Design <[email protected]>
//
// Design Name: CV32E40P RTL Lint wrapper
//
// Description: Wrapper file instantiating CV32E40P top and importing
// a configuration package to be used for RTL LINT checks.

module cv32e40p_wrapper (
// Clock and Reset
input logic clk_i,
input logic rst_ni,

input logic pulp_clock_en_i,
input logic scan_cg_en_i,

input logic [31:0] boot_addr_i,
input logic [31:0] mtvec_addr_i,
input logic [31:0] dm_halt_addr_i,
input logic [31:0] hart_id_i,
input logic [31:0] dm_exception_addr_i,

// Instruction memory interface
output logic instr_req_o,
input logic instr_gnt_i,
input logic instr_rvalid_i,
output logic [31:0] instr_addr_o,
input logic [31:0] instr_rdata_i,

// Data memory interface
output logic data_req_o,
input logic data_gnt_i,
input logic data_rvalid_i,
output logic data_we_o,
output logic [ 3:0] data_be_o,
output logic [31:0] data_addr_o,
output logic [31:0] data_wdata_o,
input logic [31:0] data_rdata_i,

// Interrupt inputs
input logic [31:0] irq_i,
output logic irq_ack_o,
output logic [ 4:0] irq_id_o,

// Debug Interface
input logic debug_req_i,
output logic debug_havereset_o,
output logic debug_running_o,
output logic debug_halted_o,

// CPU Control Signals
input logic fetch_enable_i,
output logic core_sleep_o
);

import cv32e40p_config_pkg::*;

// Instantiate the Core
cv32e40p_top #(
.COREV_PULP (COREV_PULP),
.COREV_CLUSTER (COREV_CLUSTER),
.FPU (FPU),
.FPU_ADDMUL_LAT (FPU_ADDMUL_LAT),
.FPU_OTHERS_LAT (FPU_OTHERS_LAT),
.ZFINX (ZFINX),
.NUM_MHPMCOUNTERS(1)
) top_i (
.clk_i (clk_i),
.rst_ni(rst_ni),

.pulp_clock_en_i(pulp_clock_en_i),
.scan_cg_en_i (scan_cg_en_i),

.boot_addr_i (boot_addr_i),
.mtvec_addr_i (mtvec_addr_i),
.dm_halt_addr_i (dm_halt_addr_i),
.hart_id_i (hart_id_i),
.dm_exception_addr_i(dm_exception_addr_i),

.instr_req_o (instr_req_o),
.instr_gnt_i (instr_gnt_i),
.instr_rvalid_i(instr_rvalid_i),
.instr_addr_o (instr_addr_o),
.instr_rdata_i (instr_rdata_i),

.data_req_o (data_req_o),
.data_gnt_i (data_gnt_i),
.data_rvalid_i(data_rvalid_i),
.data_we_o (data_we_o),
.data_be_o (data_be_o),
.data_addr_o (data_addr_o),
.data_wdata_o (data_wdata_o),
.data_rdata_i (data_rdata_i),

.irq_i (irq_i),
.irq_ack_o(irq_ack_o),
.irq_id_o (irq_id_o),

.debug_req_i (debug_req_i),
.debug_havereset_o(debug_havereset_o),
.debug_running_o (debug_running_o),
.debug_halted_o (debug_halted_o),

.fetch_enable_i(fetch_enable_i),
.core_sleep_o (core_sleep_o)
);

endmodule
16 changes: 16 additions & 0 deletions scripts/lint/formal_lint_rules.do
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
# define all clocks
netlist clock clk_i -period 100 -waveform 0 50

# define all reset
netlist reset rst_ni -active_low -async

# define clock domain for reset
netlist port domain rst_ni -clock clk_i

# define special case
netlist constant scan_cg_en_i 1'b0
netlist constant pulp_clock_en_i 1'b0

# disable rules
autocheck disable -type FSM_DEADLOCK_STATE FSM_LOCKOUT_STATE

Loading
Loading