jasper SLEC script changes

[mret55]

Updated jasper SLEC script for parameters usage. Added assumption files and bind file scripts/slec/cadence folder.

[MikeOpenHWGroup]

• Are the .DS_Store files required as inputs to Jasper, or are they tool artefacts? If they are artefacts, they should not be added to the repository.
• Please add the appropriate license headers to the clear-text files. The following "two liner" is sufficient:

// Copyright 2024 <your-organization>
// SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1

[MikeOpenHWGroup]

Hi @mret55, thanks for this PR. I have requested a couple of changes.

Also, the Eclipse ECA check is failing, but I checked and Eclipse reports that There is a valid ECA on file for [email protected]. I will investigate.

[MikeOpenHWGroup]

Hi @mret55, the Eclipse ECA check is now passing.

[pascalgouedo]

I only found assume files but no file containing row4 assertion.
Once added, it should be added to cv32e40p_tb_src.flist.

[mret55]

I only found assume files but no file containing row4 assertion. Once added, it should be added to cv32e40p_tb_src.flist.

I have uncommented the row4 assertion from cv32e40p/scripts/formal/src/cv32e40p_controller_assert.sv.
This file is already part of cv32e40p/scripts/formal/cv32e40p_formal.flist

[mret55]

Hi @pascalgouedo,
I responded to your comments and fixed them accordingly.
Please let me know if there are any additional questions.

[pascalgouedo]

I only found assume files but no file containing row4 assertion. Once added, it should be added to cv32e40p_tb_src.flist.

I have uncommented the row4 assertion from cv32e40p/scripts/formal/src/cv32e40p_controller_assert.sv. This file is already part of cv32e40p/scripts/formal/cv32e40p_formal.flist

Are data_assert2 and insn_assert2 really useful as they are duplicates of data_assert and insn_assert?
If you were able to reuse cv32e40p_controller_assert you should be able to reuse those 2 files?

[mret55]

I only found assume files but no file containing row4 assertion. Once added, it should be added to cv32e40p_tb_src.flist.

I have uncommented the row4 assertion from cv32e40p/scripts/formal/src/cv32e40p_controller_assert.sv. This file is already part of cv32e40p/scripts/formal/cv32e40p_formal.flist

Are data_assert2 and insn_assert2 really useful as they are duplicates of data_assert and insn_assert? If you were able to reuse cv32e40p_controller_assert you should be able to reuse those 2 files?

Hi @pascalgouedo,
I think there are differences between the two. insn_assert.sv at cv32e40p/scripts/formal/src/ imports two packages (cv32e40p_pkg and cv32e40p_tracer_pkg), which are not there in insn_assert2.sv, which you had given me.

Also, these are used for 2 different applications. One in cv32e40p/scripts/formal/ is for FPV (property verification), while one in cv32e40p/scripts/slec/cadence/tb_src is for SLEC.

I will need to run tweak run.sh for those packages, remove existing files and rerun jasper again if we were to consolidate the files. Not sure, if I will be able to get around to doing that quick.

In its existing setup (as per this pull request), it works fine.
Maybe we can merge my current changes in dev for now, and do the consolidation later?

[MikeOpenHWGroup]

Approving and merging as per @pascalgouedo request. (Note that I have no way to test this from my current location.)