Hardware verification is a fundamental, yet often painful, step of hardware design. This talk will discuss how MLIR can accelerate this process through the CIRCT infrastructure, an MLIR hardware compiler containing dialects that describe hardware at both high and low levels of abstraction. We will describe how to generate models for verification from such high-level abstractions - specifically from the finite state machine (FSM) dialect - to check properties at higher levels and optimize the overall verification procedure.