ORCID

0009-0000-0361-7506

Keywords

Abstract Interpretation, Verilog, Static Analysis, Data Flow Graph Analysis

Abstract

Modern Electronic Design Automation (EDA) flows treat structural and semantic reasoning as separate concerns. Synthesis structurally optimizes RTL, while dedicated verification teams validate functional behavior through testbenches and formal methods. This organizational divide means designers have no automatic, sound way to understand what their RTL does at the moment they are writing it. This thesis introduces AbIG4L (Abstract Interpretation of Generic 4-valued Logic), a static analysis framework that bridges this gap by delivering sound semantic reasoning automatically, directly within the hardware design loop.

The framework operates on a language-agnostic intermediate representation to compute sound over-approximations of hardware behavior across 0, 1, X, and Z logic states. The primary focus of this work is the analysis and evaluation of synthesizable Verilog. By utilizing a Reduced Product of Knownbits and Interval abstract domains, the forward fixpoint engine infers complex bit-level, vector-level, and cross-cycle invariants without requiring designer-supplied assertions or testbenches. Analysis results are mapped back to source locations via synthesis metadata and delivered to the designer through a VS Code extension, enabling "Shift-Left" visibility into design properties at the moment of authorship.

Evaluation is organized around a multi-tiered approach: a breadth study of HDLBits solutions yielding a 53% analyzability rate, a combinational case study demonstrating how surfaced properties verify behavior and a sequential case study identifying design flaws and unreachable logic. The results suggest that making semantic properties explicit early has the potential to complement existing EDA workflows, establishing a rigorous, first-principles foundation for automated hardware reasoning.

Completion Date

2026

Semester

Spring

Committee Chair

Borowczak, Mike

Degree

Master of Science in Computer Engineering (M.S.Cp.E.)

College

College of Engineering and Computer Science

Department

Department of Electrical and Computer Engineering

Document Type

Thesis

Identifier

DP0053238

Download

Share

COinS
 

Accessibility Statement

This item was created or digitized prior to April 24, 2027, or is a reproduction of legacy media created before that date. It is preserved in its original, unmodified state specifically for research, reference, or historical recordkeeping. In accordance with the ADA Title II Final Rule, the University Libraries provides accessible versions of archival materials upon request. To request an accommodation for this item, please submit an accessibility request form.