Pinned Repositories
berkeley-hardfloat
CacheProof
FpuKami
Kami
Kami - a DSL for designing Hardware in Coq, and the associated semantics and theorems for proving its correctness. Kami is inspired by Bluespec. It is actually a complete rewrite of an older version from MIT
ProcKami
Kami based processor implementations and specifications
RiscvSpecFormal
The RiscvSpecKami package provides SiFive's RISC-V processor model. Built using Coq, this processor model can be used for simulation, model checking, and semantics analysis. The RISC-V processor model can be output as Verilog and simulated/synthesized using standard Verilog tools.
SeqConsistency
StdLibKami
Standard Library of Kami Modules
StructuralSpec
Structural Spec parser based on Bluespec
VerilogParser
Limited Verilog Parser
vmurali's Repositories
vmurali/SeqConsistency
vmurali/StructuralSpec
Structural Spec parser based on Bluespec
vmurali/RiscvSpecFormal
The RiscvSpecKami package provides SiFive's RISC-V processor model. Built using Coq, this processor model can be used for simulation, model checking, and semantics analysis. The RISC-V processor model can be output as Verilog and simulated/synthesized using standard Verilog tools.
vmurali/VerilogParser
Limited Verilog Parser
vmurali/berkeley-hardfloat
vmurali/CacheProof
vmurali/CacheProofBetter
Rewrite, to make it better
vmurali/CacheProofParam
Parametrized across all protocols
vmurali/FpuKami
vmurali/Kami
Kami - a DSL for designing Hardware in Coq, and the associated semantics and theorems for proving its correctness. Kami is inspired by Bluespec. It is actually a complete rewrite of an older version from MIT
vmurali/ProcKami
Kami based processor implementations and specifications
vmurali/StdLibKami
Standard Library of Kami Modules
vmurali/UnifiedScript
Unified script for StructuralSpec and Multicycle
vmurali/cheriot-rtos
The RTOS components for the CHERIoT research platform
vmurali/cheriot-sail
Sail code model of the CHERIoT ISA
vmurali/coq-record-update
Library to create Coq record update functions
vmurali/firrtl
Flexible Intermediate Representation for RTL
vmurali/iree
👻
vmurali/kami-puar
vmurali/matmul
vmurali/ModularBsv
vmurali/QuickCheckVEngine
A RISC-V TestRIG Verification Engine based on QuickCheck
vmurali/Resume
vmurali/riscv-isa-manual
RISC-V Instruction Set Manual
vmurali/SequentialConsistencyPldi
vmurali/SMIPS
SMIPS processor code in Bluespec
vmurali/tensorflow
An Open Source Machine Learning Framework for Everyone
vmurali/test