add RTL LINT scripts.

.gitignore

@@ -18,3 +18,9 @@ TAGS
 /build
 /Bender.lock
 /Bender.local
+golden_reference_design
+golden.src
+revised.src
+cadence_conformal
+synopsys_formality
+questa_autocheck

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`
+

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

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
+
+

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
+
+

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
+
+

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
+
+

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
+
+

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
+
+

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
+
+

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
+
+

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
+
+

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

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
+