NDLI: ForEVeR: A complementary formal and runtime verification approach to correct NoC functionality

Please wait, while we are loading the content...

Issue 5s(Special Issue on Risk and Trust in Embedded Critical Systems, Special Issue on Real-Time, Embedded and Cyber-Physical Systems, Special Issue on Virtual Prototyping of Parallel and Embedded Systems (ViPES)), November 2014

Issue 4(Regular Papers), November 2014

Issue 4s(Special Issue on Real-Time and Embedded Technology and Applications, Domain-Specific Multicore Computing, Cross-Layer Dependable Embedded Systems, and Application of Concurrency to System Design (ACSD'13)), July 2014

Issue 3s(Special Issue on Design Challenges for Many-Core Processors, Special Section on ESTIMedia'13 and Regular Papers), March 2014

UWB microwave imaging for breast cancer detection: Many-core, GPU, or FPGA?

Editorial: Special Section on ESTIMedia'13

Energy optimization for real-time multiprocessor system-on-chip with optimal DVFS and DPM combination

Post-silicon platform for the functional diagnosis and debug of networks-on-chip

NoC contention analysis using a branch-and-prune algorithm

HARP: Harnessing inactive threads in many-core processors

NoC-based fault-tolerant cache design in chip multiprocessors

METEOR: Hybrid photonic ring-mesh network-on-chip for multicore architectures

Exploiting replication to improve performances of NUCA-based CMP systems

Editorial: Embedded systems -- more than methodology

Editorial: Special issue on design challenges for many-core processors

Towards a scalable, low-power all-optical architecture for networks-on-chip

HARS: A hardware-assisted runtime software for embedded many-core architectures

On-chip traffic regulation to reduce coherence protocol cost on a microthreaded many-core architecture with distributed caches

ForEVeR: A complementary formal and runtime verification approach to correct NoC functionality

Ultra-low-power adder stage design for exascale floating point units

Yield-enhancement schemes for multicore processor and memory stacked 3D ICs

Tomahawk: Parallelism and heterogeneity in communications signal processing MPSoCs

PAIS: Parallelism-aware interconnect scheduling in multicores

Issue 2s(Special Section ESFH'12, ESTIMedia'11 and Regular Papers), January 2014

Issue 3, December 2013

Issue 1s(Special Section on ESTIMedia'10), November 2013

Issue 2(Special issue on application-specific processors), September 2013

Issue 1, August 2013

ACM Transactions on Embedded Computing Systems (TECS) : Volume 12

ACM Transactions on Embedded Computing Systems (TECS) : Volume 11

ACM Transactions on Embedded Computing Systems (TECS) : Volume 11S

ACM Transactions on Embedded Computing Systems (TECS) : Volume 10

ACM Transactions on Embedded Computing Systems (TECS) : Volume 9

ACM Transactions on Embedded Computing Systems (TECS) : Volume 8

ACM Transactions on Embedded Computing Systems (TECS) : Volume 7

ACM Transactions on Embedded Computing Systems (TECS) : Volume 6

ACM Transactions on Embedded Computing Systems (TECS) : Volume 5

ACM Transactions on Embedded Computing Systems (TECS) : Volume 4

ACM Transactions on Embedded Computing Systems (TECS) : Volume 3

ACM Transactions on Embedded Computing Systems (TECS) : Volume 2

ACM Transactions on Embedded Computing Systems (TECS) : Volume 1

ForEVeR: A complementary formal and runtime verification approach to correct NoC functionality

Content Provider	ACM Digital Library
Author	Parikh, Ritesh Bertacco, Valeria
Copyright Year	2014
Abstract	As silicon technology scales, modern processor and embedded systems are rapidly shifting towards complex chip multi-processor (CMP) and system-on-chip (SoC) designs. As a side effect of complexity of these designs, ensuring their correctness has become increasingly problematic. Within these domains, Network-on-Chips (NoCs) are a de-facto choice to implement on-chip interconnect; their design is quickly becoming extremely complex in order to keep up with communication performance demands. As a result, design errors in the NoC may go undetected and escape into the final silicon. In this work, we propose ForEVeR, a solution that complements the use of formal methods and runtime verification to ensure functional correctness in NoCs. Formal verification, due to its scalability limitations, is used to verify smaller modules, such as individual router components. To deliver correctness guarantees for the complete network, we propose a network-level detection and recovery solution that monitors the traffic in the NoC and protects it against escaped functional bugs. To this end, ForEVeR augments the baseline NoC with a lightweight checker network that alerts destination nodes of incoming packets ahead of time. If a bug is detected, flagged by missed packet arrivals, our recovery mechanism delivers the in-flight data safely to the intended destination via the checker network. ForEVeR's experimental evaluation shows that it can recover from NoC design errors at only 4.9% area cost for an 8x8 mesh interconnect, over a time interval ranging from 0.5K to 30K cycles per recovery event, and it incurs no performance overhead in the absence of errors. ForEVeR can also protect NoC operations against soft-errors: a growing concern with the scaling of silicon. ForEVeR leverages the same monitoring hardware to detect soft-error manifestations, in addition to design-errors. Recovery of the soft-error affected packets is guaranteed by building resiliency features into our checker network. ForEVeR incurs minimal performance penalty up to a flit error rate of 0.01% in lightly loaded networks.
Starting Page	1
Ending Page	30
Page Count	30
File Format	PDF
ISSN	15399087
e-ISSN	15583465
DOI	10.1145/2514871
Volume Number	13
Issue Number	3s
Journal	ACM Transactions on Embedded Computing Systems (TECS)
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2014-03-28
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Network-on-chip NoC Formal verification Functional correctness Runtime verification
Content Type	Text
Resource Type	Article
Subject	Hardware and Architecture Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

ForEVeR: A Complementary Formal and Runtime Verification Approach to Correct NoC Functionality

Formally enhanced runtime verification to ensure NoC functional correctness

Formally enhanced verification at runtime to ensure noc functional correctness.

Formally enhanced runtime verification to ensure noc functional correctness.

Transport-layer-assisted routing for runtime thermal management of 3D NoC systems

AdNoC: Runtime Adaptive Network-on-Chip Architecture

Gana: A novel low-cost conflict-free NoC architecture

Formal verification of Network-on-Chip ( NoC ) Architecture

Moths: Mobile threads for on-chip networks

ForEVeR: A complementary formal and runtime verification approach to correct NoC functionality

Similar Documents

ForEVeR: A Complementary Formal and Runtime Verification Approach to Correct NoC Functionality

Formally enhanced runtime verification to ensure NoC functional correctness

Formally enhanced verification at runtime to ensure noc functional correctness.

Formally enhanced runtime verification to ensure noc functional correctness.

Transport-layer-assisted routing for runtime thermal management of 3D NoC systems

AdNoC: Runtime Adaptive Network-on-Chip Architecture

Gana: A novel low-cost conflict-free NoC architecture

Formal verification of Network-on-Chip ( NoC ) Architecture

Moths: Mobile threads for on-chip networks

ForEVeR: A complementary formal and runtime verification approach to correct NoC functionality