Ciircuit Verification using Temporal Logic: Specification and Implementation (or design) are two descriptions of a system at two different levels of abstraction - the specification being at a higher level and the implementation at a lower abstraction level. Formal Verification of an implementation (or a design) of system involves mathematically proving that the implementation implies the specification. This necessitates representing the specification as well the implementation in terms of formulae of some mathematical logic formalism. It is common to use Interval Temporal Logic (ITL) formulae (say, S) to capture the behavioural specification of a circuit. The implementation (or design) of the circuit, on the other hand, can be conceived as an interconnection network of components having known behaviour. Consequently, the implementation (that is, the interconnection network of the components and behaviour of those components) too can be captured as formulae (say, I) of Interval Temporal Logic. The circuit verfication problem, in that case, reduces to formally proving that I implies S.
Created: 23 November 2019
Vidwan
Orcid