Project

General

Profile

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
------------
....

Actions
Copy link

Also available in: Atom PDF