The Formal Verification
Research Group at the Dept. of Computer Science & Engineering, Indian Institute
of Technology Kharagpur has more than ten years of experience in the development of formal
and semi-formal validation technology. The group engages in fundamental research
to solve emerging challenges in design validation and provides solutions to industrially
relevant validation problems.
NEW !!
Open Positions For Ongoing and Forthcoming Projects
Focus
Areas
(click
on the topics for details)
Recent
Publications Tools
Group Members
Partners
in Sponsored Research
Contact
Group
members
Pallab Dasgupta P.P. Chakrabarti
Research
students (PhD.) :
-
Diganchal Chakraborty
- Arijit Mondal
- Priyankar Ghosh
- Srobona Mitra
- Padmalochan Bera
- Manoj Dixit
- Subhankar Mukherjee
- Kamalesh Ghosh
Research
students (M.S.) :
- Aritra
Hazra
- Sourasis Das
- Antara Ain
- Debjit Pal
Former Members :
Sagar Chaki Pankaj Chauhan Shuvendu Lahiri Arindam Chakrabarti
Jatin Deka
Krishnendu Chatterjee S. Sriram Anirvan Dasgupta Indrajit Bhattacharya A.C. Pathak
Sandeep Chakrabarti
Pritam Roy Samik Das Subhojit
Basu
Prasenjit Basu
Sayantan Das Ansuman Banerjee Suchismita
Ray Anindya Sundar Nandi Bhaskar
Pal
Rajdeep Mukhopadhyay Sayak Ray
Partners
in Sponsored Research
-
Intel
Corporation, USA
-
Synopsys
(India) Pvt. Ltd.
-
Sun Microsystems,
USA
-
National
Semiconductors, USA
-
Interra Systems
-
General Motors
-
Indian
National Science Academy
-
Dept.
of Science & Technology, Govt. of India
-
Google Inc.
-
IBM
Tools
-
SpecMatcher:
Analyzes
the coverage of the architectural intent of a design by the RTL specs
-
CovAnalyzer:
Analyzes the completeness of a spec against a fault model
-
BUSpec:
Generates
assertion-based verification aids from BUS protocol specifications
-
Open Module Verifier: Assume-guarantee
style formal property verification on RTL modules
-
Genstimuli: Automatic
stimulus generator for custom cell characterization
-
Constraint Solving in Hardware:
Solves and Generates stimuli during hardware
accelerated simulation that obeys certain given
constraints
-
Verification IPs
for
ARM AMBA, Hypertransport, IBM CoreConnect, PCI Express
Recent Achievements:
Incorporating
formal methods to enhance the speed of logic evaluation in Verilog Cycle
Simulators
Development
of tools and technology for formal property verification in modules under
specified
environment models. We have implemented model checkers that check both untimed as well as
real time properties on open systems (modules).
Development
of temporal logics for efficient verification of timing properties. We
have shown that
reasoning about extremal (best case/ worst case) timing properties is
tractable in practice, where as,
it is known that model checking timed logics are PSPACE complete or harder
in general.
Development
of a validation platform for high level SOC designs specified in SDL augmented
with System C.
Development
of Open Vera Assertion (OVA) checkers for standard BUS protocols
Reasoning
about the coverage of architectural level correctness properties by RTL
correctness properties.
Contact:
Dr. Pallab Dasgupta,
Phone: +91-3222-283470
Professor, Fax: +91-3222-278985
Dept. of Computer Sc. & Engg. Email: pallab@cse.iitkgp.ernet.in
Indian Institute of Technology,
Kharagpur, India-721302
List
of Conferences