Dependency Resolution Error in IBEX Cellift Build

[forlight123]

Description

When attempting to build IBEX Cellift, I'm encountering dependency resolution errors. The build process fails with conflicting requirements between ibex_cellift and various Lowrisc IP packages.

Error Details

The build is failing with the following error:

[KatCe]

Hello. Which command did you execute?

[forlight123]

I run this step in the readme:
First, we need to prepare the design sources in a format as the CellIFT Yosys pass supports, ie. we need to translate it to Verilog. Enter a design directory, e.g. cpus/kronos/cellift. Source env.sh in cellift-meta, then source env.sh in cpus/kronos/cellift (if it exists). Then run make generated/sv2v_out.v.
command: make generated/sv2v_out.v

[KatCe]

I often encountered similar issues when collecting Ibex sources. If you want to reproduce our results, you could use the pre-generated sv2v_out. For example: https://github.com/comsec-group/mucfi/blob/main/cpus/ibex_small_pr2166_pregenerated/cellift/generated/sv2v_out.v
Or if you only want to reproduce the verification results you can run one of the pregenerated verification setups, for example: https://github.com/comsec-group/mucfi/tree/main/verification/ibex_top_opentitan_941315_rst_sec1_slow_no_ls_small_ift_pregenerated_cr

[forlight123]

thanks for your response, but i run the command:
ytm:kronos_dft_pregenerated/ (main✗) $ DESIGN_CONFIG=../../inputs/kronos/kronos_config_dft.mk make run_cmd CONFIG=kronos_core_ct_to_no_taint_states
it has some errors and i don't know how to fix:

INFO (IPF121): Cleared environment completely for new design analysis.
[-- (VERI-1482)] Analyzing Verilog file '/eda/tool/cadence/jasper_2503/lib/verilog/packages/std/std.sv' into library 'std'
[-- (VERI-1482)] Analyzing Verilog file '/home/ytm/formal/mucfi/verification/kronos_dft/designs/celldft.v'
[-- (VERI-1482)] Analyzing Verilog file 'formal/bind/kronos_core_fpv.sv'
[INFO (VERI-1328)] formal/bind/kronos_core_fpv.sv(1615): analyzing included file 'formal/properties/kronos_core_ct_instr_all.sv'
[INFO (VERI-1328)] formal/properties/kronos_core_ct_instr_all.sv(18): analyzing included file 'formal/signal_defs/operand_assignments_first.sv'
[INFO (VERI-1328)] formal/properties/kronos_core_ct_instr_all.sv(21): analyzing included file '../common/formal/signal_defs/start_cond_reg.sv'
[INFO (VERI-1328)] formal/properties/kronos_core_ct_instr_all.sv(22): analyzing included file '../common/formal/signal_defs/stop_cond_reg.sv'
[INFO (VERI-1328)] formal/properties/kronos_core_ct_instr_all.sv(24): analyzing included file '../common/formal/properties/prop_ct_instr.sv'
[INFO (VERI-1328)] ../common/formal/properties/prop_ct_instr.sv(7): analyzing included file 'formal/assumptions/kronos_core_i_asm.sv'
[INFO (VERI-1328)] formal/assumptions/kronos_core_i_asm.sv(1): analyzing included file 'formal/assumptions/kronos_core_di_asm.sv'
[INFO (VERI-1328)] formal/assumptions/kronos_core_i_asm.sv(2): analyzing included file 'formal/assumptions/kronos_core_ti_asm.sv'
[INFO (VERI-1328)] ../common/formal/properties/prop_ct_instr.sv(13): analyzing included file 'formal/assumptions/kronos_core_pc_taint_asm.sv'
[INFO (VERI-1328)] ../common/formal/properties/prop_ct_instr.sv(17): analyzing included file 'formal/assumptions/kronos_core_declass_asm.sv'
[INFO (VERI-1328)] ../common/formal/properties/prop_ct_instr.sv(30): analyzing included file '../common/formal/properties/prop_instr_types.sv'
[INFO (VERI-1328)] ../common/formal/properties/prop_ct_instr.sv(31): analyzing included file '../common/formal/properties/../signal_defs/debug_insn_sigs.sv'
[INFO (VERI-1328)] ../common/formal/properties/prop_ct_instr.sv(32): analyzing included file '../common/formal/properties/get_instr_type.sv'
[INFO (VERI-1328)] ../common/formal/properties/prop_ct_instr.sv(55): analyzing included file '../common/formal/properties/prop_pc_taint_check.sv'
[INFO (VERI-1328)] ../common/formal/properties/prop_ct_instr.sv(58): analyzing included file '../common/formal/properties/checker_inst_pc_taint_checker_to_anytime.sv'
[INFO (VERI-1328)] ../common/formal/properties/prop_ct_instr.sv(59): analyzing included file '../common/formal/properties/checker_inst_pc_taint_checker_to_anytime_no_taint_states.sv'
[INFO (VERI-1328)] formal/properties/kronos_core_ct_instr_all.sv(26): analyzing included file 'formal/properties/kronos_core_no_taint_ever_checker.sv'
[INFO (VERI-1328)] formal/properties/kronos_core_ct_instr_all.sv(27): analyzing included file '../common/formal/assumptions/asm_taint_inj_once.sv'
[ERROR (VERI-1137)] ../common/formal/assumptions/asm_taint_inj_once.sv(5): syntax error near 'property'
[ERROR (VERI-2344)] ../common/formal/assumptions/asm_taint_inj_once.sv(5): SystemVerilog 2005 keyword 'property' used in incorrect context
[INFO (VERI-2561)] ../common/formal/assumptions/asm_taint_inj_once.sv(5): undeclared symbol 'untyped', assumed default net type 'wire'
[ERROR (VERI-1137)] ../common/formal/assumptions/asm_taint_inj_once.sv(5): syntax error near 'taint_source'
[ERROR (VERI-1137)] ../common/formal/assumptions/asm_taint_inj_once.sv(6): syntax error near '''
[ERROR (VERI-1137)] ../common/formal/assumptions/asm_taint_inj_once.sv(15): syntax error near 'input'
[ERROR (VERI-2344)] ../common/formal/assumptions/asm_taint_inj_once.sv(15): SystemVerilog 2005 keyword 'input' used in incorrect context
[ERROR (VERI-1137)] ../common/formal/assumptions/asm_taint_inj_once.sv(15): syntax error near 'taint_source'
[ERROR (VERI-1116)] ../common/formal/assumptions/asm_taint_inj_once.sv(16): 'clk_verif' is already declared
[INFO (VERI-1967)] formal/properties/kronos_core_ct_instr_all.sv(8): previous declaration of 'clk_verif' is from here
[ERROR (VERI-1137)] ../common/formal/assumptions/asm_taint_inj_once.sv(33): syntax error near 'until'
[WARN (VERI-2170)] ../common/formal/assumptions/asm_taint_inj_once.sv(33): data object 'taint_stop' is already declared
[INFO (VERI-1967)] ../common/formal/assumptions/asm_taint_inj_once.sv(19): previous declaration of 'taint_stop' is from here
[WARN (VERI-1329)] ../common/formal/assumptions/asm_taint_inj_once.sv(33): second declaration of 'taint_stop' is ignored
[ERROR (VERI-1137)] ../common/formal/assumptions/asm_taint_inj_once.sv(34): syntax error near 'until'
[WARN (VERI-2170)] ../common/formal/assumptions/asm_taint_inj_once.sv(34): data object 'taint_start' is already declared
[INFO (VERI-1967)] ../common/formal/assumptions/asm_taint_inj_once.sv(19): previous declaration of 'taint_start' is from here
[WARN (VERI-1329)] ../common/formal/assumptions/asm_taint_inj_once.sv(34): second declaration of 'taint_start' is ignored
[ERROR (VERI-1137)] ../common/formal/assumptions/asm_taint_inj_once.sv(35): syntax error near 'until'
[WARN (VERI-2170)] ../common/formal/assumptions/asm_taint_inj_once.sv(35): data object 'taint_start' is already declared
[INFO (VERI-1967)] ../common/formal/assumptions/asm_taint_inj_once.sv(19): previous declaration of 'taint_start' is from here
[WARN (VERI-1329)] ../common/formal/assumptions/asm_taint_inj_once.sv(35): second declaration of 'taint_start' is ignored
[INFO (VERI-2561)] ../common/formal/assumptions/asm_taint_inj_once.sv(49): undeclared symbol 'taint_start_cond', assumed default net type 'wire'
[INFO (VERI-2561)] ../common/formal/assumptions/asm_taint_inj_once.sv(49): undeclared symbol 'taint_stop_cond', assumed default net type 'wire'
[INFO (VERI-2561)] ../common/formal/assumptions/asm_taint_inj_once.sv(50): undeclared symbol 'taint_source', assumed default net type 'wire'
[ERROR (VERI-1137)] ../common/formal/assumptions/asm_taint_inj_once.sv(56): syntax error near 'pc_taint_checker_to_anytime_no_taint_states'
[ERROR (VERI-1137)] ../common/formal/assumptions/asm_taint_inj_once.sv(56): syntax error near 'taint_source'
[ERROR (VERI-1116)] ../common/formal/assumptions/asm_taint_inj_once.sv(57): 'clk_verif' is already declared
[INFO (VERI-1967)] formal/properties/kronos_core_ct_instr_all.sv(8): previous declaration of 'clk_verif' is from here
[WARN (VERI-2170)] ../common/formal/assumptions/asm_taint_inj_once.sv(60): data object 'taint_start' is already declared
[INFO (VERI-1967)] ../common/formal/assumptions/asm_taint_inj_once.sv(19): previous declaration of 'taint_start' is from here
[WARN (VERI-1329)] ../common/formal/assumptions/asm_taint_inj_once.sv(60): second declaration of 'taint_start' is ignored
[WARN (VERI-2170)] ../common/formal/assumptions/asm_taint_inj_once.sv(60): data object 'taint_stop' is already declared
[INFO (VERI-1967)] ../common/formal/assumptions/asm_taint_inj_once.sv(19): previous declaration of 'taint_stop' is from here
[WARN (VERI-1329)] ../common/formal/assumptions/asm_taint_inj_once.sv(60): second declaration of 'taint_stop' is ignored
[WARN (VERI-2170)] ../common/formal/assumptions/asm_taint_inj_once.sv(60): data object 'tainted_once' is already declared
[INFO (VERI-1967)] ../common/formal/assumptions/asm_taint_inj_once.sv(19): previous declaration of 'tainted_once' is from here
[WARN (VERI-1329)] ../common/formal/assumptions/asm_taint_inj_once.sv(60): second declaration of 'tainted_once' is ignored
[WARN (VERI-2170)] ../common/formal/assumptions/asm_taint_inj_once.sv(61): data object 'taint_active' is already declared
[INFO (VERI-1967)] ../common/formal/assumptions/asm_taint_inj_once.sv(20): previous declaration of 'taint_active' is from here
[WARN (VERI-1329)] ../common/formal/assumptions/asm_taint_inj_once.sv(61): second declaration of 'taint_active' is ignored
[WARN (VERI-2170)] ../common/formal/assumptions/asm_taint_inj_once.sv(62): data object 'taint_optional' is already declared
[INFO (VERI-1967)] ../common/formal/assumptions/asm_taint_inj_once.sv(21): previous declaration of 'taint_optional' is from here
[WARN (VERI-1329)] ../common/formal/assumptions/asm_taint_inj_once.sv(62): second declaration of 'taint_optional' is ignored
[WARN (VERI-2170)] ../common/formal/assumptions/asm_taint_inj_once.sv(64): data object 'taint_stop_cond_internal' is already declared
[INFO (VERI-1967)] ../common/formal/assumptions/asm_taint_inj_once.sv(23): previous declaration of 'taint_stop_cond_internal' is from here
[WARN (VERI-1329)] ../common/formal/assumptions/asm_taint_inj_once.sv(64): second declaration of 'taint_stop_cond_internal' is ignored
[ERROR (VERI-1137)] ../common/formal/assumptions/asm_taint_inj_once.sv(74): syntax error near 'until'
[WARN (VERI-2170)] ../common/formal/assumptions/asm_taint_inj_once.sv(74): data object 'taint_stop' is already declared
[INFO (VERI-1967)] ../common/formal/assumptions/asm_taint_inj_once.sv(19): previous declaration of 'taint_stop' is from here
[WARN (VERI-1329)] ../common/formal/assumptions/asm_taint_inj_once.sv(74): second declaration of 'taint_stop' is ignored
[ERROR (VERI-1137)] ../common/formal/assumptions/asm_taint_inj_once.sv(75): syntax error near 'until'
[WARN (VERI-2170)] ../common/formal/assumptions/asm_taint_inj_once.sv(75): data object 'taint_start' is already declared
[INFO (VERI-1967)] ../common/formal/assumptions/asm_taint_inj_once.sv(19): previous declaration of 'taint_start' is from here
[WARN (VERI-1329)] ../common/formal/assumptions/asm_taint_inj_once.sv(75): second declaration of 'taint_start' is ignored
[ERROR (VERI-1137)] ../common/formal/assumptions/asm_taint_inj_once.sv(76): syntax error near 'until'
[WARN (VERI-2170)] ../common/formal/assumptions/asm_taint_inj_once.sv(76): data object 'taint_start' is already declared
[INFO (VERI-1967)] ../common/formal/assumptions/asm_taint_inj_once.sv(19): previous declaration of 'taint_start' is from here
[WARN (VERI-1329)] ../common/formal/assumptions/asm_taint_inj_once.sv(76): second declaration of 'taint_start' is ignored
[ERROR (VERI-9011)] ../common/formal/assumptions/asm_taint_inj_once.sv(78): block id 'asm_taint_source_active' is already declared
[INFO (VERI-1967)] ../common/formal/assumptions/asm_taint_inj_once.sv(37): previous declaration of 'asm_taint_source_active' is from here
[ERROR (VERI-9011)] ../common/formal/assumptions/asm_taint_inj_once.sv(81): block id 'asm_taint_source_not_active' is already declared
[INFO (VERI-1967)] ../common/formal/assumptions/asm_taint_inj_once.sv(40): previous declaration of 'asm_taint_source_not_active' is from here
[INFO (SYS-1004)] Too many errors. Further error messages will be suppressed.
Summary of errors detected:
[ERROR (VERI-1137)] ../common/formal/assumptions/asm_taint_inj_once.sv(5): syntax error near 'property'
[ERROR (VERI-2344)] ../common/formal/assumptions/asm_taint_inj_once.sv(5): SystemVerilog 2005 keyword 'property' used in incorrect context
[ERROR (VERI-1137)] ../common/formal/assumptions/asm_taint_inj_once.sv(5): syntax error near 'taint_source'
[ERROR (VERI-1137)] ../common/formal/assumptions/asm_taint_inj_once.sv(6): syntax error near '''
[ERROR (VERI-1137)] ../common/formal/assumptions/asm_taint_inj_once.sv(15): syntax error near 'input'
[ERROR (VERI-2344)] ../common/formal/assumptions/asm_taint_inj_once.sv(15): SystemVerilog 2005 keyword 'input' used in incorrect context
[ERROR (VERI-1137)] ../common/formal/assumptions/asm_taint_inj_once.sv(15): syntax error near 'taint_source'
[ERROR (VERI-1116)] ../common/formal/assumptions/asm_taint_inj_once.sv(16): 'clk_verif' is already declared
[ERROR (VERI-1137)] ../common/formal/assumptions/asm_taint_inj_once.sv(33): syntax error near 'until'
[ERROR (VERI-1137)] ../common/formal/assumptions/asm_taint_inj_once.sv(34): syntax error near 'until'
[ERROR (VERI-1137)] ../common/formal/assumptions/asm_taint_inj_once.sv(35): syntax error near 'until'
[ERROR (VERI-1137)] ../common/formal/assumptions/asm_taint_inj_once.sv(56): syntax error near 'pc_taint_checker_to_anytime_no_taint_states'
[ERROR (VERI-1137)] ../common/formal/assumptions/asm_taint_inj_once.sv(56): syntax error near 'taint_source'
[ERROR (VERI-1116)] ../common/formal/assumptions/asm_taint_inj_once.sv(57): 'clk_verif' is already declared
[ERROR (VERI-1137)] ../common/formal/assumptions/asm_taint_inj_once.sv(74): syntax error near 'until'
[ERROR (VERI-1137)] ../common/formal/assumptions/asm_taint_inj_once.sv(75): syntax error near 'until'
[ERROR (VERI-1137)] ../common/formal/assumptions/asm_taint_inj_once.sv(76): syntax error near 'until'
[ERROR (VERI-9011)] ../common/formal/assumptions/asm_taint_inj_once.sv(78): block id 'asm_taint_source_active' is already declared
[ERROR (VERI-9011)] ../common/formal/assumptions/asm_taint_inj_once.sv(81): block id 'asm_taint_source_not_active' is already declared
ERROR (ENL034): 19 errors detected in the design file(s).

ERROR: problem encountered at line 17 in file ../common/formal/scripts/launchers/verif_cadence.tcl

[KatCe]

I just reproduced the run with the same Jasper version as you (25.03) and do not encounter any errors.
Have you modified any properties or assumptions?
The error hints that something went wrong right before the place where asm_taint_inj_once.sv is included.

[forlight123]

Thanks for your response, I had not modify the properties or assumptions,
I just replaced YOUR_FORMAL_TOOL_CMD in the common directory with the actual command

[KatCe]

Are you on the latest commit?
Can you find out more about the actual line that fails?

[forlight123]

Thanks for your response, it is the reason that my jasper uses the systemverilog 2005. I skip to sv2012 to fix the problem. However, I meet some new errors:

I have rewritten the file: mucfi/verification/common/formal/scripts/tasks/task_creations.tcl:

[KatCe]

Great that you solved the errors by switching the SystemVerilog version.

The error you see now hints that the hierarchical path to the signal is not correct. Are you using kronos_core (could have a different name) as top module?

[forlight123]

reaaly thanks for your response!
but the top module is kronos_core:

[KatCe]

If you launch in GUI (or interactive cmd line), then you can type 'puts $errorInfo' right after it stopped with the error. This normally prints the exact line that failed.
'rs1_forward' is indeed not a register, but a continuously assigned signal. Not sure though what caused the message.