Task #5886
closed
Remove redundant invariant conditions on variables
Added by Igor Melnichenko about 9 years ago.
Updated almost 9 years ago.
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.
- Status changed from New to Feedback
In which parts of the extracted EFSMs did you find the redundant invariant conditions?
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))}
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.
- Status changed from Feedback to Open
- Status changed from Open to Resolved
- % Done changed from 0 to 100
- Status changed from Resolved to Verified
- Status changed from Verified to Closed
- Published in build set to 20150701
Also available in: Atom
PDF