Project

General

Profile

Feature #3724

Unable to use SAT/SMT features of NuXMV

Added by Anonymous over 1 year ago. Updated about 1 year ago.

Status:
New
Priority:
Normal
Assignee:
-
Category:
-
Target version:
Start date:
04/28/2019
Due date:
% Done:

0%

Estimated time:

Description

While there is provision to add infinite state variables like unbounded integers and reals, formal verification doesn't work for designs since only check_property command is generated and executed using NuSMV/NuXMV. Feature to use other SAT/SMT commands can be added.

History

#1 Updated by Johannes Eder over 1 year ago

  • Target version changed from AF3 2.15 Release to AF3 2.16 RC1 (Feature Freeze)

#2 Updated by Simon Barner about 1 year ago

  • Assignee deleted (Anonymous)
  • Target version changed from AF3 2.16 RC1 (Feature Freeze) to Backlog

Also available in: Atom PDF