From 05347ca5126f335b0479b71a4576b141e082fab5 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 2 Mar 2021 10:27:33 +0000 Subject: Add RAM to HTL --- src/hls/HTL.v | 1 + 1 file changed, 1 insertion(+) (limited to 'src/hls/HTL.v') diff --git a/src/hls/HTL.v b/src/hls/HTL.v index c8a0041..1949785 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -67,6 +67,7 @@ Record module: Type := mod_clk : reg; mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl); mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl); + mod_ram : option (reg * reg * reg * reg); mod_wf : (map_well_formed mod_controllogic /\ map_well_formed mod_datapath); }. -- cgit From 57350a8ca5579b65978d7a723a20915e763a2d0b Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 3 Mar 2021 21:12:15 +0000 Subject: Add RAM semantics to HTL and fix proof --- src/hls/HTL.v | 43 ++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 40 insertions(+), 3 deletions(-) (limited to 'src/hls/HTL.v') diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 1949785..b83d313 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -51,6 +51,14 @@ Definition map_well_formed {A : Type} (m : PTree.t A) : Prop := In p0 (map fst (Maps.PTree.elements m)) -> Z.pos p0 <= Integers.Int.max_unsigned. +Record ram := mk_ram { + ram_mem: reg; + ram_addr: reg; + ram_wr_en: reg; + ram_d_in: reg; + ram_d_out: reg; +}. + Record module: Type := mkmodule { mod_params : list reg; @@ -67,7 +75,7 @@ Record module: Type := mod_clk : reg; mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl); mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl); - mod_ram : option (reg * reg * reg * reg); + mod_ram : option ram; mod_wf : (map_well_formed mod_controllogic /\ map_well_formed mod_datapath); }. @@ -112,12 +120,35 @@ Inductive state : Type := (m : module) (args : list value), state. +Inductive exec_ram: + Verilog.reg_associations -> Verilog.arr_associations -> + option ram -> + Verilog.reg_associations -> Verilog.arr_associations -> + Prop := +| exec_ram_Some_write: + forall ra ar ram d_in addr, + (Verilog.assoc_blocking ra)!(ram_wr_en ram) = Some (ZToValue 1) -> + (Verilog.assoc_blocking ra)!(ram_d_in ram) = Some d_in -> + (Verilog.assoc_blocking ra)!(ram_addr ram) = Some addr -> + exec_ram ra ar (Some ram) ra + (Verilog.nonblock_arr (ram_mem ram) (valueToNat addr) ar d_in) +| exec_ram_Some_load: + forall ra ar ram addr v_d_out, + (Verilog.assoc_blocking ra)!(ram_wr_en ram) = Some (ZToValue 0) -> + (Verilog.assoc_blocking ra)!(ram_addr ram) = Some addr -> + Verilog.arr_assocmap_lookup (Verilog.assoc_blocking ar) (ram_mem ram) (valueToNat addr) = Some v_d_out -> + exec_ram ra ar (Some ram) (Verilog.nonblock_reg (ram_d_out ram) ra v_d_out) ar +| exec_ram_None: + forall r a, + exec_ram r a None r a. + Inductive step : genv -> state -> Events.trace -> state -> Prop := | step_module : forall g m st sf ctrl data asr asa basr1 basa1 nasr1 nasa1 basr2 basa2 nasr2 nasa2 + basr3 basa3 nasr3 nasa3 asr' asa' f pstval, asr!(mod_reset m) = Some (ZToValue 0) -> @@ -138,8 +169,14 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := data (Verilog.mkassociations basr2 nasr2) (Verilog.mkassociations basa2 nasa2) -> - asr' = Verilog.merge_regs nasr2 basr2 -> - asa' = Verilog.merge_arrs nasa2 basa2 -> + exec_ram + (Verilog.mkassociations basr2 nasr2) + (Verilog.mkassociations basa2 nasa2) + (mod_ram m) + (Verilog.mkassociations basr3 nasr3) + (Verilog.mkassociations basa3 nasa3) -> + asr' = Verilog.merge_regs nasr3 basr3 -> + asa' = Verilog.merge_arrs nasa3 basa3 -> asr'!(m.(mod_st)) = Some (posToValue pstval) -> Z.pos pstval <= Integers.Int.max_unsigned -> step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa') -- cgit From 540b1fb0494e6207d6bee63721dc5deee30e1c02 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 9 Mar 2021 22:20:17 +0000 Subject: Update RAM generation proofs --- src/hls/HTL.v | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) (limited to 'src/hls/HTL.v') diff --git a/src/hls/HTL.v b/src/hls/HTL.v index b83d313..2e4987d 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -53,6 +53,7 @@ Definition map_well_formed {A : Type} (m : PTree.t A) : Prop := Record ram := mk_ram { ram_mem: reg; + ram_en: reg; ram_addr: reg; ram_wr_en: reg; ram_d_in: reg; @@ -125,9 +126,16 @@ Inductive exec_ram: option ram -> Verilog.reg_associations -> Verilog.arr_associations -> Prop := +| exec_ram_Some_idle: + forall ra ar ram, + (Verilog.assoc_blocking ra)!(ram_en ram) = Some (ZToValue 0) -> + exec_ram ra ar (Some ram) ra ar | exec_ram_Some_write: - forall ra ar ram d_in addr, - (Verilog.assoc_blocking ra)!(ram_wr_en ram) = Some (ZToValue 1) -> + forall ra ar ram d_in addr en wr_en, + en <> ZToValue 0 -> + wr_en <> ZToValue 0 -> + (Verilog.assoc_blocking ra)!(ram_en ram) = Some en -> + (Verilog.assoc_blocking ra)!(ram_wr_en ram) = Some wr_en -> (Verilog.assoc_blocking ra)!(ram_d_in ram) = Some d_in -> (Verilog.assoc_blocking ra)!(ram_addr ram) = Some addr -> exec_ram ra ar (Some ram) ra @@ -170,8 +178,8 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := (Verilog.mkassociations basr2 nasr2) (Verilog.mkassociations basa2 nasa2) -> exec_ram - (Verilog.mkassociations basr2 nasr2) - (Verilog.mkassociations basa2 nasa2) + (Verilog.mkassociations (Verilog.merge_regs nasr2 basr2) empty_assocmap) + (Verilog.mkassociations (Verilog.merge_arrs nasa2 basa2) (empty_stack m)) (mod_ram m) (Verilog.mkassociations basr3 nasr3) (Verilog.mkassociations basa3 nasa3) -> -- cgit From e9109a10aecb53e56c8110dd788495a5b0b3c88c Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 11 Mar 2021 10:32:44 +0000 Subject: Prove idempotency of array merge --- src/hls/HTL.v | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) (limited to 'src/hls/HTL.v') diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 2e4987d..6dc1856 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -52,6 +52,7 @@ Definition map_well_formed {A : Type} (m : PTree.t A) : Prop := Z.pos p0 <= Integers.Int.max_unsigned. Record ram := mk_ram { + ram_size: nat; ram_mem: reg; ram_en: reg; ram_addr: reg; @@ -128,8 +129,8 @@ Inductive exec_ram: Prop := | exec_ram_Some_idle: forall ra ar ram, - (Verilog.assoc_blocking ra)!(ram_en ram) = Some (ZToValue 0) -> - exec_ram ra ar (Some ram) ra ar + (Verilog.assoc_blocking ra)#(ram_en ram, 32) = ZToValue 0 -> + exec_ram ra ar (Some ram) ra ar | exec_ram_Some_write: forall ra ar ram d_in addr en wr_en, en <> ZToValue 0 -> @@ -141,10 +142,13 @@ Inductive exec_ram: exec_ram ra ar (Some ram) ra (Verilog.nonblock_arr (ram_mem ram) (valueToNat addr) ar d_in) | exec_ram_Some_load: - forall ra ar ram addr v_d_out, + forall ra ar ram addr v_d_out en, + en <> ZToValue 0 -> + (Verilog.assoc_blocking ra)!(ram_en ram) = Some en -> (Verilog.assoc_blocking ra)!(ram_wr_en ram) = Some (ZToValue 0) -> (Verilog.assoc_blocking ra)!(ram_addr ram) = Some addr -> - Verilog.arr_assocmap_lookup (Verilog.assoc_blocking ar) (ram_mem ram) (valueToNat addr) = Some v_d_out -> + Verilog.arr_assocmap_lookup (Verilog.assoc_blocking ar) + (ram_mem ram) (valueToNat addr) = Some v_d_out -> exec_ram ra ar (Some ram) (Verilog.nonblock_reg (ram_d_out ram) ra v_d_out) ar | exec_ram_None: forall r a, -- cgit From eeae38900cb1151edfd5c715c77adbc912ceda55 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 21 Mar 2021 19:06:24 +0000 Subject: Add many lemmas about arrays --- src/hls/HTL.v | 34 +++++++++++++++++----------------- 1 file changed, 17 insertions(+), 17 deletions(-) (limited to 'src/hls/HTL.v') diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 6dc1856..32b91ab 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -128,28 +128,28 @@ Inductive exec_ram: Verilog.reg_associations -> Verilog.arr_associations -> Prop := | exec_ram_Some_idle: - forall ra ar ram, - (Verilog.assoc_blocking ra)#(ram_en ram, 32) = ZToValue 0 -> - exec_ram ra ar (Some ram) ra ar + forall ra ar r, + (Verilog.assoc_blocking ra)#(ram_en r, 32) = ZToValue 0 -> + exec_ram ra ar (Some r) ra ar | exec_ram_Some_write: - forall ra ar ram d_in addr en wr_en, + forall ra ar r d_in addr en wr_en, en <> ZToValue 0 -> wr_en <> ZToValue 0 -> - (Verilog.assoc_blocking ra)!(ram_en ram) = Some en -> - (Verilog.assoc_blocking ra)!(ram_wr_en ram) = Some wr_en -> - (Verilog.assoc_blocking ra)!(ram_d_in ram) = Some d_in -> - (Verilog.assoc_blocking ra)!(ram_addr ram) = Some addr -> - exec_ram ra ar (Some ram) ra - (Verilog.nonblock_arr (ram_mem ram) (valueToNat addr) ar d_in) -| exec_ram_Some_load: - forall ra ar ram addr v_d_out en, + (Verilog.assoc_blocking ra)!(ram_en r) = Some en -> + (Verilog.assoc_blocking ra)!(ram_wr_en r) = Some wr_en -> + (Verilog.assoc_blocking ra)!(ram_d_in r) = Some d_in -> + (Verilog.assoc_blocking ra)!(ram_addr r) = Some addr -> + exec_ram ra ar (Some r) ra + (Verilog.nonblock_arr (ram_mem r) (valueToNat addr) ar d_in) +| exec_ram_Some_read: + forall ra ar r addr v_d_out en, en <> ZToValue 0 -> - (Verilog.assoc_blocking ra)!(ram_en ram) = Some en -> - (Verilog.assoc_blocking ra)!(ram_wr_en ram) = Some (ZToValue 0) -> - (Verilog.assoc_blocking ra)!(ram_addr ram) = Some addr -> + (Verilog.assoc_blocking ra)!(ram_en r) = Some en -> + (Verilog.assoc_blocking ra)!(ram_wr_en r) = Some (ZToValue 0) -> + (Verilog.assoc_blocking ra)!(ram_addr r) = Some addr -> Verilog.arr_assocmap_lookup (Verilog.assoc_blocking ar) - (ram_mem ram) (valueToNat addr) = Some v_d_out -> - exec_ram ra ar (Some ram) (Verilog.nonblock_reg (ram_d_out ram) ra v_d_out) ar + (ram_mem r) (valueToNat addr) = Some v_d_out -> + exec_ram ra ar (Some r) (Verilog.nonblock_reg (ram_d_out r) ra v_d_out) ar | exec_ram_None: forall r a, exec_ram r a None r a. -- cgit From 2837868fcc427b2161b083f33d3de495f0c21bf7 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 31 Mar 2021 20:45:15 +0100 Subject: Add memory disable --- src/hls/HTL.v | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'src/hls/HTL.v') diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 32b91ab..4899671 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -139,7 +139,7 @@ Inductive exec_ram: (Verilog.assoc_blocking ra)!(ram_wr_en r) = Some wr_en -> (Verilog.assoc_blocking ra)!(ram_d_in r) = Some d_in -> (Verilog.assoc_blocking ra)!(ram_addr r) = Some addr -> - exec_ram ra ar (Some r) ra + exec_ram ra ar (Some r) (Verilog.nonblock_reg (ram_en r) ra (ZToValue 0)) (Verilog.nonblock_arr (ram_mem r) (valueToNat addr) ar d_in) | exec_ram_Some_read: forall ra ar r addr v_d_out en, @@ -149,7 +149,8 @@ Inductive exec_ram: (Verilog.assoc_blocking ra)!(ram_addr r) = Some addr -> Verilog.arr_assocmap_lookup (Verilog.assoc_blocking ar) (ram_mem r) (valueToNat addr) = Some v_d_out -> - exec_ram ra ar (Some r) (Verilog.nonblock_reg (ram_d_out r) ra v_d_out) ar + exec_ram ra ar (Some r) (Verilog.nonblock_reg (ram_en r) + (Verilog.nonblock_reg (ram_d_out r) ra v_d_out) (ZToValue 0)) ar | exec_ram_None: forall r a, exec_ram r a None r a. -- cgit From 315f610b111d8d5433866fa032beac0ea29df676 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 1 Apr 2021 01:24:19 +0100 Subject: Add new enable interface --- src/hls/HTL.v | 28 +++++++++++++++------------- 1 file changed, 15 insertions(+), 13 deletions(-) (limited to 'src/hls/HTL.v') diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 4899671..92dc48c 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -23,7 +23,7 @@ Require compcert.common.Events. Require compcert.common.Globalenvs. Require compcert.common.Smallstep. Require compcert.common.Values. -Require compcert.lib.Integers. +Require Import compcert.lib.Integers. Require Import compcert.lib.Maps. Require Import vericert.common.Vericertlib. @@ -55,6 +55,7 @@ Record ram := mk_ram { ram_size: nat; ram_mem: reg; ram_en: reg; + ram_u_en: reg; ram_addr: reg; ram_wr_en: reg; ram_d_in: reg; @@ -123,34 +124,35 @@ Inductive state : Type := (args : list value), state. Inductive exec_ram: - Verilog.reg_associations -> Verilog.arr_associations -> - option ram -> - Verilog.reg_associations -> Verilog.arr_associations -> - Prop := + Verilog.reg_associations -> Verilog.arr_associations -> option ram -> + Verilog.reg_associations -> Verilog.arr_associations -> Prop := | exec_ram_Some_idle: forall ra ar r, - (Verilog.assoc_blocking ra)#(ram_en r, 32) = ZToValue 0 -> + Int.eq (Verilog.assoc_blocking ra)#(ram_en r, 32) + (Verilog.assoc_blocking ra)#(ram_u_en r, 32) = true -> exec_ram ra ar (Some r) ra ar | exec_ram_Some_write: - forall ra ar r d_in addr en wr_en, - en <> ZToValue 0 -> - wr_en <> ZToValue 0 -> + forall ra ar r d_in addr en wr_en u_en, + Int.eq en u_en = false -> + Int.eq wr_en (ZToValue 0) = false -> (Verilog.assoc_blocking ra)!(ram_en r) = Some en -> + (Verilog.assoc_blocking ra)!(ram_u_en r) = Some u_en -> (Verilog.assoc_blocking ra)!(ram_wr_en r) = Some wr_en -> (Verilog.assoc_blocking ra)!(ram_d_in r) = Some d_in -> (Verilog.assoc_blocking ra)!(ram_addr r) = Some addr -> - exec_ram ra ar (Some r) (Verilog.nonblock_reg (ram_en r) ra (ZToValue 0)) + exec_ram ra ar (Some r) (Verilog.nonblock_reg (ram_en r) ra u_en) (Verilog.nonblock_arr (ram_mem r) (valueToNat addr) ar d_in) | exec_ram_Some_read: - forall ra ar r addr v_d_out en, - en <> ZToValue 0 -> + forall ra ar r addr v_d_out en u_en, + Int.eq en u_en = false -> (Verilog.assoc_blocking ra)!(ram_en r) = Some en -> + (Verilog.assoc_blocking ra)!(ram_u_en r) = Some u_en -> (Verilog.assoc_blocking ra)!(ram_wr_en r) = Some (ZToValue 0) -> (Verilog.assoc_blocking ra)!(ram_addr r) = Some addr -> Verilog.arr_assocmap_lookup (Verilog.assoc_blocking ar) (ram_mem r) (valueToNat addr) = Some v_d_out -> exec_ram ra ar (Some r) (Verilog.nonblock_reg (ram_en r) - (Verilog.nonblock_reg (ram_d_out r) ra v_d_out) (ZToValue 0)) ar + (Verilog.nonblock_reg (ram_d_out r) ra v_d_out) u_en) ar | exec_ram_None: forall r a, exec_ram r a None r a. -- cgit From 2cec98b19da0abd58f017dadfd487a1c9caa96b3 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 4 Apr 2021 13:13:37 +0100 Subject: Finish store proof without admit --- src/hls/HTL.v | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'src/hls/HTL.v') diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 92dc48c..98ea6d0 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -60,6 +60,11 @@ Record ram := mk_ram { ram_wr_en: reg; ram_d_in: reg; ram_d_out: reg; + ram_ordering: (ram_addr < ram_en + /\ ram_en < ram_d_in + /\ ram_d_in < ram_d_out + /\ ram_d_out < ram_wr_en + /\ ram_wr_en < ram_u_en)%positive }. Record module: Type := @@ -135,7 +140,7 @@ Inductive exec_ram: forall ra ar r d_in addr en wr_en u_en, Int.eq en u_en = false -> Int.eq wr_en (ZToValue 0) = false -> - (Verilog.assoc_blocking ra)!(ram_en r) = Some en -> + (Verilog.assoc_blocking ra)#(ram_en r, 32) = en -> (Verilog.assoc_blocking ra)!(ram_u_en r) = Some u_en -> (Verilog.assoc_blocking ra)!(ram_wr_en r) = Some wr_en -> (Verilog.assoc_blocking ra)!(ram_d_in r) = Some d_in -> @@ -145,7 +150,7 @@ Inductive exec_ram: | exec_ram_Some_read: forall ra ar r addr v_d_out en u_en, Int.eq en u_en = false -> - (Verilog.assoc_blocking ra)!(ram_en r) = Some en -> + (Verilog.assoc_blocking ra)#(ram_en r, 32) = en -> (Verilog.assoc_blocking ra)!(ram_u_en r) = Some u_en -> (Verilog.assoc_blocking ra)!(ram_wr_en r) = Some (ZToValue 0) -> (Verilog.assoc_blocking ra)!(ram_addr r) = Some addr -> -- cgit From 23a2a2fb2916a7ecb240aa51686bbe049f8418e4 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 6 Apr 2021 23:08:03 +0100 Subject: Finish load and store proof, but broke top-level --- src/hls/HTL.v | 109 +++++++++++++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 105 insertions(+), 4 deletions(-) (limited to 'src/hls/HTL.v') diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 98ea6d0..e614246 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -18,6 +18,7 @@ *) Require Import Coq.FSets.FMapPositive. +Require Import Coq.micromega.Lia. Require compcert.common.Events. Require compcert.common.Globalenvs. @@ -32,6 +33,8 @@ Require Import vericert.hls.AssocMap. Require Import vericert.hls.Array. Require vericert.hls.Verilog. +Local Open Scope positive. + (** 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 @@ -49,7 +52,7 @@ Definition controllogic := PTree.t Verilog.stmnt. Definition map_well_formed {A : Type} (m : PTree.t A) : Prop := forall p0 : positive, In p0 (map fst (Maps.PTree.elements m)) -> - Z.pos p0 <= Integers.Int.max_unsigned. + (Z.pos p0 <= Integers.Int.max_unsigned)%Z. Record ram := mk_ram { ram_size: nat; @@ -64,9 +67,11 @@ Record ram := mk_ram { /\ ram_en < ram_d_in /\ ram_d_in < ram_d_out /\ ram_d_out < ram_wr_en - /\ ram_wr_en < ram_u_en)%positive + /\ ram_wr_en < ram_u_en) }. +Definition module_ordering a b c d e f g := a < b < c /\ c < d < e /\ e < f < g. + Record module: Type := mkmodule { mod_params : list reg; @@ -84,7 +89,9 @@ Record module: Type := mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl); mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl); mod_ram : option ram; - mod_wf : (map_well_formed mod_controllogic /\ map_well_formed mod_datapath); + mod_wf : map_well_formed mod_controllogic /\ map_well_formed mod_datapath; + mod_ordering_wf : module_ordering mod_st mod_finish mod_return mod_stk mod_start mod_reset mod_clk; + mod_ram_wf : forall r', mod_ram = Some r' -> mod_clk < ram_addr r'; }. Definition fundef := AST.fundef module. @@ -198,7 +205,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := asr' = Verilog.merge_regs nasr3 basr3 -> asa' = Verilog.merge_arrs nasa3 basa3 -> asr'!(m.(mod_st)) = Some (posToValue pstval) -> - Z.pos pstval <= Integers.Int.max_unsigned -> + (Z.pos pstval <= Integers.Int.max_unsigned)%Z -> step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa') | step_finish : forall g m st asr asa retval sf, @@ -237,3 +244,97 @@ Inductive final_state : state -> Integers.int -> Prop := Definition semantics (m : program) := Smallstep.Semantics step (initial_state m) final_state (Globalenvs.Genv.globalenv m). + +Definition max_pc_function (m: module) := + List.fold_left Pos.max (List.map fst (PTree.elements m.(mod_controllogic))) 1. + +Definition max_list := fold_right Pos.max 1. + +Definition max_stmnt_tree t := + PTree.fold (fun i _ st => Pos.max (Verilog.max_reg_stmnt st) i) t 1. + +Definition max_reg_ram r := + match r with + | None => 1 + | Some ram => Pos.max (ram_mem ram) + (Pos.max (ram_en ram) + (Pos.max (ram_addr ram) + (Pos.max (ram_addr ram) + (Pos.max (ram_wr_en ram) + (Pos.max (ram_d_in ram) + (Pos.max (ram_d_out ram) (ram_u_en ram))))))) + end. + +Definition max_reg_module m := + Pos.max (max_list (mod_params m)) + (Pos.max (max_stmnt_tree (mod_datapath m)) + (Pos.max (max_stmnt_tree (mod_controllogic m)) + (Pos.max (mod_st m) + (Pos.max (mod_stk m) + (Pos.max (mod_finish m) + (Pos.max (mod_return m) + (Pos.max (mod_start m) + (Pos.max (mod_reset m) + (Pos.max (mod_clk m) (max_reg_ram (mod_ram m))))))))))). + +Lemma max_fold_lt : + forall m l n, m <= n -> m <= (fold_left Pos.max l n). +Proof. induction l; crush; apply IHl; lia. Qed. + +Lemma max_fold_lt2 : + forall (l: list (positive * Verilog.stmnt)) v n, + v <= n -> + v <= fold_left (fun a p => Pos.max (Verilog.max_reg_stmnt (snd p)) a) l n. +Proof. induction l; crush; apply IHl; lia. Qed. + +Lemma max_fold_lt3 : + forall (l: list (positive * Verilog.stmnt)) v v', + v <= v' -> + fold_left (fun a0 p => Pos.max (Verilog.max_reg_stmnt (snd p)) a0) l v + <= fold_left (fun a0 p => Pos.max (Verilog.max_reg_stmnt (snd p)) a0) l v'. +Proof. induction l; crush; apply IHl; lia. Qed. + +Lemma max_fold_lt4 : + forall (l: list (positive * Verilog.stmnt)) (a: positive * Verilog.stmnt), + fold_left (fun a0 p => Pos.max (Verilog.max_reg_stmnt (snd p)) a0) l 1 + <= fold_left (fun a0 p => Pos.max (Verilog.max_reg_stmnt (snd p)) a0) l + (Pos.max (Verilog.max_reg_stmnt (snd a)) 1). +Proof. intros; apply max_fold_lt3; lia. Qed. + +Lemma max_reg_stmnt_lt_stmnt_tree': + forall l (i: positive) v, + In (i, v) l -> + list_norepet (map fst l) -> + Verilog.max_reg_stmnt v <= fold_left (fun a p => Pos.max (Verilog.max_reg_stmnt (snd p)) a) l 1. +Proof. + induction l; crush. inv H; inv H0; simplify. apply max_fold_lt2. lia. + transitivity (fold_left (fun (a : positive) (p : positive * Verilog.stmnt) => + Pos.max (Verilog.max_reg_stmnt (snd p)) a) l 1). + eapply IHl; eauto. apply max_fold_lt4. +Qed. + +Lemma max_reg_stmnt_le_stmnt_tree : + forall d i v, + d ! i = Some v -> + Verilog.max_reg_stmnt v <= max_stmnt_tree d. +Proof. + intros. unfold max_stmnt_tree. rewrite PTree.fold_spec. + apply PTree.elements_correct in H. + eapply max_reg_stmnt_lt_stmnt_tree'; eauto. + apply PTree.elements_keys_norepet. +Qed. + +Lemma max_reg_stmnt_lt_stmnt_tree : + forall d i v, + d ! i = Some v -> + Verilog.max_reg_stmnt v < max_stmnt_tree d + 1. +Proof. intros. apply max_reg_stmnt_le_stmnt_tree in H; lia. Qed. + +Lemma max_stmnt_lt_module : + forall m d i, + (mod_controllogic m) ! i = Some d \/ (mod_datapath m) ! i = Some d -> + Verilog.max_reg_stmnt d < max_reg_module m + 1. +Proof. + inversion 1 as [ Hv | Hv ]; unfold max_reg_module; + apply max_reg_stmnt_le_stmnt_tree in Hv; lia. +Qed. -- cgit From 8573889ca84a84475761b4d75d55547a2995c831 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 7 Apr 2021 01:11:04 +0100 Subject: Basically done with proof --- src/hls/HTL.v | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'src/hls/HTL.v') diff --git a/src/hls/HTL.v b/src/hls/HTL.v index e614246..61ea541 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -92,6 +92,7 @@ Record module: Type := mod_wf : map_well_formed mod_controllogic /\ map_well_formed mod_datapath; mod_ordering_wf : module_ordering mod_st mod_finish mod_return mod_stk mod_start mod_reset mod_clk; mod_ram_wf : forall r', mod_ram = Some r' -> mod_clk < ram_addr r'; + mod_params_wf : Forall (Pos.gt mod_st) mod_params; }. Definition fundef := AST.fundef module. @@ -338,3 +339,16 @@ Proof. inversion 1 as [ Hv | Hv ]; unfold max_reg_module; apply max_reg_stmnt_le_stmnt_tree in Hv; lia. Qed. + +Lemma max_list_correct l st : st > max_list l -> Forall (Pos.gt st) l. +Proof. induction l; crush; constructor; [|apply IHl]; lia. Qed. + +Definition max_list_dec (l: list reg) (st: reg) : {Forall (Pos.gt st) l} + {True}. + refine ( + match bool_dec (max_list l left _ + | _ => _ + end + ); auto. + apply max_list_correct. apply Pos.ltb_lt in e. lia. +Qed. -- cgit