In this chapter, the author describe an equivalence checking methodology for NULL Convention Logic (NCL) circuits. Note that currently, there are no commercial equivalence checkers for quasi-delay insensitive (QDI) circuits. For commercial applications, NCL circuits, and QDI circuits in general, are often synthesized from synchronous intellectual property designs. The resulting NCL design may then be further optimized and tinkered with. Therefore, the author have designed an equivalence checker that can be used in two ways: (1) to verify the functional equivalence of two NCL designs and (2) to verify the equivalence between an NCL design and a synchronous design.

Chapter Contents:

• 15.1 Overview of approach
• 15.2 Related verification works for asynchronous paradigms
• 15.3 Equivalence verification for combinational NCL circuits
• 15.3.1 Functional equivalence check
• 15.3.2 Invariant check
• 15.3.3 Handshaking check
• 15.3.4 Input-completeness check
• 15.3.4.1 Input-completeness proof obligation: NULL to DATA
• 15.3.4.2 Input-completeness proof obligation: DATA to NULL
• 15.3.4.3 Input-completeness results
• 15.3.5 Observability check
• 15.3.5.1 Observability proof obligation: NULL to DATA
• 15.3.5.2 Observability proof obligation: DATA to NULL
• 15.3.5.3 Observability results
• 15.4 Equivalence verification for sequential NCL circuits
• 15.4.1 Safety
• 15.4.2 Liveness
• 15.4.3 Sequential NCL circuit results
• 15.5 Conclusions and future work
• References

Inspec keywords: formal verification; logic design; logic circuits

Other keywords: equivalence checker; QDI circuits; NULL convention logic circuits; NCL circuits; formal verification; equivalence checking methodology; quasi-delay insensitive circuits; NCL design; synchronous design

Subjects: Formal methods; Logic design methods; Logic and switching circuits; Digital circuit design, modelling and testing; Logic circuits