Task #5886
closedRemove redundant invariant conditions on variables
100%
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.
Updated by Sergey Smolov over 9 years ago
- Status changed from New to Feedback
In which parts of the extracted EFSMs did you find the redundant invariant conditions?
Updated by Igor Melnichenko over 9 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))}
Updated by Sergey Smolov over 9 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.
Updated by Sergey Smolov over 9 years ago
- Status changed from Open to Resolved
- % Done changed from 0 to 100
Done in r1986.
Updated by Igor Melnichenko over 9 years ago
- Status changed from Resolved to Verified
Updated by Sergey Smolov over 9 years ago
- Status changed from Verified to Closed
- Published in build set to 20150701