Feature #9335: cgaa-assert-extractor engine - Retrascope - Open-Source Projects

Actions

Copy link

Feature #9335

closed

cgaa-assert-extractor engine

Added by Sergey Smolov about 6 years ago. Updated over 5 years ago.

Status:

Closed

Priority:

Normal

Assignee:

Mikhail Lebedev

Category:

Engine (Extractor)

Target version:

1.0

Start date:

10/18/2018

Due date:

% Done:

100%

Estimated time:

Published in build:

1.1.1-beta-190722

Description

Engine that extracts 'is-def' and 'is-use' constraints for every variable of every process of the design.
The extracted data should be printed to stdout in text format, like the following:

variable 'x'
============

process_1
------------
is_def_x = <SMT-LIB format formulae>
is_use_x = <SMT-LIB format formulae>

process_2
------------
....

variable 'y'
============

process_3
------------
is_def_y = <SMT-LIB format formulae>
is_use_y = <SMT-LIB format formulae>

process_4
------------
....