Project

General

Profile

Task #5886

Remove redundant invariant conditions on variables

Added by Igor Melnichenko over 5 years ago. Updated over 5 years ago.

Status:
Closed
Priority:
Normal
Assignee:
Category:
Engine (Parser)
Target version:
Start date:
04/29/2015
Due date:
% Done:

100%

Estimated time:
Detected in build:
svn
Published in build:
20150701

Description

Extracted EFSMs would be simpler without invariant conditions which duplicate constraints directly derived from types of corresponding variables.
For example, VHDL declararions of the form "variable: in bit;" are now translated to constraint "(OR (EQ variable 1) (EQ variable 0))" which may be painlessly excluded from EFSM.

History

#1

Updated by Sergey Smolov over 5 years ago

  • Status changed from New to Feedback

In which parts of the extracted EFSMs did you find the redundant invariant conditions?

#2

Updated by Igor Melnichenko over 5 years ago

Sergey Smolov wrote:

In which parts of the extracted EFSMs did you find the redundant invariant conditions?

For example, the invariants map of b01: {STATO=(AND (GREATEREQ STATO 0) (LESSEQ STATO 7)), LINE1=(OR (EQ LINE1 1) (EQ LINE1 0)), LINE2=(OR (EQ LINE2 1) (EQ LINE2 0)), RESET=(OR (EQ RESET 1) (EQ RESET 0)), OUTP=(OR (EQ OUTP 1) (EQ OUTP 0)), OVERFLW=(OR (EQ OVERFLW 1) (EQ OVERFLW 0)), CLOCK=(OR (EQ CLOCK 1) (EQ CLOCK 0))}

#3

Updated by Sergey Smolov over 5 years ago

So you mean that there is no need in invariants for Boolean and BIT_VECTOR(1) types, isn't it?

Of course I'm talking about the "general" invariants which cover all values of the specified type like "x true OR x false" for booleans.

#4

Updated by Sergey Smolov over 5 years ago

  • Status changed from Feedback to Open
#5

Updated by Sergey Smolov over 5 years ago

  • Status changed from Open to Resolved
  • % Done changed from 0 to 100

Done in r1986.

#6

Updated by Igor Melnichenko over 5 years ago

  • Status changed from Resolved to Verified
#7

Updated by Sergey Smolov over 5 years ago

  • Status changed from Verified to Closed
  • Published in build set to 20150701

Also available in: Atom PDF