Formal Coverage TSV

Simscope can track results of Formal property assertions/coverage (ie proofs).

→ See also Functional/Line TSV example

Note: if using Jasper for formal, please contact VerOps to use a jasper_parse_simscope.py formal parsing script.

Screenshot

Here is an sample Formal coverage database screenshot:

Formal TSV Fields

Formal coverage uses the following fields to describe properties:

Field	Type	Description	Example Values
`name`	string	Name of the formal property (with hierarchy).	`top.iconnect.genblk1.assert`
`group`	string	Group to organize this property.	`top`
`type`	string	Type of the property.	`assert`, `formal`, `assumption`
`engine`	string	Engine used to evaluate the property.	`abc`
`result`	string	Result of the property evaluation.	`proven`, `cex`, etc.
`bound`	int	Number of cycles the property processed until.	`10`
`time_seconds`	float	Engine time spent processing the property (in seconds).	`100.23` (ie 1min 40sec)
`status`	string	Final status of the property (see Status below).	`pass` / `fail` / `partial` / `ignore`

Type

The type field describes the property type. This can contain any string value, but the common values are:

assumption
assert
cover

Result

The result field describes the final result from processing the formal properties.

This can be any string value, but the common result values are:

Assumptions
- approved
- temporary
Assertions
- proven
- marked_proven
- cex
- ar_cex
- undetermined
- unprocessed (also called disabled)
- error
Covers
- unreachable
- covered
- ar_covered
- undetermined
- unprocessed
- error

Status

The status field determines how Simscope scores each property.

The scores of all properties are collected under each group and overall for the database.

Status	Description
`ignore`	Assumptions (ignored from scoring)
`pass`	`proven` assertions or `covered` covers
`fail`	`cex` (ie counterexample)
`partial`	Bounded proofs: note the `bound` value describes the cycle

Bounded Proofs (partial results)

For Bounded Proof properties, where the cycle value determines pass/fail status:

Set the result to undetermined
Set the status to partial
Set the bound to a cycle value, like 25

At display time, Simscope will calculate a pass/fail on the property, if this value exceeds the minimum_cycles threshold.

Example scenarios:

minimum_cycles is 10 and property bound is 5 → property computed as fail
minimum_cycles is 10 and property bound is 12 → property computed as pass

Formal TSV Example File

Here is an example formal TSV file with 4 properties:

Note: the TSV file format uses the [tab] keyboard character between fields (not spaces or commas).

name	group	type	engine	result	bound	time_seconds	status
top.iconnect..AXI_MASTER_MAGIC_ADDR_STABLE_prop	xbar_fab_port	assumption	?	temporary		0.000	ignore
top.iconnect.genblk33.genblk2.AXI_MAGIC_ID_ARVALID_prop:precondition1	xbar_fab_port	cover	Bm	covered	2	2.194	pass
xbar_fab_port.CHK_iconnect_no_read_interleaving.genblk1.p	xbar_fab_port	formal	Bm	undetermined	30 -	8533.987	partial
top.iconnect.genblk1.genblk21.AXI_ERRS_rid_STABLE_prop	xbar_fab_port	assert	Ncustom6	proven	Infinite	6.172	pass

Publishing

To publish formal coverage TSV files into Simscope, see the Data Integration topic.

Simscope Administration Guide