Add Fifo spec and proof (#919)

cava/Cava/Util/List.v

@@ -136,6 +136,23 @@ Section Misc.
     rewrite app_comm_cons, !removelast_last. reflexivity.
   Qed.
 
+  Lemma removelast_cons {A} (x0 x1:A) xs : removelast (x0 :: x1 :: xs) = x0 :: removelast (x1 :: xs).
+  Proof. reflexivity. Qed.
+
+  Lemma removelast_cons1 {A} (x:A) xs : xs <> [] -> removelast (x :: xs) = x :: removelast xs.
+  Proof. destruct xs; [contradiction|]. intros; apply removelast_cons. Qed.
+
+  Lemma length_removelast_cons {A} xs (x:A) : length (removelast (x :: xs)) = length xs.
+  Proof.
+    revert x.
+    induction xs; [reflexivity|].
+
+    intros x.
+    rewrite removelast_cons.
+    cbn [length].
+    now rewrite (IHxs _).
+  Qed.
+
   Lemma list_unit_equiv (l : list unit) : l = repeat tt (length l).
   Proof.
     induction l; [ reflexivity | ].

cava2/Fifo.v

@@ -18,6 +18,7 @@ Require Import Coq.Strings.String.
 Require Import Coq.Strings.HexString.
 Require Import Coq.Lists.List.
 Require Import Coq.NArith.NArith.
+Require Import Coq.Arith.PeanoNat.
 Require Import Cava.Util.List.
 
 Require Import Cava.Types.
@@ -38,7 +39,7 @@ Section Var.
   Definition fifo {T} fifo_size: Circuit _ [Bit; T; Bit]
     (* out_valid, out, full *)
     (Bit ** T ** Bit ** Bit) :=
-    let fifo_bits := BitVec (Nat.log2 (fifo_size) + 1) in
+    let fifo_bits := BitVec (Nat.log2_up (fifo_size + 1)) in
     {{
     fun data_valid data accepted_output =>
 
@@ -57,7 +58,7 @@ Section Var.
       initially (false,(default,(@default (Vec T fifo_size), 0)))
       : denote_type (Bit ** T ** Vec T fifo_size ** fifo_bits) in
 
-    ( valid, output
+    ( valid, if valid then output else `Constant T default`
     (* Will be empty if accepted_output is asserted next cycle *)
     , (count == `Constant fifo_bits 0` )
     (* We are full, does not assume output this cycle has been accepted yet *)
@@ -160,6 +161,4 @@ Section Var.
     (out_valid, out_data, out_length, is_last, fifo_full)
   }}.
 
-
 End Var.
-