Static Analysis
System code goes though some code quality checks.
Consistency Checking
Specs are checked for consistency. A warning is produced if specs may be unsatisfiable:
signal x: Float
spec main = always (x > 0 && x < 0)
This means that the specification is problematic, because it is impossible that any system satisfies this specification.
Inconsistencies between specs are also reported to the user:
signal x: Float
spec always_positive = always (x > 0)
spec always_negative = always (x < 0)
In this case each of the specs are satisfiable on their own, but taken together they cannot be satisfied by any system.
Redundancy Checking
If one spec is redundant, because implied by other specs of the system, this is also detected:
signal x: Float
spec positive_becomes_negative = always (x > 0 => eventually x < 0)
spec sometimes_positive = eventually x > 0
spec sometimes_negative = eventually x < 0
In this case we warn the user that the spec sometimes_negative is redundant, because this property is already implied by the combination of positive_becomes_negative and sometimes_positive. Indeed sometimes_positive implies that there is some point in time where x > 0, and using positivie_becomes_negative we conclude that therefore there must be some point in time after than when x < 0.