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

Modern SoCs are heterogeneous parallel systems comprised of componentsdeveloped by distinct teams and possibly even different vendors. The memoryconsistency model (MCM) of processors in such SoCs specifies the ordering ruleswhich constrain the values that can be read by load instructions in parallelprograms running on such systems. The implementation of required MCM orderingscan span components which may be designed and implemented by many differentteams. Ideally, each team would be able to specify the orderings enforced bytheir components independently and then connect them together when conductingMCM verification. However, no prior automated approach for formal hardware MCMverification provided this.  To bring automated hardware MCM verification in line with the realities ofthe design process, we present RealityCheck, a methodology and tool forautomated formal MCM verification of modular microarchitectural orderingspecifications. RealityCheck allows users to specify their designs as ahierarchy of distinct modules connected to each other rather than a single flatspecification. It can then automatically verify litmus test programs againstthese modular specifications. RealityCheck also provides support forabstraction, which enables scalable verification by breaking up theverification of the entire design into smaller verification problems. Wepresent results for verifying litmus tests on 7 different designs usingRealityCheck. These include in-order and out-of-order pipelines, a non-blockingcache, and a heterogeneous processor. Our case studies cover the TSO and RISC-V(RVWMO) weak memory models. RealityCheck is capable of verifying 98 RVWMOlitmus tests in under 4 minutes each, and its capability for abstractionenables up to a 32.1% reduction in litmus test verification time for RVWMO.

RealityCheck: Bringing Modularity, Hierarchy, and Abstraction to Automated Microarchitectural Memory Consistency Verification