# CREST: Hardware Formal Verification with ANSI-C Reference Specifications

## TL;DR

CREST is a tool that extends CBMC to verify hardware datapaths specified in ANSI-C, enabling formal verification in industrial EDA environments without restricting to synthesizable subsets.

## Contribution

CREST adapts CBMC for hardware verification by supporting arbitrary ANSI-C specifications, bridging software analysis tools with hardware formal verification.

## Key findings

- Successfully verified hardware datapaths using ANSI-C specifications.
- Demonstrated compatibility with commercial EDA formal verification environments.
- Showcased effectiveness through multiple verification case studies.

## Abstract

This paper presents CREST, a prototype front-end tool intended as an add-on to commercial EDA formal verifcation environments. CREST is an adaptation of the CBMC bounded model checker for C, an academic tool widely used in industry for software analysis and property verification. It leverages the capabilities of CBMC to process hardware datapath specifications written in arbitrary ANSI-C, without limiting restrictions to a synthesizable subset. We briefly sketch the architecture of our tool and show its use in a range of verification case studies.