CHARME 2001 | Sciweavers

27

CHARME
2001
Springer

73views Hardware» more CHARME 2001»

A Framework for Microprocessor Correctness Statements

14 years 5 months ago

Abstract Most veriﬁcations of out-of-order microprocessors compare state-machine-based implementations and speciﬁcations, where the speciﬁcation is based on the instruction-s...

Mark Aagaard, Byron Cook, Nancy A. Day, Robert B. ...

claim paper

Read More »

31

click to vote

CHARME
2001
Springer

98views Hardware» more CHARME 2001»

Hardware Synthesis Using SAFL and Application to Processor Design

14 years 5 months ago

Download rich.recoil.org

Abstract. We survey the work done so far in the FLaSH project (Functional Languages for Synthesising Hardware) in which the core ideas are (i) using a functional language SAFL to d...

Alan Mycroft, Richard Sharp

claim paper

Read More »

33

click to vote

CHARME
2001
Springer

68views Hardware» more CHARME 2001»

Heuristics for Hierarchical Partitioning with Application to Model Checking

14 years 5 months ago