Verifying a Carry Look-Ahead Adder with Propositional Projection Temporal Logic

ZHANG Nan; DUAN Zhenhua; TIAN Con

Article Contents

Article Navigation > Chinese Journal of Electronics > 2013 > 22(1): 21-24

ZHANG Nan, DUAN Zhenhua, TIAN Con, “Verifying a Carry Look-Ahead Adder with Propositional Projection Temporal Logic,” Chinese Journal of Electronics, vol. 22, no. 1, pp. 21-24, 2013,

Citation:

ZHANG Nan, DUAN Zhenhua, TIAN Con, “Verifying a Carry Look-Ahead Adder with Propositional Projection Temporal Logic,” Chinese Journal of Electronics, vol. 22, no. 1, pp. 21-24, 2013,

ZHANG Nan, DUAN Zhenhua, TIAN Con, “Verifying a Carry Look-Ahead Adder with Propositional Projection Temporal Logic,” Chinese Journal of Electronics, vol. 22, no. 1, pp. 21-24, 2013,

Citation:

ZHANG Nan, DUAN Zhenhua, TIAN Con, “Verifying a Carry Look-Ahead Adder with Propositional Projection Temporal Logic,” Chinese Journal of Electronics, vol. 22, no. 1, pp. 21-24, 2013,

PDF( 217 KB)

Verifying a Carry Look-Ahead Adder with Propositional Projection Temporal Logic

1.
Institute of Computing Theory and Technology, Xidian University, Xi’an 710071, China;
2.
National Key Laboratory on Integrated Services Network, Xidian University, Xi’an 710071, China

Funds: This work is supported by the National Basic Research Program of China (973 Program) (No.2010CB328102), the National Natural Science Foundation of China (No.61133001, No.60910004, No.61003078), and Foundation of National Key Laboratory on Integrated Services Network (No.ISN1102001).

Received Date: 2012-03-01
Rev Recd Date: 2012-05-01
Publish Date: 2013-01-05

Abstract

Abstract

This paper presents a case study for verifying a carry look-ahead adder using the axiom system of Propositional projection temporal logic (PPTL). To this end, the syntax, semantics and axiom system of PPTL are briefly introduced. Further, functions and architectures of the carry look-ahead adder are presented. In addition, four lemmas are proved with the axiom system of PPTL. Finally, the correctness of the adder is verified based on the lemmas and the axiom system of PPTL. The case study shows that the axiom system for PPTL is workable.
- Carry look-ahead adder,
- Verification,
- Temporal logic,
- Theorem proving

FullText(HTML)

References(16)

References

D. Cyluk, “Inverting the abstraction mapping: A methodologyfor hardware verification”, Proc. of the 1st International Conferenceon Formal Methods in Computer Aided Design, LNCS1166, Palo Alto, CA, pp.172-186, 1996.

S.P. Miller, M.K. Srivas, “Formal verification of the AAMP5microprocessor: A case study in the industrial use of formalmethods”, WIFT’95: Workshop on Industria-Strength FormalSpecification Techniques, Boca Raton, FL, pp.2-16, 1995.

J. Hooman, “Verifying Part of the ACCESS. bus Protocol UsingPVS”, Proc. of the 15th Conference on the Foundations ofSoftware Technology and Theoretical Computer Science, LNCS1026, Bangalore, India, pp.96-110, 1995.

S. Park, D.L. Dill, “Verification of the FLASH cache coherenceprotocol by aggregation of distributed transactions”, Proc. ofthe 8th ACM Symposium on Parallel Algorithm and Architectures,Padua, Italy, pp.288-296, 1996.

H. Ruess, “Hierarchical verification of two-dimensional highspeedmultiplication in PVS: A case study”, Proc. of the 1st InternationalConference on Formal Methods in Computer AidedDesign, LNCS 1166, Palo Alto, CA, USA, pp.79-93, 1996.

N. Shankar, “Verification of real time systems using PVS”, Proc.of Computer Aided Verification, CAV’93, LNCS 697, Elounda,Greece, pp.280-291, 1993.

B.L. Di Vito, R.W. Butler, “Formal techniques for synchronizedfault-tolerant system”, Proc. of Dependable Computingfor Critical Applications-3, Volume 8 of Dependable Computingand Fault-Tolerant System, Vienna, Austria, pp.163-188, 1992.

A. Gupta, “Formal hardware verification methods: A survey”,Journal of Formal Methods in System Design, Vol.1, No.2-3,pp.151-238, 1992.

P.S. Miner, S.D. Johnson, “Verification of an optimized faulttolerantclock synchronization circuit: A case study exploringthe boundary between formal reasoning systems”, Proc. of the3rd Workshop on Designing Correct Circuits, Bastad, Sweden,1996.

Z. Duan, Temporal Logic and Temporal Logic Programming,Science Press, Beijing, 2005.

B.C. Moszkowski, Executing Temporal Logic Programs, CambridgeUniversity Press, Cambridge, 1986.

Z. Duan, N. Zhang, M. Koutny, “A complete proof system forpropositional projection temporal logic”, Theoretical ComputerScience, 2012. doi: 10.1016/j.tcs.2012.01.026

D. Kapur, M. Subramaniam, “Mechanical verification of addercircuits using powerlists”, Journal of Formal Methods in SystemDesign, Vol.13, No.2, pp.127-158, 1998.

H. Chen, R. Wu, “A fast multi-bit RCLA suitable for VLSI implementation”,Acta Electronica Sinica, Vol.20, No.2, pp.83-86,1992. (in Chinese)

D. Yang, Y. Xie, G. Chen, “Built-in self-test for VLSI pipelinedlattice digital filter”, Acta Electronica Sinica, Vol.35, No.11,pp.2184-2188, 2007. (in Chinese)

S. Jia, F. Liu, L. Liu et al., “Algorithm and structure design oflogarithmic skip adder”, Acta Electronica Sinica, Vol.31, No.8,pp.1186-1189, 2003. (in Chinese)

Relative Articles

Supplements(0)

Cited By

Proportional views