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

IC3 is a famous bit-level framework for safety verification. By incorporatingdatapath abstraction, a notable enhancement in the efficiency of hardwareverification can be achieved. However, datapath abstraction entails a coarselevel of abstraction where all datapath operations are approximated asuninterpreted functions. This level of abstraction, albeit useful, can lead toan increased computational burden during the verification process as itnecessitates extensive exploration of redundant abstract state space.  In this paper, we introduce a novel approach called datapath propagation. Ourmethod involves leveraging concrete constant values to iteratively compute theoutcomes of relevant datapath operations and their associated uninterpretedfunctions. Meanwhile, we generate potentially useful datapath propagationlemmas in abstract state space and tighten the datapath abstraction. With thistechnique, the abstract state space can be reduced, and the verificationefficiency is significantly improved. We implemented the proposed approach andconducted extensive experiments. The results show promising improvements of ourapproach compared to the state-of-the-art verifiers.

Leveraging Datapath Propagation in IC3 for Hardware Model Checking