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 almost 10 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 almost 10 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 almost 10 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 almost 10 years ago
- Status changed from Feedback to Open
Updated by Sergey Smolov almost 10 years ago
- Status changed from Open to Resolved
- % Done changed from 0 to 100
Done in r1986.
Updated by Igor Melnichenko almost 10 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