Design Verification
Publications
Shivani Tripathy, Debiprasanna Sahoo, Manoranjan Satpathy. and Madhu Mutyam
IEEE Transaction on Computer-Aided Design Circuits and Systems, 2022
https://ieeexplore.ieee.org/document/9987545/
Formal Modeling and Verification of Security Properties of Ransomware-Resistant SSD
Solid State Drives (SSDs) are fast emerging as the primary choice for data storage in diverse domains. However, data protection against ransomware attacks on such storage devices is a crucial challenge. The In-SSD ransomware protection mechanism adds a new component to the FTL, making the FTL design more complex. The new component interacts with almost all other units of FTL for recovery from a ransomware attack. In this work, we discuss the derivation of a set of security properties related to protection from ransomware that covers the security requirements and the design; we next prove such properties using symbolic model checking.
Debiprasanna Sahoo, Shivani Tripathy, Manoranjan Satpathy and Madhu Mutyam
IEEE International Conference on Computer Design 2019
https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=8988756
Post-Model Validation of Victim DRAM Caches
In this work, we propose a method to validate an implementation of DRAM cache manually translated from the formal model. Our work focuses on two step approach to validate a DRAM cache implementation:
(a) We use Feedback Directed Random Testing (FDRT) to reverse engineer the state models from the execution traces; this helps us to match the implementation with the state machines associated with the formal model and also verify the state-based properties.
(b) We instrument monitors into the implementation and validate the liveness and safety properties those are already proven using model checking.
Shivani Tripathy, Debiprasanna Sahoo, Manoranjan Satpathy and Srinivas Pinisetty
IEEE International Conference on Computer Design
2019
Formal Modeling and Verification of NAND Flash Memory
Existing research works were successful to model and verify basic functionalities of older standards (ONFI-1.0 and ONFI-2.1). The advanced operations could not be verified due to resource constraints. We model and verify the advanced operations along with the basic operations of a much recent standard (ONFI-3.2) which is much more complex. We model a die as a composition of its planes to capture the device behaviour. Our model reflects the details of plane level parallelism and operation pipelining while simplifying the state machines. We also extract the requirement based properties like liveness, deadlock freedom, timing and functional properties from the ONFI-3.2 document and product data sheets. We prove all such properties using symbolic model checking.
Debiprasanna Sahoo, Swaraj Sha, Manoranjan Satpathy, Madhu Mutyam, S. Ramesh and Partha Roop
ACM Transactions on Design Automation of Electronics System (TODAES)
https://dl.acm.org/citation.cfm?id=3306491
Formal Modeling and Verification of a Victim DRAM Cache
DRAM caches are large in size and hence, when realized as a victim cache, non inclusive design is preferred. This non-inclusive design adds significant differences to the conventional DRAM cache design in terms of its probe, fill and writeback policies. The contributions of this work are:
1. Identification of agents in the system. The main agents are the DRAM cache and its predecessor cache.
2. We illustrate the interaction between the agents as a formal model of interacting state machines.
3. We identify and prove 61 properties related to the victim DRAM cache.
SAL source code:
https://drive.google.com/file/d/1OO_KHcKOUbZPUMbmKGImPjoUSMtxfRWr/view?usp=sharing
Debiprasanna Sahoo, Swaraj Sha, Manoranjan Satpathy, Madhu Mutyam, S. Ramesh and Partha Roop
ACM/IEEE International Conference on Hardware/Software Codesign and System Synthesis (CODES + ISSS), ESWEEK, 2018
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD)
https://ieeexplore.ieee.org/document/8493587
Formal Modeling and Verification of Controllers for a Family of DRAM Caches
DRAM cache controller is complex because it manages both timing aspect of the DRAM as well as the functional aspect of a cache controller. Hence, without formal verification ensuring correctness of the system becomes complex. The contributions of this work are:
1. Identification of agents in the system. The main agents are cache access agent and DRAM command scheduler.
2. We illustrate the interaction between the cache access agent and the bank scheduler as a formal model of interacting state machines. This model refers to a common design (similar to Unison Cache) and hence, is termed as the base model.
3. We identify and prove 78 properties related to the DRAM cache controllers for the base-model.
4. We show that several variants of the DRAM cache design can be derived from the base model.
Debiprasanna Sahoo and Manoranjan Satpathy
29th International Conference on VLSI Design and 15th International Conference on Embedded Systems (VLSID), 2016
MSimDRAM: Formal Model Driven Development of a DRAM Simulator
A DRAM Controller design is complex because it has to manage timing and sequence aspect of the DRAM system. Hence, formal verification is necessary to achieve correctness of the controller. This work has the following contribution:
1. We Identify the agents in the system. The main agents are bank, rank and channel schedulers.
2. We model the bank, rank and channel schedulers as interacting state machines.