Citation: | ZHANG Nan, DUAN Zhenhua, TIAN Con. Verifying a Carry Look-Ahead Adder with Propositional Projection Temporal Logic[J]. Chinese Journal of Electronics, 2013, 22(1): 21-24. |
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)
|