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

We present a novel approach to pre-silicon verification of processor designs.The purpose of pre-silicon verification is to find logic bugs in a design at anearly stage and thus avoid time- and cost-intensive post-silicon debugging. Ourapproach relies on symbolic quick error detection (Symbolic QED, or SQED). SQEDis targeted at finding logic bugs in a symbolic representation of a design bycombining bounded model checking (BMC) with QED tests. QED tests are powerfulin generating short sequences of instructions (traces) that trigger bugs. Weextend an existing SQED approach with symbolic starting states. This way, weenable the BMC tool to select starting states arbitrarily when generating atrace. To avoid false positives, (e.g., traces starting in unreachable statesthat may not be-have in accordance with the processor instruction-setarchitecture), we define constraints to restrict the set of possible startingstates. We demonstrate that these constraints, togeth-er with reasonableassumptions about the system behavior, allow us to avoid false positives. Usingour approach, we discovered previously unknown bugs in open-source RISC-Vprocessor cores that existing methods cannot detect. Moreover, our novelapproach out-performs existing ones in the detection of bugs having long tracesand in the detection of hardware Trojans, i.e., unauthorized modifications of adesign.

Effective Pre-Silicon Verification of Processor Cores by Breaking the Bounds of Symbolic Quick Error Detection