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/Verilog.v | 64 ++++++++++++++++++++------------------------------- 1 file changed, 25 insertions(+), 39 deletions(-) (limited to 'src/verilog/Verilog.v') 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