cesar/fayalite
1
0
Fork 0
forked from libre-chip/fayalite
Code Pull requests Activity

Format,

Browse source
This commit is contained in:
Cesar Strauss 2025-12-08 21:49:05 -03:00
parent 02de335e46
commit c32cdee4f7
Signed by: cesar
SSH key fingerprint: SHA256:sJUl6USz0D6c6sAQyFZab8XNPJnT05pt2ES0Lv/hCg4
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
rocq-demo/rocq_playground.v
View file

@ -1,11 +1,11 @@
(* SPDX-License-Identifier: LGPL-3.0-or-later
See Notices.txt for copyright information *)
(* This file demonstrates converting simple HDL designs into Rocq, as well
(** This file demonstrates converting simple HDL designs into Rocq, as well
as proofs by induction that parallels those of formal verification in
Symbiyosys with the "smtbmc" engine in the "prove" mode. *)
(* Models a simple register, feeding back to itself. We prove that,
(** Models a simple register, feeding back to itself. We prove that,
when initialized to zero, it stays always at zero. *)
Module simple_register.