| Title | VFCC: A Verification Framework of Cache Coherence using Parallel Simulation |
| Author | *Qiaoli Xiong, Jiangfang Yi, Tianbao Song, Zichao Xie, Dong Tong (Peking University, China) |
| Page | pp. 705 - 710 |
| Keyword | cache coherence, verification, simulation |
| Abstract | A cache coherence protocol is a vital component of a multiprocessor to maintain the data consistency. In this paper, we proposed VFCC, which is a simulation framework to validate a cache-coherence protocol implementation of a commercial 64-bit superscalar multiprocessor. It exploits multiple-level parallelism to accelerate validation without overheads among threads. Our experimental results demonstrate VFCC has a 5.0x speedup than a traditional simulator on a conventional 16-core host machine. |
| Title | A Computational Model for SAT-based Verification of Hardware-Dependent Low-Level Embedded System Software |
| Author | *Bernard Schmidt, Carlos Villarraga (University of Kaiserslautern, Germany), Jörg Bormann (-, Germany), Dominik Stoffel, Markus Wedler, Wolfgang Kunz (University of Kaiserslautern, Germany) |
| Page | pp. 711 - 716 |
| Keyword | HW/SW-Verification, low-level software, property checking |
| Abstract | This paper describes a method to generate a computational
model for formal verification of hardware-dependent
software in embedded systems. The computational model of the
combined HW/SW system is a program netlist (PN) consisting of
instruction cells connected in a directed acyclic graph that compactly
represents all execution paths of the software. The model
can be easily integrated into SAT-based verification environments
such as those based on Bounded Model Checking (BMC). The
proposed construction of the model, however, allows for an
efficient reasoning of the SAT solver over entire execution paths.
We demonstrate the efficiency of our approach by presenting
experimental results from the formal verification of an industrial
LIN (Local Interconnect Network) bus node, implemented as a
software driver on a 32-bit RISC machine. |
| Slides |
| Title | Reviving Erroneous Stability-based Clock-Gating using Partial Max-SAT |
| Author | Bao Le, *Dipanjan Sengupta, Andreas Veneris (University of Toronto, Canada) |
| Page | pp. 717 - 722 |
| Keyword | Debugging, Design Errors, Low Power design, Clock Gating, Stability Condition |
| Abstract | Although recent developments have automated most of the low power implementations, designers often manually modify the circuit in order to achieve further power savings. This human intervention is often paved with many errors that are bound to typical logic functional failures. Debugging these errors can be a resource intensive process.
This paper proposes a novel debugging methodology to rectify erroneous clock gating implementations. The net effect of the proposed
methodology leads to shorter debug time ensuring additional power savings. |
| Slides |
| Title | Simplification of C-RTL Equivalent Checking for Fused Multiply Add Unit using Intermediate Models |
| Author | *Bin Xue, Prosenjit Chatterjee (Nvidia Corp, U.S.A.), Sandeep K. Shukla (Virginia Tech, U.S.A.) |
| Page | pp. 723 - 728 |
| Keyword | sequential equivalent checking, FMA, floating point |
| Abstract | The functionality of Fused multiply add (FMA) design can be formally verified by comparing its register transition level (RTL) implementation against its system level specification often modeled by C/C++ language using sequential equivalent checking (SEC). However, C-RTL SEC does not scale for FMA because of the huge discrepancy existed between the two models. This paper analyzes the dissimilarities and proposes two intermediate models, one abstract RTL and one rewritten C model to bridge the gap. The original SEC proof are partitioned into three sub-proofs among intermediate models where a variety of simplification techniques are applied to further reduce the complexity. Experiments from an industry project show that with the two intermediate models, the SEC proof is complete and scalable for FMA design |
| Slides |