Skip to content

GitLab

Commit 99991e11 authored by GuillemCabo's avatar GuillemCabo Committed by Guillem
Browse files

add SBY equivalence check tests 

Update README.md
parent abb16c31
Hide whitespace changes
Inline Side-by-side
README.md
View file @ 99991e11
...@@ -4,7 +4,7 @@ This repository contains the RTL and documentation for the unit. ...@@ -4,7 +4,7 @@ This repository contains the RTL and documentation for the unit.
* The specs for each feature and memory map calculator can be found under the ```docs``` folder. * The specs for each feature and memory map calculator can be found under the ```docs``` folder.
* Top levels for different configurations or wrappers are foun in ```rtl```. * Top levels for different configurations or wrappers are found in ```rtl```.
* RTL for Submodules (MCCU, RDC, Counters, etc..) can be foun in ```submodules```. * RTL for Submodules (MCCU, RDC, Counters, etc..) can be found in ```submodules```.
* Synth contains scripts for early area and frequency evaluation with yosys. * Synth contains scripts for early area and frequency evaluation with yosys.
* ```tb``` contains testbenes and verification scripts. * ```tb``` contains testbenches and verification scripts.
\ No newline at end of file
tb/formal/equivalence_pmu_ahb/lint.sh 0 → 100755
View file @ 99991e11
RED='\033[7;31m'
GREEN='\033[7;32m'
BLUE='\033[7;36m'
NC='\033[0m' # No Color
#Name tmp files and VARS
VERILATOR_LOG0=.verilator_pmu_ahb.log
TOP=../../../
#Clear tmp files if any
rm -f $VERILATOR_LOG0
rm -rf ./pmu_ahb
############
## TOP pmu_ahb.sv
############
# Run Verilator
printf "Please wait, running Verilator\n"
verilator --lint-only top.sv \
$TOP/hdl/pmu_ahb.sv \
$TOP/hdl/PMU_raw.sv \
$TOP/submodules/crossbar/hdl/crossbar.sv \
$TOP/submodules/MCCU/hdl/MCCU.sv \
$TOP/submodules/RDC/hdl/RDC.sv \
$TOP/submodules/quota/PMU_quota.sv \
$TOP/submodules/counters/PMU_counters.sv \
$TOP/submodules/overflow/PMU_overflow.sv \
$TOP/submodules/seu_ip/hamming32t26d_enc.sv \
$TOP/submodules/seu_ip/hamming32t26d_dec.sv \
$TOP/submodules/seu_ip/triple_reg.sv \
$TOP/submodules/seu_ip/way3_voter.sv \
$TOP/submodules/seu_ip/way3u2a_voter.sv \
$TOP/submodules/seu_ip/way3ua_voter.sv
# Run Spyglass
printf "Please wait, running Spyglass\n"
./$TOP/ci/runLintSV.sh top.sv \
$TOP/hdl/pmu_ahb.sv \
$TOP/hdl/PMU_raw.sv \
$TOP/submodules/crossbar/hdl/crossbar.sv \
$TOP/submodules/MCCU/hdl/MCCU.sv \
$TOP/submodules/RDC/hdl/RDC.sv \
$TOP/submodules/quota/PMU_quota.sv \
$TOP/submodules/counters/PMU_counters.sv \
$TOP/submodules/overflow/PMU_overflow.sv \
$TOP/submodules/seu_ip/hamming32t26d_enc.sv \
$TOP/submodules/seu_ip/hamming32t26d_dec.sv \
$TOP/submodules/seu_ip/triple_reg.sv \
$TOP/submodules/seu_ip/way3_voter.sv \
$TOP/submodules/seu_ip/way3u2a_voter.sv \
$TOP/submodules/seu_ip/way3ua_voter.sv
tb/formal/equivalence_pmu_ahb/run.sh 0 → 100755
View file @ 99991e11
#Check that the formal properties pass
sby -f top.sby | \
GREP_COLORS='mt=01;31' egrep --color=always 'Unreached|Unreached cover statement at|Assert failed in|' | \
GREP_COLORS='mt=01;31' egrep -i --color=always 'FAIL|FAILED|ERROR|syntax|' | \
GREP_COLORS='mt=01;34' egrep --color=always 'Reached cover statement at|BMC|' | \
GREP_COLORS='mt=01;32' egrep -i --color=always 'PASS|PASSED|' | \
GREP_COLORS='mt=01;33' egrep -i --color=always 'WARNING|' | \
GREP_COLORS='mt=01;36' egrep -i --color=always 'Writing trace to VCD file:|counterexample trace:|'
#Run a particular case
#sby -f pmu_ahb_cover.sby
#Show the trace of the cover
#gtkwave ./pmu_ahb/engine_0/trace.vcd pmu_ahb.gtkw
tb/formal/equivalence_pmu_ahb/top.gtkw 0 → 100644
View file @ 99991e11
[*]
[*] GTKWave Analyzer v3.3.110 (w)1999-2020 BSI
[*] Wed Jul 7 15:07:31 2021
[*]
[dumpfile] "/home/gcabo/BSC/bsc_pmu/tb/formal/equivalence_pmu_ahb/top/engine_0/trace.vcd"
[dumpfile_mtime] "Wed Jul 7 15:02:09 2021"
[dumpfile_size] 575555
[savefile] "/home/gcabo/BSC/bsc_pmu/tb/formal/equivalence_pmu_ahb/top.gtkw"
[timestart] 3
[size] 1853 1006
[pos] -1 -1
*-3.696324 34 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
[treeopen] top.
[treeopen] top.dut_ft_pmu_ahb.
[treeopen] top.dut_ft_pmu_ahb.inst_pmu_raw.
[treeopen] top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.
[treeopen] top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst1_RDC.
[treeopen] top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.
[treeopen] top.dut_ft_pmu_ahb.Stateft.
[treeopen] top.dut_pmu_ahb.
[treeopen] top.dut_pmu_ahb.inst_pmu_raw.
[treeopen] top.dut_pmu_ahb.inst_pmu_raw.genblk16.
[sst_width] 394
[signals_width] 456
[sst_expanded] 1
[sst_vpaned_height] 282
@28
[color] 7
top.clk_i
[color] 6
top.rstn_i
@200
-Top
@28
top.fthreadyo_o
top.fthresp_o[1:0]
@22
top.ftintr_MCCU_o[3:0]
@28
top.ftintr_RDC_o
top.ftintr_overflow_o
top.ftintr_quota_o
@22
top.dut_ft_pmu_ahb.dread_slave[31:0]
[color] 1
top.hrdata_o[31:0]
top.fthrdata_o[31:0]
@28
top.hreadyo_o
top.hresp_o[1:0]
@22
top.intr_MCCU_o[3:0]
@28
top.intr_RDC_o
top.intr_overflow_o
top.intr_quota_o
@200
-
@28
top.ftintr_FT1_o
@800028
#{top.intr_FT1_o} top.intr_FT1_o
@28
top.intr_FT1_o
@1001200
-group_end
@28
top.ftintr_FT2_o
top.intr_FT2_o
@200
-pmu_ahb
@22
[color] 1
top.dut_pmu_ahb.pmu_regs_int<41>[31:0]
top.dut_ft_pmu_ahb.pmu_regs_int<41>[31:0]
[color] 1
top.dut_pmu_ahb.slv_reg<41>[31:0]
top.dut_ft_pmu_ahb.slv_reg<41>[31:0]
[color] 1
top.dut_pmu_ahb.slv_reg_D<41>[31:0]
top.dut_ft_pmu_ahb.slv_reg_D<41>[31:0]
[color] 1
top.dut_pmu_ahb.slv_reg_Q<41>[31:0]
top.dut_ft_pmu_ahb.slv_reg_Q<41>[31:0]
[color] 1
top.dut_pmu_ahb.dread_slave[31:0]
@c00022
top.dut_ft_pmu_ahb.dread_slave[31:0]
@28
(0)top.dut_ft_pmu_ahb.dread_slave[31:0]
(1)top.dut_ft_pmu_ahb.dread_slave[31:0]
(2)top.dut_ft_pmu_ahb.dread_slave[31:0]
(3)top.dut_ft_pmu_ahb.dread_slave[31:0]
(4)top.dut_ft_pmu_ahb.dread_slave[31:0]
(5)top.dut_ft_pmu_ahb.dread_slave[31:0]
(6)top.dut_ft_pmu_ahb.dread_slave[31:0]
(7)top.dut_ft_pmu_ahb.dread_slave[31:0]
(8)top.dut_ft_pmu_ahb.dread_slave[31:0]
(9)top.dut_ft_pmu_ahb.dread_slave[31:0]
(10)top.dut_ft_pmu_ahb.dread_slave[31:0]
(11)top.dut_ft_pmu_ahb.dread_slave[31:0]
(12)top.dut_ft_pmu_ahb.dread_slave[31:0]
(13)top.dut_ft_pmu_ahb.dread_slave[31:0]
(14)top.dut_ft_pmu_ahb.dread_slave[31:0]
(15)top.dut_ft_pmu_ahb.dread_slave[31:0]
(16)top.dut_ft_pmu_ahb.dread_slave[31:0]
(17)top.dut_ft_pmu_ahb.dread_slave[31:0]
(18)top.dut_ft_pmu_ahb.dread_slave[31:0]
(19)top.dut_ft_pmu_ahb.dread_slave[31:0]
(20)top.dut_ft_pmu_ahb.dread_slave[31:0]
(21)top.dut_ft_pmu_ahb.dread_slave[31:0]
(22)top.dut_ft_pmu_ahb.dread_slave[31:0]
(23)top.dut_ft_pmu_ahb.dread_slave[31:0]
(24)top.dut_ft_pmu_ahb.dread_slave[31:0]
(25)top.dut_ft_pmu_ahb.dread_slave[31:0]
(26)top.dut_ft_pmu_ahb.dread_slave[31:0]
(27)top.dut_ft_pmu_ahb.dread_slave[31:0]
(28)top.dut_ft_pmu_ahb.dread_slave[31:0]
(29)top.dut_ft_pmu_ahb.dread_slave[31:0]
(30)top.dut_ft_pmu_ahb.dread_slave[31:0]
(31)top.dut_ft_pmu_ahb.dread_slave[31:0]
@1401200
-group_end
@200
-raw
-mccu
-rdc
@c00022
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.MCCU_watermark_ft2<0><0>[7:0]
@28
(0)top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.MCCU_watermark_ft2<0><0>[7:0]
(1)top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.MCCU_watermark_ft2<0><0>[7:0]
(2)top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.MCCU_watermark_ft2<0><0>[7:0]
(3)top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.MCCU_watermark_ft2<0><0>[7:0]
(4)top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.MCCU_watermark_ft2<0><0>[7:0]
(5)top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.MCCU_watermark_ft2<0><0>[7:0]
(6)top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.MCCU_watermark_ft2<0><0>[7:0]
(7)top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.MCCU_watermark_ft2<0><0>[7:0]
@1401200
-group_end
@22
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.MCCU_watermark_ft2<0><1>[7:0]
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.MCCU_watermark_ft2<1><0>[7:0]
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.MCCU_watermark_ft2<1><1>[7:0]
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.MCCU_watermark_ft2<2><0>[7:0]
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.MCCU_watermark_ft2<2><1>[7:0]
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.MCCU_watermark_ft2<3><0>[7:0]
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.MCCU_watermark_ft2<3><1>[7:0]
[color] 1
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.watermark_int<0>[7:0]
[color] 1
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.watermark_int<1>[7:0]
[color] 1
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.watermark_int<2>[7:0]
[color] 1
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.watermark_int<3>[7:0]
[color] 1
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.watermark_int<4>[7:0]
[color] 1
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.watermark_int<5>[7:0]
[color] 1
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.watermark_int<6>[7:0]
[color] 1
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.watermark_int<7>[7:0]
@200
-tmp
-General
@24
top.dut_ft_pmu_ahb.slv_index[5:0]
@28
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.clk_i
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.enable_i
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.events_i<0>[1:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.events_i<1>[1:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.events_i<2>[1:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.events_i<3>[1:0]
@22
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.events_weights_i<0><0>[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.events_weights_i<0><1>[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.events_weights_i<1><0>[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.events_weights_i<1><1>[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.events_weights_i<2><0>[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.events_weights_i<2><1>[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.events_weights_i<3><0>[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.events_weights_i<3><1>[7:0]
@29
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.enable_i
@28
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.events_i<0>[1:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.events_i<1>[1:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.events_i<2>[1:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.events_i<3>[1:0]
@22
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.events_weights_i<0><0>[7:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.events_weights_i<0><1>[7:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.events_weights_i<1><0>[7:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.events_weights_i<1><1>[7:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.events_weights_i<2><0>[7:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.events_weights_i<2><1>[7:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.events_weights_i<3><0>[7:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.events_weights_i<3><1>[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.i[31:0]
@28
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.interruption_rdc_o
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.interruption_vector_int<0>[1:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.interruption_vector_int<1>[1:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.interruption_vector_int<2>[1:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.interruption_vector_int<3>[1:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.interruption_vector_rdc_o<0>[1:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.interruption_vector_rdc_o<1>[1:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.interruption_vector_rdc_o<2>[1:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.interruption_vector_rdc_o<3>[1:0]
@22
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.max_value<0>[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.max_value<1>[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.max_value<2>[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.max_value<3>[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.max_value<4>[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.max_value<5>[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.max_value<6>[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.max_value<7>[7:0]
@28
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.past_interruption_rdc_o
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.rstn_i
@22
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.unpacked_vector_rdc_int[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.watermark_int<0>[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.watermark_int<1>[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.watermark_int<2>[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.watermark_int<3>[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.watermark_int<4>[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.watermark_int<5>[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.watermark_int<6>[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.watermark_int<7>[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.watermark_o<0><0>[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.watermark_o<0><1>[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.watermark_o<1><0>[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.watermark_o<1><1>[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.watermark_o<2><0>[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.watermark_o<2><1>[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.watermark_o<3><0>[7:0]
top.dut_pmu_ahb.inst_pmu_raw.genblk16.inst_RDC.watermark_o<3><1>[7:0]
@28
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.clk_i
@200
-
@22
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.i[31:0]
@28
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.interruption_rdc_o
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.interruption_vector_int<0>[1:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.interruption_vector_int<1>[1:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.interruption_vector_int<2>[1:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.interruption_vector_int<3>[1:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.interruption_vector_rdc_o<0>[1:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.interruption_vector_rdc_o<1>[1:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.interruption_vector_rdc_o<2>[1:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.interruption_vector_rdc_o<3>[1:0]
@22
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.max_value<0>[7:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.max_value<1>[7:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.max_value<2>[7:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.max_value<3>[7:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.max_value<4>[7:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.max_value<5>[7:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.max_value<6>[7:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.max_value<7>[7:0]
@28
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.past_interruption_rdc_o
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.rstn_i
@22
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.unpacked_vector_rdc_int[7:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.watermark_int<0>[7:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.watermark_int<1>[7:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.watermark_int<2>[7:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.watermark_int<3>[7:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.watermark_int<4>[7:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.watermark_int<5>[7:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.watermark_int<6>[7:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.watermark_int<7>[7:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.watermark_o<0><0>[7:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.watermark_o<0><1>[7:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.watermark_o<1><0>[7:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.watermark_o<1><1>[7:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.watermark_o<2><0>[7:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.watermark_o<2><1>[7:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.watermark_o<3><0>[7:0]
[color] 1
top.dut_ft_pmu_ahb.inst_pmu_raw.Rdctrip.inst2_RDC.watermark_o<3><1>[7:0]
[pattern_trace] 1
[pattern_trace] 0
tb/formal/equivalence_pmu_ahb/top.sby 0 → 100644
View file @ 99991e11
[options]
mode bmc
depth 25
#append 6
[engines]
smtbmc boolector
smtbmc
#SystemVerilog
[script]
verific -vlog-define EQ_CHECK
verific -sv top.sv
verific -sv pmu_ahb.sv
verific -sv PMU_raw.sv
verific -sv PMU_counters.sv
verific -sv PMU_overflow.sv
verific -sv PMU_quota.sv
verific -sv MCCU.sv
verific -sv RDC.sv
verific -sv hamming32t26d_enc.sv
verific -sv hamming32t26d_dec.sv
verific -sv crossbar.sv
verific -sv way3u2a_voter.sv
verific -sv way3ua_voter.sv
verific -sv way3_voter.sv
verific -sv triple_reg.sv
verific -import -extnets -all top
prep -top top
#Verilog
#[script]
#read_verilog -formal pmu_ahb.sv
#prep -top pmu_ahb
#opt -share_all
[files]
./top.sv
../../../hdl/pmu_ahb.sv
../../../hdl/PMU_raw.sv
../../../submodules/counters/PMU_counters.sv
../../../submodules/overflow/PMU_overflow.sv
../../../submodules/quota/PMU_quota.sv
../../../submodules/MCCU/hdl/MCCU.sv
../../../submodules/RDC/hdl/RDC.sv
../../../submodules/seu_ip/hamming32t26d_enc.sv
../../../submodules/seu_ip/hamming32t26d_dec.sv
../../../submodules/seu_ip/way3_voter.sv
../../../submodules/seu_ip/way3ua_voter.sv
../../../submodules/seu_ip/way3u2a_voter.sv
../../../submodules/seu_ip/triple_reg.sv
../../../submodules/crossbar/hdl/crossbar.sv
tb/formal/equivalence_pmu_ahb/top.sv 0 → 100644
View file @ 99991e11
//-----------------------------------------------------
// ProjectName: LEON3_kc705_pmu
// Function : Integrate PMU and AHB interface
// Description: AHB interface implementation of the PMU.
//
// This module is responsible managing reads and writes from and
// AHB master and interface with pmu_ahb module.
//
// Coder : G.Cabo
// References : AMBA 3 AHB-lite specifications
// ARM IHI 0033A
// Notes : Any write to a control registers takes 2 clock cycles to
// take effect since it propagates from the wrapper to the
// internal regs of the PMU
`default_nettype none
`timescale 1 ns / 1 ps
`ifndef SYNT
`ifdef FORMAL
`define ASSERTIONS
`endif
`endif
module top #
(
parameter integer haddr = 0,
parameter integer hmask = 0,
// Width of registers data bus
parameter integer REG_WIDTH = 32,
// Number of counters
parameter integer PMU_COUNTERS = 24,
// Number of SoC events
parameter integer N_SOC_EV = 32,
// Total amount of registers (use ahb_pmu_mem_map.ods)
parameter integer N_REGS = 47,
// Fault tolerance mechanisms (FT==0 -> FT disabled)
parameter integer FT = 0,
// -- Local parameters
//haddr width
localparam integer HADDR_WIDTH = 32,
//hdata width
localparam integer HDATA_WIDTH = 32,
// Cores connected to MCCU
localparam MCCU_N_CORES = 4,
// Number of configuration registers
localparam PMU_CFG = 1
)
(
input wire rstn_i,
input wire clk_i,
// -- AHB bus slave interface
// slave select
input wire hsel_i,
// previous transfer done
input wire hreadyi_i,
// address bus
input wire [HADDR_WIDTH-1:0] haddr_i,
// read/write
input wire hwrite_i,
// transfer type
input wire [1:0] htrans_i,
// transfer size
input wire [2:0] hsize_i,
// burst type
input wire [2:0] hburst_i,
// write data bus
input wire [HDATA_WIDTH-1:0] hwdata_i,
// prtection control
input wire [3:0] hprot_i,
// locked access
input wire hmastlock_i,
// -- PMU specific signales
input wire [N_SOC_EV-1:0] events_i
);
logic hreadyo_o, fthreadyo_o;
logic [1:0] hresp_o, fthresp_o;
logic [HDATA_WIDTH-1:0] hrdata_o, fthrdata_o;
logic intr_overflow_o, ftintr_overflow_o;
logic intr_quota_o, ftintr_quota_o;
logic [MCCU_N_CORES-1:0] intr_MCCU_o, ftintr_MCCU_o;
logic intr_RDC_o, ftintr_RDC_o;
logic intr_FT1_o , ftintr_FT1_o;
logic intr_FT2_o , ftintr_FT2_o;
pmu_ahb #
(
.haddr(32'h80100000),
.hmask(32'hfff),
.REG_WIDTH(32),
.FT(1),
.N_REGS(47)
)
dut_ft_pmu_ahb
(
.rstn_i(rstn_i),
.clk_i(clk_i),
.hsel_i(hsel_i),
.hreadyi_i(1'b1),
.haddr_i(haddr_i),
.hwrite_i(hwrite_i),
.htrans_i(htrans_i),
.hsize_i(3'b0),
.hburst_i(3'b0),
.hwdata_i(hwdata_i),
.hprot_i(4'b0),
.hmastlock_i(1'b0),
.hreadyo_o(fthreadyo_o),
.hresp_o(fthresp_o),
.hrdata_o(fthrdata_o),
.events_i(events_i),
.intr_overflow_o(ftintr_overflow_o),
.intr_quota_o(ftintr_quota_o),
.intr_MCCU_o(ftintr_MCCU_o),
.intr_RDC_o(ftintr_RDC_o),
.intr_FT1_o(ftintr_FT1_o),
.intr_FT2_o(ftintr_FT2_o)
);
pmu_ahb #
(
.haddr(32'h80100000),
.hmask(32'hfff),
.REG_WIDTH(32),
.FT(0),
.N_REGS(47)
)
dut_pmu_ahb
(
.rstn_i(rstn_i),
.clk_i(clk_i),
.hsel_i(hsel_i),
.hreadyi_i(1'b1),
.haddr_i(haddr_i),
.hwrite_i(hwrite_i),
.htrans_i(htrans_i),
.hsize_i(3'b0),
.hburst_i(3'b0),
.hwdata_i(hwdata_i),
.hprot_i(4'b0),
.hmastlock_i(1'b0),
.hreadyo_o(hreadyo_o),
.hresp_o(hresp_o),
.hrdata_o(hrdata_o),
.events_i(events_i),
.intr_overflow_o(intr_overflow_o),
.intr_quota_o(intr_quota_o),
.intr_MCCU_o(intr_MCCU_o),
.intr_RDC_o(intr_RDC_o),
.intr_FT1_o(intr_FT1_o),
.intr_FT2_o(intr_FT2_o)
);
// Assert equivalence between FT and non-FT modules
`ifdef EQ_CHECK
// Initialize formal
reg f_past_valid ;
initial f_past_valid = 1'b0;
always@( posedge clk_i )
f_past_valid <= 1'b1;
//Clocking
default clocking @(posedge clk_i); endclocking;
//Assumptions
assume property ((!f_past_valid) |-> (rstn_i==0));
//Assertions
// Outputs of both modules shall be the same at all times
assert property ((f_past_valid) |=> (hreadyo_o == fthreadyo_o));