An automated formal verification approach for ensuring input completeness of NULL Convention Logic (NCL) circuits is proposed. NCL circuits have the benefit that they can operate in extreme environments where traditional synchronous circuits fail due to significant fluctuations in circuit timing. Input completeness is a critical property to ensure correct functioning of NCL circuits in extreme environments and therefore is required to be verified. Note that an NCL circuit can be functionally correct and still not be input complete, which could cause the circuit to operate correctly under normal conditions, but malfunction only when the circuit timing is substantially changed (e.g. operating in a very hot or cold environment such as outer space).

References

1. 1)
  - 8. Wijayasekara, V.M., Srinivasan, S.K., Smith, S.C.: ‘Equivalence verification for null convention logic (NCL) circuits’. 2014 IEEE 32nd Int. Conf. on Computer Design (ICCD), Seoul, South Korea, October 2014, pp. 195–201.
2. 2)
  - 11. Barrett, C., Fontaine, P., Tinelli, C.: ‘The SMT-LIB standard: version 2.6’. Tech. Rep., Department of Computer Science, The University of Iowa, 2017. Available at www.SMT-LIB.org.
3. 3)
  - 10. ‘ISCAS-85 c432 27-channel interrupt controller’. Available at http://web.eecs.umich.edu/~jhayes/iscas.restore/c432.html.
4. 4)
  - 5. Smith, S.C., Di, J.: ‘Designing asynchronous circuits using null convention logic (NCL)’, Synth. Lect. Digit. Circuits Syst., 2009, 4, (1), pp. 1–96. Available at https://doi.org/10.2200/S00202ED1V01Y200907DCS023 (doi: 10.2200/S00202ED1V01Y200907DCS023).
5. 5)
  - 13. Smith, S.C., DeMara, R.F., Yuan, J.S., et al: ‘Delay-insensitive gate-level pipelining’, Integr. VLSI J., 2001, 30, (2), pp. 103–131 (doi: 10.1016/S0167-9260(01)00013-X).
6. 6)
  - 2. Di, J., Smith, S.C.: ‘Asynchronous digital circuits’ in Mead, C.A., Conway, L.A. (Eds.), ‘Extreme environment electronics’ (CRC Press, 2012), pp. 663–673.
7. 7)
  - 7. Kondratyev, A., Neukom, L., Roig, O., et al: ‘Checking delay-insensitivity: 104 gates and beyond’. Proc. Eighth Int. Symp. on Asynchronous Circuits and Systems, Manchester, UK, April 2002, pp. 149–157.
8. 8)
  - 9. Wijayasekara, V.M., Rollie, A.T., Hodges, R.G., et al: ‘Abstraction techniques to improve scalability of equivalence verification for NCL circuits’, Electron. Lett., 2016, 52, (19), pp. 1594–1596 (doi: 10.1049/el.2016.1138).
9. 9)
  - 1. Fant, K.M., Brandt, S.A.: ‘Null convention logictm: a complete and consistent logic for asynchronous digital circuit synthesis’. Proc. of Int. Conf. on Application Specific Systems, Architectures and Processors, 1996. ASAP 96, Chicago, IL, USA, August 1996, pp. 261–273.
10. 10)
  - 6. Jeong, C., Nowick, S.M.: ‘Optimization of robust asynchronous circuits by local input completeness relaxation’. 2007 Asia and South Pacific Design Automation Conf., Yokohama, Japan, January 2007, pp. 622–627.
11. 11)
  - 4. Seitz, C.L.: ‘System timing’, ‘Introduction to VLSI systems’ (Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1979), pp. 218–262.
12. 12)
  - 3. Smith, S.C., DeMara, R.F., Yuan, J.S., et al: ‘Optimization of NULL convention self-timed circuits’, Integr. VLSI J., 2004, 37, (3), pp. 135–165. Available at http://dx.doi.org/10.1016/j.vlsi.2003.12.004 (doi: 10.1016/j.vlsi.2003.12.004).
13. 13)
  - 12. De Moura, L., Bjørner, N.: ‘Z3: an efficient SMT solver’. International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Budapest, Hungary, 29 March–6 April 2008, pp. 337–340. Available at http://dl.acm.org/citation.cfm?id=1792734.1792766.

Automated verification of input completeness for NCL circuits

References

Related content