From 32990af23915c15e5cfd4cfe32c47cafa508f11d Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 8 May 2020 23:34:15 +0100 Subject: Add AssocMap --- src/verilog/AssocMap.v | 60 ++++++++++++++++++++++++++++++++++++++++++++++ src/verilog/HTL.v | 10 ++++---- src/verilog/Test.v | 6 ++--- src/verilog/Verilog.v | 64 ++++++++++++++++++++------------------------------ 4 files changed, 93 insertions(+), 47 deletions(-) create mode 100644 src/verilog/AssocMap.v (limited to 'src/verilog') diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v new file mode 100644 index 0000000..e550072 --- /dev/null +++ b/src/verilog/AssocMap.v @@ -0,0 +1,60 @@ +(* + * 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 . + *) + +From coqup Require Import Coquplib Value. +From Coq Require Import FSets.FMapPositive. + +Definition reg := positive. + +Module AssocMap := PositiveMap. + +Module AssocMapExt. + Import AssocMap. + + Section Operations. + + Variable elt : Type. + + Definition merge : t elt -> t elt -> t elt := fold (@add elt). + + Definition find_default (a : elt) (k : reg) (m : t elt) : elt := + match find k m with + | None => a + | Some v => v + end. + + End Operations. + +End AssocMapExt. +Import AssocMapExt. + +Definition assocmap := AssocMap.t value. + +Definition find_assocmap (n : nat) : reg -> assocmap -> value := + find_default value (ZToValue n 0). + +Definition empty_assocmap : assocmap := AssocMap.empty value. + +Definition merge_assocmap : assocmap -> assocmap -> assocmap := merge value. + +Module AssocMapNotation. + Notation "a ! b" := (AssocMap.find b a) (at level 1). + Notation "a # ( b , c )" := (find_assocmap c b a) (at level 1). + Notation "a # b" := (find_assocmap 32 b a) (at level 1). + Notation "a ## b" := (List.map (fun c => find_assocmap 32 c a) b) (at level 1). +End AssocMapNotation. diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index 3d863b2..147d24b 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -17,7 +17,7 @@ *) From Coq Require Import FSets.FMapPositive. -From coqup Require Import Coquplib Value. +From coqup Require Import Coquplib Value AssocMap. From coqup Require Verilog. From compcert Require Events Globalenvs Smallstep Integers. @@ -57,7 +57,7 @@ Inductive state : Type := | State : forall (m : module) (st : node) - (assoc : Verilog.assocset), + (assoc : assocmap), state | Returnstate : forall v : value, state. @@ -67,14 +67,14 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := m.(mod_controllogic)!st = Some ctrl -> m.(mod_datapath)!st = Some data -> Verilog.stmnt_runp f - (Verilog.mkassociations assoc0 Verilog.empty_assocset) + (Verilog.mkassociations assoc0 empty_assocmap) ctrl (Verilog.mkassociations assoc1 nbassoc0) -> Verilog.stmnt_runp f (Verilog.mkassociations assoc1 nbassoc0) data (Verilog.mkassociations assoc2 nbassoc1) -> - assoc3 = Verilog.merge_assocset nbassoc1 assoc2 -> + assoc3 = merge_assocmap nbassoc1 assoc2 -> step g (State m st assoc0) t (State m st assoc3) | step_finish : forall g t m st assoc retval, @@ -86,7 +86,7 @@ Hint Constructors step : htl. Inductive initial_state (m : module) : state -> Prop := | initial_state_intro : forall st, st = m.(mod_entrypoint) -> - initial_state m (State m st Verilog.empty_assocset). + initial_state m (State m st empty_assocmap). Inductive final_state : state -> Integers.int -> Prop := | final_state_intro : forall retval retvali, diff --git a/src/verilog/Test.v b/src/verilog/Test.v index f24612e..90c5312 100644 --- a/src/verilog/Test.v +++ b/src/verilog/Test.v @@ -88,10 +88,10 @@ Proof. trivial. Qed. Definition test_fextclk := initial_fextclk test_output_module. Lemma manual_simulation : - step (State test_output_module empty_assocset empty_assocset + step (State test_output_module empty_assocmap empty_assocmap test_fextclk 1 (32'h"1")) - (State test_output_module (add_assocset 7%positive (32'h"3") empty_assocset) - empty_assocset test_fextclk 2 (32'h"3")). + (State test_output_module (add_assocmap 7%positive (32'h"3") empty_assocmap) + empty_assocmap test_fextclk 2 (32'h"3")). Proof. repeat (econstructor; eauto); try (unfold ZToValue; instantiate (1 := eq_refl (vsize (1'h"1"))); auto); diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index ba7e83d..c0bce25 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -27,24 +27,21 @@ From Coq Require Import Import ListNotations. -From coqup Require Import common.Coquplib common.Show verilog.Value. +From coqup Require Import common.Coquplib common.Show verilog.Value AssocMap. From compcert Require Integers Events. From compcert Require Import Errors Smallstep Globalenvs. Import HexNotationValue. - -Notation "a ! b" := (PositiveMap.find b a) (at level 1). +Import AssocMapNotation. Definition reg : Type := positive. Definition node : Type := positive. Definition szreg : Type := reg * nat. -Definition assocset : Type := PositiveMap.t value. - Record associations : Type := mkassociations { - assoc_blocking : assocset; - assoc_nonblocking : assocset + assoc_blocking : assocmap; + assoc_nonblocking : assocmap }. (** * Verilog AST @@ -58,8 +55,6 @@ The Verilog [value] is a bitvector containg a size and the actual bitvector. In this case, the [Word.word] type is used as many theorems about that bitvector have already been proven. *) -Definition estate : Type := assocset * assocset. - (** ** Binary Operators These are the binary operations that can be represented in Verilog. Ideally, @@ -167,8 +162,7 @@ Record module : Type := mkmodule { mod_state : szreg; (**r Variable that defines the current state, it should be internal. *) mod_args : list szreg; mod_body : list module_item; -}. - + }. (** Convert a [positive] to an expression directly, setting it to the right size. *) Definition posToLit (p : positive) : expr := @@ -204,8 +198,8 @@ retrieved and set appropriately. Inductive state : Type := | State: forall (m : module) - (assoc : assocset) - (nbassoc : assocset) + (assoc : assocmap) + (nbassoc : assocmap) (f : fextclk) (cycle : nat) (stvar : value), @@ -246,7 +240,7 @@ Definition unop_run (op : unop) : value -> value := | Vnot => vbitneg end. -Inductive expr_runp : fext -> assocset -> expr -> value -> Prop := +Inductive expr_runp : fext -> assocmap -> expr -> value -> Prop := | erun_Vlit : forall fext assoc v, expr_runp fext assoc (Vlit v) v @@ -312,7 +306,7 @@ Definition access_fext (f : fext) (r : reg) : res value := end. (* TODO FIX Vvar case without default *) -(*Fixpoint expr_run (assoc : assocset) (e : expr) +(*Fixpoint expr_run (assoc : assocmap) (e : expr) {struct e} : res value := match e with | Vlit v => OK v @@ -461,7 +455,7 @@ Inductive stmnt_runp: fext -> associations -> stmnt -> associations -> Prop := assoc' = (PositiveMap.add name rhsval assoc) -> stmnt_runp f (mkassociations assoc nbassoc) (Vblock lhs rhs) - (mkassociations assoc nbassoc) + (mkassociations assoc' nbassoc) | stmnt_runp_Vnonblock: forall lhs name rhs rhsval assoc nbassoc nbassoc' f, assign_name lhs = OK name -> @@ -514,28 +508,20 @@ Inductive mis_stepp : fext -> associations -> list module_item -> associations - mis_stepp f s nil s. Hint Constructors mis_stepp : verilog. -Definition add_assocset (r : reg) (v : value) (assoc : assocset) : assocset := - PositiveMap.add r v assoc. - -Definition merge_assocset (nbassoc assoc : assocset) : assocset := - PositiveMap.fold add_assocset nbassoc assoc. - -Definition empty_assocset : assocset := PositiveMap.empty value. - (*Definition mi_step_commit (s : state) (m : list module_item) : res state := match mi_step s m with | OK (State m assoc nbassoc f c) => - OK (State m (merge_assocset nbassoc assoc) empty_assocset f c) + OK (State m (merge_assocmap nbassoc assoc) empty_assocmap f c) | Error msg => Error msg | _ => Error (msg "Verilog: Wrong state") - end.*) + end. -(*Fixpoint mi_run (f : fextclk) (assoc : assocset) (m : list module_item) (n : nat) - {struct n} : res assocset := +Fixpoint mi_run (f : fextclk) (assoc : assocmap) (m : list module_item) (n : nat) + {struct n} : res assocmap := match n with | S n' => do assoc' <- mi_run f assoc m n'; - match mi_step_commit (State assoc' empty_assocset f (Pos.of_nat n')) m with + match mi_step_commit (State assoc' empty_assocmap f (Pos.of_nat n')) m with | OK (State assoc _ _ _) => OK assoc | Error m => Error m end @@ -548,12 +534,12 @@ other arguments to the module are also to be supported. *) Definition initial_fextclk (m : module) : fextclk := fun x => match x with - | S O => (add_assocset (fst (mod_reset m)) (ZToValue 1 1) empty_assocset) - | _ => (add_assocset (fst (mod_reset m)) (ZToValue 1 0) empty_assocset) + | S O => (AssocMap.add (fst (mod_reset m)) (ZToValue 1 1) empty_assocmap) + | _ => (AssocMap.add (fst (mod_reset m)) (ZToValue 1 0) empty_assocmap) end. -(*Definition module_run (n : nat) (m : module) : res assocset := - mi_run (initial_fextclk m) empty_assocset (mod_body m) n.*) +(*Definition module_run (n : nat) (m : module) : res assocmap := + mi_run (initial_fextclk m) empty_assocmap (mod_body m) n.*) Local Close Scope error_monad_scope. @@ -601,18 +587,18 @@ Definition genv := Genv.t unit unit. Inductive step : state -> state -> Prop := | step_module : forall m stvar stvar' cycle f assoc0 assoc1 assoc2 nbassoc, - mis_stepp (f cycle) (mkassociations assoc0 empty_assocset) + mis_stepp (f cycle) (mkassociations assoc0 empty_assocmap) m.(mod_body) (mkassociations assoc1 nbassoc) -> - assoc2 = merge_assocset nbassoc assoc1 -> + assoc2 = merge_assocmap nbassoc assoc1 -> Some stvar' = assoc2!(fst m.(mod_state)) -> - step (State m assoc0 empty_assocset f cycle stvar) - (State m assoc2 empty_assocset f (S cycle) stvar') + step (State m assoc0 empty_assocmap f cycle stvar) + (State m assoc2 empty_assocmap f (S cycle) stvar') | step_finish : forall m assoc f cycle stvar result, assoc!(fst m.(mod_finish)) = Some (1'h"1") -> assoc!(fst m.(mod_return)) = Some result -> - step (State m assoc empty_assocset f cycle stvar) + step (State m assoc empty_assocmap f cycle stvar) (Finishstate result). Hint Constructors step : verilog. @@ -620,7 +606,7 @@ Hint Constructors step : verilog. | initial_state_intro: forall hmi tmi, hmi::tmi = mod_body m -> - initial_state m (State m hmi tmi empty_assocset empty_assocset (initial_fextclk m) O xH). + initial_state m (State m hmi tmi empty_assocmap empty_assocmap (initial_fextclk m) O xH). (** A final state is a [Returnstate] with an empty call stack. *) -- cgit