An overview of the verification of a Handel-C program

被引：0

作者：

Woodcock, JCP ^{[1
]}

McEwan, AA ^{[1
]}

机构：

[1] Univ Oxford, Comp Lab, Oxford OX1 3QD, England

来源：

PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON PARALLEL AND DISTRIBUTED PROCESSING TECHNIQUES AND APPLICATIONS, VOLS I-V | 2000年

关键词：

Handel-C; hardware verification; abstraction; model checking; data refinement; the Unifying Theory of Programming; Z; CSP; FDR; Z/Eves;

D O I：

暂无

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

In this short paper we describe the verification of a Handel-C program that implements a packet-filter firewall on an FPGA. The Handel-C program is modelled as a system of co-operating CSP processes; unfortunately, the system is too large to be subjected to model checking (it is of the order of 10(50) states). A series of reductions is used to produce an abstract system that approximates the behaviour of the Handel-C program; this abstract system is small enough to be model-checked by FDR, yet exact with respect to critical system properties. The exactness of the abstraction is justified by the principles of data refinement. The most abstract description is given using Hoare & He's Unifying Theory.

引用

页码：3003 / 3007

页数：5

共 50 条

[21] FPGA implementation of frequency output and input using Handel-C
Zamora, Mayela
Henry, Manus
2007 IEEE INTERNATIONAL SYMPOSIUM ON INDUSTRIAL ELECTRONICS, PROCEEDINGS, VOLS 1-8, 2007, : 2313 - 2318
[22] Handel-c design enhancement for FPGA-based DV decoder
Cichon, Slawomir
Gorgon, Marek
Pac, Miroslaw
RECONFIGURABLE COMPUTING: ARCHITECTURES AND APPLICATIONS, 2006, 3985 : 128 - 133
[23] Designing an HMAC-hash unit on FPGAs using Handel-C
Khan, Esam
El-Kharashi, M. Watheq
Gebali, Fayez
Abd-Ei-Barr, Mostafa
2006 IEEE INTERNATIONAL SYMPOSIUM ON INDUSTRIAL ELECTRONICS, VOLS 1-7, 2006, : 1521 - +
[24] A step towards refining and translating B control annotations to Handel-C
Ifill, W.
Schneider, S.
CONCURRENCY AND COMPUTATION-PRACTICE & EXPERIENCE, 2010, 22 (08): : 1023 - 1048
[25] Handel-C for rapid prototyping of VLSI coprocessors for real time systems
Loo, SM
Wells, BE
Freije, N
Kulick, J
PROCEEDINGS OF THE THIRTY-FOURTH SOUTHEASTERN SYMPOSIUM ON SYSTEM THEORY, 2002, : 6 - 10
[26] The Improved Genetic Algorithm for Solving Knapsack Problem Based on Handel-C
Yang, Yi
Fang, Qian-sheng
2009 IEEE INTERNATIONAL CONFERENCE ON GRANULAR COMPUTING ( GRC 2009), 2009, : 702 - 705
[27] Header compression in Handel-C - an Internet application and a new design language
Torkelsson, K
Ditmar, J
EUROMICRO SYMPOSIUM ON DIGITAL SYSTEMS DESIGN, PROCEEDINGS, 2001, : 2 - 7
[28] Layering RTL, SAFL, Handel-C and Bluespec Constructs on Chisel HCL
Greaves, David J.
2015 ACM/IEEE INTERNATIONAL CONFERENCE ON FORMAL METHODS AND MODELS FOR CODESIGN (MEMOCODE), 2015, : 108 - 117
[29] A Step Towards Refining and Translating B Control Annotations to Handel-C
Ifill, Wilson
Schneider, Steve
WOTUG-30: COMMUNICATING PROCESS ARCHITECTURES 2007, 2007, 65 : 399 - +
[30] 基于Handel-C的微处理器设计
杨益
范庆春
电子技术, 2008, (10) : 19 - 22

← 1 2 3 4 5 →