Formal Framework for Hardware Safety Requirement Verification

We aim at building a formal framework to specify, describe and verify circuits embedded into safety critical systems. We extend current verification techniques that make possible to prove circuit design correctness is such a way that enables to prove that circuits behave safely. Correct circuits are only checked design fault free whereas circuits are safe if they behave correctly even when faults occurs at runtime. This has yet not been formalised. To bridge this gap, we model circuits, formalise their faults, define how the latter occur on circuits and express the safety properties circuits have to verify within a formal framework. We use the circuits as predicates paradigm in which circuit behaviour is defined by predicates. Fault semantics is then given in terms of predicate transformers as circuit behaviour could be modified when faults occur. Finally, this allows us to define formally the safety property by means of circuit behaviour stability or co-stability when faults occur on them.