Date: Tuesday 26 March 2019
Time: 17:00 - 18:30
Location / Room: Room 3
Chair:
Jaan Raik, Tallinn University of Technology, EE
Co-Chair:
Sara Vinco, Polytechnic of Turin, IT
This session targets improving coverage from different perspectives, to activate multiple targets with concolic testing, to improve functional coverage metrics for instruction set simulators, and to achieve path coverage in SystemC-AMS. Three IPs complete the session covering optimizations for system verification and design.
| Time | Label | Presentation Title Authors |
|---|---|---|
| 17:00 | 4.3.1 | (Best Paper Award Candidate) AUTOMATED ACTIVATION OF MULTIPLE TARGETS IN RTL MODELS USING CONCOLIC TESTING Speaker: Prabhat Mishra, University of Florida, US Authors: Yangdi Lyu, Alif Ahmed and Prabhat Mishra, University of Florida, US Abstract Simulation is widely used for validation of Register-Transfer-Level (RTL) models. While simulating with millions of random (or constrained-random) tests can cover majority of the targets (functional scenarios), the number of remaining targets can still be huge (hundreds or thousands) in case of today's industrial designs. Prior work on directed test generation using concolic testing can cover only one target at a time. A naive extension of prior work to activate the remaining targets would be infeasible due to wasted effort in multiple overlapping searches. In this paper, we propose an automated test generation technique for activating multiple targets in RTL models using concolic testing. This paper makes three important contributions. First, it efficiently prunes the targets that can be covered by the tests generated for activating the other targets. Next, it minimizes the overlapping searches while trying to generate tests for activating multiple targets. Finally, our approach effectively utilizes clustering of related targets as well as common path sharing between the targets in the same cluster to drastically reduce the test generation time. Experimental results demonstrate that our approach significantly outperforms the existing methods in terms of overall coverage (up to 5X, 1.2X on average) as well as test generation time (up to 146X, 80X on average). Download Paper (PDF; Only available from the DATE venue WiFi) |
| 17:30 | 4.3.2 | VERIFYING INSTRUCTION SET SIMULATORS USING COVERAGE-GUIDED FUZZING Speaker: Vladimir Herdt, University of Bremen, DE Authors: Vladimir Herdt, Daniel Grosse, Hoang M. Le and Rolf Drechsler, University of Bremen, DE Abstract Verification of Instruction Set Simulators (ISSs) is crucial. Predominantly simulation-based approaches are used. They require a comprehensive testset to ensure a thorough verification. We propose a novel coverage-guided fuzzing (CGF) approach to improve the testcase generation process. In addition to code coverage we integrate functional coverage and a custom mutation procedure tailored for ISS verification. As a case-study we apply our approach on a set of three publicly available RISC-V ISSs. We found several new errors, including one error in the official RISC-V reference simulator Spike. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 18:00 | 4.3.3 | DATA FLOW TESTING FOR SYSTEMC-AMS TIMED DATA FLOW MODELS Speaker: Muhammad Hassan, DFKI GmbH, DE Authors: Muhammad Hassan, Daniel Grosse, Hoang M. Le and Rolf Drechsler, University of Bremen, DE Abstract Internet-of-Things (IoT) devices have significantly increased the need for high quality Analog Mixed Signal (AMS) System-on-Chips (SoC). Virtual Prototyping (VP) can be utilized for an early design verification. The Timed Data Flow (TDF) model of computation available in SystemC-AMS offers here a good trade-off between accuracy and simulation-speed at the system-level. One of the main challenges in system-level verification of AMS design is to achieve full path coverage. In the software domain Data Flow Testing (DFT) has demonstrated to be a powerful testing strategy in this regard. In this paper we introduce a DFT approach for SystemC-AMS TDF models based on two major contributions: First, we develop a set of SystemC-AMS TDF models specific coverage criteria for DFT. This requires to consider the SystemC-AMS semantics of signal flow. Second, we explain how to automatically compute the data flow coverage result for given TDF models using a combination of static and dynamic analysis techniques. Our experimental results on real-world AMS VPs demonstrate the applicability and efficacy of our approach. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 18:30 | IP2-3, 653 | (Best Paper Award Candidate) HCFTL: A LOCALITY-AWARE PAGE-LEVEL FLASH TRANSLATION LAYER Speaker: Hao Chen, University of Science and Technology of China, CN Authors: Hao Chen1, Cheng Li1, Yubiao Pan2, Min Lyu1, Yongkun Li1 and Yinlong Xu1 1University of Science and Technology of China, CN; 2Huaqiao University, CN Abstract The increasing capacity of SSDs requires a large amount of built-in DRAM to hold the mapping information of logical-to-physical address translation. Due to the limited size of DRAM, existing FTL schemes selectively keep some active mapping entries in a Cached Mapping Table (CMT) in DRAM, while storing the entire mapping table on flash. To improve the CMT hit ratio with limited cache space on SSDs, in this paper, we propose a novel FTL, a hot-clusterity FTL (HCFTL) that clusters mapping entries recently evicted from the cache into dynamic translation pages (DTPs). Given the temporal localities that those hot entries are likely to be visited in near future, loading DTPs will increase the CMT hit ratio and thus improve the FTL performance. Furthermore, we introduce an index structure to speedup the lookup of mapping entries in DTPs. Our experiments show that HCFTL can improve the CMT hit ratio by up to 41.1% and decrease the system response time by up to 33.3%, compared to state-of-the-art FTL schemes. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 18:31 | IP2-4, 402 | MODEL CHECKING IS POSSIBLE TO VERIFY LARGE-SCALE VEHICLE DISTRIBUTED APPLICATION SYSTEMS Speaker: Haitao Zhang, School of Information Science and Engineering, Lanzhou University, CN Authors: Haitao Zhang1, Ayang Tuo1 and Guoqiang Li2 1Lanzhou University, CN; 2Shanghai Jiao Tong University, CN Abstract OSEK/VDX is a specification for vehicle-mounted systems. Currently, the specification has been widely adopted by many automotive companies to develop a distributed vehicle application system. However, the ever increasing complexity of the developed distributed application system has created a challenge for exhaustively ensuring its reliability. Model checking as an exhaustive technique has been applied to verify OSEK/VDX distributed application systems to discover subtle errors. Unfortunately, it faces a poor scalability for practical systems because the verification models derived from such systems are highly complex. This paper presents an efficient approach that addresses this problem by reducing the complexity of the verification model such that model checking can easily complete the verification. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 18:32 | IP2-5, 155 | AUTOMATIC ASSERTION GENERATION FROM NATURAL LANGUAGE SPECIFICATIONS USING SUBTREE ANALYSIS Speaker: Ian Harris, University of California, Irvine, US Authors: Junchen Zhao and Ian Harris, University of California Irvine, US Abstract We present an approach to generate assertions from natural language specifications by performing semantic analysis of sentences in the specification document. Other techniques for automatic assertion generation use information found in the design implementation, either by performing static or dynamic analysis. Our approach generates assertions directly from the specification document, so bugs in the implementation will not be reflected in the assertions. Our approach parses each sentence and examines the resulting syntactic parse trees to locate subtrees which are associated with important phrases, such as the antecedent and consequent of an implication. Formal assertions are generated using the information inside these subtrees to fill a set of assertion templates which we present. We evaluate the effectiveness of our approach using a set of statements taken from a real specification document. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 18:30 | End of session Exhibition Reception in Exhibition Area The Exhibition Reception will take place on Tuesday in the exhibition area, where free drinks for all conference delegates and exhibition visitors will be offered. All exhibitors are welcome to also provide drinks and snacks for the attendees. |