Date: Thursday 17 March 2016
Time: 14:00 - 15:30
Location / Room: Konferenz 2

Chair:
Pablo Sanchez, University of Cantabria, ES

Co-Chair:
Ronny Morad, IBM, IL

The session presents methodologies for automatic test generation of memory controllers and arithmetic circuits. They are complemented with techniques that improve assertion simulation and post-silicon debugging. The interactive presentations will introduce new ideas about generating properties and tests.

Time	Label	Presentation Title Authors
14:00	11.4.1	AUTOMATED TEST GENERATION FOR DEBUGGING ARITHMETIC CIRCUITS Speaker: Prabhat Mishra, University of Florida, US Authors: Farimah Farahmandi and Prabhat Mishra, University of Florida, US Abstract Optimized and custom arithmetic circuits are widely used in embedded systems such as multimedia applications, cryptography systems, signal processing and console games. Debugging of arithmetic circuits is a challenge due to increasing complexity coupled with non-standard implementations. Exiting equivalence checking techniques produce a remainder to indicate the presence of a potential bug. However, bug localization remains a major bottleneck. Simulation-based validation using random or constrained-random tests are not effective and can be infeasible for complex arithmetic circuits. In this paper, we present an automated test generation and bug location technique for debugging arithmetic circuits. This paper makes two important contributions. We propose an automated approach for generating directed tests by suitable assignments of input variables to make the reminder non-zero. The generated tests are guaranteed to activate the unknown bug(s). We also propose a bug detection/correction technique using remainder's terms scanning as well as the intersection of regions activated by the generated tests. Our experimental results demonstrate that the proposed approach can be used for automated debugging of complex arithmetic circuits. Download Paper (PDF; Only available from the DATE venue WiFi)
14:30	11.4.2	MCXPLORE: AN AUTOMATED FRAMEWORK FOR VALIDATING MEMORY CONTROLLER DESIGNS Speaker: Mohamed Hassan, University of Waterloo, CA Authors: Mohamed Hassan and Hiren Patel, University of Waterloo, CA Abstract This work presents an automated framework for the validation of dynamic random access memory controllers (DRAM MCs) called MCXplore. In developing this framework, we construct formal models for memory requests interrelation and DRAM command interaction. The framework enables validation engineers to define their test plans precisely as temporal logic specifications. We use the NuSMV model-checker to generate counter-examples that serve as test templates; hence, MCXplore uses these test templates to generate memory tests to validate the correctness properties of the memory controller. We show the effectiveness of MCXplore by validating various state-of-the-art MC features as well as hard-to-detect timing violations that often occur. We also provide a set of predefined test plans, and regression tests that validate essential properties of modern DRAM MCs. We release MCXplore as an open-source framework to allow validation engineers and researchers to extend and use. Download Paper (PDF; Only available from the DATE venue WiFi)
15:00	11.4.3	EAST: EFFICIENT ASSERTION SIMULATION TECHNIQUES Speaker: Ansuman Banerjee, Indian Statistical Institute, IN Authors: Debjyoti Bhattacharjee, Soumi Chattopadhyay and Ansuman Banerjee, Indian Statistical Institute, IN Abstract In the context of simulation-based verification, the Assertion-based Verification (ABV) methodology has become the technology of choice, with increasing proliferation of Verification / Assertion IPs for most commonly used protocols. To support the ABV flow, current generation simulators typically create threads for the assertions and evaluate each assertion separately by converting them into finite state automatons and monitoring their states during simulation. In this paper, we propose a different technique for assertion evaluation in a simulation-based verification flow. The proposed technique, EAST (Efficient Assertion Simulation Techniques), handles assertions in groups, instead of examining them in isolation, and achieves significant performance benefits. To this effect, our algorithm has a pre-processing phase (prior to simulation) which creates a shared data structure from the set of assertions using some simple rules, based on the assertion language operators. This is attached with the simulator and during simulation, at each evaluation cycle, EAST infers the decision of the assertions by a combination of lookup and substitution. We present our proposal using Linear Temporal Logic (LTL) assertions in this paper. Our prototype, EAST, achieves promising performance numbers in terms of both runtime and peak memory for both random and standard benchmark protocol designs. Download Paper (PDF; Only available from the DATE venue WiFi)
15:15	11.4.4	COMBINATIONAL TRACE SIGNAL SELECTION WITH IMPROVED STATE RESTORATION FOR POST-SILICON DEBUG Speaker: Bijan Alizadeh, University of Tehran, IR Authors: Siamack BeigMohammadi and Bijan Alizadeh, University of Tehran, IR Abstract Signal selection is the pre-silicon evaluation step which maximizes overall reconstruction rate of state elements. Due to its high complexity, recent efforts on signal selection has focused on sequential nodes in the circuit under debug. In this paper we propose a combinational signal selection algorithm which possibly selects combinational nodes of the circuit to maximize state restoration capability and achieve significant improvements compared to the state-of-the-art signal selection algorithms. To compensate for increase in problem complexity, we also propose a fast state restoration algorithm which offers significant improvement on simulation time over the state-of-the-art state restoration algorithms. Download Paper (PDF; Only available from the DATE venue WiFi)
15:30	IP5-12, 529	TOPAZ: MINING HIGH-LEVEL SAFETY PROPERTIES FROM LOGIC SIMULATION TRACES Speaker: Fadi Kurdahi, University of California, Irvine, US Authors: Ahmed Nassar1, Fadi Kurdahi1 and Salam Zantout2 1University of California, Irvine, US; 2American University of Beirut, LB Abstract Formal specifications are hard to formulate and maintain for evolving complex digital hardware designs. Specification mining offers a (partially) automated route to discovering specifications from large simulation traces. In this paper, we embark on a novel and rigorous mining methodology (data preparation, mining algorithms, selection criteria, etc.) for finite-state automata checkers using an iterative and interactive mining tool, called Topaz. Topaz is evaluated using an open-source 32-bit RISC CPU design as a case study to demonstrate extraction of complex temporal properties cross-cutting through all CPU pipeline stages, guided by the CPU instruction set specification. Download Paper (PDF; Only available from the DATE venue WiFi)
15:31	IP5-13, 808	EXPLOITING TRANSACTION LEVEL MODELS FOR OBSERVABILITY-AWARE POST-SILICON TEST GENERATION Speaker: Prabhat Mishra, University of Florida, US Authors: Farimah Farahmandi1, Prabhat Mishra1 and Sandip Ray2 1University of Florida, US; 2Intel Corporation, US Abstract A critical problem in post-silicon debug is to generate efficient tests that both activate requisite coverage goals on the target hardware as well as produce results that are observable through a given on-chip design-for-debug architecture. Unfortunately, such tests cannot be generated directly from RTL models, both due to design complexity and due to bugs in the design itself. In this paper, we propose an approach to address this problem by exploiting transaction-level models (TLM). Our approach involves mapping test and observability requirements between TLM and RTL, enabling TLM analysis to generate post-silicon tests. We provide case studies from a number of different design classes to demonstrate the flexibility and effectiveness of the approach. Download Paper (PDF; Only available from the DATE venue WiFi)
15:30		End of session Coffee Break in Exhibition Area