NDLI: Automatic generation of compact formal properties for effective error detection

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

Reducing inter-core cache contention with an adaptive bank mapping policy in DRAM cache

A reconfigurable real-time SDRAM controller for mixed time-criticality systems

A DRAM-flash index for native flash file systems

WHISK: an uncore architecture for dynamic information flow tracking in heterogeneous embedded SoCs

Synthesis-friendly techniques for tightly-coupled integration of hardware accelerators into shared-memory multi-core clusters

Embedded supercomputing in FPGAs with the VectorBlox MXP matrix processor

DHeating: dispersed heating repair for self-healing NAND flash memory

Learning the optimal operating point for many-core systems with extended range voltage/frequency scaling

Online OLED dynamic voltage scaling for video streaming applications on mobile devices

pvFPGA: accessing an FPGA-based hardware accelerator in a paravirtualized environment

CMSM: an efficient and effective code management for software managed multicores

On the automatic generation of GPU-oriented software applications from RTL IPs

Run-time adaption for highly-complex multi-core systems

Bound-oriented parallel pruning approaches for efficient resource constrained scheduling of high-level synthesis

Improving polyhedral code generation for high-level synthesis

System level synthesis of hardware for DSP applications using pre-characterized function implementations

A cyber-physical system approach to artificial pancreas design

Instruction set extensions for dynamic time warping

Scalable NoC-based architecture of neural coding for new efficient associative memories

Design space exploration and parameter tuning for neuromorphic applications

Hardware neural network accelerators

Embedded neuromorphic vision systems

Bio-inspired ultra lower-power neuromorphic computing engine for embedded systems

IVaM: implicit variant modeling and management for automotive embedded systems

Improved formal worst-case timing analysis of weighted round robin scheduling for ethernet

Dimensioning and configuration of EES systems for electric vehicles with boundary-conditioned adaptive scalarization

VarEMU: an emulation testbed for variability-aware software

Automatic generation of compact formal properties for effective error detection

Automatic refinement of requirements for verification throughout the SoC design flow

ARGO: aging-aware GPGPU register file allocation

An energy and deadline aware resource provisioning, scheduling and optimization framework for cloud systems

Designing a residential hybrid electrical energy storage system based on the energy buffering strategy

Panappticon: event-based tracing to measure mobile application and platform performance

Multi-mode monitoring for mixed-criticality real-time systems

A variability-aware OpenMP environment for efficient execution of accuracy-configurable computation on shared-FPU processor clusters

Automated, retargetable back-annotation for host compiled performance and power modeling

Automatic generation of compact formal properties for effective error detection

Content Provider	ACM Digital Library
Author	Di Guglielmo, Giuseppe Pravadelli, Graziano Bertasi, Michele
Abstract	Several approaches exist in literature for automatic extraction of model behaviours represented in the form of formal properties. Some of them rely on static analysis of the source code, others dynamically mine specifications by analysing simulation traces. In both cases, most of them work at bit level and generate properties in the form of combinational or temporal relationships among Boolean expressions. Such techniques are suited only for gate-level or RTL HW models. There are also approaches working on system-level descriptions and SW programs, but they generate properties to express only the sequential ordering of communication function calls and events, while the functional part of the implementation is ignored. To fill in the gap, this paper presents a dynamic methodology that works on gate-level, RTL and system-level HW descriptions as well as embedded SW, independently from the design model and the abstraction level. The generated properties are in the form of temporal relationships among arithmetic and logic expressions involving traditional HW description language data types (i.e., bit and logic vectors) as well as data types typically adopted in system-level models and SW programs (i.e., integer, double and string). A ranking function is also defined to classify the mined properties according to their capability of capturing meaningful design behaviours. Experimental results have shown that the approach allows generating compact properties really useful to effectively detect errors in the design implementation.
Starting Page	1
Ending Page	10
Page Count	10
File Format	PDF
ISBN	9781479914173
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2013-09-29
Access Restriction	Subscribed
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

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