From 9f0640ab94741d1d369d089fec763c9156d6be4f Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 19 Mar 2020 15:20:13 +0000 Subject: Lower case folders --- src/Common/Helper.v | 39 ------- src/Common/Show.v | 61 ----------- src/Common/Tactics.v | 29 ----- src/Common/dune | 3 - src/Driver/CompCert.v | 97 ----------------- src/Driver/Driver.ml | 22 ---- src/Driver/dune | 7 -- src/Extraction/Extraction.v | 30 ------ src/Extraction/dune | 4 - src/Verilog/PrettyPrint.ml | 66 ------------ src/Verilog/PrettyPrint.mli | 19 ---- src/Verilog/VerilogAST.v | 252 -------------------------------------------- src/Verilog/dune | 4 - src/common/Helper.v | 39 +++++++ src/common/Show.v | 61 +++++++++++ src/common/Tactics.v | 29 +++++ src/common/dune | 3 + src/driver/CompCert.v | 97 +++++++++++++++++ src/driver/Driver.ml | 22 ++++ src/driver/dune | 7 ++ src/extraction/Extraction.v | 30 ++++++ src/extraction/dune | 4 + src/verilog/PrettyPrint.ml | 66 ++++++++++++ src/verilog/PrettyPrint.mli | 19 ++++ src/verilog/VerilogAST.v | 252 ++++++++++++++++++++++++++++++++++++++++++++ src/verilog/dune | 4 + 26 files changed, 633 insertions(+), 633 deletions(-) delete mode 100644 src/Common/Helper.v delete mode 100644 src/Common/Show.v delete mode 100644 src/Common/Tactics.v delete mode 100644 src/Common/dune delete mode 100644 src/Driver/CompCert.v delete mode 100644 src/Driver/Driver.ml delete mode 100644 src/Driver/dune delete mode 100644 src/Extraction/Extraction.v delete mode 100644 src/Extraction/dune delete mode 100644 src/Verilog/PrettyPrint.ml delete mode 100644 src/Verilog/PrettyPrint.mli delete mode 100644 src/Verilog/VerilogAST.v delete mode 100644 src/Verilog/dune create mode 100644 src/common/Helper.v create mode 100644 src/common/Show.v create mode 100644 src/common/Tactics.v create mode 100644 src/common/dune create mode 100644 src/driver/CompCert.v create mode 100644 src/driver/Driver.ml create mode 100644 src/driver/dune create mode 100644 src/extraction/Extraction.v create mode 100644 src/extraction/dune create mode 100644 src/verilog/PrettyPrint.ml create mode 100644 src/verilog/PrettyPrint.mli create mode 100644 src/verilog/VerilogAST.v create mode 100644 src/verilog/dune (limited to 'src') diff --git a/src/Common/Helper.v b/src/Common/Helper.v deleted file mode 100644 index d23dbe4..0000000 --- a/src/Common/Helper.v +++ /dev/null @@ -1,39 +0,0 @@ -(* - * CoqUp: Verified high-level synthesis. - * Copyright (C) 2019-2020 Yann Herklotz - * - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU General Public License as published by - * the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * This program is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with this program. If not, see . - *) - -Module Option. - -Definition default {T : Type} (x : T) (u : option T) : T := - match u with - | Some y => y - | _ => x - end. - -Definition map {S : Type} {T : Type} (f : S -> T) (u : option S) : option T := - match u with - | Some y => Some (f y) - | _ => None - end. - -Definition liftA2 {T : Type} (f : T -> T -> T) (a : option T) (b : option T) : option T := - match a with - | Some x => map (f x) b - | _ => None - end. - -End Option. diff --git a/src/Common/Show.v b/src/Common/Show.v deleted file mode 100644 index 8f9ec36..0000000 --- a/src/Common/Show.v +++ /dev/null @@ -1,61 +0,0 @@ -(* - * CoqUp: Verified high-level synthesis. - * Copyright (C) 2019-2020 Yann Herklotz - * - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU General Public License as published by - * the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * This program is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with this program. If not, see . - *) - -From Coq Require Import - Strings.String - Bool.Bool - Arith.Arith. - -Local Open Scope string. - -Module Show. - Class Show A : Type := - { - show : A -> string - }. - - Instance showBool : Show bool := - { - show := fun b:bool => if b then "true" else "false" - }. - - Fixpoint string_of_nat_aux (time n : nat) (acc : string) : string := - let d := match n mod 10 with - | 0 => "0" | 1 => "1" | 2 => "2" | 3 => "3" | 4 => "4" | 5 => "5" - | 6 => "6" | 7 => "7" | 8 => "8" | _ => "9" - end in - let acc' := d ++ acc in - match time with - | 0 => acc' - | S time' => - match n / 10 with - | 0 => acc' - | n' => string_of_nat_aux time' n' acc' - end - end. - - Definition string_of_nat (n : nat) : string := - string_of_nat_aux n n "". - - Instance showNat : Show nat := - { - show := string_of_nat - }. - -End Show. -Export Show. diff --git a/src/Common/Tactics.v b/src/Common/Tactics.v deleted file mode 100644 index 967c642..0000000 --- a/src/Common/Tactics.v +++ /dev/null @@ -1,29 +0,0 @@ -(* - * CoqUp: Verified high-level synthesis. - * Copyright (C) 2019-2020 Yann Herklotz - * - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU General Public License as published by - * the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * This program is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with this program. If not, see . - *) - -Ltac unfold_rec c := unfold c; fold c. - -Ltac solve_by_inverts n := - match goal with | H : ?T |- _ => - match type of T with Prop => - inversion H; - match n with S (S (?n')) => subst; try constructor; solve_by_inverts (S n') end - end - end. - -Ltac solve_by_invert := solve_by_inverts 1. diff --git a/src/Common/dune b/src/Common/dune deleted file mode 100644 index de481e2..0000000 --- a/src/Common/dune +++ /dev/null @@ -1,3 +0,0 @@ -(library - (name Common) - (public_name coqup.common)) diff --git a/src/Driver/CompCert.v b/src/Driver/CompCert.v deleted file mode 100644 index d8dcb97..0000000 --- a/src/Driver/CompCert.v +++ /dev/null @@ -1,97 +0,0 @@ -(* - * CoqUp: Verified high-level synthesis. - * Copyright (C) 2019-2020 Yann Herklotz - * - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU General Public License as published by - * the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * This program is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with this program. If not, see . - *) - -From compcert.common Require Import - Errors - Linking. - -From compcert.lib Require Import - Coqlib. - -From compcert.backend Require - Selection - RTL - RTLgen - Tailcall - Inlining - Renumber - Constprop - CSE - Deadcode - Unusedglob. - -From compcert.cfrontend Require - Csyntax - SimplExpr - SimplLocals - Cshmgen - Cminorgen. - -From compcert.driver Require - Compiler. - -Notation "a @@@ b" := - (Compiler.apply_partial _ _ a b) (at level 50, left associativity). -Notation "a @@ b" := - (Compiler.apply_total _ _ a b) (at level 50, left associativity). - -Definition transf_frontend (p: Csyntax.program) : res RTL.program := - OK p - @@@ SimplExpr.transl_program - @@@ SimplLocals.transf_program - @@@ Cshmgen.transl_program - @@@ Cminorgen.transl_program - @@@ Selection.sel_program - @@@ RTLgen.transl_program. - -Local Open Scope linking_scope. - -Definition CompCert's_passes := - mkpass SimplExprproof.match_prog - ::: mkpass SimplLocalsproof.match_prog - ::: mkpass Cshmgenproof.match_prog - ::: mkpass Cminorgenproof.match_prog - ::: mkpass Selectionproof.match_prog - ::: mkpass RTLgenproof.match_prog - ::: pass_nil _. - -Definition match_prog: Csyntax.program -> RTL.program -> Prop := - pass_match (compose_passes CompCert's_passes). - -Theorem transf_frontend_match: - forall p tp, - transf_frontend p = OK tp -> - match_prog p tp. -Proof. - intros p tp T. - unfold transf_frontend in T. simpl in T. - destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; simpl in T; try discriminate. - destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; simpl in T; try discriminate. - destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; simpl in T; try discriminate. - destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; simpl in T; try discriminate. - destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. - destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. - unfold match_prog; simpl. - exists p1; split. apply SimplExprproof.transf_program_match; auto. - exists p2; split. apply SimplLocalsproof.match_transf_program; auto. - exists p3; split. apply Cshmgenproof.transf_program_match; auto. - exists p4; split. apply Cminorgenproof.transf_program_match; auto. - exists p5; split. apply Selectionproof.transf_program_match; auto. - exists p6; split. apply RTLgenproof.transf_program_match; auto. - inversion T. reflexivity. -Qed. diff --git a/src/Driver/Driver.ml b/src/Driver/Driver.ml deleted file mode 100644 index 40a45e6..0000000 --- a/src/Driver/Driver.ml +++ /dev/null @@ -1,22 +0,0 @@ -(* - * CoqUp: Verified high-level synthesis. - * Copyright (C) 2019-2020 Yann Herklotz - * - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU General Public License as published by - * the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * This program is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with this program. If not, see . - *) - -open Verilog -open Extraction - -let _ = print_string (PrettyPrint.prettyprint VerilogAST.verilog_example) diff --git a/src/Driver/dune b/src/Driver/dune deleted file mode 100644 index e295a76..0000000 --- a/src/Driver/dune +++ /dev/null @@ -1,7 +0,0 @@ -(executables - (names Driver) - (libraries compcert coqup.verilog coqup.extraction)) - -(install - (section bin) - (files (Driver.exe as coqup))) diff --git a/src/Extraction/Extraction.v b/src/Extraction/Extraction.v deleted file mode 100644 index 01b03d1..0000000 --- a/src/Extraction/Extraction.v +++ /dev/null @@ -1,30 +0,0 @@ -(* - * CoqUp: Verified high-level synthesis. - * Copyright (C) 2019-2020 Yann Herklotz - * - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU General Public License as published by - * the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * This program is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with this program. If not, see . - *) - -Require CoqUp.Verilog.VerilogAST. - -(* Standard lib *) -Require Import ExtrOcamlBasic. -Require Import ExtrOcamlString. - -(* Avoid name clashes *) -Extraction Blacklist List String Int. - -Cd "src/Extraction". -Separate Extraction - VerilogAST.nat_to_value VerilogAST.value_to_nat VerilogAST.verilog VerilogAST.verilog_example. diff --git a/src/Extraction/dune b/src/Extraction/dune deleted file mode 100644 index 731701a..0000000 --- a/src/Extraction/dune +++ /dev/null @@ -1,4 +0,0 @@ -(library - (name Extraction) - (public_name coqup.extraction) - (flags (:standard -warn-error -A))) diff --git a/src/Verilog/PrettyPrint.ml b/src/Verilog/PrettyPrint.ml deleted file mode 100644 index 9b7750d..0000000 --- a/src/Verilog/PrettyPrint.ml +++ /dev/null @@ -1,66 +0,0 @@ -(* - * CoqUp: Verified high-level synthesis. - * Copyright (C) 2019-2020 Yann Herklotz - * - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU General Public License as published by - * the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * This program is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with this program. If not, see . - *) - -open Extraction.VerilogAST - -let concat = String.concat "" - -let indent i = String.make (2 * i) ' ' - -let fold_map f s = List.map f s |> concat - -let rec pprint_value = function - | VBool l -> if l then "1" else "0" - (* Assume that array is flat if it's a literal, should probably be changed to a nat or int *) - | VArray a -> concat [List.length a |> string_of_int; "'b"; fold_map pprint_value a] - -let pprint_binop = function - | Plus -> " + " - | Minus -> " - " - | Times -> " * " - | Divide -> " / " - | LT -> " < " - | GT -> " > " - | LE -> " <= " - | GE -> " >= " - | Eq -> " == " - | And -> " & " - | Or -> " | " - | Xor -> " ^ " - -let rec pprint_expr = function - | Lit l -> pprint_value l - | Var s -> List.to_seq s |> String.of_seq - | Neg e -> concat ["(-"; pprint_expr e; ")"] - | BinOp (op, a, b) -> concat ["("; pprint_expr a; pprint_binop op; pprint_expr b; ")"] - | Ternary (c, t, f) -> concat ["("; pprint_expr c; " ? "; pprint_expr t; " : "; pprint_expr f; ")"] - -let rec pprint_stmnt i = - let pprint_case (e, s) = concat [indent (i + 1); pprint_expr e; ":\n"; pprint_stmnt (i + 2) s] - in function - | Skip -> concat [indent i; ";\n"] - | Block s -> concat [indent i; "begin\n"; fold_map (pprint_stmnt (i+1)) s; indent i; "end\n"] - | Cond (e, st, sf) -> concat [indent i; "if ("; pprint_expr e; ")\n"; - pprint_stmnt (i + 1) st; indent i; "else\n"; - pprint_stmnt (i + 1) sf] - | Case (e, es) -> concat [indent i; "case ("; pprint_expr e; ")\n"; - fold_map pprint_case es; indent i; "endcase\n"] - | Blocking (a, b) -> concat [indent i; pprint_expr a; " = "; pprint_expr b; ";\n"] - | Nonblocking (a, b) -> concat [indent i; pprint_expr a; " <= "; pprint_expr b; ";\n"] - -let prettyprint = fold_map (pprint_stmnt 0) diff --git a/src/Verilog/PrettyPrint.mli b/src/Verilog/PrettyPrint.mli deleted file mode 100644 index a8b6e01..0000000 --- a/src/Verilog/PrettyPrint.mli +++ /dev/null @@ -1,19 +0,0 @@ -(* - * CoqUp: Verified high-level synthesis. - * Copyright (C) 2019-2020 Yann Herklotz - * - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU General Public License as published by - * the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * This program is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with this program. If not, see . - *) - -val prettyprint : Extraction.VerilogAST.verilog -> string diff --git a/src/Verilog/VerilogAST.v b/src/Verilog/VerilogAST.v deleted file mode 100644 index 8bb8ba8..0000000 --- a/src/Verilog/VerilogAST.v +++ /dev/null @@ -1,252 +0,0 @@ -(* - * CoqUp: Verified high-level synthesis. - * Copyright (C) 2019-2020 Yann Herklotz - * - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU General Public License as published by - * the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * This program is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with this program. If not, see . - *) - -From Coq Require Import Lists.List Strings.String. -From Coq Require Import -Structures.OrderedTypeEx -FSets.FMapList -Program.Basics -PeanoNat. - -From coqup.common Require Import Helper Tactics Show. - -Import ListNotations. - -Module Map := FMapList.Make String_as_OT. - -Inductive value : Type := -| VBool (b : bool) -| VArray (l : list value). - -Inductive literal : Type := LitArray (l : list bool). - -Definition cons_value (a b : value) : value := - match a, b with - | VBool _, VArray b' => VArray (a :: b') - | VArray a', VBool _ => VArray (List.concat [a'; [b]]) - | VArray a', VArray b' => VArray (List.concat [a'; b']) - | _, _ => VArray [a; b] - end. - -(** * Conversion to and from value *) - -Fixpoint nat_to_value' (sz n : nat) : value := - match sz with - | 0 => VArray [] - | S sz' => - if Nat.even n then - cons_value (VBool false) (nat_to_value' sz' (Nat.div n 2)) - else - cons_value (VBool true) (nat_to_value' sz' (Nat.div n 2)) - end. - -Definition nat_to_value (n : nat) : value := - nat_to_value' ((Nat.log2 n) + 1) n. - -Definition state : Type := Map.t value * Map.t value. - -Inductive binop : Type := -| Plus -| Minus -| Times -| Divide -| LT -| GT -| LE -| GE -| Eq -| And -| Or -| Xor. - -Inductive expr : Type := -| Lit (n : value) -| Var (s : string) -| Neg (a : expr) -| BinOp (op : binop) (a1 a2 : expr) -| Ternary (c t f : expr). - -Inductive stmnt : Type := -| Skip -| Block (s : list stmnt) -| Cond (c : expr) (st sf : stmnt) -| Case (c : expr) (b : list (expr * stmnt)) -| Blocking (a b : expr) -| Nonblocking (a b : expr). - -Inductive verilog : Type := Verilog (s : list stmnt). - -Definition verilog_example := Verilog [Block [Nonblocking (Var "hello") (BinOp Plus (Lit (nat_to_value 40)) (Lit (nat_to_value 20))); Cond (BinOp LE (Lit (nat_to_value 2)) (Lit (nat_to_value 3))) (Blocking (Var "Another") (BinOp Times (Lit (nat_to_value 20)) (Lit (nat_to_value 500)))) Skip]; Block []]. - -Coercion VBool : bool >-> value. -Coercion Lit : value >-> expr. -Coercion Var : string >-> expr. - -Definition value_is_bool (v : value) : bool := - match v with - | VBool _ => true - | VArray _ => false - end. - -Definition value_is_array : value -> bool := compose negb value_is_bool. - -Definition flat_value (v : value) : bool := - match v with - | VBool _ => true - | VArray l => forallb value_is_bool l - end. - -Inductive value_is_boolP : value -> Prop := -| ValIsBool : forall b : bool, value_is_boolP (VBool b). - -Inductive value_is_arrayP : value -> Prop := -| ValIsArray : forall v : list value, value_is_arrayP (VArray v). - -Inductive flat_valueP : value -> Prop := -| FLV0 : forall b : bool, flat_valueP (VBool b) -| FLVA : forall l : list value, - Forall (value_is_boolP) l -> flat_valueP (VArray l). - -Lemma value_is_bool_equiv : - forall v, value_is_boolP v <-> value_is_bool v = true. -Proof. - split; intros. - - inversion H. trivial. - - destruct v. constructor. unfold value_is_bool in H. discriminate. -Qed. - -Lemma value_is_array_equiv : - forall v, value_is_arrayP v <-> value_is_array v = true. -Proof. - split; intros. - - inversion H. trivial. - - destruct v; try constructor. unfold value_is_array in H. - unfold compose, value_is_bool, negb in H. discriminate. -Qed. - -Lemma flat_value_equiv : - forall v, flat_valueP v <-> flat_value v = true. -Proof. - split; intros. - - unfold flat_value. inversion H. subst. trivial. - + rewrite Forall_forall in H0. rewrite forallb_forall. intros. subst. - apply value_is_bool_equiv. apply H0. assumption. - - destruct v. constructor. constructor. unfold flat_value in H. - rewrite Forall_forall. rewrite forallb_forall in H. intros. apply value_is_bool_equiv. - apply H. assumption. -Qed. - -Fixpoint value_to_nat' (i : nat) (v : value) : option nat := - match i, v with - | _, VBool b => Some (Nat.b2n b) - | _, VArray [VBool b] => Some (Nat.b2n b) - | S i', VArray ((VBool b) :: l) => - Option.map (compose (Nat.add (Nat.b2n b)) (Mult.tail_mult 2)) (value_to_nat' i' (VArray l)) - | _, _ => None - end. - -Definition value_length (v : value) : nat := - match v with - | VBool _ => 1 - | VArray l => Datatypes.length l - end. - -Definition value_to_nat (v : value) : option nat := - value_to_nat' (value_length v) v. - -Lemma empty_is_flat : flat_valueP (VArray []). -Proof. - constructor. apply Forall_forall. intros. inversion H. -Qed. - -Lemma check_5_is_101 : - value_to_nat (VArray [VBool true; VBool false; VBool true]) = Some 5. -Proof. reflexivity. Qed. - -Lemma cons_value_flat : - forall (b : bool) (v : value), - flat_valueP v -> flat_valueP (cons_value (VBool b) v). -Proof. - intros. unfold cons_value. destruct v. - - constructor. apply Forall_forall. intros. - inversion H0; subst. constructor. - inversion H1; subst. constructor. - inversion H2. - - intros. inversion H. inversion H1; subst; constructor. - + apply Forall_forall. intros. - inversion H0; subst. constructor. - inversion H2. - + repeat constructor. assumption. assumption. -Qed. - -Lemma nat_to_value'_is_flat : - forall (sz n : nat), - flat_valueP (nat_to_value' sz n). -Proof. - induction sz; intros. - - subst. apply empty_is_flat. - - unfold_rec nat_to_value'. - destruct (Nat.even n); apply cons_value_flat; apply IHsz. -Qed. - -Lemma nat_to_value_is_flat : - forall (sz n : nat), - flat_valueP (nat_to_value n). -Proof. - intros. unfold nat_to_value. apply nat_to_value'_is_flat. -Qed. - -Lemma nat_to_value_idempotent : - forall (sz n : nat), - sz > 0 -> (value_to_nat' sz (nat_to_value' sz n)) = Some n. -Proof. - induction sz; intros. - - inversion H. - - unfold_rec value_to_nat'. - assert (flat_valueP (nat_to_value' (S sz) n)). - { apply nat_to_value'_is_flat. } - destruct (nat_to_value' (S sz) n) eqn:?. -Admitted. - -Module VerilogEval. - - Definition app (f : nat -> nat -> nat) (a : value) (b : value) : option value := - Option.map nat_to_value (Option.liftA2 f (value_to_nat a) (value_to_nat b)). - - Definition state_find (k : string) (s : state) : option value := - Map.find k (fst s). - - Definition eval_binop (op : binop) (a1 a2 : value) : option value := - match op with - | Plus => app Nat.add a1 a2 - | Minus => app Nat.sub a1 a2 - | Times => app Mult.tail_mult a1 a2 - | Divide => app Nat.div a1 a2 - | _ => Some a1 - end. - -(* Fixpoint eval_expr (s : state) (e : expr) : option value := - match e with - | Lit n => Some n - | Var v => state_find v s - | Neg a => 0 - (eval_expr s a) - | BinOp op a1 a2 => eval_binop op a1 a2 - | Ternary c t f => if eval_expr s c then eval_expr s t else eval_expr s f - end. - *) -End VerilogEval. diff --git a/src/Verilog/dune b/src/Verilog/dune deleted file mode 100644 index 227d4a5..0000000 --- a/src/Verilog/dune +++ /dev/null @@ -1,4 +0,0 @@ -(library - (name Verilog) - (public_name coqup.verilog) - (libraries coqup.extraction)) diff --git a/src/common/Helper.v b/src/common/Helper.v new file mode 100644 index 0000000..d23dbe4 --- /dev/null +++ b/src/common/Helper.v @@ -0,0 +1,39 @@ +(* + * CoqUp: Verified high-level synthesis. + * Copyright (C) 2019-2020 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +Module Option. + +Definition default {T : Type} (x : T) (u : option T) : T := + match u with + | Some y => y + | _ => x + end. + +Definition map {S : Type} {T : Type} (f : S -> T) (u : option S) : option T := + match u with + | Some y => Some (f y) + | _ => None + end. + +Definition liftA2 {T : Type} (f : T -> T -> T) (a : option T) (b : option T) : option T := + match a with + | Some x => map (f x) b + | _ => None + end. + +End Option. diff --git a/src/common/Show.v b/src/common/Show.v new file mode 100644 index 0000000..8f9ec36 --- /dev/null +++ b/src/common/Show.v @@ -0,0 +1,61 @@ +(* + * CoqUp: Verified high-level synthesis. + * Copyright (C) 2019-2020 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +From Coq Require Import + Strings.String + Bool.Bool + Arith.Arith. + +Local Open Scope string. + +Module Show. + Class Show A : Type := + { + show : A -> string + }. + + Instance showBool : Show bool := + { + show := fun b:bool => if b then "true" else "false" + }. + + Fixpoint string_of_nat_aux (time n : nat) (acc : string) : string := + let d := match n mod 10 with + | 0 => "0" | 1 => "1" | 2 => "2" | 3 => "3" | 4 => "4" | 5 => "5" + | 6 => "6" | 7 => "7" | 8 => "8" | _ => "9" + end in + let acc' := d ++ acc in + match time with + | 0 => acc' + | S time' => + match n / 10 with + | 0 => acc' + | n' => string_of_nat_aux time' n' acc' + end + end. + + Definition string_of_nat (n : nat) : string := + string_of_nat_aux n n "". + + Instance showNat : Show nat := + { + show := string_of_nat + }. + +End Show. +Export Show. diff --git a/src/common/Tactics.v b/src/common/Tactics.v new file mode 100644 index 0000000..967c642 --- /dev/null +++ b/src/common/Tactics.v @@ -0,0 +1,29 @@ +(* + * CoqUp: Verified high-level synthesis. + * Copyright (C) 2019-2020 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +Ltac unfold_rec c := unfold c; fold c. + +Ltac solve_by_inverts n := + match goal with | H : ?T |- _ => + match type of T with Prop => + inversion H; + match n with S (S (?n')) => subst; try constructor; solve_by_inverts (S n') end + end + end. + +Ltac solve_by_invert := solve_by_inverts 1. diff --git a/src/common/dune b/src/common/dune new file mode 100644 index 0000000..de481e2 --- /dev/null +++ b/src/common/dune @@ -0,0 +1,3 @@ +(library + (name Common) + (public_name coqup.common)) diff --git a/src/driver/CompCert.v b/src/driver/CompCert.v new file mode 100644 index 0000000..d8dcb97 --- /dev/null +++ b/src/driver/CompCert.v @@ -0,0 +1,97 @@ +(* + * CoqUp: Verified high-level synthesis. + * Copyright (C) 2019-2020 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +From compcert.common Require Import + Errors + Linking. + +From compcert.lib Require Import + Coqlib. + +From compcert.backend Require + Selection + RTL + RTLgen + Tailcall + Inlining + Renumber + Constprop + CSE + Deadcode + Unusedglob. + +From compcert.cfrontend Require + Csyntax + SimplExpr + SimplLocals + Cshmgen + Cminorgen. + +From compcert.driver Require + Compiler. + +Notation "a @@@ b" := + (Compiler.apply_partial _ _ a b) (at level 50, left associativity). +Notation "a @@ b" := + (Compiler.apply_total _ _ a b) (at level 50, left associativity). + +Definition transf_frontend (p: Csyntax.program) : res RTL.program := + OK p + @@@ SimplExpr.transl_program + @@@ SimplLocals.transf_program + @@@ Cshmgen.transl_program + @@@ Cminorgen.transl_program + @@@ Selection.sel_program + @@@ RTLgen.transl_program. + +Local Open Scope linking_scope. + +Definition CompCert's_passes := + mkpass SimplExprproof.match_prog + ::: mkpass SimplLocalsproof.match_prog + ::: mkpass Cshmgenproof.match_prog + ::: mkpass Cminorgenproof.match_prog + ::: mkpass Selectionproof.match_prog + ::: mkpass RTLgenproof.match_prog + ::: pass_nil _. + +Definition match_prog: Csyntax.program -> RTL.program -> Prop := + pass_match (compose_passes CompCert's_passes). + +Theorem transf_frontend_match: + forall p tp, + transf_frontend p = OK tp -> + match_prog p tp. +Proof. + intros p tp T. + unfold transf_frontend in T. simpl in T. + destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; simpl in T; try discriminate. + destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; simpl in T; try discriminate. + destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; simpl in T; try discriminate. + destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; simpl in T; try discriminate. + destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. + destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. + unfold match_prog; simpl. + exists p1; split. apply SimplExprproof.transf_program_match; auto. + exists p2; split. apply SimplLocalsproof.match_transf_program; auto. + exists p3; split. apply Cshmgenproof.transf_program_match; auto. + exists p4; split. apply Cminorgenproof.transf_program_match; auto. + exists p5; split. apply Selectionproof.transf_program_match; auto. + exists p6; split. apply RTLgenproof.transf_program_match; auto. + inversion T. reflexivity. +Qed. diff --git a/src/driver/Driver.ml b/src/driver/Driver.ml new file mode 100644 index 0000000..40a45e6 --- /dev/null +++ b/src/driver/Driver.ml @@ -0,0 +1,22 @@ +(* + * CoqUp: Verified high-level synthesis. + * Copyright (C) 2019-2020 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +open Verilog +open Extraction + +let _ = print_string (PrettyPrint.prettyprint VerilogAST.verilog_example) diff --git a/src/driver/dune b/src/driver/dune new file mode 100644 index 0000000..e295a76 --- /dev/null +++ b/src/driver/dune @@ -0,0 +1,7 @@ +(executables + (names Driver) + (libraries compcert coqup.verilog coqup.extraction)) + +(install + (section bin) + (files (Driver.exe as coqup))) diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v new file mode 100644 index 0000000..01b03d1 --- /dev/null +++ b/src/extraction/Extraction.v @@ -0,0 +1,30 @@ +(* + * CoqUp: Verified high-level synthesis. + * Copyright (C) 2019-2020 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +Require CoqUp.Verilog.VerilogAST. + +(* Standard lib *) +Require Import ExtrOcamlBasic. +Require Import ExtrOcamlString. + +(* Avoid name clashes *) +Extraction Blacklist List String Int. + +Cd "src/Extraction". +Separate Extraction + VerilogAST.nat_to_value VerilogAST.value_to_nat VerilogAST.verilog VerilogAST.verilog_example. diff --git a/src/extraction/dune b/src/extraction/dune new file mode 100644 index 0000000..731701a --- /dev/null +++ b/src/extraction/dune @@ -0,0 +1,4 @@ +(library + (name Extraction) + (public_name coqup.extraction) + (flags (:standard -warn-error -A))) diff --git a/src/verilog/PrettyPrint.ml b/src/verilog/PrettyPrint.ml new file mode 100644 index 0000000..9b7750d --- /dev/null +++ b/src/verilog/PrettyPrint.ml @@ -0,0 +1,66 @@ +(* + * CoqUp: Verified high-level synthesis. + * Copyright (C) 2019-2020 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +open Extraction.VerilogAST + +let concat = String.concat "" + +let indent i = String.make (2 * i) ' ' + +let fold_map f s = List.map f s |> concat + +let rec pprint_value = function + | VBool l -> if l then "1" else "0" + (* Assume that array is flat if it's a literal, should probably be changed to a nat or int *) + | VArray a -> concat [List.length a |> string_of_int; "'b"; fold_map pprint_value a] + +let pprint_binop = function + | Plus -> " + " + | Minus -> " - " + | Times -> " * " + | Divide -> " / " + | LT -> " < " + | GT -> " > " + | LE -> " <= " + | GE -> " >= " + | Eq -> " == " + | And -> " & " + | Or -> " | " + | Xor -> " ^ " + +let rec pprint_expr = function + | Lit l -> pprint_value l + | Var s -> List.to_seq s |> String.of_seq + | Neg e -> concat ["(-"; pprint_expr e; ")"] + | BinOp (op, a, b) -> concat ["("; pprint_expr a; pprint_binop op; pprint_expr b; ")"] + | Ternary (c, t, f) -> concat ["("; pprint_expr c; " ? "; pprint_expr t; " : "; pprint_expr f; ")"] + +let rec pprint_stmnt i = + let pprint_case (e, s) = concat [indent (i + 1); pprint_expr e; ":\n"; pprint_stmnt (i + 2) s] + in function + | Skip -> concat [indent i; ";\n"] + | Block s -> concat [indent i; "begin\n"; fold_map (pprint_stmnt (i+1)) s; indent i; "end\n"] + | Cond (e, st, sf) -> concat [indent i; "if ("; pprint_expr e; ")\n"; + pprint_stmnt (i + 1) st; indent i; "else\n"; + pprint_stmnt (i + 1) sf] + | Case (e, es) -> concat [indent i; "case ("; pprint_expr e; ")\n"; + fold_map pprint_case es; indent i; "endcase\n"] + | Blocking (a, b) -> concat [indent i; pprint_expr a; " = "; pprint_expr b; ";\n"] + | Nonblocking (a, b) -> concat [indent i; pprint_expr a; " <= "; pprint_expr b; ";\n"] + +let prettyprint = fold_map (pprint_stmnt 0) diff --git a/src/verilog/PrettyPrint.mli b/src/verilog/PrettyPrint.mli new file mode 100644 index 0000000..a8b6e01 --- /dev/null +++ b/src/verilog/PrettyPrint.mli @@ -0,0 +1,19 @@ +(* + * CoqUp: Verified high-level synthesis. + * Copyright (C) 2019-2020 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +val prettyprint : Extraction.VerilogAST.verilog -> string diff --git a/src/verilog/VerilogAST.v b/src/verilog/VerilogAST.v new file mode 100644 index 0000000..8bb8ba8 --- /dev/null +++ b/src/verilog/VerilogAST.v @@ -0,0 +1,252 @@ +(* + * CoqUp: Verified high-level synthesis. + * Copyright (C) 2019-2020 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +From Coq Require Import Lists.List Strings.String. +From Coq Require Import +Structures.OrderedTypeEx +FSets.FMapList +Program.Basics +PeanoNat. + +From coqup.common Require Import Helper Tactics Show. + +Import ListNotations. + +Module Map := FMapList.Make String_as_OT. + +Inductive value : Type := +| VBool (b : bool) +| VArray (l : list value). + +Inductive literal : Type := LitArray (l : list bool). + +Definition cons_value (a b : value) : value := + match a, b with + | VBool _, VArray b' => VArray (a :: b') + | VArray a', VBool _ => VArray (List.concat [a'; [b]]) + | VArray a', VArray b' => VArray (List.concat [a'; b']) + | _, _ => VArray [a; b] + end. + +(** * Conversion to and from value *) + +Fixpoint nat_to_value' (sz n : nat) : value := + match sz with + | 0 => VArray [] + | S sz' => + if Nat.even n then + cons_value (VBool false) (nat_to_value' sz' (Nat.div n 2)) + else + cons_value (VBool true) (nat_to_value' sz' (Nat.div n 2)) + end. + +Definition nat_to_value (n : nat) : value := + nat_to_value' ((Nat.log2 n) + 1) n. + +Definition state : Type := Map.t value * Map.t value. + +Inductive binop : Type := +| Plus +| Minus +| Times +| Divide +| LT +| GT +| LE +| GE +| Eq +| And +| Or +| Xor. + +Inductive expr : Type := +| Lit (n : value) +| Var (s : string) +| Neg (a : expr) +| BinOp (op : binop) (a1 a2 : expr) +| Ternary (c t f : expr). + +Inductive stmnt : Type := +| Skip +| Block (s : list stmnt) +| Cond (c : expr) (st sf : stmnt) +| Case (c : expr) (b : list (expr * stmnt)) +| Blocking (a b : expr) +| Nonblocking (a b : expr). + +Inductive verilog : Type := Verilog (s : list stmnt). + +Definition verilog_example := Verilog [Block [Nonblocking (Var "hello") (BinOp Plus (Lit (nat_to_value 40)) (Lit (nat_to_value 20))); Cond (BinOp LE (Lit (nat_to_value 2)) (Lit (nat_to_value 3))) (Blocking (Var "Another") (BinOp Times (Lit (nat_to_value 20)) (Lit (nat_to_value 500)))) Skip]; Block []]. + +Coercion VBool : bool >-> value. +Coercion Lit : value >-> expr. +Coercion Var : string >-> expr. + +Definition value_is_bool (v : value) : bool := + match v with + | VBool _ => true + | VArray _ => false + end. + +Definition value_is_array : value -> bool := compose negb value_is_bool. + +Definition flat_value (v : value) : bool := + match v with + | VBool _ => true + | VArray l => forallb value_is_bool l + end. + +Inductive value_is_boolP : value -> Prop := +| ValIsBool : forall b : bool, value_is_boolP (VBool b). + +Inductive value_is_arrayP : value -> Prop := +| ValIsArray : forall v : list value, value_is_arrayP (VArray v). + +Inductive flat_valueP : value -> Prop := +| FLV0 : forall b : bool, flat_valueP (VBool b) +| FLVA : forall l : list value, + Forall (value_is_boolP) l -> flat_valueP (VArray l). + +Lemma value_is_bool_equiv : + forall v, value_is_boolP v <-> value_is_bool v = true. +Proof. + split; intros. + - inversion H. trivial. + - destruct v. constructor. unfold value_is_bool in H. discriminate. +Qed. + +Lemma value_is_array_equiv : + forall v, value_is_arrayP v <-> value_is_array v = true. +Proof. + split; intros. + - inversion H. trivial. + - destruct v; try constructor. unfold value_is_array in H. + unfold compose, value_is_bool, negb in H. discriminate. +Qed. + +Lemma flat_value_equiv : + forall v, flat_valueP v <-> flat_value v = true. +Proof. + split; intros. + - unfold flat_value. inversion H. subst. trivial. + + rewrite Forall_forall in H0. rewrite forallb_forall. intros. subst. + apply value_is_bool_equiv. apply H0. assumption. + - destruct v. constructor. constructor. unfold flat_value in H. + rewrite Forall_forall. rewrite forallb_forall in H. intros. apply value_is_bool_equiv. + apply H. assumption. +Qed. + +Fixpoint value_to_nat' (i : nat) (v : value) : option nat := + match i, v with + | _, VBool b => Some (Nat.b2n b) + | _, VArray [VBool b] => Some (Nat.b2n b) + | S i', VArray ((VBool b) :: l) => + Option.map (compose (Nat.add (Nat.b2n b)) (Mult.tail_mult 2)) (value_to_nat' i' (VArray l)) + | _, _ => None + end. + +Definition value_length (v : value) : nat := + match v with + | VBool _ => 1 + | VArray l => Datatypes.length l + end. + +Definition value_to_nat (v : value) : option nat := + value_to_nat' (value_length v) v. + +Lemma empty_is_flat : flat_valueP (VArray []). +Proof. + constructor. apply Forall_forall. intros. inversion H. +Qed. + +Lemma check_5_is_101 : + value_to_nat (VArray [VBool true; VBool false; VBool true]) = Some 5. +Proof. reflexivity. Qed. + +Lemma cons_value_flat : + forall (b : bool) (v : value), + flat_valueP v -> flat_valueP (cons_value (VBool b) v). +Proof. + intros. unfold cons_value. destruct v. + - constructor. apply Forall_forall. intros. + inversion H0; subst. constructor. + inversion H1; subst. constructor. + inversion H2. + - intros. inversion H. inversion H1; subst; constructor. + + apply Forall_forall. intros. + inversion H0; subst. constructor. + inversion H2. + + repeat constructor. assumption. assumption. +Qed. + +Lemma nat_to_value'_is_flat : + forall (sz n : nat), + flat_valueP (nat_to_value' sz n). +Proof. + induction sz; intros. + - subst. apply empty_is_flat. + - unfold_rec nat_to_value'. + destruct (Nat.even n); apply cons_value_flat; apply IHsz. +Qed. + +Lemma nat_to_value_is_flat : + forall (sz n : nat), + flat_valueP (nat_to_value n). +Proof. + intros. unfold nat_to_value. apply nat_to_value'_is_flat. +Qed. + +Lemma nat_to_value_idempotent : + forall (sz n : nat), + sz > 0 -> (value_to_nat' sz (nat_to_value' sz n)) = Some n. +Proof. + induction sz; intros. + - inversion H. + - unfold_rec value_to_nat'. + assert (flat_valueP (nat_to_value' (S sz) n)). + { apply nat_to_value'_is_flat. } + destruct (nat_to_value' (S sz) n) eqn:?. +Admitted. + +Module VerilogEval. + + Definition app (f : nat -> nat -> nat) (a : value) (b : value) : option value := + Option.map nat_to_value (Option.liftA2 f (value_to_nat a) (value_to_nat b)). + + Definition state_find (k : string) (s : state) : option value := + Map.find k (fst s). + + Definition eval_binop (op : binop) (a1 a2 : value) : option value := + match op with + | Plus => app Nat.add a1 a2 + | Minus => app Nat.sub a1 a2 + | Times => app Mult.tail_mult a1 a2 + | Divide => app Nat.div a1 a2 + | _ => Some a1 + end. + +(* Fixpoint eval_expr (s : state) (e : expr) : option value := + match e with + | Lit n => Some n + | Var v => state_find v s + | Neg a => 0 - (eval_expr s a) + | BinOp op a1 a2 => eval_binop op a1 a2 + | Ternary c t f => if eval_expr s c then eval_expr s t else eval_expr s f + end. + *) +End VerilogEval. diff --git a/src/verilog/dune b/src/verilog/dune new file mode 100644 index 0000000..227d4a5 --- /dev/null +++ b/src/verilog/dune @@ -0,0 +1,4 @@ +(library + (name Verilog) + (public_name coqup.verilog) + (libraries coqup.extraction)) -- cgit