Page 234 - 《软件学报》2021年第6期

1808 Journal of Software 软件学报 Vol.32, No.6, June 2021

[3] Parsons S, Taylor DE, Schuehler DV, Franklin MA, Chamberlain RD. High speed processing of financial information using FPGA
devices. United States Patent US8655764 B2. 2013.
[4] Guan Y, Yuan Z, Sun G, Cong J. FPGA-Based accelerator for long short-term memory recurrent neural networks. In: Proc. of the
22nd Asia and South Pacific Design Automation Conf. IEEE, 2017. 629−634.
[5] Ma YF, Suda N, Cao Y, Seo J, Vrudhula S. Scalable and modularized RTL compilation of convolutional neural networks onto
FPGA. In: Proc. of the 26th Int’l Conf. on Field Programmable Logic and Applications. IEEE, 2016. 1−8.
[6] Tolba MF, AbdelAty AM, Soliman NS, Said LA, Madian AH, Azar AT, Radwan AG, et al. FPGA implementation of two fractional
order chaotic systems. AEU—Int’l Journal of Electronics and Communications, 2017,78:162−172.
[7] Hu J, Li T, Li S. Equivalence checking between SLM and RTL using machine learning techniques. In: Proc. of the 17th Int’l Symp.
on Quality Electronic Design. Santa Clara: IEEE, 2016. 129−134.
[8] Vasudevan S, Abraham JA, Viswanath V, Tu JJ. Automatic decomposition for sequential equivalence checking of system level and
RTL descriptions. In: Proc. of the 4th ACM and IEEE Int’l Conf. on Formal Methods and Models for Co-design. Napa: IEEE, 2006.
71−80.
[9] Marquez CIC, Strum M, Chau WJ. Formal equivalence checking between high-level and RTL hardware designs. In: Proc. of the
14th Latin American Test Workshop (LATW). Cordoba: IEEE, 2013. 1−6.
[10] Yang Z. Scalable equivalence checking for behavioral synthesis [Ph.D. Thesis]. Broadway: Portland State University, 2015.
[11] Wang Z, Li C, Hu S, Man J. A framework on runtime verification for software behavior. In: Proc. of the 2nd Int’l Conf. on
Intelligent System Design and Engineering Application. Sanya: IEEE, 2012. 20−23.
[12] Duan ZH, Yang X, Koutny M. Framed temporal logic programming. Science of Computer Programming, 2008,70(1):31−61.
[13] Duan ZH, Koutny M. A framed temporal logic programming language. Journal of Computer Science and Technology, 2004,19(3):
341−351.
[14] Duan ZH. Temporal logic and temporal logic programming. Beijing: Science Press, 2005.
[15] Duan ZH, Tian C, Zhang N. A canonical form based decision procedure and model checkingapproach for propositional projection
temporal logic. Theoretical Computer Science, 2016,609:544−560.
[16] Yang K, Duan ZH, Tian C, Zhang N. A compiler for MSVL and its applications. Theoretical Computer Science, 2018,749:2−16.
[17] Duan ZH, Tian C. A practical decision procedure for propositional projection temporal logic with infinite models. Theoretical
Computer Science, 2014,554:169−190.
[18] Duan ZH, Tian C. A unified model checking approach with projection temporal logic. In: Proc. of the Int’l Conf. on Formal
Engineering Methods. Berlin, Heidelberg: Springer-Verlag, 2008. 167−186.
附录 1. 信号灯控制电路系统 Verilog 代码

顶层模块 output [5:0] count;
`include “counter.v” input clk, rst;
`include “signal_light.v” reg [5:0] count;
module always@(posedgeclk or negedgerst)
signal_light_top(count,clk,rst,light1,light2); begin
input clk, rst; if (!rst)
output [2:0] light1, light2; count<=′d0;
output [5:0] count; else if (count<′d60)
wire [5:0] count; count<=count+1;
counter u2(clk,rst,count); else
signal_light u1(clk,rst,count,light1,light2); count<=′d1;
endmodule end
计数器模块 endmodule
module counter(clk,rst,count);