From 0b4808a3705317c96387de036381e4e6add4e956 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 31 Mar 2020 19:40:21 +0100 Subject: Add documentation and fix makefile for Compcert --- Makefile | 7 ++++- src/common/Coquplib.v | 32 +++++++++++++++++++++ src/common/Helper.v | 39 ------------------------- src/common/Show.v | 79 ++++++++++++++++++++++++++++----------------------- src/verilog/HTL.v | 25 ++++++++++++++++ src/verilog/Verilog.v | 2 +- 6 files changed, 107 insertions(+), 77 deletions(-) delete mode 100644 src/common/Helper.v diff --git a/Makefile b/Makefile index 1b4e39b..3c62851 100644 --- a/Makefile +++ b/Makefile @@ -18,10 +18,15 @@ PREFIX ?= . .PHONY: all install proof clean extraction -all: +all: lib/COMPCERTSTAMP $(MAKE) proof $(MAKE) compile +lib/COMPCERTSTAMP: + (cd lib/CompCert && ./configure x86_64-linux) + $(MAKE) -C lib/CompCert + touch $@ + install: install -d $(PREFIX)/bin install -C _build/default/driver/compcert.ini $(PREFIX)/bin/. diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v index c633874..666d740 100644 --- a/src/common/Coquplib.v +++ b/src/common/Coquplib.v @@ -23,6 +23,8 @@ From Coq Require Export List Bool. +From coqup Require Import Show. + (* Depend on CompCert for the basic library, as they declare and prove some useful theorems. *) From compcert.lib Require Export Coqlib. @@ -42,3 +44,33 @@ Ltac solve_by_invert := solve_by_inverts 1. (* Definition const (A B : Type) (a : A) (b : B) : A := a. Definition compose (A B C : Type) (f : B -> C) (g : A -> B) (x : A) : C := f (g x). *) + +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. + +Parameter debug_print : string -> unit. + +Definition debug_show {A B : Type} `{Show A} (a : A) (b : B) : B := + let unused := debug_print (show a) in b. + +Definition debug_show_msg {A B : Type} `{Show A} (s : string) (a : A) (b : B) : B := + let unused := debug_print (s ++ show a) in b. 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 index 8f9ec36..c994df3 100644 --- a/src/common/Show.v +++ b/src/common/Show.v @@ -19,43 +19,50 @@ From Coq Require Import Strings.String Bool.Bool - Arith.Arith. + Arith.Arith + ZArith.ZArith. 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 +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' - | 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. + | 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 + }. + +Instance showZ : Show Z := + { + show a := show (Z.to_nat a) + }. + +Instance showPositive : Show positive := + { + show a := show (Zpos a) + }. diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index f2620a7..1d156ad 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -1,3 +1,28 @@ +(* + * CoqUp: Verified high-level synthesis. + * Copyright (C) 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 . + *) + +(** The purpose of the hardware transfer language (HTL) is to create a more + * hardware-like layout that is still similar to the register transfer language + * (RTL) that it came from. The main change is that function calls become + * module instantiations and that we now describe a state machine instead of a + * control-flow graph. + *) + From coqup.common Require Import Coquplib. From compcert Require Import Maps. diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 50a6809..e91ca2d 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -25,7 +25,7 @@ From Coq Require Import From bbv Require Word. -From coqup.common Require Import Helper Coquplib Show. +From coqup.common Require Import Coquplib Show. From compcert Require Integers. -- cgit