Hardware security verification is a challenging and time-consuming task. For
this purpose, design engineers may utilize tools such as formal verification,
linters, and functional simulation tests, coupled with analysis and a deep
understanding of the hardware design being inspected. Large Language Models
(LLMs) have been used to assist during this task, either directly or in
conjunction with existing tools. We improve the state of the art by proposing
MARVEL, a multi-agent LLM framework for a unified approach to decision-making,
tool use, and reasoning. MARVEL mimics the cognitive process of a designer
looking for security vulnerabilities in RTL code. It consists of a supervisor
agent that devises the security policy of the system-on-chips (SoCs) using its
security documentation. It delegates tasks to validate the security policy to
individual executor agents. Each executor agent carries out its assigned task
using a particular strategy. Each executor agent may use one or more tools to
identify potential security bugs in the design and send the results back to the
supervisor agent for further analysis and confirmation. MARVEL includes
executor agents that leverage formal tools, linters, simulation tests,
LLM-based detection schemes, and static analysis-based checks. We test our
approach on a known buggy SoC based on OpenTitan from the Hack@DATE
competition. We find that 20 of the 48 issues reported by MARVEL pose security
vulnerabilities.