Finite input-memory automaton based checker synthesis of systemverilog assertions for FPGA prototyping

Chengjie Zang, Shinji Kimura

Research output: Contribution to journalArticle

Abstract

Checker synthesis for assertion based verification becomes popular because of the recent progress on the FPGA prototyping environment. In the paper, we propose a checker synthesis method based on the finite input-memory automaton suitable for embedded RAMmodules in FPGA. There are more than 1Mbit memories in medium size FPGA's and such embedded memory cells have the capability to be used as the shift registers. The main idea is to construct a checker circuit using the finite inputmemory automata and implement shift register chain by logic elements or embedded RAM modules. When using RAM module, the method does not consume any logic element for storing the value. Note that the shift register chain of input memory can be shared with different assertions and we can reduce the hardware resource significantly. We have checked the effectiveness of the proposed method using several assertions.

Original languageEnglish
Pages (from-to)1454-1463
Number of pages10
JournalIEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences
VolumeE92-A
Issue number6
DOIs
Publication statusPublished - 2009

Fingerprint

Prototyping
Assertion
Field Programmable Gate Array
Shift registers
Automata
Field programmable gate arrays (FPGA)
Synthesis
Data storage equipment
Random access storage
Logic
Module
Finite Automata
Finite automata
Hardware
Resources
Networks (circuits)
Cell

Keywords

  • Assertion checker
  • Finite inputmemory automaton
  • SystemVerilog Assertion

ASJC Scopus subject areas

  • Electrical and Electronic Engineering
  • Computer Graphics and Computer-Aided Design
  • Applied Mathematics
  • Signal Processing

Cite this

@article{0b3e4d34271f4a2c8f657bb930337479,
title = "Finite input-memory automaton based checker synthesis of systemverilog assertions for FPGA prototyping",
abstract = "Checker synthesis for assertion based verification becomes popular because of the recent progress on the FPGA prototyping environment. In the paper, we propose a checker synthesis method based on the finite input-memory automaton suitable for embedded RAMmodules in FPGA. There are more than 1Mbit memories in medium size FPGA's and such embedded memory cells have the capability to be used as the shift registers. The main idea is to construct a checker circuit using the finite inputmemory automata and implement shift register chain by logic elements or embedded RAM modules. When using RAM module, the method does not consume any logic element for storing the value. Note that the shift register chain of input memory can be shared with different assertions and we can reduce the hardware resource significantly. We have checked the effectiveness of the proposed method using several assertions.",
keywords = "Assertion checker, Finite inputmemory automaton, SystemVerilog Assertion",
author = "Chengjie Zang and Shinji Kimura",
year = "2009",
doi = "10.1587/transfun.E92.A.1454",
language = "English",
volume = "E92-A",
pages = "1454--1463",
journal = "IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences",
issn = "0916-8508",
publisher = "Maruzen Co., Ltd/Maruzen Kabushikikaisha",
number = "6",

}

TY - JOUR

T1 - Finite input-memory automaton based checker synthesis of systemverilog assertions for FPGA prototyping

AU - Zang, Chengjie

AU - Kimura, Shinji

PY - 2009

Y1 - 2009

N2 - Checker synthesis for assertion based verification becomes popular because of the recent progress on the FPGA prototyping environment. In the paper, we propose a checker synthesis method based on the finite input-memory automaton suitable for embedded RAMmodules in FPGA. There are more than 1Mbit memories in medium size FPGA's and such embedded memory cells have the capability to be used as the shift registers. The main idea is to construct a checker circuit using the finite inputmemory automata and implement shift register chain by logic elements or embedded RAM modules. When using RAM module, the method does not consume any logic element for storing the value. Note that the shift register chain of input memory can be shared with different assertions and we can reduce the hardware resource significantly. We have checked the effectiveness of the proposed method using several assertions.

AB - Checker synthesis for assertion based verification becomes popular because of the recent progress on the FPGA prototyping environment. In the paper, we propose a checker synthesis method based on the finite input-memory automaton suitable for embedded RAMmodules in FPGA. There are more than 1Mbit memories in medium size FPGA's and such embedded memory cells have the capability to be used as the shift registers. The main idea is to construct a checker circuit using the finite inputmemory automata and implement shift register chain by logic elements or embedded RAM modules. When using RAM module, the method does not consume any logic element for storing the value. Note that the shift register chain of input memory can be shared with different assertions and we can reduce the hardware resource significantly. We have checked the effectiveness of the proposed method using several assertions.

KW - Assertion checker

KW - Finite inputmemory automaton

KW - SystemVerilog Assertion

UR - http://www.scopus.com/inward/record.url?scp=77956038405&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=77956038405&partnerID=8YFLogxK

U2 - 10.1587/transfun.E92.A.1454

DO - 10.1587/transfun.E92.A.1454

M3 - Article

VL - E92-A

SP - 1454

EP - 1463

JO - IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences

JF - IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences

SN - 0916-8508

IS - 6

ER -