Semi-formal specifications and formal verification improving the digital design: some statistics

摘要

In this work, an improvement of the traditional digital design methodology is proposed. The major change is the use of a semi-formal specification for the code implementation, the use of a verification tool and the establishment of properties for the formal verification of Finite State Machines (FSM). From semi-formal specifications, assertions were written using Property Specification Language (PSL) for an alignment circuit. Finally, a set of properties for the verification of this module were established and proved using a model checking tool. Our statistics proved that the whole design process was improved and considerable design time was saved.