From c05040dd67d8d59e1253f6ad1a8ac042c36f2e50 Mon Sep 17 00:00:00 2001 From: Pascal Gouedo Date: Mon, 8 Jan 2024 10:50:19 +0100 Subject: [PATCH 1/3] RTL LINT scripts. Signed-off-by: Pascal Gouedo --- .gitignore | 6 + scripts/lint/README.md | 28 +++++ scripts/lint/autocheck_common_rules.do | 14 +++ .../cv32e40p_config_pkg.sv | 19 +++ .../cv32e40p_config_pkg.sv | 19 +++ .../cv32e40p_config_pkg.sv | 19 +++ .../cv32e40p_config_pkg.sv | 19 +++ .../cv32e40p_config_pkg.sv | 19 +++ .../cv32e40p_config_pkg.sv | 19 +++ .../cv32e40p_config_pkg.sv | 19 +++ .../cv32e40p_config_pkg.sv | 19 +++ .../cv32e40p_config_pkg.sv | 19 +++ scripts/lint/cv32e40p_wrapper.sv | 113 ++++++++++++++++++ scripts/lint/formal_lint_rules.do | 16 +++ scripts/lint/lint.sh | 60 ++++++++++ scripts/lint/proc_dumpAutoCheckSummary.tcl | 74 ++++++++++++ scripts/lint/qverify_analysis.do | 8 ++ scripts/lint/qverify_autocheck.do | 4 + 18 files changed, 494 insertions(+) create mode 100644 scripts/lint/README.md create mode 100644 scripts/lint/autocheck_common_rules.do create mode 100644 scripts/lint/config_0p_0f_0z_0lat_0c/cv32e40p_config_pkg.sv create mode 100644 scripts/lint/config_1p_0f_0z_0lat_0c/cv32e40p_config_pkg.sv create mode 100644 scripts/lint/config_1p_1f_0z_0lat_0c/cv32e40p_config_pkg.sv create mode 100644 scripts/lint/config_1p_1f_0z_1lat_0c/cv32e40p_config_pkg.sv create mode 100644 scripts/lint/config_1p_1f_0z_2lat_0c/cv32e40p_config_pkg.sv create mode 100644 scripts/lint/config_1p_1f_1z_0lat_0c/cv32e40p_config_pkg.sv create mode 100644 scripts/lint/config_1p_1f_1z_1lat_0c/cv32e40p_config_pkg.sv create mode 100644 scripts/lint/config_1p_1f_1z_2lat_0c/cv32e40p_config_pkg.sv create mode 100644 scripts/lint/config_1p_1f_1z_2lat_1c/cv32e40p_config_pkg.sv create mode 100644 scripts/lint/cv32e40p_wrapper.sv create mode 100644 scripts/lint/formal_lint_rules.do create mode 100755 scripts/lint/lint.sh create mode 100644 scripts/lint/proc_dumpAutoCheckSummary.tcl create mode 100644 scripts/lint/qverify_analysis.do create mode 100644 scripts/lint/qverify_autocheck.do diff --git a/.gitignore b/.gitignore index ef351b194..66eb251ac 100644 --- a/.gitignore +++ b/.gitignore @@ -18,3 +18,9 @@ TAGS /build /Bender.lock /Bender.local +golden_reference_design +golden.src +revised.src +cadence_conformal +synopsys_formality +questa_autocheck diff --git a/scripts/lint/README.md b/scripts/lint/README.md new file mode 100644 index 000000000..8aade066c --- /dev/null +++ b/scripts/lint/README.md @@ -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` + diff --git a/scripts/lint/autocheck_common_rules.do b/scripts/lint/autocheck_common_rules.do new file mode 100644 index 000000000..f977f2cd7 --- /dev/null +++ b/scripts/lint/autocheck_common_rules.do @@ -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 diff --git a/scripts/lint/config_0p_0f_0z_0lat_0c/cv32e40p_config_pkg.sv b/scripts/lint/config_0p_0f_0z_0lat_0c/cv32e40p_config_pkg.sv new file mode 100644 index 000000000..aeb194c04 --- /dev/null +++ b/scripts/lint/config_0p_0f_0z_0lat_0c/cv32e40p_config_pkg.sv @@ -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 + + diff --git a/scripts/lint/config_1p_0f_0z_0lat_0c/cv32e40p_config_pkg.sv b/scripts/lint/config_1p_0f_0z_0lat_0c/cv32e40p_config_pkg.sv new file mode 100644 index 000000000..03894df90 --- /dev/null +++ b/scripts/lint/config_1p_0f_0z_0lat_0c/cv32e40p_config_pkg.sv @@ -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 + + diff --git a/scripts/lint/config_1p_1f_0z_0lat_0c/cv32e40p_config_pkg.sv b/scripts/lint/config_1p_1f_0z_0lat_0c/cv32e40p_config_pkg.sv new file mode 100644 index 000000000..fc7ba9e7c --- /dev/null +++ b/scripts/lint/config_1p_1f_0z_0lat_0c/cv32e40p_config_pkg.sv @@ -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 + + diff --git a/scripts/lint/config_1p_1f_0z_1lat_0c/cv32e40p_config_pkg.sv b/scripts/lint/config_1p_1f_0z_1lat_0c/cv32e40p_config_pkg.sv new file mode 100644 index 000000000..c74225582 --- /dev/null +++ b/scripts/lint/config_1p_1f_0z_1lat_0c/cv32e40p_config_pkg.sv @@ -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 + + diff --git a/scripts/lint/config_1p_1f_0z_2lat_0c/cv32e40p_config_pkg.sv b/scripts/lint/config_1p_1f_0z_2lat_0c/cv32e40p_config_pkg.sv new file mode 100644 index 000000000..e17cc8b70 --- /dev/null +++ b/scripts/lint/config_1p_1f_0z_2lat_0c/cv32e40p_config_pkg.sv @@ -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 + + diff --git a/scripts/lint/config_1p_1f_1z_0lat_0c/cv32e40p_config_pkg.sv b/scripts/lint/config_1p_1f_1z_0lat_0c/cv32e40p_config_pkg.sv new file mode 100644 index 000000000..0d28e20ef --- /dev/null +++ b/scripts/lint/config_1p_1f_1z_0lat_0c/cv32e40p_config_pkg.sv @@ -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 + + diff --git a/scripts/lint/config_1p_1f_1z_1lat_0c/cv32e40p_config_pkg.sv b/scripts/lint/config_1p_1f_1z_1lat_0c/cv32e40p_config_pkg.sv new file mode 100644 index 000000000..e47e861c1 --- /dev/null +++ b/scripts/lint/config_1p_1f_1z_1lat_0c/cv32e40p_config_pkg.sv @@ -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 + + diff --git a/scripts/lint/config_1p_1f_1z_2lat_0c/cv32e40p_config_pkg.sv b/scripts/lint/config_1p_1f_1z_2lat_0c/cv32e40p_config_pkg.sv new file mode 100644 index 000000000..af5b4b732 --- /dev/null +++ b/scripts/lint/config_1p_1f_1z_2lat_0c/cv32e40p_config_pkg.sv @@ -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 + + diff --git a/scripts/lint/config_1p_1f_1z_2lat_1c/cv32e40p_config_pkg.sv b/scripts/lint/config_1p_1f_1z_2lat_1c/cv32e40p_config_pkg.sv new file mode 100644 index 000000000..f0a16fe74 --- /dev/null +++ b/scripts/lint/config_1p_1f_1z_2lat_1c/cv32e40p_config_pkg.sv @@ -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 + + diff --git a/scripts/lint/cv32e40p_wrapper.sv b/scripts/lint/cv32e40p_wrapper.sv new file mode 100644 index 000000000..760712c6f --- /dev/null +++ b/scripts/lint/cv32e40p_wrapper.sv @@ -0,0 +1,113 @@ +// Copyright 2018 ETH Zurich and University of Bologna. +// Copyright and related rights are licensed under the Solderpad Hardware +// License, Version 0.51 (the "License"); you may not use this file except in +// compliance with the License. You may obtain a copy of the License at +// http://solderpad.org/licenses/SHL-0.51. Unless required by applicable law +// or agreed to in writing, software, hardware and materials distributed under +// this 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. + +// Top file instantiating a CV32E40P top for lint + +module cv32e40p_wrapper ( + // Clock and Reset + input logic clk_i, + input logic rst_ni, + + input logic pulp_clock_en_i, // PULP clock enable (only used if COREV_CLUSTER = 1) + input logic scan_cg_en_i, // Enable all clock gates for testing + + // Core ID, Cluster ID, debug mode halt address and boot address are considered more or less static + 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, // CLINT interrupts + CLINT extension interrupts + 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 diff --git a/scripts/lint/formal_lint_rules.do b/scripts/lint/formal_lint_rules.do new file mode 100644 index 000000000..a52229177 --- /dev/null +++ b/scripts/lint/formal_lint_rules.do @@ -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 + diff --git a/scripts/lint/lint.sh b/scripts/lint/lint.sh new file mode 100755 index 000000000..259f9dae6 --- /dev/null +++ b/scripts/lint/lint.sh @@ -0,0 +1,60 @@ +#!/usr/bin/env bash + +# Copyright 2023 OpenHW Group +# Copyright 2023 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. +# +# Contributor: Pascal Gouedo + +if [[ $# -eq 0 ]]; then + CONFIG=config_0p_0f_0z_0lat_0c +else + CONFIG=config_$1 + if [[ ! -d $CONFIG ]]; then + echo "Config $CONFIG does not exists." + exit + fi +fi +echo "Lint of $CONFIG" + +if [[ -d questa_autocheck/$CONFIG ]]; then + rm -rf questa_autocheck/$CONFIG +fi +mkdir -p questa_autocheck/$CONFIG + +# Creating RTL file list +if [[ $CONFIG == *1f* ]]; then + MANIFEST=cv32e40p_fpu_manifest +else + MANIFEST=cv32e40p_manifest +fi + +UPSTREAM_DIR=$(pwd)/../../rtl +echo "$upstream_dir" +sed -n '/^+incdir+/s:${DESIGN_RTL_DIR}:'"$UPSTREAM_DIR"':p' ../../$MANIFEST.flist > questa_autocheck/$CONFIG/inc_design.f +sed -n '1,/cv32e40p_sim_clock_gate/{s:^${DESIGN_RTL_DIR}:'"$UPSTREAM_DIR"':p}' ../../$MANIFEST.flist > questa_autocheck/$CONFIG/src_design.f +echo "$(pwd)/$CONFIG/cv32e40p_config_pkg.sv" >> questa_autocheck/$CONFIG/src_design.f +echo "$(pwd)/cv32e40p_wrapper.sv" >> questa_autocheck/$CONFIG/src_design.f + +cd questa_autocheck/$CONFIG + +# Compiling Verilog / SystemVerilog RTL files +vlog -64 -nologo -source -timescale "1 ns / 1 ps" -sv -f inc_design.f -f src_design.f -assertdebug -work design_lib |& tee compile_design.log + +# Launching formal lint analysis +qverify -licq -c -od formal_lint_out -do ../../qverify_analysis.do |& tee formal_lint.log + +# Launching formal lint AutoCheck Summary +qverify -licq -c -od formal_lint_out -do ../../qverify_autocheck.do + diff --git a/scripts/lint/proc_dumpAutoCheckSummary.tcl b/scripts/lint/proc_dumpAutoCheckSummary.tcl new file mode 100644 index 000000000..3c3f2f710 --- /dev/null +++ b/scripts/lint/proc_dumpAutoCheckSummary.tcl @@ -0,0 +1,74 @@ +proc dumpAutoCheckSummary { filename } { + namespace import -force Autocheck::* + if { [catch { set fp [open $filename a] } msg] } { + puts "Unable to open $filename : $msg" + exit 1 + } + + set typecnt 0 + #--------- Find types --------------------------------------- + set checks [GetChecks] + while { [set check [GetNext $checks]] != "" } { + set type [GetType $check] + set severity($type) [GetSeverity $check] + lappend types $type + } + set types [lsort [lrmdups $types]] + #--------- Collect data for each type ----------------------- + foreach type $types { + set cnt 0 + set cnt_waiv 0 + set cnt_viol 0 + set cnt_caut 0 + set cnt_inconcl 0 + set cnt_info 0 + set cnt_eval 0 + set cnt_off 0 + set cnt_def 0 + set checks [GetChecks] + while { [set check [GetNext $checks]] != "" } { + if {[GetType $check] == $type} { +# debug +#puts $fp "[GetType $check]" +#puts $fp "[GetStatus $check]" +#puts $fp "[GetSeverity $check]" + ### DM ### increment different counters depending of status + if {[GetStatus $check] == "Waived"} { + incr cnt_waiv + } else { + set Severity [GetSeverity $check] + switch $Severity { + Violation {incr cnt_viol} + Caution {incr cnt_caut} + Inconclusive {incr cnt_inconcl} + } + ### DM ### add other (off, ...) if needed + } + } + } + + ### DM ### only prints when waived exist / or when violation or inconclusive + if {$cnt_waiv != 0} { + puts $fp "# ** Waived:\t$type ($cnt_waiv)" + puts "# ** Waived:\t$type ($cnt_waiv)" + } + if {$cnt_viol != 0} { + puts $fp "# ** Violation:\t$type ($cnt_viol)" + puts "# ** Violation:\t$type ($cnt_viol)" + } + if {$cnt_caut != 0} { + puts $fp "# ** Caution:\t$type ($cnt_caut)" + puts "# ** Caution:\t$type ($cnt_caut)" + } + if {$cnt_inconcl != 0} { + puts $fp "# ** Inconclusive:\t$type ($cnt_inconcl)" + puts "# ** Inconclusive:\t$type ($cnt_inconcl)" + } + ### DM ### add other (caution, off, ...) if needed + + } + puts $fp "==============================================" + puts $fp " [llength $types] Types; [GetCount $checks] Checks" + close $fp +} + diff --git a/scripts/lint/qverify_analysis.do b/scripts/lint/qverify_analysis.do new file mode 100644 index 000000000..e66554992 --- /dev/null +++ b/scripts/lint/qverify_analysis.do @@ -0,0 +1,8 @@ +set top cv32e40p_wrapper +source ../../autocheck_common_rules.do +source ../../formal_lint_rules.do +autocheck report inconclusives +autocheck compile -work design_lib -d cv32e40p_wrapper -L design_lib -L work +autocheck verify -jobs 1 +exit + diff --git a/scripts/lint/qverify_autocheck.do b/scripts/lint/qverify_autocheck.do new file mode 100644 index 000000000..9bbcc18a4 --- /dev/null +++ b/scripts/lint/qverify_autocheck.do @@ -0,0 +1,4 @@ +autocheck load db formal_lint_out/autocheck_verify.db +source ../../proc_dumpAutoCheckSummary.tcl +dumpAutoCheckSummary formal_lint.rpt +exit From 28695f35fbc1321c48e9c48a379f00fe03f67e54 Mon Sep 17 00:00:00 2001 From: Pascal Gouedo Date: Mon, 8 Jan 2024 16:05:51 +0100 Subject: [PATCH 2/3] RTL files header proposal. Signed-off-by: Pascal Gouedo --- scripts/lint/cv32e40p_wrapper.sv | 39 ++++++++++++++++++++------------ 1 file changed, 25 insertions(+), 14 deletions(-) diff --git a/scripts/lint/cv32e40p_wrapper.sv b/scripts/lint/cv32e40p_wrapper.sv index 760712c6f..1f2449f19 100644 --- a/scripts/lint/cv32e40p_wrapper.sv +++ b/scripts/lint/cv32e40p_wrapper.sv @@ -1,24 +1,35 @@ // Copyright 2018 ETH Zurich and University of Bologna. -// Copyright and related rights are licensed under the Solderpad Hardware -// License, Version 0.51 (the "License"); you may not use this file except in -// compliance with the License. You may obtain a copy of the License at -// http://solderpad.org/licenses/SHL-0.51. Unless required by applicable law -// or agreed to in writing, software, hardware and materials distributed under -// this 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. - -// Top file instantiating a CV32E40P top for lint +// Copyright 2023 OpenHW Group +// +// 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.0 + +// Contributor(s): Pascal Gouedo, Dolphin Design +// +// 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, // PULP clock enable (only used if COREV_CLUSTER = 1) - input logic scan_cg_en_i, // Enable all clock gates for testing + input logic pulp_clock_en_i, + input logic scan_cg_en_i, - // Core ID, Cluster ID, debug mode halt address and boot address are considered more or less static input logic [31:0] boot_addr_i, input logic [31:0] mtvec_addr_i, input logic [31:0] dm_halt_addr_i, @@ -43,7 +54,7 @@ module cv32e40p_wrapper ( input logic [31:0] data_rdata_i, // Interrupt inputs - input logic [31:0] irq_i, // CLINT interrupts + CLINT extension interrupts + input logic [31:0] irq_i, output logic irq_ack_o, output logic [ 4:0] irq_id_o, From 71d83549e1a9b0f29122cf5962fdf9926ea26020 Mon Sep 17 00:00:00 2001 From: Pascal Gouedo Date: Wed, 10 Jan 2024 15:29:10 +0100 Subject: [PATCH 3/3] Header corrected. Signed-off-by: Pascal Gouedo --- scripts/lint/cv32e40p_wrapper.sv | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/scripts/lint/cv32e40p_wrapper.sv b/scripts/lint/cv32e40p_wrapper.sv index 1f2449f19..135ee4fa9 100644 --- a/scripts/lint/cv32e40p_wrapper.sv +++ b/scripts/lint/cv32e40p_wrapper.sv @@ -1,5 +1,4 @@ -// Copyright 2018 ETH Zurich and University of Bologna. -// Copyright 2023 OpenHW Group +// 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. @@ -13,7 +12,7 @@ // See the License for the specific language governing permissions and // limitations under the License. // -// SPDX-License-Identifier: Apache-2.0 WITH SHL-2.0 +// SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1 // Contributor(s): Pascal Gouedo, Dolphin Design //