High-Level Modelling, Analysis, and Verification on FPGA-Based Hardware Design
The paper presents high-level modelling and formal analysis and verification on an FPGA-based multigigabit network monitoring system called Scampi. Uppaal was applied in this work to establish some correctness and throughput results on a model intentionally built using patterns reusable in other similar projects. Some initial experiments with parametric analysis using TReX were performed too.
KeywordsTime Slot Read Time Incoming Request FIFO Queue Executive Component
- 2.Holeček, J., Kratochvíla, T., Rehák, V., Šafránek, D., Simeček, P.: How to Formalize FPGA Hardware Design. Technical Report 4/2004, CESNET (October 2004)Google Scholar
- 3.Matoušek, P., Smrčka, A., Vojnar, T.: High-Level Modeling, Analysis, and Verification of Scampi2. Technical report, CESNET (2005) (to appear)Google Scholar
- 5.Pettersson, P., Larsen, K.G.: Uppaal2k. In: Bulletin of the European Association for Theoretical Computer ScienceGoogle Scholar