English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Hardware-firmware co-verification is critical to design trustworthy systems.While formal methods can provide verification guarantees, due to the complexityof firmware and hardware, it can lead to state space explosion. There arepromising avenues to reduce the state space during firmware verificationthrough manual abstraction of hardware or manual generation of hints. Manualdevelopment of abstraction or hints requires domain expertise and can betime-consuming and error-prone, leading to incorrect proofs or inaccurateresults. In this paper, we effectively combine the scalability ofsimulation-based validation and the completeness of formal verification. Ourproposed approach is applicable to actual firmware and hardware implementationswithout requiring any manual intervention during formal model generation orhint extraction. To reduce the state space complexity, we utilize both staticmodule-level analysis and dynamic execution of verification scenarios toautomatically generate system-level hints. These hints guide the underlyingsolver to perform scalable equivalence checking using proofs. The extractedhints are validated against the implementation before using them in the proofs.Experimental evaluation on RISC-V based systems demonstrates that our proposedframework is scalable due to scenario-based decomposition and automated hintextraction. Moreover, our fully automated framework can identify complex bugsin actual firmware-hardware implementations.

HIVE: Scalable Hardware-Firmware Co-Verification using Scenario-based Decomposition and Automated Hint Extraction