logo SBA

ETD

Archivio digitale delle tesi discusse presso l’Università di Pisa

Tesi etd-10112023-182019


Tipo di tesi
Tesi di laurea magistrale
Autore
LIGABUE, LEONARDO
URN
etd-10112023-182019
Titolo
Functional verification of finite state machines: an automatic UVM based approach for the verification of generic synchronous and asynchronous FSMs
Dipartimento
INGEGNERIA DELL'INFORMAZIONE
Corso di studi
INGEGNERIA ELETTRONICA
Relatori
relatore Fanucci, Luca
relatore Sterpin, Andrea
relatore Ughettini, Claudia
Parole chiave
  • Methodology
  • UVM
  • FSM
  • Verification
  • Automation
  • Automated
  • Finite
  • State
  • Machine
  • Universal
  • Verification
  • Python
  • Petri
  • Network
  • Net
  • Scoreboard
  • Assertion
  • Checker
  • Coverage
Data inizio appello
17/11/2023
Consultabilità
Non consultabile
Data di rilascio
17/11/2093
Riassunto
This thesis addresses FSMs (Finite State Machines) functional verification through an
automated approach enabled by the mathematical representation of the FSMs
themselves. Starting from a documentation and configuration document drafted by
the verification engineer, a novel flow implemented by a Python script specifically
designed in this work generates all the code of a customizable single agent UVM
(Universal Verification Methodology) environment with selectable checkers and
assertions specifically designed for FSMs verification. The documentation analysis
phase must be done regardless of automatization. However, this solution completely
removes the initial set-up times of the environment. The flow also extrapolates the
Petri Network mathematical model of the FSM and solves the obtained systems for
every combination of starting and ending states. As an innovation on the current FSM
verification approach, the script heuristically evaluates, with a custom algorithm, the
values of the parametric solutions obtained with the Petri Network analysis. This
yields deterministic sequence vectors that can be used to implement, through another
custom algorithm, UVM sequences to fully stimulate the FSM or to make it evolve
from one state to another. This suite has been fully applied to a basic FSM specifically
designed to validate the script itself. It has also been applied on complex dummy
FSMs and real IPs until the verification phase. The results were all positive: the
generated environment correctly compiled; checkers and assertions had a 100% pass
rate; coverage yielded the expected results, in particular a 100% coverage was
achieved through the automatically generated sequence; injected errors were correctly
detected. In conclusion, the implemented flow represents an innovative, fast, scalable
and reliable solution for the verification of FSMs. If expanded, this work may
represent the state-of-the-art for the advanced verification of FSMs and even other
standard IPs.
File