GSRC Student Profile:
Divjyot Sethi
|
 |
(For more contact info, please log in.)
Princeton University
Advisor: Sharad Malik
GSRC theme: resiliency
Expected graduation: Jun, 2012 |
Research Overview: Specification and Encoding of Transaction interaction properties
Hardware verification is becoming an increasingly difficult task as the complexity of designs is increasing. In order to simplify this task, designs are modeled at a level higher than RTL. Transaction-Based models are increasingly being used for a higher level design description.
Our group at Princeton has developed transaction based models at multiple levels of abstraction. In particular, our group has developed a design methodology PRIM (PRInceton Models) based on transaction models at specification and micro-architecture levels.
I have been working on enabling specification of properties on these models. Many important properties on transaction based models involve referring to individual transactions which is difficult to do automatically. Also, transaction based models have a dynamic nature since the transactions become active and retire dynamically. I have developed a static (but infinite) formal model and a convenient form of property specification where individual transactions can be referred to by their indices. Given the property specified in this form my work derives a finite encoding with LTL assertions mechanically for model checking.
|
