Cadence JasperGold 23.03.001

*****************************IMPORTANT NOTICE***************************

UPCOMING CHANGE IN PLATFORM SUPPORT: Beginning with version 2023.06, Jasper will no longer support Red Hat Enterprise Linux 7.1, 7.2, or 7.3 or CentOS 7.1, 7.2, or 7.3.

IMPORTANT INFORMATION ON KERNEL SUPPORT: Currently, a bug in kernel versions 4.18.0-358.el8_6 through 4.18.0-372.19.el8_6, which are present in Red Hat Enterprise Linux 8.x operating systems, prevents you from running Jasper Apps. You must upgrade the kernel version to run Jasper. For additional information about this issue, consult the QTBUG-100174 bug report.

JAVA RETIREMENT: Beginning with the 2023.03 FCS release, Jasper will not load a Java Virtual Machine or provide the Java Runtime Environment with the build. One known side effect is that the “hs_err_pid<PID>.log” files will no longer be created if Jasper exits unexpectedly.
*************************************************************************

List of Features and Enhancements
––––––––––––––––-

* C to RTL Equivalence Checking (C2RTL) App
* C/C++ Call Stack Now Visible by Default in C2RTL Source Browser
* C Structs Now Accepted as Inputs for C2RTL
* Improved Messaging for Synthesis Errors
* JASPER_ASSUME Now Works as Expected for .c Files
* Automatically Constraining Enum Type Inputs
* C/C++ Compilation Warnings Now Printed to Console
* Warning Now Issued for Termination Due to Insufficient Unwind Limit
* InsufficientUnwindLimit Safety Assertion Renamed to InsufficientUnrollLimit
* Multi-Context Debugging

* Clock Domain Crossing (CDC) App
* Creating a Clock Definition
* Deprecated RPT_NO_STBL, WPT_NO_STBL, RPT_OP_GRAY, and WPT_OP_GRAY Violations
* CDC Now Automatically Detects Multi-Bit Schemes
* Editing SDC Files from the Source Line in the Signal Info Pane
* "check_cdc -init" Now Mandatory for CDC Flow
* New Violation Message Field in Violation Info Table
* Rating Multiple Ports Simultaneously from the GUI
* Violation Table Updates with New Switches and Associated Deprecations
* Renamed Tables in Schematic Viewer
* Violation Info Table Now Shows Disabled Synchronizers
* New RDC Check for Sync Reset Connected Asynchronously (RDC_RS_SYCA)
* Enhanced CDC Detection of Edge and MUX Synchronizers
* Updated Violation Info Details for RDC_RS_DFRS Violations
* Changes to RDC_RS_DFRS Detection
* New Show Parameters Dialog

* Connectivity Verification App
* "save" and "restore" Now Work with Connectivity
* Enhanced Width Mismatch Warning WCON001
* Updated Connectivity Examples in Doc Directory

* Coverage App
* COV Now Supports ProofMaster
* Viewing Details of Unknown/Unprocessed Properties After Measure
* Setting Artificial Bounds for Bound Analysis Independent of FPV
* Coverage Now Shows Proof Structure Nodes in Task Dialog
* Reusing Proof Results in Coverage App

* Coverage Unreachability (UNR) App
* Added "-covscope" and "-covworkdir" Switches to "check_unr -init"
* UNR Now Supports ProofMaster

* Low Power Verification (LPV) App
* UPF "-is_analog" Attribute Now Supported
* LPV Now Supports "query_supply_port"

* Security Path Verification (SPV) App
* Creating Precondition Covers for SPV Cover Properties
* Visualize Now Enabled for SPV and X-Prop Properties with No Trace
* SPV Now Supports "visualize -replot"
* Disabled Warnings WSPV025, WSPV026, and WSPV027
* SPV GUI Now Supports Multiple Properties for Proof Strategy
* Differentiating Between COI Analysis and Pre-Processing
* Enhanced "check_spv -list -properties"
* Enhanced SPV Initialization
* "check_spv -prove -property" Now Supports Regular Expressions
* "check_spv -create" Now Supports Wildcards
* Instances and Wildcards as Arguments to "-through" and "-not_through"
* "check_spv -create" Now Supports Wildcards

* Sequential Equivalence Checking (SEC) App
* SEC Now Supports Restoring Elaborated Designs
* Restoring an Elaborated Design to SEC Spec, Imp, or Both
* Parent Assertion Now Marked Proven if Any Related Cover is Unreachable

* Superlint App
* New Superlint Rules Files
* Enhanced CND_NR_COMM
* New Superlint Checks
* Reporting Missing Case Items for CAS_NR_DEFN Violations
* IDN_NR_ALCA Now Skips Function Ports by Default

* X-Propagation (XPROP) Verification App
* X-Prop Now Synthesizes $isunknown Properties by Default
* Prove Options in X-Prop Context Menus Now Issue "check_xprop -prove"
* X-Prop Re-Architecture
* X-Prop Does Not Support Trace Extension

* Visualize
* Plotting All Bits of Enum on Why Result
* Improve Messaging for QuietTrace
* Improved Messaging for Debugging Cell Defines

* Clocks and Reset
* Enhanced Messaging for Formal Reset Sequence

* Combinational loop
* Enhanced Glitch Debugging

* Deep Bug Hunting
* Additional Engine Support for Cycle and Bound Swarm Modes

* Design Compilation
* Related Assertions for Safety Component in Liveness
* Spurious VERI-1208 Warnings No Longer Issued for Unsized Literals

* Design Exploration
* Enhanced "-list interface*" Options for Instance and Module Scopes
* Now Showing Inline Annotation for Outermost Instead of Slicing Signal
* Visualize Now Automatically Shows the Why Result for All Traces
* Macros Automatically Expanded in Superlint Violations

* Design Exploration and Verification Management
* Enhanced Options for "get_property_info -list"

* Language Support
* Previewing Witness Properties
* Jasper Now Evaluates the Condition Expression to 1'bx

* Miscellaneous
* Updated Jasper Functional Safety Verification (FSV) App User Guide
* Proof Structure Hard Case Split
* "cte.log" Path on ISCD001 Now a Link
* Enhanced SDC Reporting

* Proofs and ProofGrid
* You Can Now Run Formal Profiler on Multiple Properties in Parallel
* Jasper Now Saves and Restores Proof Structure Operations
* Bound Aggregation in ProofGrid

* User Interface
* Traces Column of the FPV Property Table Now Beside Bound Column

* Verification Management
* "get_needed_assumptions" Now Reports Property Name
* Compressing Databases During "save"
* New "related_property_type" Attribute for "get_property_list"

* vManager Integration
* Elaborated Design Now Used to Save and Open Traces
* SPV Assertions Now Supported in vManager

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
––––––––––––––––––––-
* C Structs Now Accepted as Inputs for C2RTL

The C2RTL flow now supports structs as interfaces of the formal model.
Given a struct expression "expr", you can declare x as either an input or
output of the formal model using the existing macros JASPER_INPUT_LVAL and
JASPER_OUTPUT_RVAL. For example:

JASPER_INPUT_LVAL(expr, myname);
JASPER_OUTPUT_RVAL(expr , myname)

If "expr" is a variable and also the desired name of the interface signal
in the formal model, you can write the following:

JASPER_INPUT(expr);
JASPER_OUTPUT(expr);

* C/C++ Call Stack Now Visible by Default in C2RTL Source Browser

Jasper C2RTL now shows the C/C++ function call stack tree in the Spec
and Imp design source browser.

* C/C++ Compilation Warnings Now Printed to Console

C/C++ compilation warnings are now printed in the Jasper console along
with errors.

* Automatically Constraining Enum Type Inputs

The release includes a new switch "-create_valid_enum_value_input_constraints"
for the "check_c2rtl -compile" command. With this command, for each enum
variable declared using JASPER_INPUT(SIGNAL_NAME), the tool generates an
assumption for which the input can be only one of the declared enum values.
The assumption name is in the form
"<constraints>/_type_constraint_SIGNAL_NAME".

An additional new command "check_c2rtl -set_dynamic_pruning
-use_valid_enum_value_input_constraints", when set to "true", ensures
dynamic path pruning considers only the valid enum values for inputs declared
using JASPER_INPUT, while pruning the C++ model. Thus, when this configuration
is "true", you cannot disable the assumptions described above.

* Warning Now Issued for Termination Due to Insufficient Unwind Limit

If formal model generation finds a deterministic loop for which the unrolling
bound is too low, it issues a warning that the formal model is probably
incomplete.

* JASPER_ASSUME Now Works as Expected for .c Files

You can now use JASPER_ASSUME and JASPER_ASSERT on .c files in addition
to .cpp files.

* Multi-Context Debugging

Prior to this release, C2RTL supported a single debugging context only in
Visualize. However, debugging through C++ and RTL models is usually done at
different cycles. With this release, C2RTL now supports multi-context
debugging in Visualize by default. After a Why, Driver, or Load operation,
Visualize automatically creates two independent markers for the spec and imp
contexts and updates these for every subsequent debugging operation.

* InsufficientUnwindLimit Safety Assertion Renamed to InsufficientUnrollLimit

With the 2022.12 FCS release, unwind switches were renamed to unroll. This
release changes the name of the "InsufficientUnwindLimit" property to
"InsufficientUnrollLimit".

* Improved Messaging for Synthesis Errors

ECTR057 has been deprecated and replaced with ECTR034:

ECTR034: Synthesis errors that might indicate a tool bug have been found.
Contact support@cadence.com.

Clock Domain Crossing (CDC) App
–––––––––––––––-
* Deprecated RPT_NO_STBL, WPT_NO_STBL, RPT_OP_GRAY, and WPT_OP_GRAY Violations

CDC no longer reports RPT_NO_STBL, WPT_NO_STBL, RPT_OP_GRAY, or WPT_OP_GRAY
violations.

* Creating a Clock Definition

You can now use the following command to create a CDC clock definition
that drives the specified signals:

config_rtlds -clock -create {target_signal_list}
[-name clock_name] [-factor N] [-add]

NOTE:
. Clocks defined with this command are available for formal use only
after running the CDC command "check_cdc -clock_domain -find".
. See the full help for additional details (help config_rtlds -gui).

* Renamed Tables in Schematic Viewer

The "CDC Violation Info" and "CDC Signal Info" tables in the CDC Schematic
Viewer GUI were renamed to "Violation Info" and "Signal Info", respectively.

* CDC Now Automatically Detects Multi-Bit Schemes

CDC now automatically detects multi-bit schemes of type Pulse and Edge.

* Enhanced CDC Detection of Edge and MUX Synchronizers

CDC now automatically detects MUX_NDFF schemes that are controlled by a
single bit of an NDFF_BUS scheme. It also detects MUX_PULSE schemes that are
controlled by a single-bit Edge scheme or by a bit of a multi-bit Edge or
Pulse scheme.

* "check_cdc -init" Now Mandatory for CDC Flow

The "check_cdc" command now issues an error if "check_cdc -init" has not yet
been issued. Also, all "config_rtlds" commands require that CDC or Superlint
has already been initialized.

NOTE:
. CDC can be initialized only if "check_superlint -init" has not already
been issued.
. The "check_cdc -init" or "check_superlint -init" commands are automatically
issued if you launch Jasper with the "-cdc" or "-superlint" command-line
switches.

* Rating Multiple Ports Simultaneously from the GUI

You can now simultaneously select multiple rows of the CDC Port
Configuration table (Ctrl or Shift + Click), and then right-click the
selection to open the "Set signal clock" dialog and set the clock for the
selected ports. Also with this change, the "Set signal clock" dialog is now
wider and shows all the selected ports in the "Signal Name(s)" field.

* Violation Info Table Now Shows Disabled Synchronizers

A new "Disabled Auto Detection" row was added to the "Violation Info" table
in the CDC Schematic Viewer GUI for no_scheme (CDC_NO_SYNC) violations. This
new field contains a list of all the CDC synchronizer types for which
automatic detection is disabled (either by default or by the user).

* New Violation Message Field in Violation Info Table

The "Violation Info" table of the CDC Schematic Viewer now includes a new
"Violation Message" field. This new field contains the same violation message
that is currently displayed in the "Review Violations" pane of the CDC main
window.

* Editing SDC Files from the Source Line in the Signal Info Pane

The file name and line number in the Clock Source Location row of the
Schematic Viewer's Signal Info pane is now a hyperlink. Clicking on this
link opens the file in an editor pointing to the line number.

* Violation Table Updates with New Switches and Associated Deprecations

The following CDC violation fields were renamed as follows in the GUI, in
the output of the "check_cdc -list" command, and in the reports generated
with "check_cdc -report":

. Source Reset -> Local Source Reset
. Destination Reset -> Local Destination Reset
. Reset Sources -> Reset Domain
. Source Declared Resets -> Source Reset Domain
. Destination Declared Resets -> Destination Reset Domain
. Source Domain -> Source Clock Domain
. Destination Domain -> Destination Clock Domain

The corresponding switches in the "check_cdc -filter -add" command were also
renamed. See the full help for additional details (help check_cdc -gui).

NOTE: The old switches have been deprecated but are maintained for
backward compatibility. These will be removed in a future release.

* Updated Violation Info Details for RDC_RS_DFRS Violations

Now, the "Reset Sources" field is replaced with "Source Unit" for RDC_RS_DFRS
violations.

* Changes to RDC_RS_DFRS Detection

RDC_RS_DFRS pair detection now takes reset rating of top ports, blackbox
ports, and flops into consideration. It also uses the information available
in the hierarchical database if the above information is not available. This
violation now detects RDC pairs whose connection passes through one or more
hierarchical blackbox internal combinational connections.

The RDC_RS_DFRS violation now compares source and destination root resets
instead of reset sources. Different reset polarity between the source and the
destination of the RDC pair is no longer a sufficient condition to lead to a
different RDC_RS_RFRS violation. Also, as before, RDC pairs with destination
units with no reset conditions are ignored if "ignore_non_resettable_flop" is
"true".

Assuming "ignore_rdc_from_same_reset_source" is "true", an RDC pair does not
lead to a different reset violation when each synchronized or async reset in
the source side of the pair has at least one equivalent synchronized or async
reset in the destination side that ensures that, whenever the source flop is
in reset state, the destination side is also in reset state.

Assuming "ignore_rdc_from_same_reset_source" is "false", an RDC pair does not
lead to a different reset violation when there is a path between the
asynchronous reset pin of the source flop and the asynchronous reset pin of
the destination flop, and this path is composed of buffers and wires only.
Thus, the signals reaching the asynchronous reset pins are either equal or
inverse.

* New RDC Check for Sync Reset Connected Asynchronously (RDC_RS_SYCA)

CDC reports the new RDC_RS_SYCA RDC violation for RDC pairs where the source
unit has at least one fully sync reset connected asynchronously, which is not
connected asynchronously to the destination unit. The referred fully sync
resets can be declared using the "config_rtlds -reset -sync" command, be
synchronized by a direct reset scheme, or be a data signal that is synchronous
to the RDC pair.

The reference resets used for comparisons are as follows:
. Flop units: The signals connected to the asynchronous reset condition pins.
. Port units: The "config_rtlds" reset ratings.
. Unrated blackbox ports: The reset sequential abstract arcs from the
hierarchical flow, if available.

* New Show Parameters Dialog

This release adds a new "Show Parameters" option to the Preview Violations
context menu (right-click). When you choose this option, the tool opens a
dialog showing the list of parameters and their values that influence the
selected domain or tag.

NOTE: Some of the domain-level parameters might not affect all tags under
that domain.

Connectivity Verification App
––––––––––––––-
* "save" and "restore" Now Work with Connectivity

You can now save and restore loaded connection maps, COI check information,
toggle check results, and proof status with the Jasper "save" and "restore"
commands. The flow is as follows:

// In the current session, issue the following command:
% save -jdb my_session.jdb -capture_setup -capture_session_data
// Close the session and start a new session:
% jg -conn
// Restore the saved session:
% restore -jdb my_session.jdb

NOTE: See Appendix B in the Connectivity App user guide for additional
information.

* Updated Connectivity Examples in Doc Directory

The Connectivity examples in the doc directory have been updated to use
"clock -none" and "reset -none".

* Enhanced Width Mismatch Warning WCON001

Warning WCON001 has been enhanced to include the width of each signal and to
specify the signal used in the analysis. The message now reads as follows:

WCON001: Size mismatch in signals "%s" and "%s" from connection "%s".
Source width is %d, but destination width is %d. Width %d will be
considered for analysis."

Coverage App
––––––
* COV Now Supports ProofMaster

"check_cov -measure" now supports ProofMaster.

NOTE: The COV App does not support proof cache when running checker coverage.

* Viewing Details of Unknown/Unprocessed Properties After Measure

Now, when running bound analysis, you can click on unknown/unprocessed
results to view the bounded coverage details in the Assert Analysis tab.
Previously, the tool did not permit this action.

* Setting Artificial Bounds for Bound Analysis Independent of FPV

You can now use the following command to artificially set a bound to
an assertion and then run "check_cov -measure -type {bound}" to analyze the
results from the Assert Analysis tab:

check_cov -assert_analysis -assert <name> (-set_bound <value> |-clear_bound)

Also with this change, the Coverage Assert Analysis "Assert Bound" column
indicates when a bound is "(Artificial)".

NOTE:
. This artificial bound does not alter proof results. If you subsequently run
a "prove", the tool overwrites the artificial bounds you had previously set.
. This command does not work for proven assertions or counterexamples.
. One command must be issued per assertion.

* Reusing Proof Results in Coverage App

Previously, attempting to restore FPV proof results with "restore -jdb"
cleared the Coverage database. Now, the restoration works as expected, so you
can reuse FPV proof results for both Coverage proof and assertion analysis.

* Coverage Now Shows Proof Structure Nodes in Task Dialog

Warning WCOV103 is now issued if you use a Proof Structure node as a task in
"check_cov -measure -task". These nodes are handled as any other task and
merged results are not guaranteed to be safe and sound.

Coverage Unreachability (UNR) App
––––––––––––––––-
* Added "-covscope" and "-covworkdir" Switches to "check_unr -init"

With this release, you can use the following switches with "check_unr -init":

. -covscope: Specifies the scope directory name for the UNR database.
. -covworkdir: Specifies the working directory name for the UNR database.

* UNR Now Supports ProofMaster

"check_unr -prove" now supports ProofMaster. Use "set_proofmaster on" to
enable ProofMaster for UNR.

Low Power Verification (LPV) App
––––––––––––––––
* UPF "-is_analog" Attribute Now Supported

The UPF command "set_port_attributes" now supports the "-is_analog" switch
in UPF3.1 and the "is_analog (true | false)" attribute in UPF2.1.

* LPV Now Supports "query_supply_port"

LPV now supports the "query_suppy_port" UPF command. This command
lists created supply ports or shows information about specific
supply ports.

Security Path Verification (SPV) App
––––––––––––––––––
* Enhanced "check_spv -list -properties"

"check_spv -list -properties" now displays the following additional
details:

. no precondition covers
. include/exclude control paths
. driving logic
. feedback loops
. precise rating

* Differentiating Between COI Analysis and Pre-Processing

SPV properties that are proven structurally because the "from" signals are not
in the COI of the "to" signals will now show "COI" in the Strategy column and
"PRE in the Engine column in the GUI. Previously, these proofs showed an empty
Strategy column and "PRE" for the Engine, making them indistinguishable from
properties proven during later engine pre-processing.

* Enhanced SPV Initialization

All disabled properties are now hidden from the SPV Property table on
initialization.

* Disabled Warnings WSPV025, WSPV026, and WSPV027

Warnings WSPV025, WSPV026, and WSPV027, which are relevant only when
transitioning from the old SPV flow, are no longer printed by default.

* SPV Now Supports "visualize -replot"

You can now use "visualize -replot" on windows that were generated by SPV.

* Creating Precondition Covers for SPV Cover Properties

You can now create related precondition covers for SPV cover properties as
well as SPV assertions. These include from precondition, to precondition, and
combined precondition properties.

* Visualize Now Enabled for SPV and X-Prop Properties with No Trace

As with FPV, Visualize now runs a proof on the property and shows the found
trace or informs you that no trace exists.

* "check_spv -create" Now Supports Wildcards

The "-from" and "-to" switches of the "check_spv -create" command now support
wildcards.

* "check_spv -prove -property" Now Supports Regular Expressions

"check_spv -prove -property" now supports regular expressions with the
"-regexp" switch. Previously, only wildcards were supported.

* SPV GUI Now Supports Multiple Properties for Proof Strategy

You can now use the SPV Viewer Properties Table context-menu option "Prove
Property Proof Strategy" to prove any number of provable properties. This
option issues the "check_spv -prove -property <property_name_tcl_list>
-strategy -proof" command, which might fail if the properties do not have
the same signature or propagation environment.

* Instances and Wildcards as Arguments to "-through" and "-not_through"

You can now pass instances and wildcards as arguments to "check_spv
-create… -through" and "check_spv -create… -not_through".

* "check_spv -create" Now Supports Wildcards

The "-from" and "-to" switches of the "check_spv -create" command now support
wildcards.

Sequential Equivalence Checking (SEC) App
––––––––––––––––––––-
* SEC Now Supports Restoring Elaborated Designs

You can now restore a design elaborated with SEC and saved with the "save
-elaborated_design" command before issuing "check_sec -setup". Previously,
this required that you have a .jdb file.

* Parent Assertion Now Marked Proven if Any Related Cover is Unreachable

SEC properties are now marked proven if any of their related covers are
unreachable.

* Restoring an Elaborated Design to SEC Spec, Imp, or Both

This capability applies to designs that have been elaborated with any of the
following SEC commands:

. "check_sec -elaborate"
. "elaborate" after running "check_sec -compile_context (spec | imp | both)"
. "check_sec -setup -elaborate_opts …" (joint setup)
. "elaborate" after running "set_sec_elaborate_mode on"
NOTE: The new "set_sec_elaborate_mode on" command specifies that an
elaboration include configuration and modeling specific to SEC.

To restore the elaborated design for a specified side, first run "check_sec
-compile_context (spec | imp | both)". Then run "restore -elaborated_design
<dir_or_file>", which restores the design to the specified side.

NOTE If the directory contains more than one file, you must provide the path
of the file instead of the directory.

* New Configuration Command Enables SEC Elaboration Mode

You can now use the following configuration command to specify that
an elaboration include configuration and modeling specific to SEC:

set_sec_elaborate_mode (on | off)
. on: Run "elaborate" with SEC configurations and modeling. The elaborated
design is identical to that generated by "check_sec -elaborate".
. off: Do not run "elaborate" with SEC configurations and modeling. This is
the default.

Superlint App
––––––-
* New Superlint Rules Files

This release includes four new Superlint rules files as follows:

. superlint_core.def: Reduced set of LINT/DFT checks for initial deployment.
NOTE:
. Use "include superlint_core" to include the new core rules file in a
custom rules file.
. Beginning with this release, the following command in any Tcl scripts
will execute fewer checks: config_rtlds -rule -enable -domain {LINT DFT}
. superlint_D0254.def: Checks RTL for compliance with D0254 coding guidelines.
NOTE: Compliance with DO254 ruleset does not ensure certification.
. superlint_VHDL.def: Applicable to VHDL only.
. superlint_Verilog_SystemVerilog.def: Applicable to Verilog and SystemVerilog
only.

All new rules files are a subset of the rules available in "superlint.def",
which remains the default, and all can be found at the following location:
<install>/etc/res/rtlds/rules/.

* IDN_NR_ALCA Now Skips Function Ports by Default

The following parameter is added to IDN_NR_ALCA, which now avoids violations
on function ports by default:

params IDN_NF_ALCA {skip_function_ports=yes}

Set this parameter to "no" if you prefer Superlint report this violation on
function ports as well.

* Enhanced CND_NR_COMM

CND_NR_COMM now checks expression for logical AND operator only.

* Reporting Missing Case Items for CAS_NR_DEFN Violations

You can now set the following new parameter to report the missing items in
CAS_NR_DEFN violations:

params CAS_NR_DEFN {verbose_report_all_missing_case_items="yes"|"no"}

To report missing items, set this parameter to "yes". "no" if the default.

* New Superlint Checks

This release includes the following new checks:

. CODINGSTYLE
. INS_NR_DRCT (Warning): "In design-unit '%s', instantiation '%s' of the
VHDL entity '%s' is done directly without component declaration"
. MOD_NR_DSSL (Warning): "Design-unit '%s' contains declaration and
statement '%s' in a single line"

. STRUCTURAL
. SIG_IS_INIT (Error): "%s '%s' in the design unit '%s' is not initialized
to a uniquely determined value"

X-Propagation (XPROP) Verification App
–––––––––––––––––––
* Prove Options in X-Prop Context Menus Now Issue "check_xprop -prove"

The "Prove Property" and "Prove Task" context-menu options of the X-Prop task
task and property tables now issue a "check_xprop -prove" command instead of
the platform "prove" command.

* X-Prop Now Synthesizes $isunknown Properties by Default

The X-Prop App now always synthesizes $isunknown properties.

* X-Prop Re-Architecture

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

Beginning with this release, the X-Prop App must be initialized with
the new "check_xprop -init" command. You must call this command before
any other X-Prop-related command and before the "analyze" and
"elaborate" commands.

NOTE: When you launch Jasper with the "-xprop" command-line switch, the
X-Prop App is automatically initialized with "check_xprop -init" command.

Also with this change, you can now use a "basic" or "proof" strategy to prove
X-Prop properties:

. check-xprop -prove -strategy basic: Run the proof in a single-threaded
proof environment. This is the default.
. check_xprop -prove -strategy proof: Run the proof in a sophisticated,
multi-threaded, and collaborating proof environment.

See the X-Prop Tech Update slides for additional information about associated
command changes and limitations.

* X-Prop Does Not Support Trace Extension

X-Prop does not support trace extension. If you attempt a proof run with
a "trace_extension" value other that 0, the tool issues an error and asks you
to set "trace_extension" to 0.

Visualize
––––-
* Plotting All Bits of Enum on Why Result

Added new option "Plot all bits of Why result" in "Preferences - Visualize -
Plot", which can be set using the GUI or the "set_preference
{Visualize/PlotAllBitsOfWhyResult} true" command.

If this option is true, Visualize plots all bits of "Why" results signals to
the primary waveform when you choose the "Adding Why Signals" context menu
option or to the "Preview Why Results" waveform when performing the "Why"
operations in the Source Browser and in the primary waveform.

* Improve Messaging for QuietTrace

QuietTrace now issues a more informative message when it stops mid job:

EVS177: QuietTrace stopped with {remaining} remaining soft constraints.
Satisfied: {satisfied}. Not Satisfied: {failed}.
Proof has timed out, exceeded memory limit, or found another issue.

* Improved Messaging for Debugging Cell Defines

The tool now issues the following warning when the trace driver is on a
boundary with a cell define and visibility is "off":

WNL089: The driver trace will not go into cell defines. If you need to debug
cell defines, use "set_cell_define_debug_visibility on".

Clocks and Reset
––––––––
* Enhanced Messaging for Formal Reset Sequence

Formal reset sequence now issues the error below when you use an incorrect
bound:

ERS065: The argument to "start_formal_bound" must be an integer between 0
and the sequence's total number of cycles.

Combinational loop
–––––––––
* Enhanced Glitch Debugging

If there is a :noGlitch counterexample detected by "check_loop -formal glitch",
the "check_loop -formal -show_schematic" command displays the ":noGlitch Loop
Viewer", which is a special Schematic Viewer that displays customized colors
and annotations as follows to help with glitch debugging:

. white : Glitch gate source and the flop that contains a glitch
. red : Glitch propagation path
. green : Asynchronous variables impacted by the glitch
. symbol: High/low glitch and late posedge/negedge

Deep Bug Hunting
––––––––
* Additional Engine Support for Cycle and Bound Swarm Modes

Now, the "hunt -config -strategy" command "bound_swarm" and "cycle_swarm"
modes support engines Ht and Hts.

Design Compilation
–––––––––
* Spurious VERI-1208 Warnings No Longer Issued for Unsized Literals

Unsized decimal-based numbers larger than 64-bits (for example,
'd34359738368) are no longer truncated to 32 bits.

* Related Assertions for Safety Component in Liveness

By default, the tool now automatically creates related assertions on mixed
liveness properties. These related assertions are the pure safety part of the
mixed liveness. The related assertions behave as related covers, and an
exclamation mark in added to the main property if a CEX is found.

Design Exploration
–––––––––
* Enhanced "-list interface*" Options for Instance and Module Scopes

The "-list interface", "-list interface_instance", "-list interface_port", and
"-list interface_no_param" options of the "get_design_info -instance" and
"get_design_info -module" commands no longer return information transitively.
By default, these commands now return information for the queried hierarchy
level only.

NOTE: With this change, these commands now include an optional
"-transitive" switch for backward compatibility.

* Now Showing Inline Annotation for Outermost Instead of Slicing Signal

In the Visualize Source Browser, array slices are now annotated inline with
the value of the outermost signal instead of the slicing signal.

* Visualize Now Automatically Shows the Why Result for All Traces

Visualize now automatically shows the Why result when opening any type of
trace, including cover and liveness targets. Thus, the Visualize Plot
Preferences option "Show the Why result automatically when opening a CEX
trace" has been modified to read "Show the Why result automatically when
opening a trace".

NOTE: The Preference key "Visualize/ShowWhyOnCEXAutomatically" was not
changed.

* Macros Automatically Expanded in Superlint Violations

Now, when you click on a violation in the Superlint "Automatic Formal
Properties" table and the source location of the violation is inside
a macro, the macro is automatically expanded, and the star icon is
moved to the violation line inside the expansion.

Design Exploration and Verification Management
–––––––––––––––––––––––
* Enhanced Options for "get_property_info -list"

You can now use the following new options with "get_property_info -list":

. related_asserts: Lists any related assertions for the specified property.
. is_related_cover: Returns "1" if the property is a related cover;
otherwise, returns "0".
. is_related_assert: Returns "1" if the property is a related assertion;
otherwise, returns "0".
. related_property_type: Identifies the type of the related property:
. none
. precondition
. contrapositive
. witness
. precondition_infinite
. precondition_late
. infinite_contrapositive
. safety_in_liveness_assert

NOTE: The "precondition" attribute will be deprecated in a future release.

Language Support
––––––––
* Previewing Witness Properties

The property detail pane now shows the expression of witness properties by
default. If the tool is unable to regenerate the expression, it continues
to show the line-file of the main property in the property detail pane.

* Jasper Now Evaluates the Condition Expression to 1'bx

Now, Jasper respects the SystemVerilog LRM when dealing with constant Xs in
the condition for single-bit logic AND/OR evaluation. According to the LRM,
the condition expression should be evaluated to 1'bx.

* Improved Actual versus Formal Type Checks

Jasper has improved the checks for actual versus formal type during module
and interface instantiation. Due to this improvement, new VERI-1370 errors
might be issued if there is a type mismatch between formal and actual.

Miscellaneous
––––––-
* Updated Jasper Functional Safety Verification (FSV) App User Guide

You can now consult the new section about saving and restoring FSV designs and
session data in the Jasper FSV App User Guide.

* Proof Structure Hard Case Split

Previously, the Proof Structure case split operation worked by adding
preconditions, but sometimes, the complexity is much better if you add
assumptions instead. With this release, the new hard case split operation is
introduced. This operation implements the case split using assumptions instead
of preconditions, and adds a "-validity" switch, which checks that the proof
is safe to propagate. If the validity node fails, local proofs do not
propagate upward. However, individual case nodes can always propagate a
counterexample or cover.

NOTE: See the full help for additional details (help proof_structure -gui).

* "cte.log" Path on ISCD001 Now a Link

ISCD001 now includes a hyperlink to the "cte.log" file. Clicking on the
hyperlink opens the "cte.log" in a text editor.

* Enhanced SDC Reporting

Now, unsupported SDC commands are reported under a new "Ignored" category
in the command execution summary report, and the tool issues warning WSDC008.
Also with this release, the SDC command execution log (cte.log) is a link in
the message that can be opened directly from the console.

Proofs and ProofGrid
––––––––––
* You Can Now Run Formal Profiler on Multiple Properties in Parallel

Formal Profiler now supports multiple parallel runs. Run the
"formal_profiler -property" command repeatedly to trigger each new run.
The new "-stop" switch now optionally accepts a run name as argument,
but if no name is provided, this command stops the last run by default.

With this change, the Formal Profiler GUI now has a dropdown menu that
enables choosing from all available runs, that is, the current, ongoing
runs as well as past, completed runs.

* Jasper Now Saves and Restores Proof Structure Operations

The command "save -jdb database -capture_session_data" now captures
the data from all Proof Structure operations. The Proof Structure
tree is restored between sessions with the command "restore -jdb database".

LIMITATION: Saving and restoring Proof Structure is not supported with C2RTL.

* Bound Aggregation in ProofGrid

Each property has a "min_length" attribute, measured in cycles, that indicates
the earliest cycle where a trace might exist (for example, bounded proof depth
= min_length-1). When running hunt "cycle_swarm" or "bound_swarm" modes, or
proofs that use engines with elastic BMC configurations, individual cycles can
become fully analyzed. "min_length" calculations now automatically account
for contributions made by elastic BMC-based engines running in the same proof
thread.

User Interface
–––––––
* Traces Column of the FPV Property Table Now Beside Bound Column

The "Traces" column of the FPV Property Table is now located to the right of
the "Bound" column to improve its visibility.

Verification Management
–––––––––––-
* "get_needed_assumptions" Now Reports Property Name

Now, the "get_needed_assumptions" summary result prints the property on which
the analysis is performed.

Also with this release, you will see changes to the indentation of the
summary results.

* Compressing Databases During "save"

You can now use the new "set_save_compress_database" configuration to specify
whether a session must automatically run Gzip to compress the generated files
when saving databases. The syntax follows:

set_save_compress_database (on | off)
. on: Use Gzip to compress the databases.
. off: Does not use Gzip to compress databases. This is the default.

NOTE:
. This command is supported by "save -elaborated_design" and "save -jdb"
only, and does not affect "save -dir" or "save -script".
. Gzip cannot reduce file size when compressing a file that is encrypted
or has already been compressed.

* New "related_property_type" Attribute for "get_property_list"

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

This release adds the new attribute {related_property_type <type_list>} to the
"get_property_list (–include |-exclude)" command. This includes or excludes
the specified related property types:

. none
. precondition
. contrapositive
. witness
. precondition_infinite
. infinite_contrapositive
. safety_in_liveness_assert
. precondition_late

Also with this release, the new Boolean attributes "is_related_assert",
and "is_related_cover" return a list of all related assertions (safety_
in_liveness_assert), and all related covers, respectively.

vManager Integration
––––––––––
* SPV Assertions Now Supported in vManager

SPV assertions and covers are now exported for vManager signoff when you use
the following command-line options:

jg run.tcl -cov_init "-coverage u -covoverwrite [-task spv] -write_metrics -witness_resolution any_unr"

* Elaborated Design Now Used to Save and Open Traces

Previously, saving and opening traces from Jasper runs on Verisium Manager
required rerunning all steps, including "analyze" and "elaborate", for each
trace. Now, Jasper-Verisium Manager integration uses the elaborated design
instead. Each test saves one elaborated design database; thus, waveforms
reopen faster.


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

Clock Domain Crossing (CDC) App
–––––––––––––––-
* CDC Phases Pairs Table Filtering Again Working as Expected

You are once again able to see only the pairs associated with a selected CDC
crossing from the CDC Phases Pairs table. This functionality stopped working
with the 2022.12 release, but this release resolves the issue.

* Metastability No Longer Injected when a Synchronous Signal Toggles

You no longer see metastability effects being injected in simulation for
synchronous changes in input signals when the duration of the change is
smaller than the time window considered.

* Resolved Issue with Missing Default Clock Declaration

Assertions for constant signal constraints exported with "check_cdc -export
-type signal_config_property" now contain a sensitivity list with the fastest
clock available in the design.

For example:

//before
assert property (signal == 1'b0);
//after
assert property (@(posedge _clock) signal == 1'b0);

Connectivity Verification App
––––––––––––––-
* Macro Now Recognized as Expected in Source Block of Connection

Connectivity now processes macros on the source and destination block fields
of CSV files.

* Improved Blackbox Assistant Handling of Implicit Port Mapping Elements

Blackbox Assistant can now handle implicit port mapping elements (dot-star)
combined with port name mapping.

* Improved Error Messaging

Connectivity now correctly raises EWB045 or EWB04 when a signal does not
exist on the connection block but exists with the same name on the top module.

* Considering Clock Edge in PIPE Calculation

Reverse Connectivity now considers clock edge in PIPE calculation.

* Resolved Issue with Unexpected Connections

When running Reverse Connectivity, if you use the "-src" switch and the
instance has no output ports or you use the "-dest" switch and the instance
has no input ports, the Connectivity App stops and returns no connections.
Previously, the tool behaved as if the "-src" or "-dest" switches were not
passed to the command.

* Resolved Issue with EWB058 Error

Reverse Connectivity no longer issues EWB058 when the generated CSV file
includes function signals.

Connectivity Verification App and Coverage App
–––––––––––––––––––––––
* Resolved Issue with Undetectable COI

Intermediate wires of connections being checked by Connectivity are now,
once again, correctly reported as "Checked" by Coverage. This functionality
stopped working as expected with the 2022.12 release, but this release
resolves the issue.

Coverage App
––––––
* Resolved Issue with Proof Core when Property Proven with Engine PRE

Standard precision proof core now returns results with as much as or more
over approximation as high precision proof core.

* Resolved Issue with "Refresh Coverage Measurement" Button

Clicking the "Refresh Coverage Measurement" button in the COV GUI no longer
issues an invalid command to the console. Instead, this button issues
"check_cov -measure -refresh", which refreshes all tasks as expected.

* Disabled Assertions No Longer Spuriously Proven

Disabled properties copied among tasks are no longer spuriously proven by
Coverage Proof Core measurement in high precision mode.

* Resolved Issue with Unexpected ENL108 Error

With this release, Coverage completes the elaboration as expected when
macros are used.

* Flops Now Unchecked Only if Register Outputs Not in Proof Core

Beginning with this release, flops appear as unchecked only if their register
outputs are also not in proof core.

* Mutation Coverage Logs Now Show Percentage of Determined Cover Items

The mutation logs metric now prints the percentage of determined cover items
instead of the computing progress.

* Improved Show/Hide Columns Filter

Previously, in the Coverage App when you used the "Show/Hide Columns" filter
to show only relevant columns of the Expression and Toggle tables, the column
headers disappeared. This release resolves the issue.

* Detailed Report in GUI Now Shows Correct Coverage Percentage

The Detailed coverage model now shows correct results in the report summary
shown in the header of the table, which displays coverage percentage for
Formal, Stimuli, and Checker coverage.

* "check_cov -measure" No Longer Resets Coverage Results

Mutation results from a previous run are now reused as a starting point for
a later run.

* Resolved Issue with "check_cov -measure -refresh"

Prior to this release, the "-refresh" switch did computations, such as
traversals for COI, bound, and proof, when used with "check_cov -measure".
Now, "check_cov -measure -refresh" is interpreted as a "refresh after measure"
command that impacts only the GUI.

NOTE: The "-refresh" switch cannot be use with the "-type" switch.

* Coverage Now Supports Scoring of Expressions in Function Arguments

Coverage now scores VHDL expressions used inside function arguments.

Coverage Unreachability (UNR) App
––––––––––––––––-
* Resolved Issue with Incorrect UNR Marking

This release resolves an issue that might have previously led to incorrect
UNR marking for simple expressions.

* Resolved Spurious VHDL-1174 Error

This release resolves a spurious VHDL-1174 error found in VHDL component
instantiation with configuration.

Low Power Verification (LPV) App
––––––––––––––––
* LPV Now Correctly Handles "." as Current Scope in Top Module

LPV now correctly handles the use of dot (.) to represent the current scope
in the top module.

* Fixed Consistency of Retention Sub-Strategies Generated by LPV

Retention sub-strategies are now generated deterministically.

* Improved LPV "-signal -list" Command

"check_lpv -signal -list source_domain" and "check_lpv -signal -list
sink_domain" now return unique values and do not consider the domains that
include the supply nets.

* Now Displaying Low Power Corruption Annotation in Waveforms by Default

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

Low power corruption annotation in Visualize waveforms is now enabled by
default. Thus, corrupted signals have a red cross-hatch annotation for the
cycles where their related power domain is off.

Use the "set_lpv_enable_corrupt_annotation off" command to disable this
feature .

Security Path Verification (SPV) App
––––––––––––––––––
* "visualize -stopat" Blocked for X-Prop and SVA Traces

You can no longer use "visualize -stopat" on an X-Prop or SPV trace.

* "-no_preconditions" Switch Replaced with "-no_precondition_covers"

This release replaces the "-no_preconditions" switch of the "check_spv
-create" command with "-no_precondition_covers". The old "-no_preconditions"
switch has been maintained for backward compatibility but will be removed
in a future release.

Sequential Equivalence Checking (SEC) App
––––––––––––––––––––-
* Incremental Elaboration Automatically Disabled on Initialization

With this release, the following apps automatically disable
"incremental_elaborate_wrapper_mode" on initialization:

. SEC (Excluding hierarchical flow)
. SPV
. XPROP
. FSV

* Resolved Issue with Unexpected Exit after Incremental Elaboration

SEC, SPV, FSV, and SPV now automatically enable "elaborate_single_run_mode".
This setting cannot be changed for these apps.

* Imp Packages Now Displayed on Right Side as Expected

Jasper FSV, C2RTL, and SEC Apps now show packages and compilation units from
the imp side on the right side of the hierarchy and source browser windows.

Superlint App
––––––-
* ASG_IS_OVFL Now Supported for Assignment Statements

Superlint now supports ASG_IS_OVFL checks for continuous assignments.

* Improved MOD_NR_SYXZ Check

MOD_NR_SYXZ is now generated as expected when "skip_tristate_logic" is set to
"yes".

* Improved SHF_IS_ABSO Check

Shift operations that include constant RHS no longer generate all bits
are lost violations.

* Resolved Issue with PRT_NR_ORDR

Superlint now reports PRT_NR_ORDR violations as expected, though only one
violation is reported in the GUI. all connected violations are passed to an
extra data report.

* ESW023 No Longer Issued Unexpectedly

Previously, Superlint might have exited unexpectedly with ESW023 in the event
of a loop. This release resolves the issue.

* Improved FIL_NR_MLEN Check

Superlint no longer considers the size of macro expansions as part of the
physical line length.

* Resolved Violations Tree Refresh Issue

Previously, the error and warning count on the Superlint violations tree
might not have been updated after adding waivers. This release resolves the
issue.

* Resolved Issue with Spurious FNC_MS_MTYP/FNC_MS_AFPR Violations

Superlint no longer issues FNC_MS_MTYP or FNC_MS_AFPR violations if a
function is declared in class.

X-Propagation (XPROP) Verification App
–––––––––––––––––––
* Expert System No Longer Supports SPV or X-Prop

Beginning with this release, the Jasper Expert System does not support the
SPV or X-Prop Apps. Thus, running "check_spv -init" or "check_xprop -init"
automatically disables the Expert System.

This limitation will be removed in a future release.

Visualize
––––-
* Resolved Issue with Spurious ETR032 Errors

Jasper no longer issues spurious trace inconsistency errors (ETR032) when
clocked bounded assumptions are present. Previously, clocked bounded
assumptions triggered a pessimistic inconsistency check.

* Resolved Issue "visualize -trace_id"

The "visualize -trace_id" command now shows the following error when used
without the switch "-property":

ERROR (ESW011): The "-trace_id" switch is only allowed with "-property"."

The TclHelp for "visualize -trace_id" was updated to reflect more accurately
the tool behavior. This switch selects one trace to plot when a property has
multiple traces. You must combine it with "-property" to indicate which
property the ID is related to.

Auto Black Box
–––––––
* Blackbox Assistant Not Supported with CDC, COV, FSV, Superlint, SEC, UNR

Jasper does not currently support using Blackbox Assistant with CDC, COV,
FSV, SUPERLINT, SEC, or UNR.

Clocks and Reset
––––––––
* ESW064 Now Issued if "-none" Is Used with Reset Expression

When "reset -formal -none" is used with a reset expression, the tool now
issues ESW064.

Clocks and Reset and Engines
––––––––––––––
* Improved Messaging for Property Declaration

When a property is declared with @(edge <clock name>) or @(<clock name>)
and its clock is not declared as -both_edges, the tool now displays the
following downgradable error:

ECK062: Jasper detected a property that requires a different clock declaration
for clock <clock name>.
Consider changing the clocking of the property, or declare clock
<clock name> with both_edges.
Use "sanity_check" for more information about which clocks have an
inconsistent clock declaration.

NOTE: The fix addresses only properties with a simple clock without factors
declared with @(edge <clock name>) or @(<clock name>). It DOES NOT cover
property declarations with @(posedge clk or negedge clk) or flop declarations,
gated clock declarations, or slow clock declarations. These situations
still do not result in an error.

Deep Bug Hunting
––––––––
* Resolved Issue with Spurious EHT003 Errors

Previously, the tool might have generated an invalid set of first trace
attempts and issued an error if you defined invalid "max_first_trace_attempts"
with engine Bm for Cycle Swarm and Bound Swarm "hunt" strategies. This release
resolves the issue.

* Handling Property Names with Name Clashes and Escaped IDs

Now, Jasper correctly handles property names with escaped IDs when there are
name clashes with other properties or signals.

Design Compilation
–––––––––
* Signals No Longer Incorrectly Reported as Multiple-Driven

Jasper no longer incorrectly reports signals as multiple-driven.

* Issue with Default Clocking Clauses Resolved

The Jasper clock flow is now correctly resolved concerning default clocking
clauses together with SystemVerilog interfaces.

* "connect -bind" Now Returns Warning Instead of Exiting Unexpectedly

Jasper no longer exits unexpectedly when the "connect -bind" command binds
one bus of multidimensional array input port to the elaborated module
port bus. If the port cannot be connected, the tool now issues a message like
the following:

WARNING (WNL024): Connect: unable to connect port
"i_cpux_link0_rom_start_addr[0]"

* VERI-2669 Now Issued when "disable iff" Used as Property Operand

Jasper now issues the following error when a property instance with disable
iff clause is used as a property operand:

[ERROR (VERI-2669)] test.v(16): property instances with disable iff cannot be
used as operand of property expression

* Spurious ENL163 Errors No Longer Issued

This release resolves an unexpected elaboration error related to invalid
external references involving missing indexation, for example, "m1i.si.b",
where "m1i" is an external module instance and "si" is an array without
indexation.

* Resolved Issue with "elaborate -extract_case_assertions"

Now, when extracting case assertions (elaborate -extract_case_assertions),
unique and unique0 automatic properties follow section 12.5.3 of the
SystemVerilog LRM'17 and do not fail if more than one case item expression
matches the case expression in a single case item.

NOTE: Related Superlint properties have also been impacted by this change.

* Resolved Issue with Property Hash Mismatch

This release resolves an issue with non-determinism in property hash when
running a design with hierarchical references in different sessions.

* Resolved Elaboration Run Time Degradation Introduced in 2022.09

Fixed elaboration performance degradation that might have affected modules
with many unresolved references.

Design Compilation and Infrastructure
––––––––––––––––––-
* WOBS004 Now Upgradeable

You can now upgrade WOBS004 to an error with the following command:

set_message -error WOBS004

To revert, use "set_message -warning WOBS004".

Design Compilation and Language Support
–––––––––––––––––––-
* Resolved Unexpected Exit During Elaboration

The related cover preview flow no longer exits unexpectedly when a functional
with only internal signals has a loop in itself, for example,
$past(function_call(sig)).

Design Exploration
–––––––––
* "show_source_browser -signal" Now Accepts Packed Structs

Now, "show_source_browser -signal" accepts packed struct signals as argument.

Infrastructure
–––––––
* Resolved Issue with "export -to_sva"

"export -to_sva" now correctly exports the reset expression when there is an
"assume -bound".

Infrastructure and Proofs and ProofGrid
–––––––––––––––––––-
* Jasper No Longer Exits Unexpectedly on Long Directory Path Name

Jasper no longer exits unexpectedly when the path to the "trace database"
file is too long. However, the solution to avert this issue comes at the
cost of traces not being "converted", which means that affected properties
do not have any traces, though their statuses are updated properly. When a
problematic situation has been detected during a proof, Jasper issues error
message ETR087 for every failure to "convert" a trace. For example,

ERROR (ETR087): Unable to convert trace for "counter == 'hF0".
Details: database connection failure: unable to open database file

NOTE:
. By default, the "trace database" file is located in the project directory.
. What the tool determines to be too long is dependent on the system and can
even be different for different paths on the same system since it might
depend on the file system type.

Language Support
––––––––
* Resolved Issue with Unexpected Precondition Expression

This release resolves an issue with the synthesis of precondition expressions
with the following pattern:

@(posedge clk) disable iff (rst) expr1 ##1 1'b1 |-> expr2

Before this change, Jasper created a precondition like the following:

@(posedge clk) disable iff (rst) expr

However, the 1'b1 cannot be optimized since there is still one cycle for
which disable iff might work. The precondition Jasper now generates follows:

@(posedge clk) disable iff (rst) expr1 ##1 1'b1

Miscellaneous
––––––-
* Updated CDC Documentation for "all_clocks_sync_by_default=false"

The CDC documentation now includes information on "all_clocks_sync_by_default=
false" for all applicable examples.

* Corrected Typo in the "set_sec_show_proof_log" Command Documentation

The Jasper Apps Command Reference Manual now shows the proper options for the
"set_sec_show_proof_log" command.

* Corrected Documentation for the "-cov_init" Command-line Options

The Jasper Apps Command Reference Manual now shows the proper options for the
"-cov_init" command-line options.

* Correctly Mapping SDC Constraint Targets when Using VHDL

You can now use the new "set_sdc_vhdl_expr_mode on" command to enable the
processing of SDC files in VHDL. By default, the tool processes SDC commands
in Verilog (sdc_vhdl_expr_mode=off).

Proofs and ProofGrid
––––––––––
* Proof Structure Now Updates GUI as Expected in the Absence of Any Operation

Proof Structure now shows results on root nodes even when the root node has
no operation.

* ProofMaster Cache Now Generating Consistent Results for Liveness

The information retrieved from the cache and displayed in the Property Table
is now consistent across runs as expected.

* Improved ProofMaster Summary

The ProofMaster summary report now includes visible build-in targets and is,
thus, more consistent with what the regular proof summary reports.

* Corrected ProofMaster Summary

When there are no properties to prove, the ProofMaster summary now shows
"0%" instead of "-nan%".

Property and Configuration Database
–––––––––––––––––-
* Improved Messaging for "get_property_list -task"

Previously, the command "get_property_list -task" returned the properties of
the current task if the specified task was not found. With this change, when
at least one of the task names specified is not found, the command issues a
warning. If none of the specified task names are found, it issues an error.

User Interface
–––––––
* Failed :live Property No Longer Reported as Vacuous

When the :live property fails, all liveness properties are labeled vacuous,
but the :live property itself is no longer reported as vacuous.

Verification Management
–––––––––––-
* Jasper Now Supports "assume -from_assert -env"

You can now use the "-env" switch with "assume -from_assert" to apply a newly
created assumption to the global environment instead of the current task.


Deprecation Notices
===================
The following commands 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_cdc -filter -add -source_domain: Use "-source_clock_domain" instead.
. check_cdc -filter -add -destination_domain: Use "-destination_clock_domain"
instead.
. check_cdc -filter -add -source_reset: Use "-local_source_reset" instead.
. check_cdc -filter -add -destination_reset: Use "-local_destination_reset"
instead.
. check_cdc -filter -add -source_declared_resets: Use "-source_reset_domain"
instead.
. check_cdc -filter -add -destination_declared_resets: Use
"-destination_reset_domain" instead.
. check_cdc -filter -add -reset_sources: Use "-reset_domain" instead.
. check_superlint -waiver -add -message: Use "check_superlint -waiver -add
-argument" instead.
. visualize -explore

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_lpv -save triggers EDEP283: Use "save -elaborated_design" instead.
. check_lpv -restore triggers EDEP283: Use "restore -elaborated_design" instead.
. export -afl: Use "check_superlint -export" instead or "set_message -warning
EDEP287" to downgrade this message to a warning.
. export -sps: Use "check_superlint -export" instead or "set_message -warning
EDEP287" to downgrade this message to a warning.
. export -superlint: Use "check_superlint -export" instead or "set_message
-warning EDEP287" to downgrade this message to a warning.
. check_superlint -waiver -import -text_format triggers ESL042: Use
"check_superlint -waiver -import -file_name" to generate a Tcl waiver file.
. check_superlint -waiver -add -check_type triggers ESL041
. check_superlint -waiver -list -check_type triggers ESL041
. check_superlint -waiver -export -text_format triggers ESL043
. set_auto_bothedge_optimization triggers EDEP290
. get_auto_bothedge_optimization triggers EDEP290
. prove -max_licenses: Use "prove -per_engine_max_jobs" instead or "set_message
-warning EPF111" to downgrade this message to a warning.
. set_proofgrid_privileged_licenses: Use
"set_jasper_proofgrid_per_engine_privileged_jobs" instead or use "set_message
-warning EPF110" to downgrade this message to a warning.
. get_proofgrid_privileged_licenses: Use
"get_jasper_proofgrid_per_engine_privileged_jobs" instead or use "set_message
-warning EPF110" to downgrade this message to a warning.
. set_proofgrid_max_local_licenses: Use
"set_jasper_proofgrid_per_engine_max_local_jobs" instead or use "set_message
-warning EPF109" to downgrade this message to a warning.
. get_proofgrid_max_local_licenses: Use
"get_jasper_proofgrid_per_engine_max_local_jobs" instead or use "set_message
-warning EPF109" to downgrade this message to a warning.
. set_proofgrid_max_licenses: Use "set_jasper_proofgrid_per_engine_max_jobs"
instead or use "set_message -warning EPF108" to downgrade this message to a
warning.
. get_proofgrid_max_licenses: Use "get_jasper_proofgrid_per_engine_max_jobs"
instead or use "set_message -warning EPF108" to downgrade this message to a
warning.
. jg_history triggers EDEP284: Use "jasper_history" instead or use
"set_message -warning EDEP284" to downgrade this message to a warning.
. set_jg_history_per_command_limit triggers EDEP285: Use
"set_jasper_history_per_command_limit" instead or use "set_message -warning
EDEP285" to downgrade this message to a warning.
. get_jg_history_per_command_limit triggers EDEP285: Use
"get_jasper_history_per_command_limit" instead or use "set_message -warning
EDEP285" to downgrade this message to a warning.

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

. get_fanin -addClockLogic: Use "get_fanin -add_clock_logic" (snake case).



Changes in Messaging
====================
Also see sections above.

***** Messages Removed from the Current Version *****
EXPR004: error {EXPR004 {{Unable to start the proof. The required setting for the "-leverage_sec" switch was not completed before design setup.}}}
WDFV008: warning {WDFV008 {{The expression computed for signal %s at time %s (sequence %s) is not boolean.}}}
––-

***** Messages That Were Introduced in the Current Version *****
EAS033: error {EAS033 {{Cannot convert X-Prop assertions to environment assumptions.}}}
ECDC135: error {ECDC135 {{The CDC App has not been initialized. You must first run "check_cdc -init".}}}
ECDC136: error {ECDC136 {{Unable to initialize CDC App because {app_name} App is already initialized.}}}
ECK062: error {ECK062 {{Jasper detected a property that requires a different clock declaration for clock "%s".\n Consider changing the clocking of the property, or declare clock "%s" with both_edges.\n Use "sanity_check" for more information about which clocks have an inconsistent clock declaration.}}}
ECOV083: error {ECOV083 {{The "-set_bound_analysis" subcommand works with assertions only.}}}
ECOV084: error {ECOV084 {{The "-set_bound" switch does not work on CEX or Proven targets.}}}
ECSR033: error {ECSR033 {{Cannot load a .csv file with "check_csr -load_ipxact". The file must be an IP-XACT .xml file.\n Use "check_csr -load" to load a .csv workbook.}}}
ECTR062: error {ECTR062 {{Unable to find Property {property}.}}}
ECTR063: error {ECTR063 {{C/C++ linker error in file "{file}", line {line}:\n {error}}}}
ECTR064: error {ECTR064 {{Cannot %s property "%s" as this enum constraint is already embedded in the model.}}}
ECTR065: error {ECTR065 {{Formal model generation errors have been found.}}}
EDA003: error {EDA003 {{An internal error has occurred in the %s setup. Results are not guaranteed to be accurate.\n Contact support@cadence.com for additional information.}}}
EDA004: error {EDA004 {{%s encountered %s error(s).}}}
EDA010: error {EDA010 {{Cannot use the "check_{app1} -init" command after initializing the {app2} App.}}}
EDA011: error {EDA011 {{Cannot run "prove" on task while a background proof is running.\n Use "-basic" to run "prove" in parallel.}}}
EDA012: error {EDA012 {{Cannot run "prove" on task while a background proof is running.}}}
EDA013: error {EDA013 {{Cannot add a Visualize stopat on an X-Prop or SPV trace.}}}
EDEP283: error {EDEP283 {{The subcommands "check_lpv -save" and "check_lpv -restore" have been deprecated.\n Please use "save -elaborated_design" and "restore -elaborated_design" instead or use "set_message -warning EDEP283" to downgrade this message to a warning.}}}
EDEP284: error {EDEP284 {{The command "jg_history" has been deprecated and will be removed in the next release.\n Use "jasper_history" instead or use "set_message -warning EDEP284" to downgrade this message to a warning.}}}
EDEP285: error {EDEP285 {{The command "get/set_jg_history_per_command_limit" has been deprecated and will be removed in the next release.\n Use "get/set_jasper_history_per_command_limit" instead or use "set_message -warning EDEP285" to downgrade this message to a warning.}}}
EDEP286: error {EDEP286 {{The command "get/set_jg_history_arg_limit" has been deprecated and will be removed in the next release.\n Use "set_message -warning EDEP286" to downgrade this message to a warning.}}}
EDEP287: error {EDEP287 {{The command "export -superlint|-afl|-sps" has been deprecated.\n Use "check_superlint -export" instead or "set_message -warning EDEP287" to downgrade this message to a warning.}}}
EDEP288: error {EDEP288 {{The command "get/set_visualize_enable_quiet_last_cycles" has been deprecated.\n Remove it or use "set_message -warning EDEP288" to downgrade this message to a warning.}}}
EDEP289: error {EDEP289 {{The command "get/set_visualize_enable_quiet_selected_signals" has been deprecated.\n Remove it or use "set_message -warning EDEP289" to downgrade this message to a warning.}}}
EDEP290: error {EDEP290 {{The command "get/set_auto_bothedge_optimization" has been deprecated.\n Remove it or use "set_message -warning EDEP290" to downgrade this message to a warning.}}}
EDEP291: error {EDEP291 {{The command "%s" has been deprecated and will be removed in the next release.\n Use "%s" instead or use "set_message -warning EDEP291" to downgrade this message to a warning.}}}
EFSV092: error {EFSV092 {{FSV does not support "elaborate %s".}}}
EFSV093: error {EFSV093 {{FSV does not support the "connect %s" command.}}}
EMTR414: error {EMTR414 {{%s does not support "elaborate %s".}}}
EMTR415: error {EMTR415 {{Running the clock gating proof strategy requires %s jobs, but max jobs is only %s.\n Either change proof strategy to basic or increase max jobs.}}}
EMTR416: error {EMTR416 {{Miter had %s error(s).}}}
ENL195: error {ENL195 {{"elaborate_single_run_mode" has been automatically {enabled_or_disabled}.\n "set_elaborate_single_run_mode" must be "{on_or_off}" to use this app or flow, and you cannot change this setting.\n Run "clear -all" to run a different app or flow.}}}
ENL196: error {ENL196 {{This app or flow does not support incremental elaboration.\n Run "clear -all" to run a different app or flow.}}}
EPF104: error {EPF104 {{{thread_id}: Morphing to a new engine when the proof is running with engineDFV alone is not supported.}}}
EPF105: error {EPF105 {{{thread_id}: Adding a new engine when the proof is running with engineDFV alone is not supported.}}}
EPF106: error {EPF106 {{{thread_id}: Running a new engine when the proof is running with engineDFV alone is not supported.}}}
EPF107: error {EPF107 {{{thread_id}: No eligible engines in engine mode.}}}
EPF108: error {EPF108 {{The command "get/set_proofgrid_max_licenses" has been deprecated and will be removed in the next release.\n Use "get/set_proofgrid_per_engine_max_jobs" instead or use "set_message -warning EPF108" to downgrade this message to a warning.}}}
EPF109: error {EPF109 {{The command "get/set_proofgrid_max_local_licenses" has been deprecated and will be removed in the next release.\n Use "get/set_proofgrid_per_engine_max_local_jobs" instead or use "set_message -warning EPF109" to downgrade this message to a warning.}}}
EPF110: error {EPF110 {{The command "get/set_proofgrid_privileged_licenses" has been deprecated and will be removed in the next release.\n Use "get/set_proofgrid_per_engine_privileged_jobs" instead or use "set_message -warning EPF110" to downgrade this message to a warning.}}}
EPF111: error {EPF111 {{The command "prove -max_licenses" has been deprecated and will be removed in the next release.\n Use "prove -per_engine_max_jobs" instead or use "set_message -warning EPF111" to downgrade this message to a warning.}}}
EPGJ006: error {EPGJ006 %s}
EPGJ007: error {EPGJ007 {{Unable to %s server with Jasper Cloud solution pipe mode.}}}
EPGJ008: error {EPGJ008 {{Invalid server ID.}}}
EPGJ009: error {EPGJ009 {{Unable to communicate with Jasper Cloud solution Manager.}}}
EPST048: error {EPST048 {{Unable to proceed with restoration of Proof Structure because of deprecated property "{propName}".\n Proof Structure cannot contain deprecated properties.}}}
ERS065: error {ERS065 {{The argument to "start_formal_bound" must be an integer between 0 and the sequence's total number of cycles.}}}
ERTL042: error {ERTL042 {{Configuration name "%s" is already used.}}}
ERTL043: error {ERTL043 {{Unable to continue as no supported app was initialized.\n You must first run "check_cdc -init" or "check_superlint -init".}}}
ESCH023: error {ESCH023 {{The design contains non-printable characters, which are not supported by the Schematic Viewer.}}}
ESEC391: error {ESEC391 {{An invalid elaborated design has been found for {spec_or_imp} side.\n Design must be elaborated with SEC commands.}}}
ESEC392: error {ESEC392 {{Specified directory must contain one elaborated design file only while using SEC compile context.\n Specify path of desired elaborated design file instead.}}}
ESEC393: error {ESEC393 {{Switch "{switch}" is not supported with "set_sec_elaborate_mode on".}}}
ESL041: error {ESL041 {{The switch "-check_type" has been deprecated.}}}
ESL042: error {ESL042 {{The waivers text file is deprecated.\n Use "check_superlint -waiver -import file_name" to generate a tcl waiver file.}}}
ESL043: error {ESL043 {{The waivers export with "text_format" switch is deprecated.\n Use "check_superlint -waiver -export -file_name file_name" to generate a Tcl waiver file.}}}
ESPV339: error {ESPV339 {{No signals matched the specified wildcard(s) %s.}}}
ESPV340: error {ESPV340 {{No signals or instances match the wildcard(s) passed to the "%s" %s.}}}
ESPV341: error {ESPV341 {{Invalid signal: The signal %s does not exist in this design.}}}
ESPV342: error {ESPV342 {{Invalid instance: The instance %s does not exist in this design.}}}
ESR019: error {ESR019 {{Periodic save is already running.\n Run "set_save_restore_periodic_save off" or "clear -all" before trying to save a new database.}}}
EVS177: error {EVS177 {{QuietTrace stopped with {remaining} remaining soft constraints. Satisfied: {satisfied}. Not Satisfied: {failed}.\n Proof has timed out, exceeded memory limit, or found another issue.}}}
EVS178: error {EVS178 {{The "visualize -replot" command does not support traces originated from a "prove -sst" flow.}}}
EVS179: error {EVS179 {{"visualize -sst" is not supported in the presence of a Compositional Assume-Guarantee assumption.}}}
EWB059: error {EWB059 {{Missing keyword "%s".}}}
EXPR018: error {EXPR018 {{Only the "basic" proof strategy provides the option to specify an engine mode.}}}
EXPR023: error {EXPR023 {{An internal error has occurred. Any results produced by this command are not guaranteed.\n Contact support@cadence.com for additional information.}}}
EXPR024: error {EXPR024 {{You must run "check_xprop -init" before running this command.}}}
EXPR025: error {EXPR025 {{X-Prop supports only "trace_extension" value 0.\n To enable the X-Prop proof run, use the following command: "set_trace_extension 0"}}}
EXPR026: error {EXPR026 {{Cannot run prove on X-Prop task while a background proof is running.}}}
EXPR027: error {EXPR027 {{Cannot run prove on X-Prop task while a background proof is running.\n Use "-basic" in order to run prove in parallel.}}}
EXPR028: error {EXPR028 {{X-Prop does not support the "visualize -replot" command.}}}
ICTR028: info {ICTR028 {{%s%u.%s: The Property "%s" under case %s was proven in %s.}}}
ICTR029: info {ICTR029 {{%s%u.%s: The Cover property "%s" under case %s was proven unreachable in %s.}}}
ICTR030: info {ICTR030 {{%s%u.%s: A counterexample (cex) with %u cycles was found for the property "%s" under case %s in %s.}}}
ICTR031: info {ICTR031 {{%s%u.%s: The Cover property "%s" under case %s was covered in %u cycles in %s.}}}
ICTR032: info {ICTR032 {{The Property "%s" was proven in %s.}}}
ICTR033: info {ICTR033 {{The Cover property "%s" was proven unreachable in %s.}}}
IDA011: info {IDA011 {{Preparing %s environment - started.}}}
IDA012: info {IDA012 {{Preparing %s environment - done.}}}
IHT028: info {IHT028 {{hunt -auto: Terminating run since no helper covers could be generated.}}}
IMTR159: info {IMTR159 {{Auto init mapping has been enabled for all tasks.}}}
IPF076: info {IPF076 {{%sTry "prove -add QT" to get SST traces starting close to reset. For the next proof, you can get this automatically by using "-prefer_quiet".}}}
IPF183: info {IPF183 {{Starting to retrieve cached TraceReplay traces.}}}
IPF184: info {IPF184 {{Finished retrieving cached TraceReplay traces in %#2.2f s.}}}
IRS041: info {IRS041 {{"reset -sequence -auto_align" transitioned the reset simulation into formal reset at cycle %u out of %u of the reset sequence.}}}
VERI-2664: warning {VERI-2664 {{symbol '%s' is not declared, assumed default net type '%s'}}}
VERI-2665: warning {VERI-2665 {{local qualifier is used to access external object '%s'}}}
VERI-2666: info {VERI-2666 {{mapped module '%s' for '%s' does not exist; creating it}}}
VERI-2667: error {VERI-2667 {{illegal select-expression; expected select-condition after '!'}}}
VERI-2668: warning {VERI-2668 {{use of string type in 'inside' constraint is an extension of LRM}}}
VERI-2669: error {VERI-2669 {{property instances with disable iff cannot be used as operand of property expression}}}
VERI-2670: warning {VERI-2670 {{non-blocking assignment in final block is illegal}}}
VERI-2671: warning {VERI-2671 {{$bits system function cannot have an argument of Interface class type}}}
VERI-2672: error {VERI-2672 {{illegal index expression; expected integral type}}}
VERI-2673: error {VERI-2673 {{virtual interface type variable '%s' is not allowed in continuous assignments}}}
VERI-2674: warning {VERI-2674 {{parameter '%s' of bind instantiation '%s' cannot be used in generate condition}}}
VERI-2675: warning {VERI-2675 {{querying system functions are only allowed on the first variable-size dimension}}}
VERI-2676: warning {VERI-2676 {{illegal zero or negative value for dimension in array querry function '%s'}}}
VERI-2677: warning {VERI-2677 {{dimension value out of bounds in array querry function '%s'}}}
VERI-2678: warning {VERI-2678 {{first argument of array querry function '%s' is missing}}}
VERI-2679: info {VERI-2679 {{target enum variable '%s' is here}}}
VERI-2680: error {VERI-2680 {{illegal size casting to zero or negative value for width}}}
VERI-2681: error {VERI-2681 {{illegal reference to clocking variable '%s'}}}
VERI-2682: error {VERI-2682 {{reference to block/label id '%s' is not valid in an expression}}}
VERI-2683: error {VERI-2683 {{continuous assignments to nettype nets can only have single value delays.}}}
VERI-2684: error {VERI-2684 {{continuous assignments to nettype net must be atomic}}}
VERI-2685: error {VERI-2685 {{illegal use of string literal as scope in assertion control task '%s'}}}
VERI-2686: error {VERI-2686 {{controlled timing check needs an edge as its first argument}}}
VERI-2687: error {VERI-2687 {{timing check '$%s' can only be used within specify blocks}}}
VERI-2688: warning {VERI-2688 {{'%s' inside always_latch block does not represent latched logic}}}
VERI-8038: warning {VERI-8038 {{non-constant loop has been unrolled %d times. Use "elaborate -non_constant_loop_limit" command to increase loop limit}}}
VERI-9107: warning {VERI-9107 {{resilient compilation has ignored %s '%s', due to (%s) at %s}}}
VHDL-1858: error {VHDL-1858 {{variable '%s' can only be of mode 'inout'}}}
VHDL-1859: error {VHDL-1859 {{formal variable '%s' should be of a protected type or composite type with a subelement of protected type}}}
VHDL-1860: warning {VHDL-1860 {{directive %s expects no argument}}}
WCB014: warning {WCB014 {{Unable to identify the path for the loop violation.\n The cex still indicates a loop and needs to be investigated.\n Use "check_loop -global" command to learn more about the loops in the design.}}}
WCD053: warning {WCD053 {{The properties below have free variables.\n When using "prove -from", consider using "assert -simulation_friendly" to create new propeties suitable for this and use them instead.\n {properties}}}}
WCDC241: warning {WCDC241 {{At least one SDC clock exceeded maximum factor %d after normalization.\n All SDC clock factors will be set to 1.}}}
WCOV102: warning {WCOV102 {{An artificial bound was set for property "%s" using the "check_cov -set_bound_analysis -assert -set_bound" command.\n This will not clean checker results from measure nor alter proof results.}}}
WCOV103: warning {WCOV103 {{Proof Structure node "%s" will be handled as a regular task by Coverage.\n Merging results with other tasks/nodes should be done with caution to guarantee safeness.}}}
WCOV104: warning {WCOV104 {{Checker coverage does not support proof cache.}}}
WCOV105: warning {WCOV105 {{Coverage checker mode "%s" is not enabled.}}}
WCTR030: warning {WCTR030 {{C/C++ compilation warning:\n {warning}}}}
WCTR031: warning {WCTR031 {{Formal model generation warning in file "{file}", line {line}:\n {warning}}}}
WDA002: warning {WDA002 {{The following X-Prop assumptions will be ignored since their targets are driven signals:\n %s.}}}
WDA003: warning {WDA003 {{The switch "%s" is set to "%s" in the %s App.}}}
WDIN005: warning {WDIN005 {{In a future release, you will no longer be able to use the "precondition" attribute with "get_property_info" to check whether the property is a precondition.\n Instead, to check if a property is a related cover, you will use the new "is_related_cover" attribute.\n To get the property's related property type, use "related_property_type", which returns one of the following attributes:\n\n . none\n . precondition\n . late_precondition\n . infinite_precondition\n . witness\n . contrapositive\n . infinite_contrapositive\n . safety_in_liveness}}}
WG020: warning {WG020 {{Unable to find task "%s".}}}
WLPV111: warning {WLPV111 {{{filename}({line_number}): The attribute "{attr}" is not supported.\n This switch will be ignored.}}}
WNL088: warning {WNL088 {{"elaborate_single_run_mode" has been enabled.}}}
WNL089: warning {WNL089 {{The driver trace will not go into cell defines.\n If you need to debug cell defines, use "set_cell_define_debug_visibility on".}}}
WPF084: warning {WPF084 {{The "parallel prove from" feature is enabled. Skipping Advanced Proof Simplification Step.}}}
WPF085: warning {WPF085 {{{thread_id}: QuietTrace is not supported for engineDFV. Ignoring it.}}}
WPF086: warning {WPF086 {{{thread_id}: "engineDFV" is not supported for this proof; ignoring it.}}}
WPF087: warning {WPF087 {{A trace extension (in this case, %s) is part of the property environment (just like clock and reset) and will alter the meaning of your properties.\n Increasing the trace extension can turn the property status from cex/covered to proven/unreachable.\n Trace extension does not apply to liveness properties.\n A trace extension forces the proof engines to look for longer traces, which will most likely slow them down whether a trace exists or not.\n NOTE: When the trace extension exceeds the SST trace length, here %u, properties are allowed to fail anywhere and do not effectively constrain\n the trace.}}}
WPF088: warning {WPF088 {{The properties below have a posedge trace extension.\n When using "prove -sst", it is difficult to predict when they will be allowed to fail and whether they will constrain the trace at all.\n {properties}}}}
WPF089: warning {WPF089 {{The properties below have a trace extension no shorter than the SST trace length ({length}).\n When using "prove -sst", this means that they will not effectively constrain the trace.\n {properties}}}}
WSDC008: warning {WSDC008 {{{num_errors} errors were encountered while processing SDC files.\n Check the CTE log file at cte.log for details.}}}
WSDC009: warning {WSDC009 %s}
WSL075: warning {WSL075 {{The waivers persistency data in the file are deprecated.\n Use "check_superlint -waiver -export file_name" to generate new tcl waiver file with new persistency data.}}}
WSL076: warning {WSL076 {{Reset is not defined. Check "%s" will be ignored.\n Define reset using "reset expression".}}}
WTR038: warning {WTR038 {{Maximum error/warning count (%d) reached. Further errors/warnings will be suppressed.}}}
WUNR018: warning {WUNR018 {{"check_unr -prove" has been interrupted because the specified task has been deleted.}}}
WXPR004: warning {WXPR004 {{You must run "check_xprop -init" before using the "%s" switch.}}}
WXPR005: warning {WXPR005 {{The following X-Prop assumptions will be ignored since their targets are driven signals:\n %s.}}}
––-

***** Messages with a Change to the Default Text *****
E0005 changed from:
E0005 {{Stack overflow. Increase the stack size using "ulimit -s %s" before running Jasper.}}
to:
E0005 {{Stack overflow. Increase the stack size using Bash "ulimit -s %s" or Csh "limit stacksize %s" before running Jasper.}}

ECD041 changed from:
ECD041 {{Command has been interrupted by user.\n You may have hit Ctrl+C from console to exit.} {"elaborate -static" is not supported by the old hierarchical handler.}}
to:
ECD041 {{"elaborate -static" is not supported by the old hierarchical handler.} {Command has been interrupted by user.\n You may have hit Ctrl+C from console to exit.}}

ECD058 changed from:
ECD058 {{There were failures when restoring configurations to their default values.\n Some configurations might not have been successfully restored.\n See previous messages for details.} {Command run on session "{session_name}" failed.}}
to:
ECD058 {{Command run on session "{session_name}" failed.} {There were failures when restoring configurations to their default values.\n Some configurations might not have been successfully restored.\n See previous messages for details.}}

ECK033 changed from:
ECK033 {{Clock pin "%s" for PSL/SVA property is gated; therefore, it might introduce clock glitches via the enable logic.\n Ensure that the design has no glitches and use "set_clock_assume_enable_stable_at_sampling_edge on".} {Clock pin "%s" for flop "%s" is gated; therefore, it might introduce clock glitches via the enable logic.\n Ensure that the design has no glitches and use "set_clock_assume_enable_stable_at_sampling_edge on".}}
to:
ECK033 {{Clock pin "%s" for flop "%s" is gated; therefore, it might introduce clock glitches via the enable logic.\n Ensure that the design has no glitches and use "set_clock_assume_enable_stable_at_sampling_edge on".} {Clock pin "%s" for PSL/SVA property is gated; therefore, it might introduce clock glitches via the enable logic.\n Ensure that the design has no glitches and use "set_clock_assume_enable_stable_at_sampling_edge on".}}

ECK036 changed from:
ECK036 {{The signal "%s" can cause glitches as an enable of clock "%s".\n You can resolve this problem in two ways:\n a) Apply "clock -rate" to the enable of the gated clock.\n b) Use "set_clock_accept_enable_with_glitches on" to allow the tool to support gated clocks with glitches.} {The signal "%s" can have glitches as an enable of clock "%s" (fast clock).\n You can resolve this problem in two ways:\n a) Add "-both_edges" to the "clock" command and apply "clock -rate" to the enable of the gated clock.\n b) Use "set_clock_accept_enable_with_glitches on" to allow the tool to support gated clocks with glitches.}}
to:
ECK036 {{The signal "%s" can have glitches as an enable of clock "%s" (fast clock).\n You can resolve this problem in two ways:\n a) Add "-both_edges" to the "clock" command and apply "clock -rate" to the enable of the gated clock.\n b) Use "set_clock_accept_enable_with_glitches on" to allow the tool to support gated clocks with glitches.} {The signal "%s" can cause glitches as an enable of clock "%s".\n You can resolve this problem in two ways:\n a) Apply "clock -rate" to the enable of the gated clock.\n b) Use "set_clock_accept_enable_with_glitches on" to allow the tool to support gated clocks with glitches.}}

ECK100 changed from:
ECK100 {{Clock "%s" for flop in PSL/SVA property is driven by AND-gated tree, but none of its inputs is defined as a clock.\nHigh-level clock signal is %s\n Connected driver(s): %s\n For information on the clock tree, run "clock -analyze" and do one of the following:\n - Declare all clocks from property's COI that are inputs or have an environmental stopat.\n - Add an environmental stopat to the flop's clock logic and declare it as clock.\n - Use "set_clock_handle_complex_logic on" to enable undeclared clock logic analysis.} {Clock "%s" for flop "%s" is driven by AND-gated tree, but none of its inputs is defined as a clock.\n High-level clock signal is %s\n Connected driver(s): %s\nFor information on the clock tree, run "clock -analyze" and do one of the following:\n - Declare all clocks from property's COI that are inputs or have an environmental stopat.\n - Add an environmental stopat to the flop's clock logic and declare it as clock.\n - Use "set_clock_handle_complex_logic on" to enable undeclared clock logic analysis.}}
to:
ECK100 {{Clock "%s" for flop "%s" is driven by AND-gated tree, but none of its inputs is defined as a clock.\n High-level clock signal is %s\n Connected driver(s): %s\nFor information on the clock tree, run "clock -analyze" and do one of the following:\n - Declare all clocks from property's COI that are inputs or have an environmental stopat.\n - Add an environmental stopat to the flop's clock logic and declare it as clock.\n - Use "set_clock_handle_complex_logic on" to enable undeclared clock logic analysis.} {Clock "%s" for flop in PSL/SVA property is driven by AND-gated tree, but none of its inputs is defined as a clock.\nHigh-level clock signal is %s\n Connected driver(s): %s\n For information on the clock tree, run "clock -analyze" and do one of the following:\n - Declare all clocks from property's COI that are inputs or have an environmental stopat.\n - Add an environmental stopat to the flop's clock logic and declare it as clock.\n - Use "set_clock_handle_complex_logic on" to enable undeclared clock logic analysis.}}

ECK102 changed from:
ECK102 {{Clock "%s" for flop "%s" is assigned to constant value (%s), hence it will never tick.\n High-level clock signal is: %s\nFor information on the clock tree, run "clock -analyze" and do one of the following:\n - If listed clock is not an input, add an environmental stopat and declare it as clock.\n - Use "set_clock_handle_complex_logic on" to enable constant clock analysis.} {Clock "%s" for flop in PSL/SVA property is assigned to constant value (%s); hence, it will never tick.\n High-level clock signal is: %s\nFor information on the clock tree, run "clock -analyze" and do one of the following:\n - If listed clock is not an input add an environmental stopat and declare it as clock.\n - Use "set_clock_handle_complex_logic on" to enable constant clock analysis.}}
to:
ECK102 {{Clock "%s" for flop in PSL/SVA property is assigned to constant value (%s); hence, it will never tick.\n High-level clock signal is: %s\nFor information on the clock tree, run "clock -analyze" and do one of the following:\n - If listed clock is not an input add an environmental stopat and declare it as clock.\n - Use "set_clock_handle_complex_logic on" to enable constant clock analysis.} {Clock "%s" for flop "%s" is assigned to constant value (%s), hence it will never tick.\n High-level clock signal is: %s\nFor information on the clock tree, run "clock -analyze" and do one of the following:\n - If listed clock is not an input, add an environmental stopat and declare it as clock.\n - Use "set_clock_handle_complex_logic on" to enable constant clock analysis.}}

ECK103 changed from:
ECK103 {{Clock "%s" for flop in PSL/SVA property has a complex, gated-clock structure %s.\n High-level clock signal is: %s\n Problematic gate is: %s\n Connected driver(s): %s\nFor information on the clock tree, run "clock -analyze" and do one of the following:\n - If listed clock is not an input, add an environmental stopat and declare it as clock.\n - Use "set_clock_handle_complex_logic on" to enable complex clock logic analysis.} {Clock "%s" for flop "%s" has a complex, gated-clock structure %s.\n High-level clock signal is: %s\n Problematic gate is: %s\n Connected driver(s): %s\nFor information on the clock tree, run "clock -analyze" and do one of the following:\n - If listed clock is not an input, add an environmental stopat and declare it as clock.\n - Use "set_clock_handle_complex_logic on" to enable complex clock logic analysis.}}
to:
ECK103 {{Clock "%s" for flop "%s" has a complex, gated-clock structure %s.\n High-level clock signal is: %s\n Problematic gate is: %s\n Connected driver(s): %s\nFor information on the clock tree, run "clock -analyze" and do one of the following:\n - If listed clock is not an input, add an environmental stopat and declare it as clock.\n - Use "set_clock_handle_complex_logic on" to enable complex clock logic analysis.} {Clock "%s" for flop in PSL/SVA property has a complex, gated-clock structure %s.\n High-level clock signal is: %s\n Problematic gate is: %s\n Connected driver(s): %s\nFor information on the clock tree, run "clock -analyze" and do one of the following:\n - If listed clock is not an input, add an environmental stopat and declare it as clock.\n - Use "set_clock_handle_complex_logic on" to enable complex clock logic analysis.}}

ECK104 changed from:
ECK104 {{Clock "%s" for flop "%s" is an input that is not defined as a clock.\n Current clock definition is: %s\nFor information on the clock tree, run "clock -analyze" and do one of the following:\n - Declare flop's clock as clock.\n - Use "set_clock_handle_complex_logic on" to enable undeclared clock analysis.} {Clock "%s" for flop in PSL/SVA property is an input that is not defined as a clock.\n Current clock definition is: %s\nFor information on the clock tree, run "clock -analyze" and do one of the following:\n - Declare flop's clock as clock.\n - Use "set_clock_handle_complex_logic on" to enable undeclared clock analysis.}}
to:
ECK104 {{Clock "%s" for flop in PSL/SVA property is an input that is not defined as a clock.\n Current clock definition is: %s\nFor information on the clock tree, run "clock -analyze" and do one of the following:\n - Declare flop's clock as clock.\n - Use "set_clock_handle_complex_logic on" to enable undeclared clock analysis.} {Clock "%s" for flop "%s" is an input that is not defined as a clock.\n Current clock definition is: %s\nFor information on the clock tree, run "clock -analyze" and do one of the following:\n - Declare flop's clock as clock.\n - Use "set_clock_handle_complex_logic on" to enable undeclared clock analysis.}}

ECK106 changed from:
ECK106 {{Clock "%s" for flop in PSL/SVA property is connected to a hard stopat "%s", which is not defined as a clock.\n Current clock definition is: %s\nFor information on the clock tree, run "clock -analyze" and do one of the following:\n - Declare the listed signal as a clock.\n - If the hard stopat is not environmental, re-define it as such and declare it as clock.\n - Use "set_clock_handle_complex_logic on" to enable undeclared clock logic analysis.\n - Remove the hard stopat.} {Clock "%s" for flop "%s" is connected to a hard stopat "%s", which is not defined as a clock.\n Current clock definition is: %s\nFor information on the clock tree, run "clock -analyze" and do one of the following:\n - Declare the listed signal as a clock.\n - If the hard stopat is not environmental, re-define it as such and declare it as clock.\n - Remove the hard stopat.\n - Use "set_clock_handle_complex_logic on" to enable undeclared clock logic analysis.}}
to:
ECK106 {{Clock "%s" for flop "%s" is connected to a hard stopat "%s", which is not defined as a clock.\n Current clock definition is: %s\nFor information on the clock tree, run "clock -analyze" and do one of the following:\n - Declare the listed signal as a clock.\n - If the hard stopat is not environmental, re-define it as such and declare it as clock.\n - Remove the hard stopat.\n - Use "set_clock_handle_complex_logic on" to enable undeclared clock logic analysis.} {Clock "%s" for flop in PSL/SVA property is connected to a hard stopat "%s", which is not defined as a clock.\n Current clock definition is: %s\nFor information on the clock tree, run "clock -analyze" and do one of the following:\n - Declare the listed signal as a clock.\n - If the hard stopat is not environmental, re-define it as such and declare it as clock.\n - Use "set_clock_handle_complex_logic on" to enable undeclared clock logic analysis.\n - Remove the hard stopat.}}

ECK108 changed from:
ECK108 {{Clock "%s" logic for PSL/SVA property is connected to a fast clock.\n Define the clock as "-both_edges" to enable verification of the property.} {Clock "%s" logic for flop "%s" is connected to a fast clock.\n Define the clock as "-both_edges" to enable verification of the property.}}
to:
ECK108 {{Clock "%s" logic for flop "%s" is connected to a fast clock.\n Define the clock as "-both_edges" to enable verification of the property.} {Clock "%s" logic for PSL/SVA property is connected to a fast clock.\n Define the clock as "-both_edges" to enable verification of the property.}}

ECSR026 changed from:
ECSR026 {{File "%s" has no valid format.\n The file must be a .csv workbook. Use "check_csr -load_ipxact" to load an IP-XACT .xml file.}}
to:
ECSR026 {{Cannot load an IP-XACT .xml file with "check_csr -load". The file must be a .csv workbook.\n Use "check_csr -load_ipxact" to load an IP-XACT .xml file.}}

ECTR004 changed from:
ECTR004 {{"check_c2rtl -set_unwind_limit" was used for file {file}, line {line}.\n Cannot associate this location with any of the supported loops, recursive function declarations, or object array declarations.\n Review the "check_c2rtl -set_unwind_limit" command details.}}
to:
ECTR004 {{"check_c2rtl -set_unroll_limit" was used for file {file}, line {line}.\n Cannot associate this location with any of the supported loops, recursive function declarations, or object array declarations.\n Review the "check_c2rtl -set_unroll_limit" command details.}}

ECTR014 changed from:
ECTR014 {{C compilation error:\n function "{function}" in file "{file}", line {line}\n {error}.}}
to:
ECTR014 {{Formal model generation error in function "{function}" in file "{file}", line {line}:\n {error}.}}

ECTR015 changed from:
ECTR015 {{C compilation error:\n {error}.}}
to:
ECTR015 {{Formal model generation error:\n {error}.}}

ECTR034 changed from:
ECTR034 {{Synthesis errors have been found.}}
to:
ECTR034 {{Formal model generation errors that might indicate a tool bug have been found.\n Contact support@cadence.com.}}

ECTR045 changed from:
ECTR045 {{The value of #pragma JASPER_NAME "{name}" in file in file "{fileName}" matches a field or variable that is non-array or an array without auto initialization.\n Remove the "check_c2rtl -set_unwind_limit" command related to this field or variable.}}
to:
ECTR045 {{The value of #pragma JASPER_NAME "{name}" in file "{fileName}" matches a field or variable that is non-array or an array without auto initialization.\n Remove the "check_c2rtl -set_unroll_limit" command related to this field or variable.}}

ECTR057 changed from:
ECTR057 {{Synthesis errors found.}}
to:
ECTR057 {{Formal model generation errors found.}}

EDA006 changed from:
EDA006 {{Visualize cannot generate a trace on DA properties.}}
to:
EDA006 {{Visualize cannot generate a trace on this DA property.}}

EDA007 changed from:
EDA007 {{The property is proven. No violation trace exists.}}
to:
EDA007 {{Visualize cannot generate a trace on this DA property. Run prove first.}}

EFL039 changed from:
EFL039 {{parsing file %s%s%s parse error(s).} {File extension "%s" is not a valid extension.}}
to:
EFL039 {{File extension "%s" is not a valid extension.} {parsing file %s%s%s parse error(s).}}

EGNA006 changed from:
EGNA006 {{Property "%s" is disabled.} {Use the command "set_parallel_proof_mode on" to enable parallel mode of "get_needed_assumptions".}}
to:
EGNA006 {{Use the command "set_parallel_proof_mode on" to enable parallel mode of "get_needed_assumptions".} {Property "%s" is disabled.}}

EGNA008 changed from:
EGNA008 {{Cannot achieve "%s" status for "%s".}}
to:
EGNA008 {{Cannot achieve "%s" status for "%s".\n Try adding the "-include_properties" switch or running "check_assumptions -minimize".}}

EGNA009 changed from:
EGNA009 {{Failed to achieve "%s" status with the current "-attempts_time_limit".} {Failed to achieve "%s" status with the current "-max_trace_length".}}
to:
EGNA009 {{Failed to achieve "%s" status with the current "-max_trace_length".} {Failed to achieve "%s" status with the current "-attempts_time_limit".}}

ELPV051 changed from:
ELPV051 {{%s(%s): Problem creating power domain "%s", supply net "%s": invalid scope "%s".}}
to:
ELPV051 {{%s(%s): Internal error handling attributes for port "%s".}}

ELPV138 changed from:
ELPV138 {{%s(%s): Supply net "%s" is invalid for port "%s".}}
to:
ELPV138 {{{file_name}({start_line}): The value "{value}" is not valid for attribute "{attr}".\n The expected values are "{valid}".}}

ELPV180 changed from:
ELPV180 {{%s(%s): Repeater rule "%s" is missing its supply specification.\n Add the repeater supply in the "set_repeater" command.} {Conflicting repeater rules of same precedence level apply to the target "%s".\n Check rule "%s" defined in %s(%s) and rule "%s" defined in %s(%s).}}
to:
ELPV180 {{Conflicting repeater rules of same precedence level apply to the target "%s".\n Check rule "%s" defined in %s(%s) and rule "%s" defined in %s(%s).} {%s(%s): Repeater rule "%s" is missing its supply specification.\n Add the repeater supply in the "set_repeater" command.}}

ELPV200 changed from:
ELPV200 {{Circularity found between handles: {loop}.} {Conflicting retention rules of same precedence level apply to the target "%s".\n Check rule "%s" defined in %s(%s) and rule "%s" defined in %s(%s).}}
to:
ELPV200 {{Conflicting retention rules of same precedence level apply to the target "%s".\n Check rule "%s" defined in %s(%s) and rule "%s" defined in %s(%s).} {Circularity found between handles: {loop}.}}

EMTR364 changed from:
EMTR364 {{An internal error has occurred in MITER. Any results produced by your command are not guaranteed. Contact support@cadence.com.} {Sanity check failed on violating init mappings since a stopat mapping on the same signals exists, which makes init mapping redundant.\n Violating IDs: %s}}
to:
EMTR364 {{Sanity check failed on violating init mappings since a stopat mapping on the same signals exists, which makes init mapping redundant.\n Violating IDs: %s} {An internal error has occurred in MITER. Any results produced by your command are not guaranteed. Contact support@cadence.com.}}

ENL165 changed from:
ENL165 {{"elaborate -keep_hier_tree" and "elaborate -incremental" are not supported with %s.} {"elaborate -keep_hier_tree" and "elaborate -incremental" are not supported in Coverage flow.}}
to:
ENL165 {{"elaborate -keep_hier_tree" and "elaborate -incremental" are not supported in Coverage flow.} {"elaborate -keep_hier_tree" and "elaborate -incremental" are not supported with %s.}}

EPF008 changed from:
EPF008 {{"_set_property" is not allowed to modify "{internal_property_name}".} {Illegal proof expression "%s"; expression must have a width of 1.}}
to:
EPF008 {{Illegal proof expression "%s"; expression must have a width of 1.} {"_set_property" is not allowed to modify "{internal_property_name}".}}

EPF043 changed from:
EPF043 {{max_trace_length cannot be lower than first_trace_attempt.} {max_trace_length cannot be lower than engineB_first_trace_attempt.}}
to:
EPF043 {{max_trace_length cannot be lower than engineB_first_trace_attempt.} {max_trace_length cannot be lower than first_trace_attempt.}}

EPM048 changed from:
EPM048 {{The following "-from" signals in the X-Prop property are not inputs or stopats:\n%s} {The following "-from" signals in the "cover -path" property are not inputs or stopats:\n%s} {The following "-from" signals in the SPV property are not inputs or stopats:\n%s}}
to:
EPM048 {{The following "-from" signals in the SPV property are not inputs or stopats:\n%s} {The following "-from" signals in the X-Prop property are not inputs or stopats:\n%s} {The following "-from" signals in the "cover -path" property are not inputs or stopats:\n%s}}

ERS038 changed from:
ERS038 {{The signal "%s" is not a declared clock.} {Clock ticks or postfix information missing in file: "%s" on line %d.}}
to:
ERS038 {{Clock ticks or postfix information missing in file: "%s" on line %d.} {The signal "%s" is not a declared clock.}}

ERTL035 changed from:
ERTL035 {{For rule '%s", you can specify only one complete signal.} {Signal "%s" is duplicated in argument.}}
to:
ERTL035 {{Signal "%s" is duplicated in argument.} {For rule '%s", you can specify only one complete signal.}}

ESEC300 changed from:
ESEC300 {{Update %s enum in both:\n 'shell/SECApp/SECCmdEnums.java' and 'database/miterdb/basictypes/MiterDefinitions.h'}}
to:
ESEC300 {{Update %s enum in 'database/miterdb/basictypes/MiterDefinitions.h'}}

ESL006 changed from:
ESL006 {{Unable to export SVA because the database is not open.\n For message help, type "help -message ESL006".} {Unable to export SVA due to an internal database problem.\n For message help, type "help -message ESL006".}}
to:
ESL006 {{Unable to export SVA due to an internal database problem.\n For message help, type "help -message ESL006".} {Unable to export SVA because the database is not open.\n For message help, type "help -message ESL006".}}

ESL040 changed from:
ESL040 {{This command requires a list of check IDs.}}
to:
ESL040 {{This command requires a list of check IDs.} {Unable to leverage due to a database error.}}

ESPV007 changed from:
ESPV007 {{"%s" is the top module. A top module cannot be abstracted.} {"%s" is the top module. A top module cannot be abstracted.\n The following abstractions were done without any issue: %s}}
to:
ESPV007 {{"%s" is the top module. A top module cannot be abstracted.\n The following abstractions were done without any issue: %s} {"%s" is the top module. A top module cannot be abstracted.}}

ESPV010 changed from:
ESPV010 {{Argument for switch "-mode" should be "comb", "seq", or "mixed" in this SPV flow.} {Argument for switch "-mode" should be "comb", "seq", "auto", "manual", or N[:M] where N>=0, N<M, or M=$.}}
to:
ESPV010 {{Argument for switch "-mode" should be "comb", "seq", "auto", "manual", or N[:M] where N>=0, N<M, or M=$.} {Argument for switch "-mode" should be "comb", "seq", or "mixed" in this SPV flow.}}

ESPV012 changed from:
ESPV012 {{Error when trying to perform abstraction. Connection spec is empty.} {Error when trying to perform abstraction. Connection spec is empty.\n The following abstractions were done without any issue: %s}}
to:
ESPV012 {{Error when trying to perform abstraction. Connection spec is empty.\n The following abstractions were done without any issue: %s} {Error when trying to perform abstraction. Connection spec is empty.}}

ESPV282 changed from:
ESPV282 {{Unable to prove SPV property: %s. The "-from" signal "%s" has the following SPV abstraction: "%s".} {Unable to prove SPV property "%s". The "-from" signal "%s" has the following abstraction "%s".\n If an abstraction is intersecting with a "-from" signal, all bits of the abstraction need to be added to the "-from".\n NOTE: This flow will support "-from" signals with abstractions in a future release.}}
to:
ESPV282 {{Unable to prove SPV property "%s". The "-from" signal "%s" has the following abstraction "%s".\n If an abstraction is intersecting with a "-from" signal, all bits of the abstraction need to be added to the "-from".\n NOTE: This flow will support "-from" signals with abstractions in a future release.} {Unable to prove SPV property: %s. The "-from" signal "%s" has the following SPV abstraction: "%s".}}

ESPV325 changed from:
ESPV325 {{The SPV abstraction you are attempting to create conflicts with another SPV abstraction "%s" in task "%s".\n You cannot use "to" signals in multiple SPV abstractions.} {The SPV abstraction you are attempting to create conflicts with another SPV abstraction "%s" in the global environment.\n You cannot use "to" signals in multiple SPV abstractions.}}
to:
ESPV325 {{The SPV abstraction you are attempting to create conflicts with another SPV abstraction "%s" in the global environment.\n You cannot use "to" signals in multiple SPV abstractions.} {The SPV abstraction you are attempting to create conflicts with another SPV abstraction "%s" in task "%s".\n You cannot use "to" signals in multiple SPV abstractions.}}

ESR005 changed from:
ESR005 {{Cannot restore database "%s". Check format and version of database file.} {Unable to open database directory "%s". Database is locked by another session.}}
to:
ESR005 {{Unable to open database directory "%s". Database is locked by another session.} {Cannot restore database "%s". Check format and version of database file.}}

ESW052 changed from:
ESW052 {{Too many arguments.\n The "%s" switch only accepts one of the following: %s} {Too many arguments.}}
to:
ESW052 {{Too many arguments.} {Too many arguments.\n The "%s" switch only accepts one of the following: %s}}

ESW053 changed from:
ESW053 {{Invalid argument "%s" value.\n The argument must be a non-zero integer.} {Invalid argument "%s".\n The argument must be one of the following: %s.} {Invalid argument.\n "%s" value cannot be greater than "%s" value.} {Invalid argument "%s".}}
to:
ESW053 {{Invalid argument "%s".} {Invalid argument "%s".\n The argument must be one of the following: %s.} {Invalid argument "%s" value.\n The argument must be a non-zero integer.} {Invalid argument.\n "%s" value cannot be greater than "%s" value.}}

ESW054 changed from:
ESW054 {{A required switch is missing.} {A required switch "%s" is missing.} {Required switch missing. You must specify one of the following: %s}}
to:
ESW054 {{Required switch missing. You must specify one of the following: %s} {A required switch is missing.} {A required switch "%s" is missing.}}

ESW124 changed from:
ESW124 {{Unable to find an elaborated design file in directory "%s".\n NOTE: Files saved by the "save" command must not be renamed.} {Invalid range formation "%s".\n It should be either L:U or L:s:U, where "L" is the lower bound, "U" the upper, and "s" the non-zero step between successive elements.}}
to:
ESW124 {{Invalid range formation "%s".\n It should be either L:U or L:s:U, where "L" is the lower bound, "U" the upper, and "s" the non-zero step between successive elements.} {Unable to find an elaborated design file in directory "%s".\n NOTE: Files saved by the "save" command must not be renamed.}}

ETR032 changed from:
ETR032 {{Either provide a signal name as an argument or use the "-file" switch.} {Trace might contain signals with incorrect values. Contact support@cadence.com.\n For message help, type "help -message etr032".}}
to:
ETR032 {{Trace might contain signals with incorrect values. Contact support@cadence.com.\n For message help, type "help -message etr032".} {Either provide a signal name as an argument or use the "-file" switch.}}

EUNR016 changed from:
EUNR016 {{Unable to load Refinement file "%s". This might be due to memory limit.\n Increase memory limit using "set_unr_refinement_memlimit <memory_limit>" and try again.\n Example: set_unr_refinement_memlimit 8G}}
to:
EUNR016 {{Unable to load refinement file "%s". This might be due to the current memory limit setting, 32G.\n Increase memory limit using "set_unr_refinement_memlimit <memory_limit>" and try again.\n NOTE: This configuration must be set prior to issuing the "check_unr -setup" command.\n Example: set_unr_refinement_memlimit 64G}}

ICD006 changed from:
ICD006 {{%sThe "prove" command was aborted because of a per_property_time_limit or per_property_stagnation_time_limit expiration.\n The current per_property_time_limit is %d seconds.\n The current per_property_stagnation_time_limit is %d seconds.\n Modify them with the "-per_property_time_limit" switch or "set_prove_per_property_time_limit" and "set_prove_per_property_stagnation_time_limit" commands.\n See also the "set_prove_per_property_time_limit_factor" command.} {%sThe "prove" command was aborted because of a per_property_time_limit expiration.\n The current limit is %d seconds.\n Modify it with the "-per_property_time_limit" switch or "set_prove_per_property_time_limit" command.\n See also the "set_prove_per_property_time_limit_factor" command.}}
to:
ICD006 {{%sThe "prove" command was aborted because of a per_property_time_limit expiration.\n The current limit is %d seconds.\n Modify it with the "-per_property_time_limit" switch or "set_prove_per_property_time_limit" command.\n See also the "set_prove_per_property_time_limit_factor" command.} {%sThe "prove" command was aborted because of a per_property_time_limit or per_property_stagnation_time_limit expiration.\n The current per_property_time_limit is %d seconds.\n The current per_property_stagnation_time_limit is %d seconds.\n Modify them with the "-per_property_time_limit" switch or "set_prove_per_property_time_limit" and "set_prove_per_property_stagnation_time_limit" commands.\n See also the "set_prove_per_property_time_limit_factor" command.}}

ICK002 changed from:
ICK002 {{Setting buffer-equivalent source "%s" corresponding to signal\n "%s" as posedge clock.} {Setting buffer-equivalent source "%s" corresponding to signal\n "%s" as negedge clock.}}
to:
ICK002 {{Setting buffer-equivalent source "%s" corresponding to signal\n "%s" as negedge clock.} {Setting buffer-equivalent source "%s" corresponding to signal\n "%s" as posedge clock.}}

ICM001 changed from:
ICM001 {{Formal effort analysis completed for bound %s.}}
to:
ICM001 {{{run_name}: Formal effort analysis for target "{target}" completed for bound {bound}.}}

ICTR024 changed from:
ICTR024 {{Compiling {file}}}
to:
ICTR024 {{Parsing {file}}}

IFSV112 changed from:
IFSV112 {{FSV proof finished after %ds.} {Calculating fault distances.}}
to:
IFSV112 {{Calculating fault distances.} {FSV proof finished after %ds.}}

ILC014 changed from:
ILC014 {{License "{license}" has been queued.\n Number of checked out licenses: {numberCheckedOut}\n Number of reserved licenses: {numberReserved}\n Number of queued licenses: {numberQueued}} {License "{license}" has been queued. Approximate time until timeout: {timeout} s\n Number of checked out licenses: {numberCheckedOut}\n Number of reserved licenses: {numberReserved}\n Number of queued licenses: {numberQueued}}}
to:
ILC014 {{License "{license}" has been queued. Approximate time until timeout: {timeout} s\n Number of checked out licenses: {numberCheckedOut}\n Number of reserved licenses: {numberReserved}\n Number of queued licenses: {numberQueued}} {License "{license}" has been queued.\n Number of checked out licenses: {numberCheckedOut}\n Number of reserved licenses: {numberReserved}\n Number of queued licenses: {numberQueued}}}

ILC015 changed from:
ILC015 {{License "{license}" is still queued. Approximate time until timeout: {timeout} s} {License "{license}" is still queued.}}
to:
ILC015 {{License "{license}" is still queued.} {License "{license}" is still queued. Approximate time until timeout: {timeout} s}}

IMTR116 changed from:
IMTR116 {{Preparing the MITER environment for "%s" strategy%s}}
to:
IMTR116 {{Preparing the MITER environment for "%s" strategy - %s.}}

IMTR134 changed from:
IMTR134 {{Miter %s: %s.} {%s: %s.}}
to:
IMTR134 {{%s: %s.} {Miter %s: %s.}}

INTERNAL changed from:
INTERNAL {%s %s%s {INTERNAL: %s.}}
to:
INTERNAL {%s%s %s {INTERNAL: %s.}}

IOBS001 changed from:
IOBS001 {{Liveness property has safety component.} {%sLiveness property has safety component.}}
to:
IOBS001 {{%sLiveness property has safety component.} {Liveness property has safety component.}}

IPF048 changed from:
IPF048 {{The cover property "%s" was covered.} {Automatic cover generation identified %d signals of type "%s" in design.}}
to:
IPF048 {{Automatic cover generation identified %d signals of type "%s" in design.} {The cover property "%s" was covered.}}

IPM033 changed from:
IPM033 {{Clearing traces of disabled properties.} {The name "%s" is assigned to cover "%s".}}
to:
IPM033 {{The name "%s" is assigned to cover "%s".} {Clearing traces of disabled properties.}}

IRS008 changed from:
IRS008 {{Computing reset analysis from trace core…} {Computing reset analysis from file "%s"…}}
to:
IRS008 {{Computing reset analysis from file "%s"…} {Computing reset analysis from trace core…}}

ISDC001 changed from:
ISDC001 {{SDC file "%s" was successfully processed. The CTE log file can be found at "%s/cte.log".}}
to:
ISDC001 {{SDC file "%s" was successfully processed. The CTE log file can be found at cte.log.}}

ISEC028 changed from:
ISEC028 {{Exposing %s mapping properties…}}
to:
ISEC028 {{Exposing %s mapping properties - started.}}

ISEC029 changed from:
ISEC029 {{Exposing %s mapping properties, DONE.}}
to:
ISEC029 {{Exposing %s mapping properties - done.}}

ISEC116 changed from:
ISEC116 {{Preparing the SEC environment for "%s" strategy%s}}
to:
ISEC116 {{Preparing the SEC environment for "%s" strategy - %s.}}

ISPV116 changed from:
ISPV116 {{Preparing the SPV environment for "%s" strategy %s.}}
to:
ISPV116 {{Preparing the SPV environment for "%s" strategy - %s.}}

ISPV134 changed from:
ISPV134 {{SPV %s: %s.} {%s: %s.}}
to:
ISPV134 {{%s: %s.} {SPV %s: %s.}}

IVS019 changed from:
IVS019 {{Constraint inconsistency detected at cycle %u after adding target.} {Constraint inconsistency detected at cycle %u after adding configuration %s.} {Constraint inconsistency detected at cycle %u after setting\n minlength to %u.} {Constraint inconsistency detected at cycle %u after setting\n distinct state to %s.} {Constraint inconsistency detected at cycle %u after setting max_length to %u.}}
to:
IVS019 {{Constraint inconsistency detected at cycle %u after adding target.} {Constraint inconsistency detected at cycle %u after setting\n distinct state to %s.} {Constraint inconsistency detected at cycle %u after adding configuration %s.} {Constraint inconsistency detected at cycle %u after setting max_length to %u.} {Constraint inconsistency detected at cycle %u after setting\n minlength to %u.}}

IXP021 changed from:
IXP021 {{Preparing the X-Prop environment for "%s" strategy %s.}}
to:
IXP021 {{Preparing the X-Prop environment for "%s" strategy - %s.}}

VERI-2642 changed from:
VERI-2642 {{constant epression is not allowed in unique constraint}}
to:
VERI-2642 {{constant expression is not allowed in unique constraint}}

VERI-8005 changed from:
VERI-8005 {{Unintentional Sequential element inferred for %s read before write using blocking assignment}}
to:
VERI-8005 {{Unintentional sequential element inferred for %s read before write using blocking assignment}}

VERI-9104 changed from:
VERI-9104 {{building the expression can cause a stack overflow due to its length}}
to:
VERI-9104 {{building the expression can cause a stack overflow due to its length. Increase the stack size using Bash "ulimit -s %lu" or Csh "limit stacksize %lu" before running Jasper}}

WCD038 changed from:
WCD038 {{The text above was too large to be printed completely and has been truncated.\n The log file for the analysis session contains the entire result.\n Full path to the log file: %s} {The Tcl-result above was too large to be printed completely and has been truncated.\n The log file for the analysis session contains the entire result.\n Full path to the log file: %s}}
to:
WCD038 {{The Tcl-result above was too large to be printed completely and has been truncated.\n The log file for the analysis session contains the entire result.\n Full path to the log file: %s} {The text above was too large to be printed completely and has been truncated.\n The log file for the analysis session contains the entire result.\n Full path to the log file: %s}}

WCD047 changed from:
WCD047 {{Set configuration "%s" should be used before any design is analyzed.} {Set configuration "%s" before design elaboration.}}
to:
WCD047 {{Set configuration "%s" before design elaboration.} {Set configuration "%s" should be used before any design is analyzed.}}

WCK010 changed from:
WCK010 {{%sCannot proceed with the structural glitch analysis of register(s) "%s" due to complex logic found in clock scheme.} {%sThe signal "%s" is being used as an enable of gated clock(s) whose clock logic is driven by "%s".\n This might cause glitches as "%s" is not guaranteed to be stable during edge occurrences of "%s".} {%sCannot proceed with the structural glitch analysis of register(s) "%s" due to complex clock scheme found in "%s".} {%sThe signals "%s" and "%s" can cause glitches in the clock scheme of "%s".}}
to:
WCK010 {{%sThe signal "%s" is being used as an enable of gated clock(s) whose clock logic is driven by "%s".\n This might cause glitches as "%s" is not guaranteed to be stable during edge occurrences of "%s".} {%sCannot proceed with the structural glitch analysis of register(s) "%s" due to complex logic found in clock scheme.} {%sCannot proceed with the structural glitch analysis of register(s) "%s" due to complex clock scheme found in "%s".} {%sThe signals "%s" and "%s" can cause glitches in the clock scheme of "%s".}}

WCON001 changed from:
WCON001 {{Size mismatch in signals %s from connection "%s".}}
to:
WCON001 {{Size mismatch in signals "%s" and "%s" from connection "%s".\n Source width is %d, but destination width is %d. Width %d will be considered for analysis.}}

WCTR020 changed from:
WCTR020 {{An unwind limit on line {line} in file {fileName} is set both by "check_c2rtl -set_unwind_limit" and by #pragma {pragmaName}. The unwind limit will be {unwindLimit}.}}
to:
WCTR020 {{An unroll limit on line {line} in file {fileName} is set both by "check_c2rtl -set_unroll_limit" and by #pragma {pragmaName}. The unroll limit will be {unwindLimit}.}}

WCTR024 changed from:
WCTR024 {{Synthesis warnings found.}}
to:
WCTR024 {{Formal model generation warnings found.}}

WCTR025 changed from:
WCTR025 {{{warning}}}
to:
WCTR025 {{Formal model generation warning:\n {warning}}}

WDIN004 changed from:
WDIN004 {{In a future release, you will no longer be able to use the "precondition" attribute with "get_property_list" to include or exclude all types of related covers.\n Instead, the "precondition" attribute will refer to preconditions only.\n To include or exclude related covers, you will use the new "related_covers" attribute.\n\nUse "set_legacy_precondition_reporting off" to disable the legacy behavior, in which "preconditions" included or excluded all types of related covers, and enable the following new attributes:\n . late_precondition\n . infinite_precondition\n . witness\n . contrapositive\n . infinite_contrapositive}}
to:
WDIN004 {{In a future release, you will no longer be able to use the "precondition" attribute with "get_property_list" to include or exclude all types of related covers.\n Instead, to include or exclude related covers, you will use the new "related_covers" attribute.\n To include or exclude any type of related properties, use "related_property_type" and specify a list containing any of the following attributes:\n\n . precondition\n . late_precondition\n . infinite_precondition\n . witness\n . contrapositive\n . infinite_contrapositive\n . safety_in_liveness}}

WGI031 changed from:
WGI031 {{Target signal "%s" is a primary clock.} {Custom button with name "%s" does not exist in "%s" window.}}
to:
WGI031 {{Custom button with name "%s" does not exist in "%s" window.} {Target signal "%s" is a primary clock.}}

WHT008 changed from:
WHT008 {{The calculated job ratio between strategies resulted in 0 jobs for state_swarm.\n This value cannot be zero and will be adjusted to one.}}
to:
WHT008 {{The calculated job ratio between strategies resulted in 0 jobs for "%s".\n This value cannot be zero and will be adjusted to one.}}

WLPV087 changed from:
WLPV087 {{%s(%s): Unsupported supply power state "%s".} {%s(%s): Ignoring power state "%s". Simstate "%s" is not supported.}}
to:
WLPV087 {{%s(%s): Ignoring power state "%s". Simstate "%s" is not supported.} {%s(%s): Unsupported supply power state "%s".}}

WLPV093 changed from:
WLPV093 {{The command "%s" is deprecated.\n Use "check_lpv -load_query_upf_file" to call the command from a UPF file instead.}}
to:
WLPV093 {{The signal "{signal_name}" has {direction} supplies that are not tied to power domains.\n Use {supply_option} option to obtain the complete list of supplies.}}

WLPV098 changed from:
WLPV098 {{%s(%s): Scope "%s" belongs to a Liberty cell.\n UPF commands defined within it are not applied during power transformation.\n For message help type "help -message WLPV098".} {%s(%s): Repeater cell "%s" is from a rule without a supply specification. Assigning X value to its power enable pin.}}
to:
WLPV098 {{%s(%s): Repeater cell "%s" is from a rule without a supply specification. Assigning X value to its power enable pin.} {%s(%s): Scope "%s" belongs to a Liberty cell.\n UPF commands defined within it are not applied during power transformation.\n For message help type "help -message WLPV098".}}

WNL024 changed from:
WNL024 {{%s(%s): Pull-down device found for pull-up multiple driver.}}
to:
WNL024 {{Connect: unable to connect port "%s"}}

WNL025 changed from:
WNL025 {{%s(%s): Pull-up device found for pull-down multiple driver.}}
to:
WNL025 {{Connect: unable to connect unnamed port}}

WP2P001 changed from:
WP2P001 {{%s(%s): %s discarded due to unsynthesizable construct (%s)} {%s(%s): unsynthesizable construct: %s} {%s(%s): %s discarded due to unsynthesizable construct (%s)\n Unsynthesizable construct at: %s(%s)}}
to:
WP2P001 {{%s(%s): unsynthesizable construct: %s} {%s(%s): %s discarded due to unsynthesizable construct (%s)\n Unsynthesizable construct at: %s(%s)} {%s(%s): %s discarded due to unsynthesizable construct (%s)}}

WP2P005 changed from:
WP2P005 {{%s(%s): %s discarded due to unsupported construct (%s)\n Unsupported construct at: %s(%s)} {%s(%s): %s discarded due to unsupported construct (%s)} {%s(%s): unsupported construct: %s}}
to:
WP2P005 {{%s(%s): unsupported construct: %s} {%s(%s): %s discarded due to unsupported construct (%s)} {%s(%s): %s discarded due to unsupported construct (%s)\n Unsupported construct at: %s(%s)}}

WPF043 changed from:
WPF043 {{%s%u.%s: Internal limit reached.} {%s%u.%s: Internal limit reached at cycle %u. Engine has exited.} {%s%u.%s: Internal limit reached. Engine has exited.}}
to:
WPF043 {{%s%u.%s: Internal limit reached. Engine has exited.} {%s%u.%s: Internal limit reached at cycle %u. Engine has exited.} {%s%u.%s: Internal limit reached.}}

WPF082 changed from:
WPF082 {%s%s%s {Cannot convert the following related properties: "%s".}}
to:
WPF082 {{Cannot convert the following related properties: "%s".} %s%s%s}

WPM021 changed from:
WPM021 {{No properties matched the specified wildcard(s) "%s".}}
to:
WPM021 {{No properties matched the specified %s(s) "%s".}}

WSEC187 changed from:
WSEC187 {{Unable to create a mapping on blackbox output signal pair "%s -> %s" because the signals have different arithmetic operations. Ignoring the command.}}
to:
WSEC187 {{Unable to create a mapping on blackbox output signal pair "%s -> %s" because the signals have different arithmetic operations.\n Ignoring the command.}}

WSL061 changed from:
WSL061 {{Cannot find source location of a waiver: empty source or empty waiver content.} {Unable to update the waivers from block to SoC. Issue with module %s.}}
to:
WSL061 {{Unable to update the waivers from block to SoC. Issue with module %s.} {Cannot find source location of a waiver: empty source or empty waiver content.}}

WSL072 changed from:
WSL072 {{Command has reached its time-out limit and is being interrupted.\n See the documentation for "set_superlint_compute_deadcode_root_cause_overall_time_limit", or "set_superlint_compute_deadcode_root_cause_property_time_limit" for more information.} {Prove in the background, unreachable root cause debug is not supported.\n Use "check_superlint -prove" without -bg.}}
to:
WSL072 {{Prove in the background, unreachable root cause debug is not supported.\n Use "check_superlint -prove" without -bg.} {Command has reached its time-out limit and is being interrupted.\n See the documentation for "set_superlint_compute_deadcode_root_cause_overall_time_limit", or "set_superlint_compute_deadcode_root_cause_property_time_limit" for more information.}}

WSPV031 changed from:
WSPV031 {{The following signal in the from or to precondition of property "%s" is in the fanout of the from signals: %s. This might cause incorrect results.\n Create a new property using "-keep_driving_logic" to resolve this issue.}}
to:
WSPV031 {{The following signal(s) in the from or to precondition of property "%s" are in the fanout of the from signals:\n %s.\n This might result in an invalid cex.\n Create a new property using "-keep_driving_logic" to resolve this issue.\n For message help, type "help -message WSPV031".}}

WSPV036 changed from:
WSPV036 {{Unable to create the SPV abstraction for instance "%s" because it conflicts with another SPV abstraction, "%s" in task "%s".\n You cannot use "-to" signals in multiple SPV abstractions.} {Unable to create the SPV abstraction for instance "%s" because it conflicts with another SPV abstraction, "%s" in the global environment.\n You cannot use "-to" signals in multiple SPV abstractions.}}
to:
WSPV036 {{Unable to create the SPV abstraction for instance "%s" because it conflicts with another SPV abstraction, "%s" in the global environment.\n You cannot use "-to" signals in multiple SPV abstractions.} {Unable to create the SPV abstraction for instance "%s" because it conflicts with another SPV abstraction, "%s" in task "%s".\n You cannot use "-to" signals in multiple SPV abstractions.}}

––––––––––––––––––––
| version : v2023.03p001 |
| frozen on : Apr 18, 2023 |
––––––––––––––––––––

ENHANCEMENTS
============
The following new features and enhancements are included in Jasper(TM) Apps
2023.03p001.

C to RTL Equivalence Checking (C2RTL) App
––––––––––––––––––––-
* C2RTL Now Uses Platform "save" and "restore" Commands

C2RTL now supports the following Jasper platform "save" and "restore"
commands:

. save -elaborated_design
. restore -elaborated_design
. save -jdb database -capture_session_data [-no_setup]
. restore -jdb

These are the only platform "save" and "restore" commands supported
by the C2RTL App.

Clock Domain Crossing (CDC) App
–––––––––––––––-
* Parameter for Rounding Value of Clock Periods in SDC Files

This release introduces a new CDC parameter "round_sdc_clock_periods". If this
parameter is "true", the values of clock periods and waveforms in SDC files
are rounded to match Jasper clock factors and phases as closely as possible
while still maintaining their proportions. The default value for this
parameter is "false".

Superlint App
––––––-
* SIG_IS_INIT Moved to DFT_FUNCTIONAL Category

With this release, the SIG_IS_INIT check has been moved from the STRUCTURAL
category to the DFT_FUNCTIONAL category.

* New Superlint Checks

This release adds the CLK_IS_DRCK check to the DFT_FUNCTIONAL category:

CLK_IS_DRCK (Warning): "User-declared clock '%h' is driving another user-
declared clock '%h'"

Design Compilation
–––––––––
* Support for Blackboxing 1D Arrays

Starting with the 2023.03 FCS release, Jasper supports blackboxing 1D arrays.
Use the following command:

"compilation -config -module <mod> -array <array> {blackbox (0 | 1)}".

Refer to the "compilation" TclHelp for command details:
% help compilation -gui

Infrastructure
–––––––
* Improved Message Printed when Jasper Exits Unexpectedly

The INFO message printed to stderr when Jasper writes a crash dump file has
been changed. It now spans multiple lines and prompts you to run a command
that converts the dump file to a human readable text file that contains the
stack traces. The message follows:

INFO: A crash dump was written to the following path: <dump-file>
Run '<install-dir>/bin/jg_stackwalker <dump-file> > <dump-dir>/jg_stackwalker.txt'
and provide Cadence with this file for further debugging.

. <dump-file> is the name of the dump file.
. <install-dir> is the Jasper installation directory.
. <dump-dir> is the directory in which the dump file was written.

NOTE: <dump-dir> is normally the Jasper project directory or a directory
inside the project directory.

RESOLVED ISSUES
===============
The following reported issues have been fixed in 2023.03p001.

C to RTL Equivalence Checking (C2RTL) App
––––––––––––––––––––-
* pow(double,int) Now Compiled as Expected

C2RTL now correctly complies function pow(double,int) from <cmath> when
compiling C++ programs.

Clock Domain Crossing (CDC) App
–––––––––––––––-
* Improved RST_RS_RIDP Check

The tool longer reports RST_RS_RIDP violations on flops that are not connected
directly to the reset signal but, instead, have another flop between them and
the reset.

Connectivity Verification App
––––––––––––––-
* Resolved Issue with "check_conn -signoff" Console Output Size

The tool no longer exits unexpectedly when the console output of "check_conn
-signoff -port" is too large.

Coverage App
––––––
* Improve Coverage App Messaging

WCOV063 is deprecated, and the COV App now issues WCOV106 when a Covergroup
will not be added or removed because it is in an excluded instance.

* Covergroup Properties Now Copied as Expected

Prior to this change, if the top had two instances with Covergroups, but one
instance was excluded using "check_cov -init -exclude_instances", the
Covergroups of the instance that was not excluded would be present in the
<embedded> task. However, when you subsequently attempted to copy this task,
the new task had no Covergroups. This patch resolves the issue.

* Resolved Issue with Jasper/IMC Merge of VHDL

With this release, you can now merge Jasper and simulator databases for VHDL
blocks.

* Improved Coverage App Merge of Structure Literals to Unicov

The Coverage App is now able to correctly dump multidimensional
and one-dimensional structure literals in the Unicov database.

Functional Safety Verification (FSV) App
––––––––––––––––––––
* Overconstraint No Longer Produces Invalid Results

Now, if the tool finds an overconstraint during a proof, all checks proven
with that "prove" command are marked "Unknown" and the proof stops.

* FSV Design Hierarchy Now Updated Automatically

The FSV GUI design hierarchy is now updated automatically without the need to
manually refresh it.

Sequential Equivalence Checking (SEC) App
––––––––––––––––––––-
* Resolved Issue with Reading Traces from Cache

This release resolves an issue what might have previously caused Jasper to
misread traces from the cache.

* Resolved Unexpected ENL108 Errors

This release fixes unexpected ENL108 elaboration errors affecting "-inst_top"
scenarios without "-top" specification.

X-Propagation (XPROP) Verification App
–––––––––––––––––––
* Resolved Issue with EMTR354 Errors

X-Prop no longer attempts to prove properties defined with a sampling clock
when one of the signals in the "to" or "to_precondition" is a clock signal.

Deep Bug Hunting
––––––––
* Resolved Issue with Progressive Memory Consumption in Main Session

In previous versions, you might have seen a progressive memory increase in
the Jasper session when running "hunt -auto" or "hunt trace_swarm" strategies.
This release resolves the issue.

Infrastructure
–––––––
* All "/bin/sh" References Moved to "/bin/bash"

This patch resolves issues with shell scripts shipped with Jasper that might
have previously used the incorrect shell interpreter on systems where
"/bin/sh" does not refer to "bash". The affected scripts now explicitly use
"/bin/bash" instead of "/bin/sh".

Changes in Messaging
====================
Also see sections above.

***** Messages That Were Introduced in the Current Version *****
WCOV106: warning {WCOV106 {{Covergroup bin "%s" will not be added/removed like user covers because it is in an excluded instance.}}}
WSR015: warning {WSR015 {{The {component} of database "{database}" is not compatible with this version of {tool}.\n Database version: {databaseVersion} ({tool} {currentVersion}). Supported version: "{expectedDatabaseVersion} (since {tool} {expectedToolVersion})".}}}
WXPR006: warning {WXPR006 {{Unable to prove the following properties: %s.\n Currently, the X-Prop App does not support properties that have a sampling clock and a "-to" or "-to_precondition" that are clock signals.}}}
––-

***** Messages with a Change to the Default Text *****
EFSV091 changed from:
EFSV091 {{FSV does not support the "save" command after "check_spv -init -no_miter".}}
to:
EFSV091 {{FSV does not support the "save" command after "check_fsv -init -no_miter".}}

ESR005 changed from:
ESR005 {{Unable to open database directory "%s". Database is locked by another session.} {Cannot restore database "%s". Check format and version of database file.}}
to:
ESR005 {{Cannot restore database "%s". Check format and version of database file.} {Unable to open database directory "%s". Database is locked by another session.}}

Base_JASPER23.03.000_lnx86
Update_JASPER23.03.001_lnx86

Bonus: Update_JASPER22.12.001_lnx86