C

Coq

Fork of https://github.com/smtcoq/smtcoq.

Utilities for dealing with RISC-V instructions in Coq

Things which probably ought to be in Coq's standard library

Formalization in Coq and Why3 of a theory about weak control dependence

A rule-based HDL embedded within Coq

A Kôika implementation of a pipelined RV32I processor with interrupts and exceptions

A Coq port of FIRRTL

Teaching material for an industrial audience

Coherent predicates: translation validation of properties of various types of predicates at runtime, interfacing with SMTCoq for validation of SMT unsatisfiability certificates.

An efficient bitvector type for Coq