[行业软件]Cadence JasperGold 24.03.000 Linux [复制链接]

Cadence has released JasperGold 24.03.000 is the first verification product to deliver complete “deep formal” systematic verification, ensuring correctness where it matters most.
Jasper Apps Version 2024.03
The release of Jasper(TM) Apps version 2024.03 includes several new features and enhancements in the areas listed below.



List of Features and Enhancements


* C to RTL Equivalence Checking (C2RTL) App
* Controlling the Generation of ReachableUFC Assertions
* Added the Ability to Customize the C2RTL Design Top Name
* Improved Error Messages
* Using Structs in C2RTL Formal Model
* C2RTL Dynamic Path Pruning Time
* Improved C2RTL Warning and Error Reporting
* Using Environment Variables for File Paths with "check_c2rtl -compile"
* New C2RTL C++ Model Profiler
* Debugging C++ Code with GDB

* Clock Domain Crossing (CDC) App
* New Information on CDC Violations
* Resolved Simulation Run Time Error Caused by Metastability Injection
* CDC_NO_SYNC No Longer Reported on Clock Signals
* CDC Now Detects NDFF Schemes with strict_ndff_detection
* Jasper CDC Supports "set_false_path" to Create Async Clock Groups
* CDC No Longer Reports Noisy Violations on Retention Cell Shadow Registers
* Nets on the Reset Path Now Shown as Signal Type Reset
* Improved CDC_PR_LOGC Violations
* Removed Violation Merging for Specific CDC Violations
* Nets on the Clock Path Now Shown as Signal Type Clock
* Resolved Issue with CDC_NO_SYNC Violations
* CDC No Longer Reports RST_NO_SYNC/RST_RS_CONV Violations Due to LPV Signals
* New Switch for "session -new"
* Enhanced NDFF Detection Scheme
* New FLP_RS_UDCL Violation Detects Undeclared Flop Reset Signals
* New Uninitialized Flop Violation
* Enabled "check_cdc -debug -reset_domain_all_nets" by Default in CDC
* New Switch for "check_cdc -metastability -export"
* New Constant Reset Violation

* Clock Domain Crossing (CDC) App and Superlint App
* New Option for Grouping in CDC Report

* Connectivity Verification App
* New Switch for "check-conn -validate"
* Improved Strategy for Prove Combinational Connections
* Improved Performance for the "check_conn -list path" Command

* Coverage App
* New Switch for "check_cov -measure"
* New "check_cov -configure_gui" Command
* New Default Checker Status for COV Functionally Undetectable Cover Items
* Improved "check_cov -list" and "check_cov -report"
* New Columns in the COV Assert Analysis Window
* Remove Cover Items Defined by Constants
* New Exclude Option for "check_cov -list" and "check_cov -report"

* Coverage Unreachability (UNR) App
* New UNR Command
* UNR Prove Cache Now Enabled by "set_proofmaster"
* UNR Auto Partition
* New UNR Command to Select Functional Coverage Mode

* Functional Safety Verification (FSV) App
* FSV Super Faults Now a Public Feature

* Low Power Verification (LPV) App
* New Option of "check_lpv -generate_power_design -corrupt"

* Security Path Verification (SPV) App
* SPV GUI Now Includes an SPV Analysis Toolbar
* Updated Arguments for "check_spv -clear"
* Enabling Enhanced Proof Status in SEC, SPV, and X-Prop
* New Color in SPV Complexity Graphs
* Improved SPV GUI Information

* Security Path Verification (SPV) App, Sequential Equivalence Checking (SEC) App and X-Propagation (XPROP) Verification App
* "set_word_level_reduction" Not Supported by SEC, SPV, X-Prop, and C2RTL

* Sequential Equivalence Checking (SEC) App
* SEC Native Split Setup Mode Now Supported by LPV Load and Power Transformation
* Updated "App Extensions" Options for SEC
* Task Creation Based on SEC Mapping Table
* New Command for Creating Task-Based Mapping Entries in the SEC Setup
* "check_sec -generate_verification" Now Runs after New Task Creation
* Enhanced "check_sec -copy_mapping" and "check_sec -copy_imported_properties"

* Superlint App
* Enhanced “config_rtlds -rule -parameter” with New "-app" Switch
* New Command for Reporting a SIG_IS_MLAS Property When Drivers Are the Same
* Enhanced Superlint Arithmetic Overflow Checks
* Added New Configuration Commands for Power Overflow
* New Superlint Command
* “Show Parameter” Highlights Changed Parameters of Tag/Domain
* New Parameter Can Reduce Noise of EXP_NR_MXSU
* Improved MOD_NR_SYXZ Check
* Enhanced INS_IS_FEED Source Location to Assignment Statement

* X-Propagation (XPROP) Verification App
* Use "check_xprop -prove" on Related Covers of X-Prop Assumptions
* Improved Issue with IMTR145
* "abstract -counter -values" Now Supported by X-Prop and SPV

* Visualize
* "visualize -run_recipe" and "visualize -save_recipe" Deprecated
* Highlighting Frozen Traces on Visualize Waveform
* Adding Force Soft Constraint to an Infinite Trace
* QuietTrace on "Last N Cycles" on Infinite Traces
* New Command to Unroll Loops in Visualize
* New Command for Controlling Waveform Transparency in WaveEdit Mode

* Abstraction
* Added Support for Dynamic Critical Values in Counter Abstraction

* Clocks and Reset
* Enhanced "sanity_check" Command

* Deep Bug Hunting
* Specifying Time Limit in Trace Search Hunt Strategy
* Hunt Manager Now Supports Updating Strategy Parameters Back to "auto"
* Restricted Engines for the Loop Swarm Hunt Strategy

* Design Compilation
* Library List for Design Configuration Now Working as Expected
* Extended UDP Handling Now Default in Jasper
* Parallel Launch of Synthesis Processes Now Possible

* Design Exploration
* Highlighting Cursor Line With Color

* Design Exploration and Miscellaneous
* Listing Parameters for a Specified Interface or Module Only
* Using "complexity_manager" without Arguments

* Engines
* Enhanced EngineJ to Stop Automatically

* Language Support
* Updated Default Semantics for Cover Property
* Returning the Number of Flop Bits of a Specified Property
* Enhanced SVA Local Variable Support
* Improved Check for "genvar"

* Miscellaneous
* Added New Jasper Tcl Library Documentation
* New Proof Structure Command to Copy Embedded Properties into Nodes
* Jasper No Longer Supports the "=>" Implication Operator

* Proofs and ProofGrid
* Formal Profile Restarts with Same Configurations as Original
* Enhanced Formal Profiler to Start at 0 Instead of 1
* Enhanced Formal Profiler to Use Design Hierarchy
* New Default Layout for Formal Profiler
* New Behavior of the "proof_structure -init" Command
* Creating Underconstraint and Overconstraint Proof Structure Nodes
* New Proof Structure Option
* Setting "per_engine_max_jobs" to Unlimited
* Added "trace_bound" Switch to "get_property_info -list" Command
* Fixed Oracle Grid Engine Parallel Environment Warning Issue
* Extended "get_trace_info" to Explicitly Report SST Information

* Proofs and ProofGrid and Property and Configuration Database
* New Alternative to "visualize -sst"

* User Interface
* Renamed "Cover (live)" to "Cover (infinite)"
* Setting GUI Colors using "set_preference" Commands
* Updated View SST Trace Context Menu

* Verification Management
* Saving a Database Periodically

* vManager Integration
* Added New Argument to Run Single Run Script Mode

New Features and Enhancements
=============================
This section provides details about the new features and enhancements listed
above. Refer to the Jasper Apps manuals and incremental training slides
(Tech Updates) for additional information.

C to RTL Equivalence Checking (C2RTL) App
––––––––––––––––––––-
* Added the Ability to Customize the C2RTL Design Top Name

You can now define a preferred alias for the RTL top-level name on the imp
side using the "-rename_top" switch with the "check_c2rtl -elaborate" command.

Example: check_c2rtl -elaborate -imp -rename_top dut

* Controlling the Generation of ReachableUFC Assertions

You can now control the generation of ReachableUFC assertions for a set of
unimplemented functions. This set is defined by a list of function names that
can include wildcards. Use the following commands to set and get the set of
unimplemented functions for which no ReachableUFC assertions are generated:

. check_c2rtl -set_ignore_unimplemented_functions
. check_c2rtl -get_ignore_unimplemented_functions

NOTE: For additional information, check the online command help of the
"check_c2rtl" command.

* Improved Error Messages

C2RTL now issues more exact compilation error messages when you use
invalid JASPER_ASSUME and JASPER_ASSERT macro names.

* Using Environment Variables for File Paths with "check_c2rtl -compile"

You can now use environment variables for file paths in the
"check_c2rtl -compile -spec -f" command:

check_c2rtl -compile -spec -f <filelist>

If you do not define an environment variable, Jasper shows the following
error:

"The environment variable $<environment_variables> is not defined."

* Using Structs in C2RTL Formal Model

You can now use structs as inputs and outputs in the C2RTL formal model.

* C2RTL Dynamic Path Pruning Time

Dynamic path pruning now measures time correctly and respects its time limit.

* Improved C2RTL Warning and Error Reporting

Use the "check_c2rtl -complie -verbosity N" command to specify the level of
message verbosity you want. If N = 5, the tool shows a brief description of
warning messages.

Note: The default is N = 6, which leads the tool to print all warning and
error messages as is.

* New C2RTL C++ Model Profiler

The C2RTL flow now has a new feature called C++ Model Profiler. This new
feature lets you track where the tool spends time during a formal generation.

You can get the following information using the C++ Model Profiler:

. Check where, in the C++ code, the tool is spending time.
. Check the call stack tree of the generated C model.
. Have information on the number of calls to each C++ function.
. Have overall accumulated execution time for each function.
. Open the C++ Source Browser in a specific function or debug using your
preferred editor and copying the file path the profiler shows.

Use the "check_c2rtl -start_profiler" command to start running the C++ Model
Profiler.

Note: This command must be used before the "check_c2rtl -compile" command.

* Debugging C++ Code with GDB

You can now debug C++ code using GDB-based debugging with values from a CEX
created by Jasper, according to the procedure described below.

Save the trace after a CEX and run the following command, including the
property name and the cycle number:

check_c2rtl -export_trace_for_gdb -spec -propertyName <property_name>
-cycle <N>

Compile C++ files using g++ with the "–g" option:

g++ <filename.cpp> -g -o <output>

Run GDB:

gdb <output> -x
<JASPER_INSTALLATION_FOLDER>/etc/res/c2rtl/GDBLikeDebugging/c2rtl-gdb.py

Note: Use GDB version 10.1 and above. We recommend Python configured version 3
and above.

Load the saved trace:

c2rtl load-trace <saved_trace>

You can use the "c2rtl info" command to print the trace file info (name, time
of loading, and content).

Note: Currently, GDB-based debugging does not support SystemC arrays as
inputs, C language, and undriven signals.

Clock Domain Crossing (CDC) App
–––––––––––––––-
* Resolved Simulation Run Time Error Caused by Metastability Injection

In the metastability injection flow, integer candidate members of arrays and
natural or positive candidates are now exported successfully to simulation.
Candidates of type enumerated are discarded and not exported.

* CDC Now Detects NDFF Schemes with strict_ndff_detection

Jasper CDC automatically detects NDFF schemes if the strict_ndff_detection
parameter is true, even if the clock signal nets connected to the scheme
flops are different but are driven by the same single clock.

* CDC_NO_SYNC No Longer Reported on Clock Signals

CDC no longer reports the CDC_NO_SYNC violation for CDC pairs that have clock
ports as destination.

* CDC No Longer Reports Noisy Violations on Retention Cell Shadow Registers

Latch units are now being handled in the same manner as regular CDC units.
Specifically, CDC will no longer report:
. latch_cdc on latches that are not visible to the user
. latch_cdc on unconnected latches if the
report_violations_on_unconnected_load RTLDS rule is set to false.
Therefore, the tool no longer reports noisy latch_cdc violations on
retention cell shadow registers.

* New Information on CDC Violations

The RST_RS_FSAR and FLP_NO_INIT violations now have the following new fields:

. Reset Domain: Shows the reset domain of the occurrence flop.
. Local Source Reset: Shows the design reset connected to the occurrence
flop's RC pin.

* Jasper CDC Supports "set_false_path" to Create Async Clock Groups

Jasper CDC now processes the "set_false_path" command and creates two
asynchronous clock groups with the clocks listed in the "-from" and "-to"
switches.

* Enabled "check_cdc -debug -reset_domain_all_nets" by Default in CDC

This release enables the "check_cdc -debug -reset_domain_all_nets" checks in
CDC by default.

* New Switch for "check_cdc -metastability -export"

The "check_cdc -metastability -export" command now supports the "-tolerance"
switch:

-tolerance (N | time_unit | N time_unit)

The new switch lets you specify the tolerance for changes happening close to
the clock edges for hold violations during metastability injection in the
simulation model.

* Removed Violation Merging for Specific CDC Violations

With the addition of basic CDC violation grouping in the 2023.06 release,
violation merging was removed for "no_scheme", "no_reset_scheme", and
"latch_cdc" violations. Thus, the "set_cdc_no_waiver_for_multipair_violation"
command has been deprecated. Now, instead of all the pairs with the same
destination unit being merged into a single violation, CDC creates one
violation for each pair and groups these.

* Resolved Issue with CDC_NO_SYNC Violations

CDC no longer reports a CDC_NO_SYNC violation in the hierarchical flow for a
port in a blackboxed module that contains an internal scheme connected to
that port.

* Enhanced NDFF Detection Scheme

Jasper CDC now automatically detects NDFF schemes with flops in different
instances that have the same immediate parent instance, even if the
“strict_ndff_detection” parameter is set to true.

* New FLP_RS_UDCL Violation Detects Undeclared Flop Reset Signals

This release adds a new flop_with_undeclared_reset (FLP_RS_UDCL) violation
to report on flops whose reset condition pin is connected to one or more
undeclared reset signals. Additionally, the associated reset_not_declared
(RST_NO_DECL) violation now reports internal signals used as resets but are
not declared as such.

* New Uninitialized Flop Violation

CDC now generates the following violation for flops that are uninitialized,
that is, their reset condition is never asserted due to constant reset
signals:

FLP_NO_INIT (Error): "Reset condition of flop '%s' is never asserted, keeping
it stuck at run state"

* New Constant Reset Violation

CDC now generates the following violation for the nets in which the reset
signals become constant in the design:

RST_RS_CNST (Warning): "Reset signal becomes constant at '%s'"

* New Switch for "session -new"

The "session -new" command now supports the "-dont_use_as_current_session"
switch. The new switch lets you prevent switching to the created session and
keeping the analysis session executing the "session -new" command as the
current session.

* Nets on the Reset Path Now Shown as Signal Type Reset

CDC now shows all nets that are on the reset path in the blue color and marks
them as Signal Type Reset in the Signal Info pane of the Schematic Viewer.

* Nets on the Clock Path Now Shown as Signal Type Clock

CDC now shows all nets that are on the clock path in the green color and marks
them as Signal Type Clock in the Signal Info pane of the Schematic Viewer.

* CDC No Longer Reports RST_NO_SYNC/RST_RS_CONV Violations Due to LPV Signals

CDC no longer generates DesignResets for LPV signals or adds them
to the reset tree. In addition, convergences of a single real reset and one
or more LPV signals do not produce internal DesignResets. As a result,
the tool no longer reports no_reset_scheme (RST_NO_SYNC) or
reset_convergence (RST_RS_CONV) violations due to LPV signals.

* Improved CDC_PR_LOGC Violations

CDC no longer takes isolation cells into consideration when evaluating
CDC_PR_LOGC violations.

The tool reports a CDC crossing as a CDC_PR_LOGC violation only when a
forbidden logic is in the path between source and destination. The
CDC_PR_LOGC parameter determines the most complex logic allowed in the CDC
path and its default value is "Buffer". Therefore, the tool reports the
violation for any CDC path containing combinational logic or latches by
default.

With this fix, the tool classifies the isolation cell gates as buffers
instead of combinational logic, letting them pass the check without a
violation report.

Clock Domain Crossing (CDC) App and Superlint App
––––––––––––––––––––––––-
* New Option for Grouping in CDC Report

You can now use the "check_cdc -report -grouping (none | basic)" command to
generate a report with the specified grouping, regardless of the current
grouping mode of the App. Grouping is a GUI concept that groups related checks
and shows only one check, which is the primary.

By default, the report is generated with the App's current grouping option.

Connectivity Verification App
––––––––––––––-
* New Switch for "check-conn -validate"

The "check-conn -validate" command now supports the "-include" switch:

–include (( condition | disable | clock )+ | all)

The new switch lets you choose which signals must be searched in the cone of
influence of the destination in addition to the source.

* Improved Strategy for Prove Combinational Connections

The Connectivity App now applies an optimized strategy to prove combinational
connections, in addition to straight-through connections, when you invoke the
"check_conn -prove" command. Further, the existing proof messages now include
combinational connections into the counts.

* Improved Performance for the "check_conn -list path" Command

You can now improve the performance of the "check_conn -list path" command by
adding the "-limit 1" option.

NOTE: This improvement works only for the connections extracted by the
"check_conn -reverse -load" command.

Coverage App
––––––
* New Switch for "check_cov -measure"

The "check_cov -measure" command now supports the
"-skip_covered_or_checked_from_other_tasks" switch. Use the new switch to
prevent spending resources on cover items that are already checked in other
tasks (or covered in case of stimuli), thus letting the tool converge faster
and spend less resources without affecting the final merged result of all
tasks.

* Improved "check_cov -list" and "check_cov -report"

Coverage now properly supports the top instance name with the
"-include_instance" and "-exclude_instance" switches of the "check_cov -list"
and "check_cov -report" commands.

* New Columns in the COV Assert Analysis Window

COV now shows two extra columns in the assert analysis window by default:
"Proof Core Bound" and "Proof Core Engine". These show the progress of proof
core measurement on checker properties.

* New Default Checker Status for COV Functionally Undetectable Cover Items

COV now marks both functionally and structurally undetectable cover items with
the "Undetectable" checker status by default. Previously, the tool reported
the "Undetectable" checker status for structurally undetectable cover items
only, that is, cover items marked as out of the cone of influence.

* New Exclude Option for "check_cov -list" and "check_cov -report"

The "check_cov -list" and "check_cov -report" commands now support the
"-exclude synthesis_optimized" option. This option disconsiders cover items
that have been optimized during synthesis and can never be checked.

* New "check_cov -configure_gui" Command

You can now use the "check_cov -configure_gui" command to set up the Coverage
GUI environment through the command line. This lets you change the "Tasks",
"Excludes", and "Checker Mode" options without having to manually use the GUI
(using a Tcl script instead).

* Remove Cover Items Defined by Constants

You can now use the "check_cov -list -exclude constant_input_port" command to
remove cover items with stimuli status defined by constants assigned to ports.

Coverage Unreachability (UNR) App
––––––––––––––––-
* New UNR Command

You can now use the following command to specify a limit on the number of UNR
partitions that run in parallel:

set_unr_partition_max_jobs <N>

Note: By default, the UNR Auto partition runs three partitions in parallel.

* New UNR Command to Select Functional Coverage Mode

Use the new "set_unr_functional_coverage_mode (assertion |covergroup |all)"
command to select the mode of functional coverage for the UNR analysis:

. assertion: Select only covergroup items
. covergroup: Select only assertion witnesses and covers
. all: Extract all functional coverage items (default option)

* UNR Auto Partition

UNR now supports Auto Partition. Use the following commands:

. "check_unr -generate_partition": Generate partitions of the given design for
UNR Analysis.
. "check_unr -load_partition": Load the specified file to run the partitions
for UNR Analysis.
. "check_unr -run_partition": Run each partition in a different session for
UNR Analysis.

* UNR Prove Cache Now Enabled by "set_proofmaster"

The "set_proofmaster on" command now enables the UNR prove cache by default.

Functional Safety Verification (FSV) App
––––––––––––––––––––
* FSV Super Faults Now a Public Feature

The FSV "open" faults are now a public feature. Use the "check_fsv -fault -add
-type open" command to add a fault of the "open" type.

Low Power Verification (LPV) App
––––––––––––––––
* New Option of "check_lpv -generate_power_design -corrupt"

You can now use the "check_lpv -generate_power_design -corrupt ports_only"
command to corrupt the output of the gates directly connected to the boundary
interface of the power domains.

Security Path Verification (SPV) App
––––––––––––––––––
* New Color in SPV Complexity Graphs

SPV now uses the orange color to show the conditionally proven nodes.

* SPV GUI Now Includes an SPV Analysis Toolbar

The SPV GUI now has an SPV Analysis toolbar that shows a "Clear" button, which
opens a dialog box where you can choose the options for the SPV clear
operation.

* Enabling Enhanced Proof Status in SEC, SPV, and X-Prop

The SEC, SPV, and X-Prop apps now have enhanced proof status enabled by
default.

* Improved SPV GUI Information

The SPV GUI now shows the proof progress information in the design tree,
including a progress bar with information about proven, unknown, and CEX, and
a tooltip for the "Result" column that details conditionally proven
properties.

* Updated Arguments for "check_spv -clear"

The "check_spv -clear" command now requires the following extended syntax:

check_spv -clear (all | result [-task task_name])

. Use "check_spv -clear all" to clear all the SPV environment from the current
session.
. Use "check_spv -clear result" to clear the proof result of all the tasks.
Use the "-task" switch to clear the proof information from a specified task.

NOTE: Without additional arguments, the “check_spv -clear” command now returns
an error (ESW041).

Security Path Verification (SPV) App, Sequential Equivalence Checking (SEC) App and X-Propagation (XPROP) Verification App
–––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––
* "set_word_level_reduction" Not Supported by SEC, SPV, X-Prop, and C2RTL

The SEC, SPV, X-Prop, and C2RTL Apps do not support the
"set_word_level_reduction" command.

Sequential Equivalence Checking (SEC) App
––––––––––––––––––––-
* SEC Native Split Setup Mode Now Supported by LPV Load and Power Transformation

The "check_lpv -load_upf" and "check_lpv -generate_power_design" commands now
support the SEC split mode.

* Task Creation Based on SEC Mapping Table

To create a new task based on the SEC mapping table, right click on a mapping
entries selection from the SEC Signal Mapping table and choose "Create task".

* Updated "App Extensions" Options for SEC

When you right-click on a source task and choose the option "Create Task", the
following options of the "App Extensions" section are now displayed in the
dialog for you to select which attributes must be copied from the source task
to the target task:

. All SEC task-based verification target mappings, SEC imported properties,
and clock gating toggle covers
. Selected SEC task-based verification target mappings, SEC imported
properties, and clock gating toggle covers
. All task-based connection mappings, user init mappings, helpers, and
abstractions
. Selected task-based connection mappings, user init mappings, helpers, and
abstractions
. Auto map reset x values
. Map one side reset x
. All global SEC mappings

When you create a new task from the task tree, the check boxes starting with
"Selected" are disabled and the ones starting with "All" are enabled and
checked. The "Auto map reset x values" check box is checked if the case auto
map reset x is "on" for the source task (the same is true for
"Map one side reset x").

When you create a new task from the property table, the selected properties
that have a global mapping pair are ignored, as they are always available
across all tasks. Creating a task with properties that have a task-based
mapping pair leads to have a new task with relevant mappings. The related
properties are not added as they are created in "check_sec
-generate_verification". The "Auto map reset x values" checkbox is checked if
the case auto map reset x is "on" for one of the task-based mapping entries'
task (the same is true for "Map one side reset x"). The mapping entries of
type "auto init" are not copied as they are generated in the
"-generate_verification" step.

Notes:
. The "All <data>" and "Selected <data>" check boxes cannot be selected at the
same time. Selecting one option unchecks the other option.
. The "Map One Side Reset X" check box can be checked only if
"Auto Map Reset X Values" is checked.
. Clicking "Select All" leads to selecting enabled options only - "All <data>"
check boxes are checked.
. Clicking "Clear All" leads to unchecked check boxes for all options.
. Clicking "Default" leads to have checked and unchecked options just like
when the "Create Task" dialog has been opened.

* Enhanced "check_sec -copy_mapping" and "check_sec -copy_imported_properties"

This release provides enhancements to the following commands:

. "check_sec -copy_mapping": You can now copy specified task-based mapping
entries to the target task using the new "-id" switch.
. "check_sec -copy_imported_properties": You can now copy specified imported
properties to the target task using the new "-property" switch.

See the full command help for additional information (help check_sec).

* New Command for Creating Task-Based Mapping Entries in the SEC Setup

You can now create task-based mapping entries for verification targets and
toggle covers in the SEC setup (instead of global mappings) using the
following command:

set_sec_task_based_auto_mapping_on_setup on

NOTE:
. You must turn this setting "on" before running the "check_sec -setup"
command.
. The default option is "off".

* "check_sec -generate_verification" Now Runs after New Task Creation

Now, when you create a new SEC task using the GUI, the tool runs the
"check_sec -generate_verification" command automatically after creating the
task and copying the relative data.

Superlint App
––––––-
* Enhanced “config_rtlds -rule -parameter” with New "-app" Switch

You can use the new "-app" switch in conjunction with
"config_rtlds -rule -parameter" to modify the default parameters for the
apps in "app_list". If you specify unsupported parameters within a specific
scope, any reported errors apply to all scopes (Tag, Domain, and App).

* New Command for Reporting a SIG_IS_MLAS Property When Drivers Are the Same

When extracting properties of the Superlint auto-formal tag SIG_IS_MLAS, the
tool can discard multiple assignments by the same driver or consider them.

Use the following command to consider same drivers when generating SIG_IS_MLAS
properties:

set_superlint_report_same_drivers_multiple_assignment true

NOTE: The default option is "false".

* Added New Configuration Commands for Power Overflow

You can now use the "set_superlint_arithmetic_overflow_enable_exponentiation"
and "get_superlint_arithmetic_overflow_enable_exponentiation" configuration
commands to control power operation overflow.

* New Superlint Command

You can now use the following command to set the engine mode of Superlint for
FSM Deadlock and Livelock checks (FSM_IS_DDLK and FSM_IS_LVLK):

set_superlint_engine_mode_fsm_deadlock_livelock (Tri | M)+

Note: The default value is {Tri M}.

* Enhanced Superlint Arithmetic Overflow Checks

The ASG_AR_OVFL and EXP_AR_OVFL Superlint checks now support division
operation overflow.

* New Parameter Can Reduce Noise of EXP_NR_MXSU

You can now use the "skip_concat" to control the behavior of the EXP_NR_MXSU
check. When the value of this parameter is "yes", the expressions
that include a constant integer and an unsigned variable are skipped,
reducing noise. When the value of this parameter is "no", these expressions
are not skipped, and violations are reported. The default value of the
"skip_concat" is "no".

* “Show Parameter” Highlights Changed Parameters of Tag/Domain

The 'Show Parameters' context menu on a tag/domain displays the parameters
associated with that tag/domain. With this feature, altering the value of
the parameter using “config_rtlds -rule -parameter {key=value}
–<tag/domain> <tag_name/domain_name>” and using the context menu displays
“Show Parameters” dialog. This dialog window highlights the modified
parameter in bold and asterisk and a footnote with a message saying,
"This parameter has been modified".

* Improved MOD_NR_SYXZ Check

The MOD_NR_SYXZ check now successfully filters 1-bit tristate when the value
of the "skip_tristate_logic" parameter is "yes":

config_rtlds -rule -parameter {skip_tristate_logic=yes}

* Enhanced INS_IS_FEED Source Location to Assignment Statement

Previously, the source location of the INS_IS_FEED was at the output
declaration. This is now changed to an assignment statement, which helps
the tool to understand and waive any violation that depends on the
assignment.

X-Propagation (XPROP) Verification App
–––––––––––––––––––
* Use "check_xprop -prove" on Related Covers of X-Prop Assumptions

The "prove" command does no work on related covers of X-Prop assumptions. Run
the "check_xprop -prove" command instead.

* "abstract -counter -values" Now Supported by X-Prop and SPV

The "-values" switch of the "abstract -counter" command is now supported by
the X-Prop and SPV apps.

* Improved Issue with IMTR145

The tool no longer issues the info message IMTR145 during the X-Prop proof
setup.

Visualize
––––-
* "visualize -run_recipe" and "visualize -save_recipe" Deprecated

"visualize -run_recipe" and "visualize -save_recipe" now issue downgradable
deprecation error messages. The commands will be removed in a future release.

With this change, the Visualize GUI buttons to capture or edit a recipe have
been removed.

* Highlighting Frozen Traces on Visualize Waveform

When you freeze a section of the trace in Visualize, the frozen cycles are
now highlighted with a gray background and a new range marker in gray.
Previously, the background for frozen traces was beige.

* Adding Force Soft Constraint to an Infinite Trace

Visualize now lets you apply "-force -soft" constraint switches on infinite
traces using the "-loop" switch.

* QuietTrace on "Last N Cycles" on Infinite Traces

Visualize now supports QuietTrace on "Last N cycles" on infinite traces.

* New Command to Unroll Loops in Visualize

You can now use the "visualize -loop_unroll" command to expand the trace by
unrolling the loop N times (that is, repeat the looped portion of the trace).

NOTE:
. This command applies to looping traces only.
. The previous "visualize -liveness_loop_unroll" command is deprecated.

* New Command for Controlling Waveform Transparency in WaveEdit Mode

You can now control the transparency percentage of the WaveEdit background
using the "set_visualize_waveedit_transparency" command.

Abstraction
–––––-
* Added Support for Dynamic Critical Values in Counter Abstraction

The "abstract -counter" command now accepts Verilog or VHDL expressions as
arguments to the "-values" switch, which previously accepted constants only.
This lets you abstract counters whose output is compared to values that can
change during the proof.

Example:

abstract -counter cnt_inst.out -values {0 cnt_inst.limit 127 {data1 || data2}
255}

Clocks and Reset
––––––––
* Enhanced "sanity_check" Command

"sanity_check -analyze simple_clk -verbose" now lists the property name
when it finds an incorrect edge declaration in a property.

Deep Bug Hunting
––––––––
* Restricted Engines for the Loop Swarm Hunt Strategy

The "hunt -config -engine_mode" command now accepts only the B and B4 engines
for the loop swarm strategy.

Note: If you do not specify this switch, the tool defaults to engine B.

* Specifying Time Limit in Trace Search Hunt Strategy

You can now use the "-interval_time_limit" switch in the "hunt -config
-strategy -mode trace_search" command to specify the time limit for each
interval search.

If you specify zero, any new search takes the remaining time limit as the
search time limit. If you specify any value greater than zero, any new search
time limit is that value. If you specify "auto", an estimated value based on
the total time limit and the total number of searches launched is used as the
interval search time limit. If you do not specify this switch, the tool sets
it to "auto".

* Hunt Manager Now Supports Updating Strategy Parameters Back to "auto"

Hunt Manager now lets you update the following strategy parameters back to the
"auto" configuration when this value is possible for the corresponding
parameter of the strategy:

Cycle Swarm and Bound Swarm:
. first_trace_attempt
. max_first_trace_attempt
. per_property_time_limit
. per_property_time_limit_factor

Trace Search:
. interval_cycles
. interval_time_limit

Trace Swarm:
. per_trace_time_limit

Previously, once you had changed a parameter with the "auto" value to a value
different from "auto", it was not possible to set it back to the "auto" value.

Design Compilation
–––––––––
* Library List for Design Configuration Now Working as Expected

Now, if a module or package is added in a library that is not specified in
the library mapping statements, but the library mapping exists, that library
will also be searched for modules.

* Extended UDP Handling Now Default in Jasper

The extended UDP handling feature is now default in Jasper. To disable this
feature, use the following command:

elaborate -disable_extended_udp_handling

Note: The elaborate switch "-extended_udp_handling" is now a no-op switch.

* Parallel Launch of Synthesis Processes Now Possible

Previously, Jasper submitted each job in Parallel Synthesis Shell mode
sequentially, thus preventing the parallel launch of the synthesis process.
This release improves this issue, and synthesis processes are now launched in
parallel.

Design Exploration
–––––––––
* Highlighting Cursor Line With Color

Added new option "Highlight cursor line with color" in "Preferences ‐
Source Browser ‐ Highlight Cursor Line Color", which can be set using the
GUI or the "set_preference
{SourceCodeBrowser/SyntaxHighlighting/HighlightCursorLineColor}" command.

Design Exploration and Miscellaneous
––––––––––––––––––
* Listing Parameters for a Specified Interface or Module Only

You can now use the new "interface_port_local_parameter" and
"interface_port_parameter" arguments with "get_design_info -list" to list only
interface port and local port parameters for the instance and modules scopes.

* Using "complexity_manager" without Arguments

When you launch the Complexity Manager Viewer for the entire design logic
using the "complexity_manager" command without arguments, the tool does not
consider properties or abstractions in any task.

NOTE: When analyzing the full design, the Complexity Manager considers
environmental abstractions, although it does not consider abstractions that
are local to a single task. It also ignores all stopats, both environmental
and local.

Engines
–––-
* Enhanced EngineJ to Stop Automatically

EngineJ now automatically stops when only liveness properties remain,
preventing unnecessary running.

Language Support
––––––––
* Updated Default Semantics for Cover Property

Prior to this change, the default semantics for cover property resulted
in a finite cover trace for all properties. After this change, the
sub property "always a" will have an infinite semantics and produce an
infinite trace where "a" is true throughout.

* Returning the Number of Flop Bits of a Specified Property

You can now use the following new command to return the number of flop bits
of a specified property:

get_design_info -property <property_name> -list property_flop_bit

* Enhanced SVA Local Variable Support

Jasper now provides basic support for SVA local variables used in assertions
for operators "intersect" and "and".

* Improved Check for "genvar"

Jasper now has an improved check for the use of "genvar" outside generate
contexts. This might lead to new VERI-1289 error messages.

Note: You can downgrade the error messages to warnings using the
"set_message -warning VERI-1289" command.

* Enforcing the Check of VHDL Clock Edge Pattern

Jasper enforces the check of the VHDL clock edge pattern. The clock edge in
VHDL has the following pattern (for posedge):

if (clk'event and clk = '1') then

Jasper now verifies also if the pattern is complete and if the same signal is
used in the event operator and in the comparison. If that is not the case,
Jasper issues one of the following error messages: VHDL-1136, VHDL-1414, or
VHDL-1741.

* Using Enum Parameters

Jasper enforces the type check for parameter declaration with no type or range
specified. A parameter declaration with no type or range specification
defaults to the type and range of the final value assigned to the parameter,
after any value overrides have been applied. If the expression is real, the
parameter is real. If the expression is integral, the parameter is a logic
vector of the same size with range [size-1:0]. Then, if the parameter value
is an enum value, the parameter type is a logic vector of the same size with
range [size-1:0]. This might lead to later errors when using the parameter in
enum contexts. To avoid the issue, declare the type of the parameter as the
enum type.

Miscellaneous
––––––-
* Added New Jasper Tcl Library Documentation

This release adds a new Jasper Tcl Library documentation, which provides a
library of useful Tcl functions. You can access it from the
Help – Application Guides – Jasper Tcl Library. Alternatively, you can also
access this document from the doc directory (doc/jasper_tcl_library.pdf).

* New Proof Structure Command to Copy Embedded Properties into Nodes

You can now use the following command to edit the target proof structure node
by copying properties from the source task:

proof_structure -edit <target_node_name>
-copy <property_name_list>
-source_task <source_task_name>

. Use "-copy" with a Tcl list to copy specified assertions or covers from the
specified task.
. Use "-source_task" to copy contents from the specified task instead of the
current task.

Note: The switch "-edit" is valid for any Proof Structure node that is an
implementation node with no child nodes (no Proof Structure operation based on
it).

* Jasper No Longer Supports the "=>" Implication Operator

With this release, support for the deprecated "=>" implication operator in
Tcl expressions has been fully removed. Now, if you use "=>" in a Tcl
expression, the tool issues the following error message:

ERROR (ENL063): Syntax error near "=>" in expression "a => b".

Proofs and ProofGrid
––––––––––
* Formal Profile Restarts with Same Configurations as Original

When you restart a Formal Profiler run using the play button in the GUI,
the new run now has the same configurations as the original run.

* Enhanced Formal Profiler to Start at 0 Instead of 1

Formal profiler now starts at "formalprofiler:0" instead of
"formalprofiler:1".

* Enhanced Formal Profiler to Use Design Hierarchy

Previously, instances enclosed by scopes were flattened. Now, they are
displayed as separate nodes in the Design Hierarchy tree view to match
other sections of the tool.

* New Default Layout for Formal Profiler

Now, the Formal Profiler has a dedicated window, which is located below
the Toolbar in the main window default layout. Previously, the Formal
Profiler was a part of the Complexity Manager window, and only one window
can be displayed at a time. With this feature, you can now open them
simultaneously.

* New Behavior of the "proof_structure -init" Command

The "proof_structure -init" command now copies all abstractions, assumptions,
and hard stopats from the source task to the Proof Structure node by default.

Use the newly added "-no_copy_env" switch to prevent such copying operation,
thus creating the new node without anything from the source task.

* Creating Underconstraint and Overconstraint Proof Structure Nodes

You can now use the "proof_structure -create underconstraint" and
"proof_structure -create overconstraint" commands to create a node where only
underconstraint or overconstrained operations can be performed using the node
specified as the source for the operation.

The commands create one node with copies of all properties and abstractions
from the target node, allowing changes to the created node.

* New Proof Structure Option

You can now use the new "-copy_related_asserts" switch with the
"proof_structure -create" command for the operations of partition,
compositional assume-guarantee, and assume-guarantee. This gives you the
option to copy all automatically extracted related assertions for the
properties that are being copied.

NOTE: This is limited to "safety_in_liveness" assertions.

* Setting "per_engine_max_jobs" to Unlimited

The "proofgrid_per_engine_max_local_jobs" and "proofgrid_per_engine_max_jobs"
configurations and the "prove -per_engine_max_jobs" switch now accept 0 as a
value, which means that there is no limit on the number of jobs per engine. If
set to 0, the proof is limited by the number of properties and other settings
such as "max_jobs".

* Added "trace_bound" Switch to "get_property_info -list" Command

This release introduces the "trace_bound" switch to the
"get_property_info -list" command, which refines the minimum and maximum
length of the properties. The trace bound is a representation of the
possible lengths of the shortest trace, displayed as a list of intervals of
lengths. An interval {a b} means the shortest trace may have a length
a <= l <= b. Intervals with a single value {a a} are abbreviated as a, and
an unlimited value is represented with $. For example, the set of intervals
{1 3 {5 8} 10} means the shortest trace is 1, 3, 5-8, or 10 cycles long.

* Fixed Oracle Grid Engine Parallel Environment Warning Issue

This release fixes a warning where the ProofGrid mode for Oracle(R) Grid
Engine warned about a possibly missing parallel environment even when
specified.

* Extended "get_trace_info" to Explicitly Report SST Information

The "Tag" column of the Property Detail dialog now explicitly reports
whether a trace is an SST trace when you use the "get_trace_info" command.

Proofs and ProofGrid and Property and Configuration Database
––––––––––––––––––––––––––––––
* New Alternative to "visualize -sst"

You can now use the "prove -sst" command instead of "visualize -sst". This
enables the "prove" command to run State-Space Tunneling proofs.

In a State-Space Tunneling proof, the tool ignores reset, that is, the proof
starts at an arbitrary state, and all helper assertions in the task are forced
to pass for a specified number of cycles. After that, the tool checks if the
helper assertions can fail. This creates an interactive proof flow where,
based on the SST traces, you can add more helper assertions and rerun the
proof until no more SST traces are possible. When the required "min_length"
bound is established for the full set of helpers, the tool achieves full
proof.

Compared to the "visualize -sst" command, "prove -sst" shows the following
advantages:

. multi property proofs
. multiple proof threads (background proofs)
. full integration with the results presented in the property table,
accessible using "get_property_info", "get_property_list", and so on
. given sufficient "min_length" bounds, full proof is reported
. proof performance improvement, in particular, trace engines like B* and Ht*
work better with "prove -sst" and might be sufficient when they are not in
"visualize -sst"
. support for standard proof flow features, for example: trace extension,
store_trace unlimited, evaluate in trace, proof structure, liveness, and so
on

NOTE: "prove -sst" does not support "visualize -replot" with added
configurations.

User Interface
–––––––
* Renamed "Cover (live)" to "Cover (infinite)"

With this release, "Cover (live)" is renamed on the Property Table and
Property Table filter to "Cover (infinite)", and some GUI windows and
messages have been edited to disambiguate between liveness assertions and
infinite covers.

* Updated View SST Trace Context Menu

The "View SST Trace" context‐menu option has been replaced with the
"View Visualize SST Trace…" to prevent conflicts with the "prove -sst"
flow.

* Setting GUI Colors using "set_preference" Commands

You can change the console log's special text colors in run time using
relevant "set_preference" commands. Prior to this, the console log's special
text color had to be manually edited in the user configuration file
("~/.config/cadence/jasper.conf") to initialize it in non-default settings.

You can use the "set_preference" command to set Jasper GUI colors for future
use. See the full help for additional details (help set_preference -gui).

NOTE:
. The colors mentioned are identical to those in the "Changing GUI
Background and Foreground Colors" section of the general user guide.
. The colors cannot be updated while the program is running. They can be set
only in the project preferences, which are read during start-up. Jasper
restart is necessary to apply the colors through the "set_preference"
function.
. You can override the "GUI/BackgroundColor" and "GUI/ForegroundColor"
colors using the "-bg" or "-fg" Jasper switches.
. You can manually save the preferred colors in the user settings
("~/.config/cadence/jasper.conf"). If project preferences are available,
they take priority over user preference, especially specific preferences
given higher priority.
. You can always override all these color settings using the "-stylesheet"
Jasper switch.

Verification Management
–––––––––––-
* Saving a Database Periodically

This release includes a new periodic save feature that periodically updates
proof results in a database. To create a periodically updated database, run
"save -jdb database -capture_session_data -periodic [-period time]". To stop
periodic save, run the "save -periodic -stop", "clear", or "restore"
commands.

NOTE:
. If a database is created without the "-periodic" switch, it cannot be
periodically updated later.
. If a periodic database is saved again without the "-periodic" switch,
it becomes a non-periodic database.
. A periodic JDB database can be overwritten with other options
(for example, adding a setup script using "save -jdb database
-capture_session_data -capture_setup -periodic" where "database" is an
existing periodic database). This operation stops periodic save, removes
the old database, saves a new one, and restarts periodic save if
"-periodic" is enabled.
. Periodic save time period supports the same inputs as "prove -time_limit".
. The minimum and default periodic save time period is equal to 30 minutes.

vManager Integration
––––––––––
* Added New Argument to Run Single Run Script Mode

This release includes a new "override_deprecation_error" argument to allow
the Single Run Script mode to operate without error. If not used, an error
will occur. In the future, the Single Run Script mode (jg_vm_single_run.py)
Python script will be removed from the installation directory.


Resolved Issues
===============
The following reported issues have been fixed in 2023.09.

C to RTL Equivalence Checking (C2RTL) App
––––––––––––––––––––-
* Loop Bound Inside Unused Inline Function

The tool produces an error if a loop bound is set inside an unused inline
function. Use "set_message -warning ECTR004", "set_message -warning ECTR068",
and "set_message -warning ECTR069" to downgrade errors from this command into
warnings.

* Fixed Issue with Engine WHp

The tool no longer exits unexpectedly when using the engine WHp.

* Fixed Issue with C2RTL JASPER_BUFFER

***IMPORTANT: CHANGE IN TOOL BEHAVIOR***

This release changes the behavior of JASPER_BUFFER interface definitions.

Previously, constants were propagated through a variable declared as a BUFFER.
As a result, these constants were visible in the formal model after putting a
stopat on the buffer signal.

Now, the formal model after setting a stopat on a signal x is equivalent to
the formal model obtained by declaring x as an INPUT instead of a BUFFER in
the software model.

CSR Verification App
––––––––––
* Resolved Issue with DATA_WIDTH

The CSR checker for AHB lite now supports DATA_WIDTH of 8 and 16 bits.

Clock Domain Crossing (CDC) App
–––––––––––––––-
* Default Rating of Power Control Ports Now "async-to-all"

"Power Control" ports now rated "async-to-all" by default, and they are not
affected by the "treat_data_ports_as_async" parameter. You can change their
rating using "config_rtlds -port -clock" command.

* Resolved Issue with CDC_NO_SYNC Violations

The CDC hierarchical flow no longer reports a CDC_NO_SYNC violation in a port
of a blackboxed module that is connected to an internal multi-bit
recirculating scheme.

* Improved Clock Period Normalization Algorithm in SDC Clocks

The clock period normalization algorithm in SDC clocks has been improved in
CDC. This algorithm matches the SDC clock periods to Jasper clock factors,
keeping those factors below 10 and keeping the clock proportions as much
as possible. As a result, the “round_sdc_clock_periods” parameter has been
deprecated from the CDC rule file. This is now enabled by default.

* Fixed Issue with MUX Synchronization Violation in Hierarchical Flow

CDC no longer reports no_scheme violations in ports connected internally to
MUX_NDFF schemes in hierarchical flow.

* Fixed Issue with CDC Waived Violations

CDC waived violations are no longer excluded from the violation groups. They
have a lower priority, and will be the primary violation only if all the other
violations from that group are also waived.

* CDC Recognizes Liberty Blackboxes as Retention Cells

CDC now recognizes Liberty blackboxes declared as retention cells as any other
retention cell. Therefore:
. The Ports Table no longer lists the retention cells of Ports of Liberty
that are blackboxed.
. The tool now considers the output ports of Liberty blackboxed retention
cells as regular retention flops (just like the UPF-declared ones).
CDC also considers the Liberty blackboxes declared as retention cells as valid
flop units. Therefore, the tool now detects convergence cases passing through
Liberty blackboxed retention cells.

* CDC No Longer Reports "no_scheme" Violations on Power-Control Path Crossings

CDC no longer reports "no_scheme" violations on crossings in power-control
paths if the connection to the retention cell is via save or restore pins.

* Assigned New Port Roles to Liberty Blackbox Retention Cells Pins

Power_Control and Power_Supply ports connected to the Liberty blackbox
retention cell pins now have their respective roles on the Ports Table.

Connectivity Verification App
––––––––––––––-
* COI Validation Checks Now Consistent for Single and Multiple Connections

The behavior of the "check_conn -validate" command is now the same for single
and multiple connections: a connection is marked as "Inside COI" only if all
bits of the source are in the COI of the destination.

* "check_conn -load" Now Works Properly with Linked Files

The "check_conn -load" command can now load linked files that do not contain
CSV files. This change applies to the file name only, not to the content.

* Corrected Issue with Reverse Connectivity GUI

The "Remove" button in the Reverse Connectivity window now correctly removes
rows with the "Relative Depth" set to "$".

* Resolved Issue with Reverse Connectivity GUI

The Reverse Connectivity GUI now works properly with escaped names on signal
paths.

Coverage App
––––––
* Corrected Issue with "check_cov -list" Command

The "check_cov -list" command can now return more than 500000 cover items and
also use the "jforeach" command to iterate through them.

* Updated Documentation of "check_cov -report -type"

The "check_cov -report -type" command now has all the options properly
documented.

* Fixed Issue with Proof Core Warning Message

The coverage report command no longer issues spurious WCOV011 warning message
if proof core is not enabled.

* License Hold During Mutation Coverage Measurement

The Jasper Coverage App now holds an advanced license checked out during
measurement if "-type {mutation}" is passed to the "check_cov -measure"
command.

Note: The current behavior of checking an advanced licensed during
"check_cov -init" when mutation type is enabled continues to happen.

* Toggle Cover Items No Longer Incorrectly Reported as Out of Proof Core

Toggle cover items for abstracted counters are no longer spuriously marked as
unchecked for Proof Core (normal and high precision modes).

* Resolved Issue with "cover -extend" Command

Coverage now properly supports extended covers as part of its "property" cover
item database.

* Corrected Inconsistency Between "get_property_list" and "get_property_info"

The tool now marks Covergroup properties as embedded, that is, not Tcl. Hence,
the commands "get_property_info" and "get_property_list" consider the same
information to report this value for properties.

* Resolved Issue with "gui -filter"

The "gui -filter" command no longer makes Jasper exit unexpectedly when the
COV App GUI is open.

Coverage Unreachability (UNR) App
––––––––––––––––-
* Resolved Unexpected Exit of Elaboration When Running UNR

Jasper no longer exits unexpectedly during P2P elaboration when using
“-unr” switch, and now works as expected by elaborating on previously
unelaborated modules.

* Fixed Issue with Wildcards in the P2P "analyze -bbox_m" Command

The P2P "analyze -bbox_m" command now supports wildcards in module names.

* Option Names Can Now Contain a Period

UNR can now create cover properties when a covergroup option name
("option.name") contains a period.

* Updated GUI Design Hierarchy for UNR

The GUI Design Hierarchy for UNR now complies with the Jasper standard,
including the expansion of intermediate scopes enclosing instances.

* Resolved Issue with UNR Segmentation Fault

UNR no longer exits unexpectedly due to a segmentation fault during
elaboration caused by invalid objects at JNetlist.

Functional Safety Verification (FSV) App
––––––––––––––––––––
* Updated Help Information of the "check_fsv -generate -copy_env" Command

Use the "check_fsv -generate -copy_env" command to copy all the task
assumptions and task abstractions (except stopats) from the current task to
the new task(s).

Note: By default, newly generated FSV tasks contain only the environment
assumptions and abstractions.

* Fixed Issue with FSV Analysis with CO Strobe Outside "inst_top"

In FSV integration use-case, when there is at least one CO strobe outside of
the defined "inst_top", the FSV structural and formal analysis assumes that
detection might happen on those missing strobes.

* Corrected Issue with FST Scripts

When the originating strobe file provided to the campaign has strobes with the
second strobe being a textual subset of the first strobe (for example: data10,
data1), the FST produces invalid Safe or UU fault annotations.

Sort the originating strobe file before providing it to the campaign and
update the Jasper version to 2023.09 to solve the issue.

Security Path Verification (SPV) App
––––––––––––––––––
* Fixed Issue with SPV Prove

You can now prove SPV properties and get the traces without workarounds.

Sequential Equivalence Checking (SEC) App
––––––––––––––––––––-
* Resolved Issue with SEC GUI

The tool now shows the "Vacuous" entry in the SEC Property Table GUI.

* Fixed Issue with Sub-Instances Containing Modports in SEC

Previously, when sub-instances contained modports, hierarchical sequential
equivalence checking returned errors while elaborating. This release fixes
this issue, and hierarchical sequential equivalence checking now handles
the design with interfaces and modport correctly.

* Improved Run Time for SEC Signoff

This release improves the run time of the "check_sec -signoff" command.

* Updated Jasper Sequential Equivalence Checking App User Guide

The Jasper Sequential Equivalence Checking App User Guide document no longer
has blank pages.

Superlint App
––––––-
* Added FSM Disabling State Capability to FSM_IS_LVLK

Previously, the FSM disabling state capability was supported only by
FSM_IS_PLLK and FSM_IS_NLLK tags. This release adds the FSM disabling
state capability to the FSM_IS_LVLK tag.

* "check_superlint -report" Now Reports Violations Summary as Expected

The "check_superlint -report" command now reports the violations summary
to the console as expected when issued without additional arguments.

* "-exclude_hierarchies" Switch Now Filters CLK_NF_NMCF Violations

The "-exclude_hierarchies" switch now functions correctly by filtering
CLK_NF_NMCF and other structural module-based violations, just like it
does for all other types of violations.

* Fixed Issue with Superlint FSM Properties Export

This release resolves an issue with the Superlint FSM properties export that
caused the same port to be written multiple times.

* Fixed Issue with CAS_NR_DEFA Violations

The tool now considers the case items that use inverse range (high to low) as
empty and no longer issues the CAS_NR_DEFA violation for them.

The following changes are visible in case statements:

. Violations related to case statements that are dependent on fully covered
cases, for example: CAS_NR_DEFA.
. Other checks that do not report violations on a case item of type inverse
range are: CAS_NR_CMUL, CAS_NR_OVCI, CAS_NR_PUOV, CAS_NR_UCIT.

* Resolved Issue with IDN_NR_VHKW Violation

Superlint can now report the IDN_NR_VHKW violation for generate variables
during elaboration.

* New Superlint Checks

This release includes the following new checks:

. AUTO_FORMAL_BUS
. SIG_IS_MLAS (Error): "More than one assignment found for signal '%s'".

. CODINGSTYLE
. ALW_NR_OLDS (Warning): "In the module '%s', it is recommended to replace
old style always block with new '%s'".

. FILEFORMAT
. VHF_NO_HDCM (Warning): "VHDL file '%s' does not contain header comment".

. RACES
. CLK_NR_FNBA (Warning): "Flip-flop '%s' with a non-blocking assignment
drives the clock pin of one or more flip-flops where data inputs are
synced to the same clock."

Visualize
––––-
* Resolved Issue with Plotting Incorrect Signal in Concatenation

The Source Browser now identifies and correctly plots the first signal of
the concatenation as expected.

Clocks and Reset
––––––––
* "get_property_info -list edge" Now Shows Properties Edge Correctly

The "get_property_info -list edge" command now correctly shows the edge of
properties that are triggered on both positive and negative edges.

* Improved Message for Clock Rate on a Signal

Jasper now issues the WCK020 message when a non-standard clock is rated into a
signal that is not a PI or a stopat:

WCK020: Ignoring signal "%s" in "clock -rate" command. Signal is not an input
or environment stopat.

* Fixed Issue with Clock “sanity_check” Not Skipping Deactivated Properties

Previously, clock “sanity_check” did not skip the deactivated properties
while looking for inconsistencies. This release fixes this issue, and the
clock “sanity_check” now correctly skips the deactivated properties.

Design Compilation
–––––––––
* Resolved Copied FileLocker Keeping Original Permission Issue

Now, FileLocker keeps the original file permissions to prevent unwanted
extended data access permission.

* Resolved Issue with VERI-2695 Messages

Jasper no longer issues VERI-2695 messages when a checker is instantiated
within an interface.

* Overwriting Struct Parameters in Elaboration

When using "-inst_top" in elaboration, you can now replace the parameter
associated with a struct.

* Resolved Issue with Sequence Fusion and Empty First Operand

Previously, the sequence that only matches the empty word as a left-hand
operand to ##{0:n} could result in a semantic error. This release resolves
the sequence and empty first operand issues.

* Fixed Issue with "elaborate"

Jasper now works properly during the elaboration of scenarios involving
unresolved references.

* Fixed Issue with Functions in Packages Reporting Incorrect VERI-1128

Jasper no longer reports the incorrect VERI-1128 when dealing with functions
defined in a package.

* Fixed Issue with Clock Signal Reporting Incorrect VERI-1330

Jasper no longer reports the incorrect VERI-1330 when dealing with an array
of interfaces passed as actual in a module instantiated using indexing.

* Fixed Issue with Unexpected VERI-2695

Jasper no longer issues unexpected VERI-2695 messages due to default clocking
in different generate "if" branches.

* Corrected Issue with Warning Message

Jasper now issues the correct warning message for unmatched sizes.

* Corrected Issue with the "analyze -f" Command

The "analyze -f" command now properly processes ".f*" files whose file names
contain the "-f_" sequence and does not stop reading the script.

Design Compilation and Miscellaneous
––––––––––––––––––
* Resolved Issue with Genvar Usage in "for loop" Statements

Previously, debugging a for loop statement pointed to the incorrect linefile
due to genvar usage within the for loop. This release fixes this issue, and
now debugging points to the correct linefile.

Design Exploration
–––––––––
* New Marker Placement for Vertical Net Names in Schematics

When a net name is vertical in a schematic, the markers are now turned
vertically to avoid being squished due to lack of space.

Infrastructure
–––––––
* Stopped Support for "Ignore" Severity in Jasper Error Messages

Previously, you could change the following error codes to "Ignore", but
now they can only be changed to "Warning" or "Info":
* ENL169
* VERI-1187
* EPF020
* ERS024
* VERI-1896
* VERI-2228
* EIPX024
* EIPX025
* EIPX026
* EDEP146
* EAD019
* EG017
* ECDC137

* Corrected Issue with "-include_instance" and "-exclude_instance"

Coverage, FSV, SEC, and X-Prop now properly support instances inside
generate-block hierarchies in "-include_instance" and "-exclude_instance"
switches from their respective Tcl commands.

Language Support
––––––––
* Fixed Compilation Issue with 'upward name referencing' Checkers

Jasper no longer has compilation issues with checkers that use
'upward name referencing'.

* Resolved Issue with Mapping of Verilog Logic Parameter

Mapping of Verilog logic parameter with "std_logic" component "generic" is
now fixed.

Miscellaneous
––––––-
* Updated Jasper Coverage App User Guide

The Jasper Coverage App User Guide document no longer has blank pages.

* Corrected Ambiguity in LTC_NO_INIT Description

The Jasper CDC Checks Reference Manual now shows the correct description
for the LTC_NO_INIT category.

* Fixed Issue with "session -new -reuse_elaborated_design"

The switch "-reuse_elaborated_design" of the "session -new" command now
properly loads LPV and Liberty databases.

* Fixed Issue with "capture_testcase" Command

Jasper now works as expected with the "capture_testcase" command that
previously caused errors when a file with a symbolic link directory was
included through the "-include_files" switch during testcase execution.

* "get_tool -list_apps" No Longer Causes Jasper to Stop Responding

"get_tool -list_apps" now works as expected when running Jasper in batch mode.

* Resolved Issue with "capture_testcase"

Previously, "capture_testcase" might not have successfully created or
processed the symbolic link or the symbolic link might have pointed to the
wrong place. This release resolves the issue.

Proofs and ProofGrid
––––––––––
* Improved "-get_node_info" for Propagation Results and Status

"proof_structure -get_node_info" command now improved to propagate the
results and compute the propagation status.

* Fixed Proof Structure GUI Pane Displaying Inaccurate Target Numbers

Previously, the tool incorrectly counted assumptions as targets when they
were added or removed from a node. However, this was not the case during
the initial setup. As a result, removing assertions led to inaccurate
numbers being displayed on the Proof Structure property GUI pane.
This release fixes this issue. The targets are now counted accurately, and
assumptions are ignored.

* Non-Liveness Properties Become Liveness When Trace Extension Is "$"

The "get_property_info" command now reports liveness=1 when trace extension is
"$", indicating that the property is effectively liveness.

State Space Tunneling (SST) and User Interface
–––––––––––––––––––––––
* Property Table Now Displays Maximum SST Length

Property Table now displays information when no SST trace is found.
The "Bounds" column now shows the maximum SST length.

Verification Management
–––––––––––-
* Resolved Issue with EG014 Error

Restoring elaborated design and jdb no longer exits unexpectedly and issues
EG014 when the database file contains corrupted traces.

* WPM021 Now Issued in All Cases

The "task -create -copy" command now issues one WPM021 warning per
argument that does not match any task. Previously, if any property matched
any of the arguments passed, Jasper did not warn you that other arguments
did not match.


Deprecation Notices
===================
The following commands/variables are being deprecated.

The tool issues a warning if you use the following commands. No changes to
your scripts are required at this time; however, in a future release, these
commands will trigger a downgradable error message, and ultimately, they will
be retired. We strongly encourage you to adjust your scripts as soon as it
is practical to do so.

. check_c2rtl -set_dynamic_pruning -measure_time_fully
. get_cdc_no_waiver_for_multipair_violation
. set_cdc_no_waiver_for_multipair_violation
. check_cdc -signal_config -condition
. check_cdc -signal_config -prove
. check_cov -init -enable_checker_undetectable: Checker undetectable is now
enabled by default.
. check_lpv -generate_power_design -exclude_modules: Use "set_simstate_behavior
DISABLE -model" instead.
. get_sec_autoprove_design_style_type
. set_sec_autoprove_design_style_type
. set_sec_autoprove_strategy design_style
. check_sec -prove -strategy design_style
. get_sec_autoprove_bug_hunting_bswarming_bound_factor
. set_sec_autoprove_bug_hunting_bswarming_bound_factor
. get_sec_autoprove_bug_hunting_helpers_on_auto_generated_signals
. set_sec_autoprove_bug_hunting_helpers_on_auto_generated_signals
. get_sec_autoprove_bug_hunting_number_of_bswarming_threads
. set_sec_autoprove_bug_hunting_number_of_bswarming_threads
. set_sec_autoprove_strategy bug_hunting
. check_sec -prove -strategy bug_hunting
. check_superlint -export -extended_property_name
. get_export_sva_use_escaped_identifier_with_extended_names
. set_export_sva_use_escaped_identifier_with_extended_names
. get_superlint_include_latch_data
. set_superlint_include_latch_data
. visualize -liveness_loop_unroll

The following commands have been deprecated, and any use of them triggers a
downgradable error message. Remove them from your scripts or use
"set_message -warning". These commands will be retired in a future version of
the tool.

. check_cdc -sdc triggers ECDC137: Use "read_sdc" instead or use
"set_message -warning ECDC137" to downgrade this message to a warning.
. check_cdc -structural_cell triggers EDEP291: Use "check_cdc -glitch_free"
instead or use "set_message -warning EDEP291" to downgrade this message to a
warning.
. database -sync triggers EDEP309
. visualize -run_recipe triggers EDEP301: Remove it or use "set_message -warning
EDEP301" to downgrade this message to a warning.
. visualize -save_recipe triggers EDEP302: Remove it or use "set_message
-warning EDEP302" to downgrade this message to a warning.
. set_tool_mode triggers EDEP303: Use "set_current_gui" instead or use
"set_message -warning EDEP303" to downgrade this message to a warning.
. assert -task -update_db
. assert -task -update_all_sessions
. assert -task -suppress_db_update
. assert -replace -update_db
. assert -replace -update_all_sessions
. assert -replace -suppress_db_update
. assert -from_assume -update_db
. assert -from_assume -update_all_sessions
. assert -from_assume -suppress_db_update
. assert -rename -update_db
. assert -rename -update_all_sessions
. assert -rename -suppress_db_update
. assume -env -update_db
. assume -env -update_all_sessions
. assume -env -suppress_db_update
. assume -soft -update_db
. assume -soft -update_all_sessions
. assume -soft -suppress_db_update
. assume -from_assert -bound -update_db
. assume -from_assert -bound -update_all_sessions
. assume -from_assert -bound -suppress_db_update
. assume -from_assert -env -update_db
. assume -from_assert -env -update_all_sessions
. assume -from_assert -env -suppress_db_update
. assume -rename -update_db
. assume -rename -update_all_sessions
. assume -rename -suppress_db_update
. cover -task -update_db
. cover -task -update_all_sessions
. cover -task -suppress_db_update
. cover -replace -update_db
. cover -replace -update_all_sessions
. cover -replace -suppress_db_update
. cover -rename -update_db
. cover -rename -update_all_sessions
. cover -rename -suppress_db_update
. set_property_auto_update_db
. get_property_auto_update_db

The following commands are retired. They no longer have any effect, and you
should remove them from your scripts.

. check_superlint -waiver -export -text_format
. set_clock_handle_self_disabling_registers
. get_clock_handle_self_disabling_registers
. set_clock_process_reconvergent_logic
. get_clock_process_reconvergent_logic
. set_clock_accept_enable_with_glitches
. get_clock_accept_enable_with_glitches
. set_clock_handle_complex_logic
. get_clock_handle_complex_logic
. database -get_description
. "=>" implication operator: This operator is no longer supported and its use in
a Tcl expression triggers a non-downgradable error message (ENL063).
. visualize -explore
. get_database_autosave_mode
. set_database_autosave_mode
Jasper Apps Version 2023.09p001 - Date: Oct 17, 2023
The following new features and enhancements are included in Jasper Apps 2023.09p001.



ENHANCEMENTS


Jasper is the premier electronic design automation (EDA) supplier of high-level formal functional verification software. All the big 3 already have their own formal technology but the technology the leading companies seem to depend on most heavily is Jasper’s JasperGold technology, which is perceived as having the most advanced technology. Cadence put the Jasper technology together with their existing Incisive technology. In fact, they put it together will all their verification technology: Verilog simulation, Palladium emulation, virtual platforms and more. The theme in verification these days is to take all the various approaches and unify them so that they use the same debuggers, same user interfaces, take the same inputs, assertions and then put some sort of metric-driven methodology together so that the most appropriate technology is used without overlap (so you don’t waste time using simulation to test something that has already been formally proven, for example).

Simplifying Formal 3: The JasperGold Visualize Debug Environment – Gargi Sharma







Gargi demonstrates the powerful yet easy-to-use formal exploration and debug capabilities of the JasperGold GUI and Visualize environment.
Jasper Design Automation, Inc. is an electronic design automation company developing verification system that provides bug detection and debugging solutions.The company's products include JasperGold verification system that provides bug detection and debugging solutions; and GamePlan verification planner Web site. The company was founded in 1999 as Tempus Fugit, Inc. and changed its name to Jasper Design Automation, Inc. in 2003. Jasper Design Automation, Inc. is based in Mountain View, California.
Cadence is a pivotal leader in electronic design and computational expertise, using its Intelligent System Design strategy to turn design concepts into reality. Cadence customers are the world’s most creative and innovative companies, delivering extraordinary electronic products from chips to boards to systems for the most dynamic market applications.
Cadence Design Systems acquired Jasper Design Automation, Inc on 2014-04-21. The completion of this transaction expands differentiation of Cadence’s System Development Suite, Cadence’s flagship system design and verification platform. Integration of Jasper’s solutions with Cadence’s connected debug analysis and software and hardware verification platforms will improve customers’ ability to leverage Cadence’s unified verification planning, metric-driven verification flow, and extensive dynamic and formal Verification IP portfolio for embedded processor system verification.

Owner: Cadence
Product Name: JasperGold
Version: 23.09.001 *
Supported Architectures: x86_x64
Website Home Page : www.cadence.com
Languages Supported: english
System Requirements: Linux **
Size: 2.9 Gb



* included:


Base_JASPER23.09.000_lnx86
Update_JASPER23.09.001_lnx86

图片:22.png