coq-hardware

Verification and synthesis of hardware linear arithmetic structures. Verification and synthesis of hardware linear arithmetic structures. Example of a left-to-right comparator. Three approaches are tackled : - the usual verification of a circuit, consisting in proving that the description satisfies the specification, - the synthesis of a circuit from its specification using the Coq extractor, - the same approach as above but using the Program tactic.

opam install coq-hardware.8.5.0
homepage
https://github.com/coq-contribs/hardware
license
LGPL 2
bugs tracker
https://github.com/coq-contribs/hardware/issues
dependencies
coq (>= 8.5 & < 8.6~)
source
https://github.com/coq-contribs/hardware/archive/v8.5.0.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-hardware/coq-hardware.8.5.0