http://iet.metastore.ingenta.com
1887

Formal verification of NCL circuits

Formal verification of NCL circuits

For access to this article, please select a purchase option:

Buy chapter PDF
$16.00
(plus tax if applicable)
Buy Knowledge Pack
10 chapters for $120.00
(plus taxes if applicable)

IET members benefit from discounts to all IET publications and free access to E&T Magazine. If you are an IET member, log in to your account and the discounts will automatically be applied.

Learn more about IET membership 

Recommend Title Publication to library

You must fill out fields marked with: *

Librarian details
Name:*
Email:*
Your details
Name:*
Email:*
Department:*
Why are you recommending this title?
Select reason:
 
 
 
 
 
Asynchronous Circuit Applications — Recommend this title to your library

Thank you

Your recommendation has been sent to your librarian.

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

Preview this chapter:
Zoom in
Zoomout

Formal verification of NCL circuits, Page 1 of 2

| /docserver/preview/fulltext/books/cs/pbcs061e/PBCS061E_ch15-1.gif /docserver/preview/fulltext/books/cs/pbcs061e/PBCS061E_ch15-2.gif

Related content

content/books/10.1049/pbcs061e_ch15
pub_keyword,iet_inspecKeyword,pub_concept
6
6
Loading
This is a required field
Please enter a valid email address