USA flag logo/image

An Official Website of the United States Government

SBIR Phase II: Automatic Scalable Architectural Validation for Microprocessors

Award Information

Agency:
National Science Foundation
Branch:
N/A
Award ID:
Program Year/Program:
2013 / SBIR
Agency Tracking Number:
1330952
Solicitation Year:
2013
Solicitation Topic Code:
EI
Solicitation Number:
Small Business Information
Reveal Design Automation, Inc.
330 E. Liberty St., Lower Levelm Ann Arbor, MI 48104-2274
View profile »
Woman-Owned: No
Minority-Owned: No
HUBZone-Owned: No
 
Phase 2
Fiscal Year: 2013
Title: SBIR Phase II: Automatic Scalable Architectural Validation for Microprocessors
Agency: NSF
Contract: 1330952
Award Amount: $720,644.00
 

Abstract:

This Small Business Innovation Research (SBIR) Phase II project addresses the challenge of automating and scaling formal equivalence verification between architectural SystemC models and RTL Verilog models for microprocessors and ASIC microcontrollers. The complexity of industrial processors, together with the differences in semantics of SystemC and Verilog, create a significant modeling gap that makes it infeasible to verify RTL Verilog implementations against their SystemC specification models. This gap impedes the progression currently taking place in EDA, wherein designers are moving upwards in the abstraction level for modeling and verifying hardware designs. Our formal equivalence verification technology will allow automatically obtaining RTL from ESL models using high-level synthesis tools, and formally verifying the correctness of the resulting models against the specification models. It will also allow manually written RTL models to be verified against ESL models originally created for architectural simulation. Expected challenges include overcoming the spatial and temporal modeling gaps, and verifying equivalence for an unlimited depth using finite equivalence formulations. By end of project, we anticipate to prototype a software program that will represent a product for architectural validation of general purpose microcontrollers, capable of proving equivalence or finding bugs with reasonable computational resources. The broader impact/commercial potential of this project is to make formal verification technologies scalable and directly usable by designers at higher abstraction levels, enabling exponential growth in design complexity without exponential growth in verification cost. The products resulting from this project will provide substantial benefit by ensuring design correctness for mission-critical components such as implantable medical devices, aviation hardware, and satellite/space systems. In addition to hardware verification, the work done in this project will contribute to firmware and software verification, which has utilized similar techniques in the past. It will additionally contribute to exploring industrial-oriented algorithms and heuristics in the domain of automated reasoning and constraint satisfaction problems, used in theorem proving, machine learning, scheduling optimization, gaming, and network security.

Principal Investigator:

Zaher S. Andraus
7342728231
zaher.andraus@reveal-da.com

Business Contact:

Zaher S. Andraus
7342728231
zaher.andraus@reveal-da.com
Small Business Information at Submission:

Reveal Design Automation, Inc.
330 E. Liberty St., Lower Levelm Ann Arbor, MI 48104-2274

EIN/Tax ID: 271120436
DUNS: N/A
Number of Employees:
Woman-Owned: No
Minority-Owned: No
HUBZone-Owned: No