View Code? Open in Web Editor
NEW
A Coq framework to support structural design and proof of hardware cache-coherence protocols
License: MIT License
Coq 51.58%
Makefile 0.06%
Shell 0.02%
Bluespec 48.32%
C++ 0.02%
hemiola's Introduction
Hemiola: A Framework for Structural Design and Proof of Cache-Coherence Protocols
- To machine-check the Coq proofs in Hemiola
- Check all the framework code:
make -j4
in ./src
- Only the library code:
make lib
in ./src
- To compile Hemiola case-study:
make
in ./syn
- The default source protocol is the 3-level noninclusive MESI protocol.
- It will generate
./syn/CC.bsv
.
- All the case-study protocols are precompiled in
./syn/integration
:
./syn/integration/CC_L1LL4
: the 2-level noninclusive MESI protocol
./syn/integration/CC_L1L2LL
: the 3-level noninclusive MESI protocol
- To simulate a compiled protocol:
make
in ./syn/integration/sim
- To synthesize a compiled protocol:
make -j4 build.vc707g2
in ./syn/integration/syn
hemiola's People
Contributors