diff options
author | James Pollard <james@pollard.dev> | 2020-05-30 18:38:50 +0100 |
---|---|---|
committer | James Pollard <james@pollard.dev> | 2020-05-30 18:38:50 +0100 |
commit | c3fe9469171bbf706dcb7bc84297123590377100 (patch) | |
tree | bfaa79704f70eb0c896d598ae2abc5235db56211 /src | |
parent | 6059f00139e2ce90525a1e1023ca97b6ba65e6bb (diff) | |
parent | acf638b44023c5593e0758e82d161c087062dc39 (diff) | |
download | vericert-kvx-c3fe9469171bbf706dcb7bc84297123590377100.tar.gz vericert-kvx-c3fe9469171bbf706dcb7bc84297123590377100.zip |
Merge branch 'develop' into arrays-proof
Diffstat (limited to 'src')
-rw-r--r-- | src/Compiler.v | 2 | ||||
-rw-r--r-- | src/Simulator.v | 2 | ||||
-rw-r--r-- | src/common/Maps.v | 6 | ||||
-rw-r--r-- | src/common/Monad.v | 48 | ||||
-rw-r--r-- | src/common/Statemonad.v | 61 | ||||
-rw-r--r-- | src/extraction/Extraction.v | 2 | ||||
-rw-r--r-- | src/translation/HTLgen.v | 487 | ||||
-rw-r--r-- | src/translation/HTLgenproof.v | 396 | ||||
-rw-r--r-- | src/translation/HTLgenspec.v | 359 | ||||
-rw-r--r-- | src/translation/Veriloggen.v | 71 | ||||
-rw-r--r-- | src/translation/Veriloggenproof.v | 46 | ||||
-rw-r--r-- | src/translation/Veriloggenspec.v | 130 | ||||
-rw-r--r-- | src/verilog/AssocMap.v | 210 | ||||
-rw-r--r-- | src/verilog/HTL.v | 146 | ||||
-rw-r--r-- | src/verilog/Test.v | 99 | ||||
-rw-r--r-- | src/verilog/Value.v | 143 | ||||
-rw-r--r-- | src/verilog/Verilog.v | 335 |
17 files changed, 2195 insertions, 348 deletions
diff --git a/src/Compiler.v b/src/Compiler.v index 697732d..e998521 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -1,4 +1,4 @@ -(* -*- mode: coq -*- +(* * CoqUp: Verified high-level synthesis. * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> * diff --git a/src/Simulator.v b/src/Simulator.v index 6849f80..930971b 100644 --- a/src/Simulator.v +++ b/src/Simulator.v @@ -1,4 +1,4 @@ -(* -*- mode: coq -*- +(* * CoqUp: Verified high-level synthesis. * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> * diff --git a/src/common/Maps.v b/src/common/Maps.v index 7a542b7..3236417 100644 --- a/src/common/Maps.v +++ b/src/common/Maps.v @@ -40,10 +40,4 @@ Definition traverse (A B : Type) (f : positive -> A -> res B) m := xtraverse f m Definition traverse1 (A B : Type) (f : A -> res B) := traverse (fun _ => f). -Lemma traverse1_inversion: - forall (A B : Type) (f : A -> res B) (i j : positive) (m : t A) (m' : t B), - traverse1 f m = OK m' -> - list_forall2 (fun x y => f (snd x) = OK (snd y) /\ fst x = fst y) (elements m) (elements m'). -Proof. Admitted. - End PTree. diff --git a/src/common/Monad.v b/src/common/Monad.v new file mode 100644 index 0000000..8517186 --- /dev/null +++ b/src/common/Monad.v @@ -0,0 +1,48 @@ +From Coq Require Import Lists.List. + +Module Type Monad. + + Parameter mon : Type -> Type. + + Parameter ret : forall (A : Type) (x : A), mon A. + Arguments ret [A]. + + Parameter bind : forall (A B : Type) (f : mon A) (g : A -> mon B), mon B. + Arguments bind [A B]. + + Parameter bind2 : forall (A B C: Type) (f: mon (A * B)) (g: A -> B -> mon C), mon C. + Arguments bind2 [A B C]. + +End Monad. + +Module MonadExtra(M : Monad). + Import M. + + Module MonadNotation. + + Notation "'do' X <- A ; B" := + (bind A (fun X => B)) + (at level 200, X ident, A at level 100, B at level 200). + Notation "'do' ( X , Y ) <- A ; B" := + (bind2 A (fun X Y => B)) + (at level 200, X ident, Y ident, A at level 100, B at level 200). + + End MonadNotation. + Import MonadNotation. + + Fixpoint traverselist {A B: Type} (f: A -> mon B) (l: list A) {struct l}: mon (list B) := + match l with + | nil => ret nil + | x::xs => + do r <- f x; + do rs <- traverselist f xs; + ret (r::rs) + end. + + Fixpoint collectlist {A : Type} (f : A -> mon unit) (l : list A) {struct l} : mon unit := + match l with + | nil => ret tt + | x::xs => do _ <- f x; collectlist f xs + end. + +End MonadExtra. diff --git a/src/common/Statemonad.v b/src/common/Statemonad.v new file mode 100644 index 0000000..ed1b9e7 --- /dev/null +++ b/src/common/Statemonad.v @@ -0,0 +1,61 @@ +From compcert Require Errors. +From coqup Require Import Monad. +From Coq Require Import Lists.List. + +Module Type State. + Parameter st : Type. + Parameter st_prop : st -> st -> Prop. + + Axiom st_refl : forall s, st_prop s s. + Axiom st_trans : forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3. +End State. + +Module Statemonad(S : State) <: Monad. + + Inductive res (A: Type) (s: S.st): Type := + | Error : Errors.errmsg -> res A s + | OK : A -> forall (s' : S.st), S.st_prop s s' -> res A s. + + Arguments OK [A s]. + Arguments Error [A s]. + + Definition mon (A: Type) : Type := forall (s: S.st), res A s. + + Definition ret {A: Type} (x: A) : mon A := + fun (s : S.st) => OK x s (S.st_refl s). + + Definition bind {A B: Type} (f: mon A) (g: A -> mon B) : mon B := + fun (s : S.st) => + match f s with + | Error msg => Error msg + | OK a s' i => + match g a s' with + | Error msg => Error msg + | OK b s'' i' => OK b s'' (S.st_trans s s' s'' i i') + end + end. + + Definition bind2 {A B C: Type} (f: mon (A * B)) (g: A -> B -> mon C) : mon C := + bind f (fun xy => g (fst xy) (snd xy)). + + Definition handle_error {A: Type} (f g: mon A) : mon A := + fun (s : S.st) => + match f s with + | OK a s' i => OK a s' i + | Error _ => g s + end. + + Definition error {A: Type} (err: Errors.errmsg) : mon A := fun (s: S.st) => Error err. + + Definition get : mon S.st := fun s => OK s s (S.st_refl s). + + Definition set (s: S.st) (i: forall s', S.st_prop s' s) : mon unit := + fun s' => OK tt s (i s'). + + Definition run_mon {A: Type} (s: S.st) (m: mon A): Errors.res A := + match m s with + | OK a s' i => Errors.OK a + | Error err => Errors.Error err + end. + +End Statemonad. diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index 319e2eb..0028fcb 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -1,4 +1,4 @@ -(* -*- mode: coq -*- +(* * CoqUp: Verified high-level synthesis. * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> * diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index d7f88c1..4564237 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -16,171 +16,374 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From coqup Require Import HTL Coquplib. - From compcert Require Import Maps. From compcert Require Errors. From compcert Require Import AST RTL. +From coqup Require Import Verilog HTL Coquplib AssocMap Value Statemonad. + +Hint Resolve AssocMap.gempty : htlh. +Hint Resolve AssocMap.gso : htlh. +Hint Resolve AssocMap.gss : htlh. +Hint Resolve Ple_refl : htlh. +Hint Resolve Ple_succ : htlh. Record state: Type := mkstate { - st_nextinst: positive; - st_instances: instances; + st_st : reg; + st_freshreg: reg; + st_freshstate: node; + st_datapath: datapath; + st_controllogic: controllogic; }. -Inductive res (A: Type) (S: Type): Type := - | Error: Errors.errmsg -> res A S - | OK: A -> S -> res A S. +Definition init_state (st : reg) : state := + mkstate st + 1%positive + 1%positive + (AssocMap.empty stmnt) + (AssocMap.empty stmnt). + +Module HTLState <: State. + + Definition st := state. + + Inductive st_incr: state -> state -> Prop := + state_incr_intro: + forall (s1 s2: state), + st_st s1 = st_st s2 -> + Ple s1.(st_freshreg) s2.(st_freshreg) -> + Ple s1.(st_freshstate) s2.(st_freshstate) -> + (forall n, + s1.(st_datapath)!n = None \/ s2.(st_datapath)!n = s1.(st_datapath)!n) -> + (forall n, + s1.(st_controllogic)!n = None + \/ s2.(st_controllogic)!n = s1.(st_controllogic)!n) -> + st_incr s1 s2. + Hint Constructors st_incr : htlh. + + Definition st_prop := st_incr. + Hint Unfold st_prop : htlh. + + Lemma st_refl : forall s, st_prop s s. Proof. auto with htlh. Qed. + + Lemma st_trans : + forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3. + Proof. + intros. inv H. inv H0. apply state_incr_intro; eauto using Ple_trans. + - rewrite H1. rewrite H. reflexivity. + - intros. destruct H4 with n. + + left; assumption. + + destruct H8 with n; + [ rewrite <- H0; left; assumption + | right; rewrite <- H0; apply H10 + ]. + - intros. destruct H5 with n. + + left; assumption. + + destruct H9 with n. + * rewrite <- H0. left. assumption. + * right. rewrite <- H0. apply H10. + Qed. + +End HTLState. +Export HTLState. -Arguments OK [A S]. -Arguments Error [A S]. +Module HTLMonad := Statemonad(HTLState). +Export HTLMonad. -Definition mon (A: Type) : Type := res A state. +Module HTLMonadExtra := Monad.MonadExtra(HTLMonad). +Import HTLMonadExtra. +Export MonadNotation. -Definition ret {A: Type} (x: A) (s: state) : mon A := OK x s. +Definition state_goto (st : reg) (n : node) : stmnt := + Vnonblock (Vvar st) (Vlit (posToValue 32 n)). -Definition bind {A B: Type} (f: mon A) (g: A -> mon B) : mon B := - match f with - | Error msg => Error msg - | OK a s => g a +Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt := + Vnonblock (Vvar st) (Vternary c (posToExpr 32 n1) (posToExpr 32 n2)). + +Definition check_empty_node_datapath: + forall (s: state) (n: node), { s.(st_datapath)!n = None } + { True }. +Proof. + intros. case (s.(st_datapath)!n); intros. right; auto. left; auto. +Defined. + +Definition check_empty_node_controllogic: + forall (s: state) (n: node), { s.(st_controllogic)!n = None } + { True }. +Proof. + intros. case (s.(st_controllogic)!n); intros. right; auto. left; auto. +Defined. + +Lemma add_instr_state_incr : + forall s n n' st, + (st_datapath s)!n = None -> + (st_controllogic s)!n = None -> + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))). +Proof. + constructor; intros; + try (simpl; destruct (peq n n0); subst); + auto with htlh. +Qed. + +Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit := + fun s => + match check_empty_node_datapath s n, check_empty_node_controllogic s n with + | left STM, left TRANS => + OK tt (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))) + (add_instr_state_incr s n n' st STM TRANS) + | _, _ => Error (Errors.msg "HTL.add_instr") end. -Definition bind2 {A B C: Type} (f: mon (A * B)) (g: A -> B -> mon C) : mon C := - bind f (fun xy => g (fst xy) (snd xy)). +Lemma add_instr_skip_state_incr : + forall s n st, + (st_datapath s)!n = None -> + (st_controllogic s)!n = None -> + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n Vskip s.(st_controllogic))). +Proof. + constructor; intros; + try (simpl; destruct (peq n n0); subst); + auto with htlh. +Qed. + +Definition add_instr_skip (n : node) (st : stmnt) : mon unit := + fun s => + match check_empty_node_datapath s n, check_empty_node_controllogic s n with + | left STM, left TRANS => + OK tt (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n Vskip s.(st_controllogic))) + (add_instr_skip_state_incr s n st STM TRANS) + | _, _ => Error (Errors.msg "HTL.add_instr") + end. + +Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e. +Definition block (dst : reg) (e : expr) := Vblock (Vvar dst) e. + +Definition bop (op : binop) (r1 r2 : reg) : expr := + Vbinop op (Vvar r1) (Vvar r2). + +Definition boplit (op : binop) (r : reg) (l : Integers.int) : expr := + Vbinop op (Vvar r) (Vlit (intToValue l)). -Definition bindS {A B: Type} (f: mon A) (g: A -> state -> mon B) : mon B := - match f with - | Error msg => Error msg - | OK a s => g a s +Definition boplitz (op: binop) (r: reg) (l: Z) : expr := + Vbinop op (Vvar r) (Vlit (ZToValue 32%nat l)). + +Definition translate_comparison (c : Integers.comparison) (args : list reg) : mon expr := + match c, args with + | Integers.Ceq, r1::r2::nil => ret (bop Veq r1 r2) + | Integers.Cne, r1::r2::nil => ret (bop Vne r1 r2) + | Integers.Clt, r1::r2::nil => ret (bop Vlt r1 r2) + | Integers.Cgt, r1::r2::nil => ret (bop Vgt r1 r2) + | Integers.Cle, r1::r2::nil => ret (bop Vle r1 r2) + | Integers.Cge, r1::r2::nil => ret (bop Vge r1 r2) + | _, _ => error (Errors.msg "Veriloggen: comparison instruction not implemented: other") end. -Notation "'do' X <- A ; B" := (bind A (fun X => B)) - (at level 200, X ident, A at level 100, B at level 200). -Notation "'do' ( X , Y ) <- A ; B" := (bindS A (fun X Y => B)) - (at level 200, X ident, Y ident, A at level 100, B at level 200). +Definition translate_comparison_imm (c : Integers.comparison) (args : list reg) (i: Integers.int) + : mon expr := + match c, args with + | Integers.Ceq, r1::nil => ret (boplit Veq r1 i) + | Integers.Cne, r1::nil => ret (boplit Vne r1 i) + | Integers.Clt, r1::nil => ret (boplit Vlt r1 i) + | Integers.Cgt, r1::nil => ret (boplit Vgt r1 i) + | Integers.Cle, r1::nil => ret (boplit Vle r1 i) + | Integers.Cge, r1::nil => ret (boplit Vge r1 i) + | _, _ => error (Errors.msg "Veriloggen: comparison_imm instruction not implemented: other") + end. -Definition handle_error {A: Type} (f g: mon A) : mon A := - match f with - | OK a s' => OK a s' - | Error _ => g +Definition translate_condition (c : Op.condition) (args : list reg) : mon expr := + match c, args with + | Op.Ccomp c, _ => translate_comparison c args + | Op.Ccompu c, _ => translate_comparison c args + | Op.Ccompimm c i, _ => translate_comparison_imm c args i + | Op.Ccompuimm c i, _ => translate_comparison_imm c args i + | Op.Cmaskzero n, _ => error (Errors.msg "Veriloggen: condition instruction not implemented: Cmaskzero") + | Op.Cmasknotzero n, _ => error (Errors.msg "Veriloggen: condition instruction not implemented: Cmasknotzero") + | _, _ => error (Errors.msg "Veriloggen: condition instruction not implemented: other") end. -Definition init_state : state := - mkstate 1%positive empty_instances. - -Module PTree. - Export Maps.PTree. - - Fixpoint xtraverse {A B : Type} (f : positive -> A -> state -> mon B) - (m : PTree.t A) (s : state) (i : positive) - {struct m} : mon (PTree.t B) := - match m with - | Leaf => OK Leaf s - | Node l o r => - let newo := - match o with - | None => OK None s - | Some x => - match f (prev i) x s with - | Error err => Error err - | OK val s' => OK (Some val) s' - end - end in - match newo with - | OK no s => - do (nl, s') <- xtraverse f l s (xO i); - do (nr, s'') <- xtraverse f r s' (xI i); - OK (Node nl no nr) s'' - | Error msg => Error msg - end +Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon expr := + match a, args with + | Op.Aindexed off, r1::nil => ret (boplitz Vadd r1 off) + | Op.Aindexed2 off, r1::r2::nil => ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 off)) + | Op.Ascaled scale offset, r1::nil => + ret (Vbinop Vadd (boplitz Vadd r1 scale) (Vlit (ZToValue 32%nat offset))) + | Op.Aindexed2scaled scale offset, r1::r2::nil => + ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) + | _, _ => error (Errors.msg "Veriloggen: eff_addressing instruction not implemented: other") + end. + +(** Translate an instruction to a statement. *) +Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := + match op, args with + | Op.Omove, r::nil => ret (Vvar r) + | Op.Ointconst n, _ => ret (Vlit (intToValue n)) + | Op.Oneg, r::nil => ret (Vunop Vneg (Vvar r)) + | Op.Osub, r1::r2::nil => ret (bop Vsub r1 r2) + | Op.Omul, r1::r2::nil => ret (bop Vmul r1 r2) + | Op.Omulimm n, r::nil => ret (boplit Vmul r n) + | Op.Omulhs, _ => error (Errors.msg "Veriloggen: Instruction not implemented: Omulhs") + | Op.Omulhu, _ => error (Errors.msg "Veriloggen: Instruction not implemented: Omulhu") + | Op.Odiv, r1::r2::nil => ret (bop Vdiv r1 r2) + | Op.Odivu, r1::r2::nil => ret (bop Vdivu r1 r2) + | Op.Omod, r1::r2::nil => ret (bop Vmod r1 r2) + | Op.Omodu, r1::r2::nil => ret (bop Vmodu r1 r2) + | Op.Oand, r1::r2::nil => ret (bop Vand r1 r2) + | Op.Oandimm n, r::nil => ret (boplit Vand r n) + | Op.Oor, r1::r2::nil => ret (bop Vor r1 r2) + | Op.Oorimm n, r::nil => ret (boplit Vor r n) + | Op.Oxor, r1::r2::nil => ret (bop Vxor r1 r2) + | Op.Oxorimm n, r::nil => ret (boplit Vxor r n) + | Op.Onot, r::nil => ret (Vunop Vnot (Vvar r)) + | Op.Oshl, r1::r2::nil => ret (bop Vshl r1 r2) + | Op.Oshlimm n, r::nil => ret (boplit Vshl r n) + | Op.Oshr, r1::r2::nil => ret (bop Vshr r1 r2) + | Op.Oshrimm n, r::nil => ret (boplit Vshr r n) + | Op.Oshrximm n, r::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Oshrximm") + | Op.Oshru, r1::r2::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Oshru") + | Op.Oshruimm n, r::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Oshruimm") + | Op.Ororimm n, r::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Ororimm") + | Op.Oshldimm n, r::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Oshldimm") + | Op.Ocmp c, _ => translate_condition c args + | Op.Olea a, _ => translate_eff_addressing a args + | _, _ => error (Errors.msg "Veriloggen: Instruction not implemented: other") + end. + +Lemma add_branch_instr_state_incr: + forall s e n n1 n2, + (st_datapath s) ! n = None -> + (st_controllogic s) ! n = None -> + st_incr s (mkstate + s.(st_st) + (st_freshreg s) + (st_freshstate s) + (AssocMap.set n Vskip (st_datapath s)) + (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))). +Proof. + intros. apply state_incr_intro; simpl; + try (intros; destruct (peq n0 n); subst); + auto with htlh. +Qed. + +Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit := + fun s => + match check_empty_node_datapath s n, check_empty_node_controllogic s n with + | left NSTM, left NTRANS => + OK tt (mkstate + s.(st_st) + (st_freshreg s) + (st_freshstate s) + (AssocMap.set n Vskip (st_datapath s)) + (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))) + (add_branch_instr_state_incr s e n n1 n2 NSTM NTRANS) + | _, _ => Error (Errors.msg "Veriloggen: add_branch_instr") end. - Definition traverse {A B : Type} (f : positive -> A -> state -> mon B) m := - xtraverse f m init_state xH. - - Definition traverse1 {A B : Type} (f : A -> state -> mon B) := traverse (fun _ => f). - -End PTree. - -Definition transf_instr (pc: node) (rtl: RTL.instruction) (s: state) - : mon HTL.instruction := - match rtl with - | RTL.Inop n => - (** Nop instruction should just become a Skip in Verilog, which is just a - semicolon. *) - ret (HTL.Hnop n) s - | RTL.Iop op args res n => - (** Perform an arithmetic operation over registers. This will just become - one binary operation in Verilog. This will contain a list of registers, - so these will just become a chain of binary operations in Verilog. *) - ret (HTL.Hnonblock op args res n) s - | RTL.Iload chunk addr args dst n => - (** Load from memory, which will maybe become a load from RAM, however, I'm - not sure yet how memory will be implemented or how it will formalised - be. *) - ret (HTL.Hload chunk addr args dst n) s - | RTL.Istore chunk addr args src n => - (** How memory will be laid out will also affect how stores are handled. For - now hopefully these can be ignored, and hopefull they are not used that - often when they are not required in C. *) - ret (HTL.Hstore chunk addr args src n) s - | RTL.Icall sig ros args res n => - (** Function call should become a module instantiation with start and end - signals appropriately wired up. *) - match ros with - | inr i => - let inst := mkinst i args in - let newinstances := PTree.set s.(st_nextinst) inst s.(st_instances) in - ret (HTL.Hinst sig i res n) - (mkstate ((s.(st_nextinst) + 1)%positive) - newinstances) - | _ => Error (Errors.msg "Function pointers are not supported.") - end - | RTL.Itailcall sig ros args => - (** Should be converted into a reset of the modules state, setting the - initial variables correctly. This would simulate a tailcall as it is - similar to jumping back to the top of the function in assembly. *) - match ros with - | inr i => ret (HTL.Htailcall sig i args) s - | _ => Error (Errors.msg "Function pointers are not supported.") +Definition transf_instr (fin rtrn: reg) (ni: node * instruction) : mon unit := + match ni with + (n, i) => + match i with + | Inop n' => add_instr n n' Vskip + | Iop op args dst n' => + do instr <- translate_instr op args; + add_instr n n' (nonblock dst instr) + | Iload _ _ _ _ _ => error (Errors.msg "Loads are not implemented.") + | Istore _ _ _ _ _ => error (Errors.msg "Stores are not implemented.") + | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.") + | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.") + | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.") + | Icond cond args n1 n2 => + do e <- translate_condition cond args; + add_branch_instr e n n1 n2 + | Ijumptable _ _ => error (Errors.msg "Jumptable not implemented") + | Ireturn r => + match r with + | Some r' => + add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r'))) + | None => + add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vlit (ZToValue 1%nat 0%Z)))) + end end - | RTL.Ibuiltin ef args res n => - (** Builtin functions will have to supported manually, by implementing the - Verilog myself. *) - Error (Errors.msg "builtin functions are not supported.") - | RTL.Icond cond args n1 n2 => - (** Will be converted into two separate processes that are combined by a mux - at the end, with a start flag that propagates in the construct that should - be chosen. *) - ret (HTL.Hcond cond args n1 n2) s - | RTL.Ijumptable arg tbl => - (** A jump to a specific instruction in the list, this will require setting - the state in the state machine appropriately. This is trivial to - implement if no scheduling is involved, but as soon as that isn't the - case it might be difficult to find that location. It would help to - transform the CFG to a few basic blocks first which cannot have any - branching. *) - ret (HTL.Hjumptable arg tbl) s - | RTL.Ireturn r => - (** The return value of the function, which will just mean that the finished - signal goes high and the result is stored in the result register. *) - ret (HTL.Hfinish r) s end. -Definition transf_function (f: function) : Errors.res module := - match (PTree.traverse transf_instr f.(fn_code)) with - | OK code s => - Errors.OK (mkmodule - f.(fn_sig) - f.(fn_params) - f.(fn_stacksize) - code - s.(st_instances) - f.(fn_entrypoint)) - | Error err => Errors.Error err - end. +Lemma create_reg_state_incr: + forall s, + st_incr s (mkstate + s.(st_st) + (Pos.succ (st_freshreg s)) + (st_freshstate s) + (st_datapath s) + (st_controllogic s)). +Proof. constructor; simpl; auto with htlh. Qed. + +Definition create_reg: mon reg := + fun s => let r := s.(st_freshreg) in + OK r (mkstate + s.(st_st) + (Pos.succ r) + (st_freshstate s) + (st_datapath s) + (st_controllogic s)) + (create_reg_state_incr s). + +Definition transf_module (f: function) : mon module := + do fin <- create_reg; + do rtrn <- create_reg; + do _ <- collectlist (transf_instr fin rtrn) (Maps.PTree.elements f.(RTL.fn_code)); + do start <- create_reg; + do rst <- create_reg; + do clk <- create_reg; + do current_state <- get; + ret (mkmodule + f.(RTL.fn_params) + current_state.(st_datapath) + current_state.(st_controllogic) + f.(fn_entrypoint) + current_state.(st_st) + fin + rtrn). -Definition transf_fundef (fd: fundef) : Errors.res moddecl := - transf_partial_fundef transf_function fd. +Definition max_state (f: function) : state := + let st := Pos.succ (max_reg_function f) in + mkstate st + (Pos.succ st) + (Pos.succ (max_pc_function f)) + (st_datapath (init_state st)) + (st_controllogic (init_state st)). -Definition transf_program (p: program) : Errors.res design := - transform_partial_program transf_fundef p. +Definition transl_module (f : function) : Errors.res module := + run_mon (max_state f) (transf_module f). + +Fixpoint main_function (main : ident) (flist : list (ident * AST.globdef fundef unit)) +{struct flist} : option function := + match flist with + | (i, AST.Gfun (AST.Internal f)) :: xs => + if Pos.eqb i main + then Some f + else main_function main xs + | _ :: xs => main_function main xs + | nil => None + end. + +Definition transf_program (d : program) : Errors.res module := + match main_function d.(AST.prog_main) d.(AST.prog_defs) with + | Some f => transl_module f + | _ => Errors.Error (Errors.msg "HTL: could not find main function") + end. diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v new file mode 100644 index 0000000..2d2129c --- /dev/null +++ b/src/translation/HTLgenproof.v @@ -0,0 +1,396 @@ +(* + * CoqUp: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * + * 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 <https://www.gnu.org/licenses/>. + *) + +From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap. +From coqup Require HTL Verilog. +From compcert Require RTL Registers Globalenvs AST. + +Import AssocMapNotation. + +Hint Resolve Smallstep.forward_simulation_plus : htlproof. +Hint Resolve AssocMap.gss : htlproof. +Hint Resolve AssocMap.gso : htlproof. + +Hint Unfold find_assocmap AssocMapExt.get_default : htlproof. + +Inductive match_assocmaps : RTL.function -> RTL.regset -> assocmap -> Prop := + match_assocmap : forall f rs am, + (forall r, Ple r (RTL.max_reg_function f) -> + val_value_lessdef (Registers.Regmap.get r rs) am#r) -> + match_assocmaps f rs am. +Hint Constructors match_assocmaps : htlproof. + +Definition state_st_wf (m : HTL.module) (s : HTL.state) := + forall st assoc, + s = HTL.State m st assoc -> + assoc!(m.(HTL.mod_st)) = Some (posToValue 32 st). +Hint Unfold state_st_wf : htlproof. + +Inductive match_states : RTL.state -> HTL.state -> Prop := +| match_state : forall (rs : RTL.regset) assoc sf f sp rs mem m st + (MASSOC : match_assocmaps f rs assoc) + (TF : tr_module f m) + (WF : state_st_wf m (HTL.State m st assoc)), + match_states (RTL.State sf f sp st rs mem) + (HTL.State m st assoc) +| match_returnstate : forall v v' stack m, + val_value_lessdef v v' -> + match_states (RTL.Returnstate stack v m) (HTL.Returnstate v'). +Hint Constructors match_states : htlproof. + +Inductive match_program : RTL.program -> HTL.module -> Prop := + match_program_intro : + forall ge p b m f, + ge = Globalenvs.Genv.globalenv p -> + Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b -> + Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal f) -> + tr_module f m -> + match_program p m. +Hint Constructors match_program : htlproof. + +Lemma regs_lessdef_add_greater : + forall f rs1 rs2 n v, + Plt (RTL.max_reg_function f) n -> + match_assocmaps f rs1 rs2 -> + match_assocmaps f rs1 (AssocMap.set n v rs2). +Proof. + inversion 2; subst. + intros. constructor. + intros. unfold find_assocmap. unfold AssocMapExt.get_default. + rewrite AssocMap.gso. eauto. + apply Pos.le_lt_trans with _ _ n in H2. + unfold not. intros. subst. eapply Pos.lt_irrefl. eassumption. assumption. +Qed. +Hint Resolve regs_lessdef_add_greater : htlproof. + +Lemma regs_lessdef_add_match : + forall f rs am r v v', + val_value_lessdef v v' -> + match_assocmaps f rs am -> + match_assocmaps f (Registers.Regmap.set r v rs) (AssocMap.set r v' am). +Proof. + inversion 2; subst. + constructor. intros. + destruct (peq r0 r); subst. + rewrite Registers.Regmap.gss. + unfold find_assocmap. unfold AssocMapExt.get_default. + rewrite AssocMap.gss. assumption. + + rewrite Registers.Regmap.gso; try assumption. + unfold find_assocmap. unfold AssocMapExt.get_default. + rewrite AssocMap.gso; eauto. +Qed. +Hint Resolve regs_lessdef_add_match : htlproof. + +Lemma valToValue_lessdef : + forall v v', + valToValue v = Some v' <-> + val_value_lessdef v v'. +Proof. + split; intros. + destruct v; try discriminate; constructor. + unfold valToValue in H. inversion H. + Admitted. + +(* Need to eventually move posToValue 32 to posToValueAuto, as that has this proof. *) +Lemma assumption_32bit : + forall v, + valueToPos (posToValue 32 v) = v. +Admitted. + +Lemma assumption_32bit_bool : + forall b, + valueToBool (boolToValue 32 b) = b. +Admitted. + +Lemma st_greater_than_res : + forall m res : positive, + m <> res. +Admitted. + +Lemma finish_not_return : + forall r f : positive, + r <> f. +Admitted. + +Lemma finish_not_res : + forall f r : positive, + f <> r. +Admitted. + +Ltac inv_state := + match goal with + MSTATE : match_states _ _ |- _ => + inversion MSTATE; + match goal with + TF : tr_module _ _ |- _ => + inversion TF; + match goal with + TC : forall _ _, + Maps.PTree.get _ _ = Some _ -> tr_code _ _ _ _ _ _ _, + H : Maps.PTree.get _ _ = Some _ |- _ => + apply TC in H; inversion H; + match goal with + TI : tr_instr _ _ _ _ _ _ |- _ => + inversion TI + end + end + end + end; subst. + +Section CORRECTNESS. + + Variable prog : RTL.program. + Variable tprog : HTL.module. + + Hypothesis TRANSL : match_program prog tprog. + + Let ge : RTL.genv := Globalenvs.Genv.globalenv prog. + Let tge : HTL.genv := HTL.genv_empty. + + Lemma eval_correct : + forall sp op rs args m v v' e assoc f, + Op.eval_operation ge sp op +(List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some v -> + tr_op op args e -> + valToValue v = Some v' -> + Verilog.expr_runp f assoc e v'. + Admitted. + + Lemma eval_cond_correct : + forall cond (args : list Registers.reg) s1 c s' i rs args m b f assoc, + translate_condition cond args s1 = OK c s' i -> + Op.eval_condition cond (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some b -> + Verilog.expr_runp f assoc c (boolToValue 32 b). + Admitted. + + (** The proof of semantic preservation for the translation of instructions + is a simulation argument based on diagrams of the following form: +<< + match_states + code st rs ---------------- State m st assoc + || | + || | + || | + \/ v + code st rs' --------------- State m st assoc' + match_states +>> + where [tr_code c data control fin rtrn st] is assumed to hold. + + The precondition and postcondition is that that should hold is [match_assocmaps rs assoc]. + *) + + Definition transl_instr_prop (instr : RTL.instruction) : Prop := + forall m assoc fin rtrn st stmt trans, + tr_instr fin rtrn st instr stmt trans -> + exists assoc', + HTL.step tge (HTL.State m st assoc) Events.E0 (HTL.State m st assoc'). + + Lemma greater_than_max_func : + forall f st, + Plt (RTL.max_reg_function f) st. + Proof. Admitted. + + Theorem transl_step_correct: + forall (S1 : RTL.state) t S2, + RTL.step ge S1 t S2 -> + forall (R1 : HTL.state), + match_states S1 R1 -> + exists R2, Smallstep.plus HTL.step tge R1 t R2 /\ match_states S2 R2. + Proof. + induction 1; intros R1 MSTATE; try inv_state. + - (* Inop *) + econstructor. + split. + apply Smallstep.plus_one. + eapply HTL.step_module; eauto. + (* processing of state *) + econstructor. + simpl. trivial. + econstructor. trivial. + econstructor. + + (* prove stval *) + unfold_merge. simpl. apply AssocMap.gss. + + (* prove match_state *) + rewrite assumption_32bit. + constructor; auto. + unfold_merge. simpl. apply regs_lessdef_regs. apply greater_than_max_func. + assumption. + unfold state_st_wf. inversion 1. subst. unfold_merge. apply AssocMap.gss. + - (* Iop *) + econstructor. + split. + apply Smallstep.plus_one. + eapply HTL.step_module; eauto. + econstructor; simpl; trivial. + constructor; trivial. + econstructor; simpl; eauto. + eapply eval_correct; eauto. + unfold_merge. simpl. + rewrite AssocMap.gso. + apply AssocMap.gss. + apply st_greater_than_res. + trivial. + + (* match_states *) + assert (pc' = valueToPos (posToValue 32 pc')). symmetry. apply assumption_32bit. + rewrite <- H1. + constructor. apply rs0. + unfold_merge. + apply regs_add_match. + apply regs_lessdef_regs. + assumption. + apply valToValue_lessdef. + assumption. + + unfold state_st_wf. intros. inversion H2. subst. + unfold_merge. + rewrite AssocMap.gso. + apply AssocMap.gss. + apply st_greater_than_res. + - econstructor. split. apply Smallstep.plus_one. + eapply HTL.step_module; eauto. + eapply Verilog.stmnt_runp_Vnonblock with + (rhsval := if b then posToValue 32 ifso else posToValue 32 ifnot). + simpl. trivial. + destruct b. + eapply Verilog.erun_Vternary_true. + eapply eval_cond_correct; eauto. + constructor. + apply assumption_32bit_bool. + eapply Verilog.erun_Vternary_false. + eapply eval_cond_correct; eauto. + constructor. + apply assumption_32bit_bool. + trivial. + constructor. + trivial. + unfold_merge. + apply AssocMap.gss. + trivial. + + destruct b. + rewrite assumption_32bit. + apply match_state. apply rs0. + unfold_merge. + apply regs_lessdef_regs. assumption. + assumption. + + unfold state_st_wf. intros. inversion H1. + subst. unfold_merge. + apply AssocMap.gss. + rewrite assumption_32bit. + apply match_state. apply rs0. + unfold_merge. + apply regs_lessdef_regs. assumption. + assumption. + + unfold state_st_wf. intros. inversion H1. + subst. unfold_merge. + apply AssocMap.gss. + + - (* Return *) + econstructor. split. + eapply Smallstep.plus_two. + + eapply HTL.step_module; eauto. + constructor. + econstructor; simpl; trivial. + econstructor; simpl; trivial. + constructor. + econstructor; simpl; trivial. + constructor. + unfold_merge. + trivial. + rewrite AssocMap.gso. + rewrite AssocMap.gso. + unfold state_st_wf in WF. apply WF. trivial. + apply st_greater_than_res. apply st_greater_than_res. trivial. + + apply HTL.step_finish. + unfold_merge; simpl. + rewrite AssocMap.gso. + apply AssocMap.gss. + apply finish_not_return. + apply AssocMap.gss. + rewrite Events.E0_left. trivial. + + constructor. constructor. + - destruct (assoc!r) eqn:?. + inversion H11. subst. + econstructor. split. + eapply Smallstep.plus_two. + eapply HTL.step_module; eauto. + constructor. + econstructor; simpl; trivial. + econstructor; simpl; trivial. + constructor. + econstructor; simpl; trivial. + apply Verilog.erun_Vvar. + rewrite AssocMap.gso. + apply Heqo. apply not_eq_sym. apply finish_not_res. + unfold_merge. + trivial. + rewrite AssocMap.gso. + rewrite AssocMap.gso. + unfold state_st_wf in WF. apply WF. trivial. + apply st_greater_than_res. apply st_greater_than_res. trivial. + + apply HTL.step_finish. + unfold_merge. + rewrite AssocMap.gso. + apply AssocMap.gss. + apply finish_not_return. + apply AssocMap.gss. + rewrite Events.E0_left. trivial. + + constructor. simpl. + Admitted. + Hint Resolve transl_step_correct : htlproof. + + Lemma senv_preserved : + forall id : AST.ident, + Globalenvs.Senv.public_symbol (Smallstep.symbolenv (HTL.semantics tprog)) id = + Globalenvs.Senv.public_symbol (Smallstep.symbolenv (RTL.semantics prog)) id. + Proof. Admitted. + Hint Resolve senv_preserved : htlproof. + + Lemma transl_initial_states : + forall s1 : Smallstep.state (RTL.semantics prog), + Smallstep.initial_state (RTL.semantics prog) s1 -> + exists s2 : Smallstep.state (HTL.semantics tprog), + Smallstep.initial_state (HTL.semantics tprog) s2 /\ match_states s1 s2. + Proof. Admitted. + Hint Resolve transl_initial_states : htlproof. + + Lemma transl_final_states : + forall (s1 : Smallstep.state (RTL.semantics prog)) (s2 : Smallstep.state (HTL.semantics tprog)) + (r : Integers.Int.int), + match_states s1 s2 -> + Smallstep.final_state (RTL.semantics prog) s1 r -> Smallstep.final_state (HTL.semantics tprog) s2 r. + Proof. Admitted. + Hint Resolve transl_final_states : htlproof. + + Theorem transf_program_correct: + Smallstep.forward_simulation (RTL.semantics prog) (HTL.semantics tprog). + Proof. eauto with htlproof. Qed. + +End CORRECTNESS. diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v new file mode 100644 index 0000000..713a373 --- /dev/null +++ b/src/translation/HTLgenspec.v @@ -0,0 +1,359 @@ +(* + * CoqUp: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * + * 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 <https://www.gnu.org/licenses/>. + *) + +From compcert Require RTL Op Maps Errors. +From compcert Require Import Maps. +From coqup Require Import Coquplib Verilog Value HTL HTLgen AssocMap. + +Hint Resolve Maps.PTree.elements_keys_norepet : htlspec. +Hint Resolve Maps.PTree.elements_correct : htlspec. + +Remark bind_inversion: + forall (A B: Type) (f: mon A) (g: A -> mon B) + (y: B) (s1 s3: st) (i: st_incr s1 s3), + bind f g s1 = OK y s3 i -> + exists x, exists s2, exists i1, exists i2, + f s1 = OK x s2 i1 /\ g x s2 = OK y s3 i2. +Proof. + intros until i. unfold bind. destruct (f s1); intros. + discriminate. + exists a; exists s'; exists s. + destruct (g a s'); inv H. + exists s0; auto. +Qed. + +Remark bind2_inversion: + forall (A B C: Type) (f: mon (A*B)) (g: A -> B -> mon C) + (z: C) (s1 s3: st) (i: st_incr s1 s3), + bind2 f g s1 = OK z s3 i -> + exists x, exists y, exists s2, exists i1, exists i2, + f s1 = OK (x, y) s2 i1 /\ g x y s2 = OK z s3 i2. +Proof. + unfold bind2; intros. + exploit bind_inversion; eauto. + intros [[x y] [s2 [i1 [i2 [P Q]]]]]. simpl in Q. + exists x; exists y; exists s2; exists i1; exists i2; auto. +Qed. + +Ltac monadInv1 H := + match type of H with + | (OK _ _ _ = OK _ _ _) => + inversion H; clear H; try subst + | (Error _ _ = OK _ _ _) => + discriminate + | (ret _ _ = OK _ _ _) => + inversion H; clear H; try subst + | (error _ _ = OK _ _ _) => + discriminate + | (bind ?F ?G ?S = OK ?X ?S' ?I) => + let x := fresh "x" in ( + let s := fresh "s" in ( + let i1 := fresh "INCR" in ( + let i2 := fresh "INCR" in ( + let EQ1 := fresh "EQ" in ( + let EQ2 := fresh "EQ" in ( + destruct (bind_inversion _ _ F G X S S' I H) as [x [s [i1 [i2 [EQ1 EQ2]]]]]; + clear H; + try (monadInv1 EQ2))))))) + | (bind2 ?F ?G ?S = OK ?X ?S' ?I) => + let x1 := fresh "x" in ( + let x2 := fresh "x" in ( + let s := fresh "s" in ( + let i1 := fresh "INCR" in ( + let i2 := fresh "INCR" in ( + let EQ1 := fresh "EQ" in ( + let EQ2 := fresh "EQ" in ( + destruct (bind2_inversion _ _ _ F G X S S' I H) as [x1 [x2 [s [i1 [i2 [EQ1 EQ2]]]]]]; + clear H; + try (monadInv1 EQ2)))))))) + end. + +Ltac monadInv H := + match type of H with + | (ret _ _ = OK _ _ _) => monadInv1 H + | (error _ _ = OK _ _ _) => monadInv1 H + | (bind ?F ?G ?S = OK ?X ?S' ?I) => monadInv1 H + | (bind2 ?F ?G ?S = OK ?X ?S' ?I) => monadInv1 H + | (?F _ _ _ _ _ _ _ _ = OK _ _ _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + | (?F _ _ _ _ _ _ _ = OK _ _ _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + | (?F _ _ _ _ _ _ = OK _ _ _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + | (?F _ _ _ _ _ = OK _ _ _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + | (?F _ _ _ _ = OK _ _ _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + | (?F _ _ _ = OK _ _ _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + | (?F _ _ = OK _ _ _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + | (?F _ = OK _ _ _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + end. + +(** * Relational specification of the translation *) + +(** We now define inductive predicates that characterise the fact that the +statemachine that is created by the translation contains the correct +translations for each of the elements *) + +Inductive tr_op : Op.operation -> list reg -> expr -> Prop := +| tr_op_Omove : forall r, tr_op Op.Omove (r::nil) (Vvar r) +| tr_op_Ointconst : forall n l, tr_op (Op.Ointconst n) l (Vlit (intToValue n)) +| tr_op_Oneg : forall r, tr_op Op.Oneg (r::nil) (Vunop Vneg (Vvar r)) +| tr_op_Osub : forall r1 r2, tr_op Op.Osub (r1::r2::nil) (bop Vsub r1 r2) +| tr_op_Omul : forall r1 r2, tr_op Op.Omul (r1::r2::nil) (bop Vmul r1 r2) +| tr_op_Omulimm : forall r n, tr_op (Op.Omulimm n) (r::nil) (boplit Vmul r n) +| tr_op_Odiv : forall r1 r2, tr_op Op.Odiv (r1::r2::nil) (bop Vdiv r1 r2) +| tr_op_Odivu : forall r1 r2, tr_op Op.Odivu (r1::r2::nil) (bop Vdivu r1 r2) +| tr_op_Omod : forall r1 r2, tr_op Op.Omod (r1::r2::nil) (bop Vmod r1 r2) +| tr_op_Omodu : forall r1 r2, tr_op Op.Omodu (r1::r2::nil) (bop Vmodu r1 r2) +| tr_op_Oand : forall r1 r2, tr_op Op.Oand (r1::r2::nil) (bop Vand r1 r2) +| tr_op_Oandimm : forall n r, tr_op (Op.Oandimm n) (r::nil) (boplit Vand r n) +| tr_op_Oor : forall r1 r2, tr_op Op.Oor (r1::r2::nil) (bop Vor r1 r2) +| tr_op_Oorimm : forall n r, tr_op (Op.Oorimm n) (r::nil) (boplit Vor r n) +| tr_op_Oxor : forall r1 r2, tr_op Op.Oxor (r1::r2::nil) (bop Vxor r1 r2) +| tr_op_Oxorimm : forall n r, tr_op (Op.Oxorimm n) (r::nil) (boplit Vxor r n) +| tr_op_Onot : forall r, tr_op Op.Onot (r::nil) (Vunop Vnot (Vvar r)) +| tr_op_Oshl : forall r1 r2, tr_op Op.Oshl (r1::r2::nil) (bop Vshl r1 r2) +| tr_op_Oshlimm : forall n r, tr_op (Op.Oshlimm n) (r::nil) (boplit Vshl r n) +| tr_op_Oshr : forall r1 r2, tr_op Op.Oshr (r1::r2::nil) (bop Vshr r1 r2) +| tr_op_Oshrimm : forall n r, tr_op (Op.Oshrimm n) (r::nil) (boplit Vshr r n) +| tr_op_Ocmp : forall c l e s s' i, translate_condition c l s = OK e s' i -> tr_op (Op.Ocmp c) l e +| tr_op_Olea : forall a l e s s' i, translate_eff_addressing a l s = OK e s' i -> tr_op (Op.Olea a) l e. +Hint Constructors tr_op : htlspec. + +Inductive tr_instr (fin rtrn st : reg) : RTL.instruction -> stmnt -> stmnt -> Prop := +| tr_instr_Inop : + forall n, + tr_instr fin rtrn st (RTL.Inop n) Vskip (state_goto st n) +| tr_instr_Iop : + forall n op args e dst, + tr_op op args e -> + tr_instr fin rtrn st (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n) +| tr_instr_Icond : + forall n1 n2 cond args s s' i c, + translate_condition cond args s = OK c s' i -> + tr_instr fin rtrn st (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2) +| tr_instr_Ireturn_None : + tr_instr fin rtrn st (RTL.Ireturn None) (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) + (block rtrn (Vlit (ZToValue 1%nat 0%Z)))) Vskip +| tr_instr_Ireturn_Some : + forall r, + tr_instr fin rtrn st (RTL.Ireturn (Some r)) + (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r))) Vskip. +Hint Constructors tr_instr : htlspec. + +Inductive tr_code (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt) + (fin rtrn st : reg) : Prop := + tr_code_intro : + forall s t, + stmnts!pc = Some s -> + trans!pc = Some t -> + tr_instr fin rtrn st i s t -> + tr_code pc i stmnts trans fin rtrn st. +Hint Constructors tr_code : htlspec. + +Inductive tr_module (f : RTL.function) : module -> Prop := + tr_module_intro : + forall data control fin rtrn st m, + (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> + tr_code pc i data control fin rtrn st) -> + m = (mkmodule f.(RTL.fn_params) + data + control + f.(RTL.fn_entrypoint) + st fin rtrn) -> + tr_module f m. +Hint Constructors tr_module : htlspec. + +Lemma create_reg_datapath_trans : + forall s s' x i, + create_reg s = OK x s' i -> + s.(st_datapath) = s'.(st_datapath). +Proof. intros. monadInv H. trivial. Qed. +Hint Resolve create_reg_datapath_trans : htlspec. + +Lemma create_reg_controllogic_trans : + forall s s' x i, + create_reg s = OK x s' i -> + s.(st_controllogic) = s'.(st_controllogic). +Proof. intros. monadInv H. trivial. Qed. +Hint Resolve create_reg_controllogic_trans : htlspec. + +Lemma get_refl_x : + forall s s' x i, + get s = OK x s' i -> + s = x. +Proof. inversion 1. trivial. Qed. +Hint Resolve get_refl_x : htlspec. + +Lemma get_refl_s : + forall s s' x i, + get s = OK x s' i -> + s = s'. +Proof. inversion 1. trivial. Qed. +Hint Resolve get_refl_s : htlspec. + +Ltac inv_incr := + repeat match goal with + | [ H: create_reg ?s = OK _ ?s' _ |- _ ] => + let H1 := fresh "H" in + assert (H1 := H); eapply create_reg_datapath_trans in H; + eapply create_reg_controllogic_trans in H1 + | [ H: get ?s = OK _ _ _ |- _ ] => + let H1 := fresh "H" in + assert (H1 := H); apply get_refl_x in H; apply get_refl_s in H1; + subst + | [ H: st_prop _ _ |- _ ] => unfold st_prop in H; destruct H + | [ H: st_incr _ _ |- _ ] => destruct st_incr + end. + +Ltac rewrite_states := + match goal with + | [ H: ?x ?s = ?x ?s' |- _ ] => + let c1 := fresh "c" in + let c2 := fresh "c" in + remember (?x ?s) as c1; remember (?x ?s') as c2; try subst + end. + +Lemma translate_instr_tr_op : + forall op args s s' e i, + translate_instr op args s = OK e s' i -> + tr_op op args e. +Proof. + intros. + destruct op eqn:?; eauto with htlspec; try discriminate; simpl in *; + try (match goal with + [ H: match ?args with _ => _ end _ = _ _ _ |- _ ] => + repeat (destruct args; try discriminate) + end); + monadInv H; constructor. +Qed. +Hint Resolve translate_instr_tr_op : htlspec. + +Ltac unfold_match H := + match type of H with + | context[match ?g with _ => _ end] => destruct g; try discriminate + end. + +Ltac inv_add_instr' H := + match type of H with + | ?f _ _ _ = OK _ _ _ => unfold f in H + | ?f _ _ _ _ = OK _ _ _ => unfold f in H + | ?f _ _ _ _ _ = OK _ _ _ => unfold f in H + end; repeat unfold_match H; inversion H. + +Ltac inv_add_instr := + match goal with + | H: context[add_instr_skip _ _ _] |- _ => + inv_add_instr' H + | H: context[add_instr_skip _ _] |- _ => + monadInv H; inv_incr; inv_add_instr + | H: context[add_instr _ _ _ _] |- _ => + inv_add_instr' H + | H: context[add_instr _ _ _] |- _ => + monadInv H; inv_incr; inv_add_instr + | H: context[add_branch_instr _ _ _ _ _] |- _ => + inv_add_instr' H + | H: context[add_branch_instr _ _ _ _] |- _ => + monadInv H; inv_incr; inv_add_instr + end. + +Ltac destruct_optional := + match goal with H: option ?r |- _ => destruct H end. + +Lemma iter_expand_instr_spec : + forall l fin rtrn s s' i x, + HTLMonadExtra.collectlist (transf_instr fin rtrn) l s = OK x s' i -> + list_norepet (List.map fst l) -> + (forall pc instr, In (pc, instr) l -> + tr_code pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st)). +Proof. + induction l; simpl; intros; try contradiction. + destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr. + destruct (peq pc pc1). + + subst. + destruct instr1 eqn:?; try discriminate; try destruct_optional; inv_add_instr; econstructor. + + * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; + [ discriminate | apply H7 ]. + * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; + [ discriminate | apply H7 ]. + * inversion H1. inversion H7. rewrite H. apply tr_instr_Inop. + eapply in_map with (f := fst) in H7. simpl in H7. contradiction. + + * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; + [ discriminate | apply H7 ]. + * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; + [ discriminate | apply H7 ]. + * inversion H1. inversion H7. unfold nonblock. rewrite <- e2. rewrite H. constructor. + eapply translate_instr_tr_op. apply EQ1. + eapply in_map with (f := fst) in H7. simpl in H7. contradiction. + + * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; + [ discriminate | apply H7 ]. + * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; + [ discriminate | apply H7 ]. + * inversion H1. inversion H7. rewrite <- e2. rewrite H. econstructor. apply EQ1. + eapply in_map with (f := fst) in H7. simpl in H7. contradiction. + + * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; + [ discriminate | apply H7 ]. + * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; + [ discriminate | apply H7 ]. + * inversion H1. inversion H7. constructor. + eapply in_map with (f := fst) in H7. simpl in H7. contradiction. + + * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; + [ discriminate | apply H7 ]. + * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; + [ discriminate | apply H7 ]. + * inversion H1. inversion H7. constructor. + eapply in_map with (f := fst) in H7. simpl in H7. contradiction. + + + eapply IHl. apply EQ0. assumption. + destruct H1. inversion H1. subst. contradiction. + assumption. +Qed. +Hint Resolve iter_expand_instr_spec : htlspec. + +Theorem transl_module_correct : + forall f m, + transl_module f = Errors.OK m -> tr_module f m. +Proof. + intros until m. + unfold transl_module. + unfold run_mon. + destruct (transf_module f (max_state f)) eqn:?; try discriminate. + intros. inv H. + inversion s; subst. + + unfold transf_module in *. + monadInv Heqr. + econstructor; simpl; trivial. + intros. + inv_incr. + assert (st_controllogic s8 = st_controllogic s2) by congruence. + rewrite <- H10. + assert (st_datapath s8 = st_datapath s2) by congruence. + assert (st_st s5 = st_st s2) by congruence. + rewrite H80. rewrite H81. rewrite H82. + eauto with htlspec. +Qed. diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v index 412dc28..4a6f23e 100644 --- a/src/translation/Veriloggen.v +++ b/src/translation/Veriloggen.v @@ -1,4 +1,4 @@ -(* -*- mode: coq -*- +(* * CoqUp: Verified high-level synthesis. * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> * @@ -38,6 +38,18 @@ Inductive statetrans : Type := | StateGoto (p : node) | StateCond (c : expr) (t f : node). +Definition state_goto (st : reg) (n : node) : stmnt := + Vnonblock (Vvar st) (Vlit (posToValue 32 n)). + +Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt := + Vnonblock (Vvar st) (Vternary c (posToExpr 32 n1) (posToExpr 32 n2)). + +Definition statetrans_transl (stvar : reg) (st : statetrans) : stmnt := + match st with + | StateGoto p => state_goto stvar p + | StateCond c t f => state_cond stvar c t f + end. + Definition valid_freshstate (stm: PositiveMap.t stmnt) (fs: node) := forall (n: node), Plt n fs \/ stm!n = None. @@ -371,6 +383,10 @@ Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit := | _, _, _ => Error (Errors.msg "Veriloggen.add_instr") end. +(** Add a register to the state without changing the [st_freshreg], as this +should already be the right value. This can be assumed because the max register +is taken from the RTL code. *) + Definition add_reg (r: reg) (s: state) : state := mkstate (st_freshreg s) (st_freshstate s) @@ -410,6 +426,9 @@ Lemma decl_io_state_incr: (st_wf s)). Proof. constructor; simpl; auto using Ple_succ with verilog_state. Qed. +(** Declare a new register by incrementing the [st_freshreg] by one and +returning the old [st_freshreg]. *) + Definition decl_io (d: decl) : mon (reg * decl) := fun s => let r := s.(st_freshreg) in OK (r, d) (mkstate @@ -421,6 +440,9 @@ Definition decl_io (d: decl) : mon (reg * decl) := (st_wf s)) (decl_io_state_incr s). +(** Declare a new register which is given, by changing [st_decl] and without +affecting anything else. *) + Definition declare_reg (r: reg) (d: decl): mon (reg * decl) := fun s => OK (r, d) (mkstate (st_freshreg s) @@ -431,6 +453,9 @@ Definition declare_reg (r: reg) (d: decl): mon (reg * decl) := (st_wf s)) (change_decl_state_incr s (PositiveMap.add r d s.(st_decl))). +(** Declare a new fresh register by first getting a valid register to increment, +and then adding it to the declaration list. *) + Definition decl_fresh_reg (d: decl) : mon (reg * decl) := do (r, d) <- decl_io d; declare_reg r d. @@ -557,18 +582,17 @@ Definition make_stm (r : reg) (s : PositiveMap.t stmnt) : stmnt := Definition make_statetrans_cases (r : reg) (st : positive * statetrans) : expr * stmnt := match st with - | (n, StateGoto n') => (posToExpr 32 n, nonblock r (posToExpr 32 n')) - | (n, StateCond c n1 n2) => (posToExpr 32 n, nonblock r (Vternary c (posToExpr 32 n1) (posToExpr 32 n2))) + | (n, StateGoto n') => (posToExpr 32 n, state_goto r n') + | (n, StateCond c n1 n2) => (posToExpr 32 n, state_cond r c n1 n2) end. Definition make_statetrans (r : reg) (s : PositiveMap.t statetrans) : stmnt := Vcase (Vvar r) (map (make_statetrans_cases r) (PositiveMap.elements s)) (Some Vskip). -Fixpoint allocate_regs (e : list (reg * decl)) {struct e} : list module_item := +Definition allocate_reg (e : reg * decl) : module_item := match e with - | (r, (mkdecl n 0))::es => Vdecl r n :: allocate_regs es - | (r, (mkdecl n l))::es => Vdeclarr r n l :: allocate_regs es - | nil => nil + | (r, (mkdecl n 0)) => Vdecl r n + | (r, (mkdecl n l)) => Vdeclarr r n l end. Definition make_module_items (entry: node) (clk st rst: reg) (s: state) : list module_item := @@ -577,7 +601,7 @@ Definition make_module_items (entry: node) (clk st rst: reg) (s: state) : list m (nonblock st (posToExpr 32 entry)) (make_statetrans st s.(st_statetrans)))) :: (Valways_ff (Vposedge clk) (make_stm st s.(st_stm))) - :: (allocate_regs (PositiveMap.elements s.(st_decl))). + :: (map allocate_reg (PositiveMap.elements s.(st_decl))). (** To start out with, the assumption is made that there is only one function/module in the original code. *) @@ -598,20 +622,9 @@ Definition transf_module (f: function) : mon module := do st <- decl_fresh_reg (mkdecl 32 0); do current_state <- get; let mi := make_module_items f.(fn_entrypoint) (fst clk) (fst st) (fst rst) current_state in - ret (mkmodule (get_sz start) (get_sz rst) (get_sz clk) (get_sz fin) (get_sz rtrn) + ret (mkmodule (get_sz start) (get_sz rst) (get_sz clk) (get_sz fin) (get_sz rtrn) (get_sz st) (map set_int_size f.(fn_params)) mi). -Fixpoint main_function (main : ident) (flist : list (ident * AST.globdef fundef unit)) -{struct flist} : option function := - match flist with - | (i, AST.Gfun (AST.Internal f)) :: xs => - if Pos.eqb i main - then Some f - else main_function main xs - | _ :: xs => main_function main xs - | nil => None - end. - Lemma max_state_valid_freshstate: forall f, valid_freshstate (st_stm init_state) (Pos.succ (max_pc_function f)). @@ -632,6 +645,24 @@ Definition max_state (f: function) : state := (st_decl init_state) (max_state_st_wf f). +Definition transl_module (f : function) : Errors.res module := + run_mon (max_state f) (transf_module f). + +(** Retrieve the main function from the RTL, this should probably be replaced by +retrieving a designated function instead. This could be passed on the +commandline and be assumed as a [Parameter] in this code. *) + +Fixpoint main_function (main : ident) (flist : list (ident * AST.globdef fundef unit)) +{struct flist} : option function := + match flist with + | (i, AST.Gfun (AST.Internal f)) :: xs => + if Pos.eqb i main + then Some f + else main_function main xs + | _ :: xs => main_function main xs + | nil => None + end. + Definition transf_program (d : program) : Errors.res module := match main_function d.(AST.prog_main) d.(AST.prog_defs) with | Some f => run_mon (max_state f) (transf_module f) diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v new file mode 100644 index 0000000..942a83a --- /dev/null +++ b/src/translation/Veriloggenproof.v @@ -0,0 +1,46 @@ +(* + * CoqUp: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * + * 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 <https://www.gnu.org/licenses/>. + *) + +From compcert Require Import Smallstep. +From compcert Require RTL. +From coqup Require Verilog. + +Section CORRECTNESS. + + Variable prog: RTL.program. + Variable tprog: Verilog.module. + + Inductive match_states: RTL.state -> Verilog.state -> Prop := + | match_state: + forall, + + match_states (RTL.State f s k sp e m) + (Verilog.State m mi mis assoc nbassoc f cycle pc) + | match_returnstate: + forall v tv k m tm cs + (MS: match_stacks k cs) + (LD: Val.lessdef v tv) + (MEXT: Mem.extends m tm), + match_states (CminorSel.Returnstate v k m) + (RTL.Returnstate cs tv tm). + + Theorem transf_program_correct: + forward_simulation (RTL.semantics prog) (Verilog.semantics tprog). + Admitted. + +End CORRECTNESS. diff --git a/src/translation/Veriloggenspec.v b/src/translation/Veriloggenspec.v new file mode 100644 index 0000000..09d08ed --- /dev/null +++ b/src/translation/Veriloggenspec.v @@ -0,0 +1,130 @@ +(* + * CoqUp: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * + * 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 <https://www.gnu.org/licenses/>. + *) + +From Coq Require Import FSets.FMapPositive. +From compcert Require RTL Op Maps. +From coqup Require Import Coquplib Verilog Veriloggen Value. + +(** * Relational specification of the translation *) + +(** We now define inductive predicates that characterise the fact that the +statemachine that is created by the translation contains the correct +translations for each of the elements *) + +Inductive tr_op : Op.operation -> list reg -> expr -> Prop := +| tr_op_Omove : forall r, tr_op Op.Omove (r::nil) (Vvar r) +| tr_op_Ointconst : forall n l, tr_op (Op.Ointconst n) l (Vlit (intToValue n)) +| tr_op_Oneg : forall r, tr_op Op.Oneg (r::nil) (Vunop Vneg (Vvar r)) +| tr_op_Osub : forall r1 r2, tr_op Op.Osub (r1::r2::nil) (bop Vsub r1 r2) +| tr_op_Omul : forall r1 r2, tr_op Op.Omul (r1::r2::nil) (bop Vmul r1 r2) +| tr_op_Omulimm : forall r n, tr_op (Op.Omulimm n) (r::nil) (boplit Vmul r n) +| tr_op_Odiv : forall r1 r2, tr_op Op.Odiv (r1::r2::nil) (bop Vdiv r1 r2) +| tr_op_Odivu : forall r1 r2, tr_op Op.Odivu (r1::r2::nil) (bop Vdivu r1 r2) +| tr_op_Omod : forall r1 r2, tr_op Op.Omod (r1::r2::nil) (bop Vmod r1 r2) +| tr_op_Omodu : forall r1 r2, tr_op Op.Omodu (r1::r2::nil) (bop Vmodu r1 r2) +| tr_op_Oand : forall r1 r2, tr_op Op.Oand (r1::r2::nil) (bop Vand r1 r2) +| tr_op_Oandimm : forall n r, tr_op (Op.Oandimm n) (r::nil) (boplit Vand r n) +| tr_op_Oor : forall r1 r2, tr_op Op.Oor (r1::r2::nil) (bop Vor r1 r2) +| tr_op_Oorimm : forall n r, tr_op (Op.Oorimm n) (r::nil) (boplit Vor r n) +| tr_op_Oxor : forall r1 r2, tr_op Op.Oxor (r1::r2::nil) (bop Vxor r1 r2) +| tr_op_Oxorimm : forall n r, tr_op (Op.Oxorimm n) (r::nil) (boplit Vxor r n) +| tr_op_Onot : forall r, tr_op Op.Onot (r::nil) (Vunop Vnot (Vvar r)) +| tr_op_Oshl : forall r1 r2, tr_op Op.Oshl (r1::r2::nil) (bop Vshl r1 r2) +| tr_op_Oshlimm : forall n r, tr_op (Op.Oshlimm n) (r::nil) (boplit Vshl r n) +| tr_op_Oshr : forall r1 r2, tr_op Op.Oshr (r1::r2::nil) (bop Vshr r1 r2) +| tr_op_Oshrimm : forall n r, tr_op (Op.Oshrimm n) (r::nil) (boplit Vshr r n) +| tr_op_Ocmp : forall c l e s s' i, translate_condition c l s = OK e s' i -> tr_op (Op.Ocmp c) l e +| tr_op_Olea : forall a l e s s' i, translate_eff_addressing a l s = OK e s' i -> tr_op (Op.Olea a) l e. + +Inductive tr_instr (fin rtrn st : reg) : RTL.instruction -> stmnt -> stmnt -> Prop := +| tr_instr_Inop : + forall n, + tr_instr fin rtrn st (RTL.Inop n) Vskip (state_goto st n) +| tr_instr_Iop : + forall n op args e dst, + tr_op op args e -> + tr_instr fin rtrn st (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n) +| tr_instr_Icond : + forall n1 n2 cond args s s' i c, + translate_condition cond args s = OK c s' i -> + tr_instr fin rtrn st (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2) +| tr_instr_Ireturn_None : + tr_instr fin rtrn st (RTL.Ireturn None) (block fin (Vlit (ZToValue 1%nat 1%Z))) Vskip +| tr_instr_Ireturn_Some : + forall r, + tr_instr fin rtrn st (RTL.Ireturn (Some r)) + (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r))) Vskip. + +Inductive tr_code (c : RTL.code) (stmnts trans : PositiveMap.t stmnt) + (fin rtrn st : reg) : Prop := +| tr_code_intro : + forall i s t n, + Maps.PTree.get n c = Some i -> + stmnts!n = Some s -> + trans!n = Some t -> + tr_instr fin rtrn st i s t -> + tr_code c stmnts trans fin rtrn st. + +(** [tr_module_items start clk st rst s mis] holds if the state is correctly +translated to actual Verilog, meaning it is correctly implemented as a state +machine in Verilog. Currently it does not seem that useful because it models +the [make_module_items] nearly exactly. Therefore it might have to be changed +to make up for that. *) + +Inductive tr_module_items : node -> reg -> reg -> reg -> state -> list module_item -> Prop := + tr_module_items_intro : + forall start clk st rst s mis, + Valways_ff (Vposedge clk) + (Vcond (Vbinop Veq (Vinputvar rst) (Vlit (ZToValue 1 1))) + (nonblock st (posToExpr 32 start)) + (make_statetrans st s.(st_statetrans))) + :: Valways_ff (Vposedge clk) (make_stm st s.(st_stm)) + :: List.map allocate_reg (PositiveMap.elements s.(st_decl)) = mis -> + tr_module_items start clk st rst s mis. + +(** [tr_module function module] Holds if the [module] is the correct translation +of the [function] that it was given. *) + +Inductive tr_module : RTL.function -> module -> Prop := + tr_module_intro : + forall f mi st rtrn fin clk rst start s0 s1 s2 s3 s4 s5 s6 i1 i2 i3 i4 i5 i6, + decl_io 1 s0 = OK fin s1 i1 -> + decl_io 32 s1 = OK rtrn s2 i2 -> + decl_io 1 s2 = OK start s3 i3 -> + decl_io 1 s3 = OK rst s4 i4 -> + decl_io 1 s4 = OK clk s5 i5 -> + decl_fresh_reg 32 s5 = OK st s6 i6 -> + tr_code f.(RTL.fn_code) s6.(st_stm) + (PositiveMap.map (statetrans_transl (fst st)) s6.(st_statetrans)) + (fst fin) (fst rtrn) (fst st) -> + tr_module_items f.(RTL.fn_entrypoint) (fst clk) (fst st) (fst rst) s6 mi -> + tr_module f (mkmodule + start + rst + clk + fin + rtrn + st + (List.map set_int_size f.(RTL.fn_params)) + mi). + +Lemma tr_module_correct: + forall f m, + transl_module f = Errors.OK m -> + tr_module f m. +Admitted. diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v new file mode 100644 index 0000000..88b13a6 --- /dev/null +++ b/src/verilog/AssocMap.v @@ -0,0 +1,210 @@ +(* + * CoqUp: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * + * 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 <https://www.gnu.org/licenses/>. + *) + +From coqup Require Import Coquplib Value. +From compcert Require Import Maps. + +Definition reg := positive. + +Module AssocMap := Maps.PTree. + +Module AssocMapExt. + Import AssocMap. + + Hint Resolve elements_correct elements_complete + elements_keys_norepet : assocmap. + Hint Resolve gso gss : assocmap. + + Section Operations. + + Variable A : Type. + + Definition get_default (a : A) (k : reg) (m : t A) : A := + match get k m with + | None => a + | Some v => v + end. + + Fixpoint merge (m1 m2 : t A) : t A := + match m1, m2 with + | Node l1 (Some a) r1, Node l2 _ r2 => Node (merge l1 l2) (Some a) (merge r1 r2) + | Node l1 None r1, Node l2 o r2 => Node (merge l1 l2) o (merge r1 r2) + | Leaf, _ => m2 + | _, _ => m1 + end. + + Lemma merge_base_1 : + forall am, + merge (empty A) am = am. + Proof. auto. Qed. + Hint Resolve merge_base_1 : assocmap. + + Lemma merge_base_2 : + forall am, + merge am (empty A) = am. + Proof. + unfold merge. + destruct am; trivial. + destruct o; trivial. + Qed. + Hint Resolve merge_base_2 : assocmap. + + Lemma merge_add_assoc : + forall r am am' v, + merge (set r v am) am' = set r v (merge am am'). + Proof. + induction r; intros; destruct am; destruct am'; try (destruct o); simpl; + try rewrite IHr; try reflexivity. + Qed. + Hint Resolve merge_add_assoc : assocmap. + + Lemma merge_correct_1 : + forall am bm k v, + get k am = Some v -> + get k (merge am bm) = Some v. + Proof. + induction am; intros; destruct k; destruct bm; try (destruct o); simpl; + try rewrite gempty in H; try discriminate; try assumption; auto. + Qed. + Hint Resolve merge_correct_1 : assocmap. + + Lemma merge_correct_2 : + forall am bm k v, + get k am = None -> + get k bm = Some v -> + get k (merge am bm) = Some v. + Proof. + induction am; intros; destruct k; destruct bm; try (destruct o); simpl; + try rewrite gempty in H; try discriminate; try assumption; auto. + Qed. + Hint Resolve merge_correct_2 : assocmap. + + Definition merge_fold (am bm : t A) : t A := + fold_right (fun p a => set (fst p) (snd p) a) bm (elements am). + + Lemma add_assoc : + forall (k : elt) (v : A) l bm, + List.In (k, v) l -> + list_norepet (List.map fst l) -> + @get A k (fold_right (fun p a => set (fst p) (snd p) a) bm l) = Some v. + Proof. + induction l; intros. + - contradiction. + - destruct a as [k' v']. + destruct (peq k k'). + + inversion H. inversion H1. inversion H0. subst. + simpl. auto with assocmap. + + inversion H0; subst. apply in_map with (f:=fst) in H1. contradiction. + + + inversion H. inversion H1. inversion H0. subst. simpl. rewrite gso; try assumption. + apply IHl. contradiction. contradiction. + simpl. rewrite gso; try assumption. apply IHl. assumption. inversion H0. subst. assumption. + Qed. + Hint Resolve add_assoc : assocmap. + + Lemma not_in_assoc : + forall k v l bm, + ~ List.In k (List.map (@fst elt A) l) -> + @get A k bm = Some v -> + get k (fold_right (fun p a => set (fst p) (snd p) a) bm l) = Some v. + Proof. + induction l; intros. + - assumption. + - destruct a as [k' v']. + destruct (peq k k'); subst; + simpl in *; apply Decidable.not_or in H; destruct H. contradiction. + rewrite AssocMap.gso; auto. + Qed. + Hint Resolve not_in_assoc : assocmap. + + Lemma elements_iff : + forall am k, + (exists v, get k am = Some v) <-> + List.In k (List.map (@fst _ A) (elements am)). + Proof. + split; intros. + destruct H. apply elements_correct in H. apply in_map with (f := fst) in H. apply H. + apply list_in_map_inv in H. destruct H. destruct H. subst. + exists (snd x). apply elements_complete. assert (x = (fst x, snd x)) by apply surjective_pairing. + rewrite H in H0; assumption. + Qed. + Hint Resolve elements_iff : assocmap. + + Lemma elements_correct' : + forall am k, + ~ (exists v, get k am = Some v) <-> + ~ List.In k (List.map (@fst _ A) (elements am)). + Proof. auto using not_iff_compat with assocmap. Qed. + Hint Resolve elements_correct' : assocmap. + + Lemma elements_correct_none : + forall am k, + get k am = None -> + ~ List.In k (List.map (@fst _ A) (elements am)). + Proof. + intros. apply elements_correct'. unfold not. intros. + destruct H0. rewrite H in H0. discriminate. + Qed. + Hint Resolve elements_correct_none : assocmap. + + Lemma merge_fold_add : + forall k v am bm, + am ! k = Some v -> + (merge_fold am bm) ! k = Some v. + Proof. unfold merge_fold; auto with assocmap. Qed. + Hint Resolve merge_fold_add : assocmap. + + Lemma merge_fold_not_in : + forall k v am bm, + get k am = None -> + get k bm = Some v -> + get k (merge_fold am bm) = Some v. + Proof. intros. apply not_in_assoc; auto with assocmap. Qed. + Hint Resolve merge_fold_not_in : assocmap. + + Lemma merge_fold_base : + forall am, + merge_fold (empty A) am = am. + Proof. auto. Qed. + Hint Resolve merge_fold_base : assocmap. + + End Operations. + +End AssocMapExt. +Import AssocMapExt. + +Definition assocmap := AssocMap.t value. + +Definition find_assocmap (n : nat) : reg -> assocmap -> value := + get_default value (ZToValue n 0). + +Definition empty_assocmap : assocmap := AssocMap.empty value. + +Definition merge_assocmap : assocmap -> assocmap -> assocmap := merge value. + +Ltac unfold_merge := + unfold merge_assocmap; try (repeat (rewrite merge_add_assoc)); + rewrite AssocMapExt.merge_base_1. + +Module AssocMapNotation. + Notation "a ! b" := (AssocMap.get 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 1d156ad..a21064c 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -16,89 +16,83 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -(** 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 Coq Require Import FSets.FMapPositive. +From coqup Require Import Coquplib Value AssocMap. +From coqup Require Verilog. +From compcert Require Events Globalenvs Smallstep Integers. From compcert Require Import Maps. -From compcert Require Op AST Memory Registers. - -Definition node := positive. -Definition reg := Registers.reg. - -Definition ident := AST.ident. - -Inductive instruction : Type := -| Hnop : node -> instruction -| Hnonblock : Op.operation -> list reg -> reg -> node -> instruction - (** [Hnonblock op args res next] Defines a nonblocking assignment to a - register, using the operation defined in Op.v. *) -| Hload : AST.memory_chunk -> Op.addressing -> list reg -> reg -> node -> instruction -| Hstore : AST.memory_chunk -> Op.addressing -> list reg -> reg -> node -> instruction -| Hinst : AST.signature -> ident -> reg -> node -> instruction - (** [Hinst sig fun args rst strt end res next] Defines the start of a - module instantiation, meaning the function will run until the result is - returned. *) -| Htailcall : AST.signature -> ident -> list reg -> instruction -| Hcond : Op.condition -> list reg -> node -> node -> instruction -| Hjumptable : reg -> list node -> instruction -| Hfinish : option reg -> instruction. - -Record inst : Type := - mkinst { - inst_moddecl : ident; - inst_args : list reg - }. +Import HexNotationValue. -Definition code : Type := PTree.t instruction. +(** 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. *) -Definition instances : Type := PTree.t inst. +Definition reg := positive. +Definition node := positive. -Definition empty_instances : instances := PTree.empty inst. +Definition datapath := PTree.t Verilog.stmnt. +Definition controllogic := PTree.t Verilog.stmnt. -(** Function declaration for VTL also contain a construction which describes the - functions that are called in the current function. This information is used - to print out *) -Record module : Type := +Record module: Type := mkmodule { - mod_sig : AST.signature; mod_params : list reg; - mod_stacksize : Z; - mod_code : code; - mod_insts : instances; - mod_entrypoint : node + mod_datapath : datapath; + mod_controllogic : controllogic; + mod_entrypoint : node; + mod_st : reg; + mod_finish : reg; + mod_return : reg }. -Definition moddecl := AST.fundef module. - -Definition design := AST.program moddecl unit. - -Definition modsig (md : moddecl) := - match md with - | AST.Internal m => mod_sig m - | AST.External ef => AST.ef_sig ef - end. - -(** Describes various transformations that can be applied to HTL. This applies - the transformation to each instruction in the function and returns the new - function with the modified instructions. *) -Section TRANSF. - - Variable transf_instr : node -> instruction -> instruction. - - Definition transf_module (m : module) : module := - mkmodule - m.(mod_sig) - m.(mod_params) - m.(mod_stacksize) - (PTree.map transf_instr m.(mod_code)) - m.(mod_insts) - m.(mod_entrypoint). - -End TRANSF. +(** * Operational Semantics *) + +Definition genv := Globalenvs.Genv.t unit unit. +Definition genv_empty := Globalenvs.Genv.empty_genv unit unit nil. + +Inductive state : Type := +| State : + forall (m : module) + (st : node) + (assoc : assocmap), + state +| Returnstate : forall v : value, state. + +Inductive step : genv -> state -> Events.trace -> state -> Prop := +| step_module : + forall g t m st ctrl data assoc0 assoc1 assoc2 assoc3 nbassoc0 nbassoc1 f stval pstval, + m.(mod_controllogic)!st = Some ctrl -> + m.(mod_datapath)!st = Some data -> + Verilog.stmnt_runp f + (Verilog.mkassociations assoc0 empty_assocmap) + ctrl + (Verilog.mkassociations assoc1 nbassoc0) -> + Verilog.stmnt_runp f + (Verilog.mkassociations assoc1 nbassoc0) + data + (Verilog.mkassociations assoc2 nbassoc1) -> + assoc3 = merge_assocmap nbassoc1 assoc2 -> + assoc3!(m.(mod_st)) = Some stval -> + valueToPos stval = pstval -> + step g (State m st assoc0) t (State m pstval assoc3) +| step_finish : + forall g t m st assoc retval, + assoc!(m.(mod_finish)) = Some (1'h"1") -> + assoc!(m.(mod_return)) = Some retval -> + step g (State m st assoc) t (Returnstate retval). +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 empty_assocmap). + +Inductive final_state : state -> Integers.int -> Prop := +| final_state_intro : forall retval retvali, + value_int_eqb retval retvali = true -> + final_state (Returnstate retval) retvali. + +Definition semantics (m : module) := + Smallstep.Semantics step (initial_state m) final_state genv_empty. diff --git a/src/verilog/Test.v b/src/verilog/Test.v new file mode 100644 index 0000000..90c5312 --- /dev/null +++ b/src/verilog/Test.v @@ -0,0 +1,99 @@ +(* + * CoqUp: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * + * 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 <https://www.gnu.org/licenses/>. + *) + +From coqup Require Import Verilog Veriloggen Coquplib Value. +From compcert Require Import AST Errors Maps Op Integers. +From compcert Require RTL. +From Coq Require Import FSets.FMapPositive. +From bbv Require Import Word. +Import ListNotations. +Import HexNotationValue. +Import WordScope. + +Local Open Scope word_scope. + +Definition test_module : module := + let mods := [ + Valways (Vposedge 3%positive) (Vseq (Vnonblock (Vvar 6%positive) (Vlit (ZToValue 32 5))) + (Vnonblock (Vvar 7%positive) + (Vvar 6%positive))) + ] in + mkmodule (1%positive, 1%nat) + (2%positive, 1%nat) + (3%positive, 1%nat) + (4%positive, 1%nat) + (5%positive, 32%nat) + (6%positive, 32%nat) + nil + mods. + +Definition test_input : RTL.function := + let sig := mksignature nil Tvoid cc_default in + let params := nil in + let stacksize := 0 in + let entrypoint := 3%positive in + let code := PTree.set 1%positive (RTL.Ireturn (Some 1%positive)) + (PTree.set 3%positive (RTL.Iop (Ointconst (Int.repr 5)) nil 1%positive 1%positive) + (PTree.empty RTL.instruction)) in + RTL.mkfunction sig params stacksize code entrypoint. + +Definition test_input_program : RTL.program := + mkprogram [(1%positive, Gfun (Internal test_input))] nil 1%positive. + +Compute transf_program test_input_program. + +Definition test_output_module : module := + {| mod_start := (4%positive, 1%nat); + mod_reset := (5%positive, 1%nat); + mod_clk := (6%positive, 1%nat); + mod_finish := (2%positive, 1%nat); + mod_return := (3%positive, 32%nat); + mod_state := (7%positive, 32%nat); + mod_args := []; + mod_body := + [Valways_ff (Vposedge 6%positive) + (Vcond (Vbinop Veq (Vinputvar 5%positive) (1'h"1")) + (Vnonblock (Vvar 7%positive) (32'h"3")) + (Vcase (Vvar 7%positive) + [(Vlit (32'h"1"), Vnonblock (Vvar 7%positive) (32'h"1")); + (Vlit (32'h"3"), Vnonblock (Vvar 7%positive) (32'h"1"))] + (Some Vskip))); + Valways_ff (Vposedge 6%positive) + (Vcase (Vvar 7%positive) + [(Vlit (32'h"1"), Vseq (Vblock (Vvar 2%positive) (Vlit (1'h"1"))) + (Vblock (Vvar 3%positive) (Vvar 1%positive))); + (Vlit (32'h"3"), Vblock (Vvar 1%positive) (Vlit (32'h"5")))] + (Some Vskip)); + Vdecl 1%positive 32; Vdecl 7%positive 32] |}. + +Lemma valid_test_output : + transf_program test_input_program = OK test_output_module. +Proof. trivial. Qed. + +Definition test_fextclk := initial_fextclk test_output_module. + +Lemma manual_simulation : + step (State test_output_module empty_assocmap empty_assocmap + test_fextclk 1 (32'h"1")) + (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); + apply nevalue; apply weqb_false; trivial. Unshelve. exact 0%nat. +Qed. diff --git a/src/verilog/Value.v b/src/verilog/Value.v index fe53dbc..34cb0d2 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -1,4 +1,4 @@ -(* -*- mode: coq -*- +(* * CoqUp: Verified high-level synthesis. * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> * @@ -18,8 +18,9 @@ (* begin hide *) From bbv Require Import Word. -From Coq Require Import ZArith.ZArith. -From compcert Require Import lib.Integers. +From bbv Require HexNotation WordScope. +From Coq Require Import ZArith.ZArith FSets.FMapPositive. +From compcert Require Import lib.Integers common.Values. (* end hide *) (** * Value @@ -47,7 +48,7 @@ Definition wordToValue : forall sz : nat, word sz -> value := mkvalue. Definition valueToWord : forall v : value, word (vsize v) := vword. -Definition valueToNat (v : value) : nat := +Definition valueToNat (v :value) : nat := wordToNat (vword v). Definition natToValue sz (n : nat) : value := @@ -59,13 +60,6 @@ Definition valueToN (v : value) : N := Definition NToValue sz (n : N) : value := mkvalue sz (NToWord sz n). -Definition posToValue sz (p : positive) : value := - mkvalue sz (posToWord sz p). - -Definition posToValueAuto (p : positive) : value := - let size := Z.to_nat (Z.succ (log_inf p)) in - mkvalue size (Word.posToWord size p). - Definition ZToValue (s : nat) (z : Z) : value := mkvalue s (ZToWord s z). @@ -75,9 +69,29 @@ Definition valueToZ (v : value) : Z := Definition uvalueToZ (v : value) : Z := uwordToZ (vword v). +Definition posToValue sz (p : positive) : value := + ZToValue sz (Zpos p). + +Definition posToValueAuto (p : positive) : value := + let size := Pos.to_nat (Pos.size p) in + ZToValue size (Zpos p). + +Definition valueToPos (v : value) : positive := + Z.to_pos (uvalueToZ v). + Definition intToValue (i : Integers.int) : value := ZToValue Int.wordsize (Int.unsigned i). +Definition valueToInt (i : value) : Integers.int := + Int.repr (valueToZ i). + +Definition valToValue (v : Values.val) : option value := + match v with + | Values.Vint i => Some (intToValue i) + | Values.Vundef => Some (ZToValue 32 0%Z) + | _ => None + end. + (** Convert a [value] to a [bool], so that choices can be made based on the result. This is also because comparison operators will give back [value] instead of [bool], so if they are in a condition, they will have to be converted before @@ -91,8 +105,8 @@ Definition boolToValue (sz : nat) (b : bool) : value := (** ** Arithmetic operations *) -Lemma unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1. -Proof. intros; subst; assumption. Qed. +Definition unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1. +intros; subst; assumption. Defined. Definition value_eq_size: forall v1 v2 : value, { vsize v1 = vsize v2 } + { True }. @@ -137,6 +151,64 @@ Definition eq_to_opt (v1 v2 : value) (f : vsize v1 = vsize v2 -> value) | _ => None end. +Lemma eqvalue {sz : nat} (x y : word sz) : x = y <-> mkvalue sz x = mkvalue sz y. +Proof. + split; intros. + subst. reflexivity. inversion H. apply existT_wordToZ in H1. + apply wordToZ_inj. assumption. +Qed. + +Lemma eqvaluef {sz : nat} (x y : word sz) : x = y -> mkvalue sz x = mkvalue sz y. +Proof. apply eqvalue. Qed. + +Lemma nevalue {sz : nat} (x y : word sz) : x <> y <-> mkvalue sz x <> mkvalue sz y. +Proof. split; intros; intuition. apply H. apply eqvalue. assumption. + apply H. rewrite H0. trivial. +Qed. + +Lemma nevaluef {sz : nat} (x y : word sz) : x <> y -> mkvalue sz x <> mkvalue sz y. +Proof. apply nevalue. Qed. + +(*Definition rewrite_word_size (initsz finalsz : nat) (w : word initsz) + : option (word finalsz) := + match Nat.eqb initsz finalsz return option (word finalsz) with + | true => Some _ + | false => None + end.*) + +Definition valueeq (sz : nat) (x y : word sz) : + {mkvalue sz x = mkvalue sz y} + {mkvalue sz x <> mkvalue sz y} := + match weq x y with + | left eq => left (eqvaluef x y eq) + | right ne => right (nevaluef x y ne) + end. + +Definition valueeqb (x y : value) : bool := + match value_eq_size x y with + | left EQ => + weqb (vword x) (unify_word (vsize x) (vsize y) (vword y) EQ) + | right _ => false + end. + +Definition value_projZ_eqb (v1 v2 : value) : bool := Z.eqb (valueToZ v1) (valueToZ v2). + +Theorem value_projZ_eqb_true : + forall v1 v2, + v1 = v2 -> value_projZ_eqb v1 v2 = true. +Proof. intros. subst. unfold value_projZ_eqb. apply Z.eqb_eq. trivial. Qed. + +Theorem valueeqb_true_iff : + forall v1 v2, + valueeqb v1 v2 = true <-> v1 = v2. +Proof. + split; intros. + unfold valueeqb in H. destruct (value_eq_size v1 v2) eqn:?. + - destruct v1, v2. simpl in H. +Abort. + +Definition value_int_eqb (v : value) (i : int) : bool := + Z.eqb (valueToZ v) (Int.unsigned i). + (** Arithmetic operations over [value], interpreting them as signed or unsigned depending on the operation. @@ -208,3 +280,48 @@ Definition shift_map (sz : nat) (f : word sz -> nat -> word sz) (w1 w2 : word sz Definition vshl v1 v2 := map_word2 (fun sz => shift_map sz (@wlshift sz)) v1 v2. Definition vshr v1 v2 := map_word2 (fun sz => shift_map sz (@wrshift sz)) v1 v2. + +Module HexNotationValue. + Export HexNotation. + Import WordScope. + + Notation "sz ''h' a" := (NToValue sz (hex a)) (at level 50). + +End HexNotationValue. + +Inductive val_value_lessdef: val -> value -> Prop := +| val_value_lessdef_int: + forall i v', + Integers.Int.unsigned i = valueToZ v' -> + val_value_lessdef (Vint i) v' +| lessdef_undef: forall v, val_value_lessdef Vundef v. + +Lemma valueToZ_ZToValue : + forall n z, + (- Z.of_nat (2 ^ n) <= z < Z.of_nat (2 ^ n))%Z -> + valueToZ (ZToValue (S n) z) = z. +Proof. + unfold valueToZ, ZToValue. simpl. + auto using wordToZ_ZToWord. +Qed. + +Lemma uvalueToZ_ZToValue : + forall n z, + (0 <= z < 2 ^ Z.of_nat n)%Z -> + uvalueToZ (ZToValue n z) = z. +Proof. + unfold uvalueToZ, ZToValue. simpl. + auto using uwordToZ_ZToWord. +Qed. + +Lemma valueToPos_posToValueAuto : + forall p, valueToPos (posToValueAuto p) = p. +Proof. + intros. unfold valueToPos, posToValueAuto. + rewrite uvalueToZ_ZToValue. auto. rewrite positive_nat_Z. + split. apply Zle_0_pos. + + assert (p < 2 ^ (Pos.size p))%positive. apply Pos.size_gt. + inversion H. rewrite <- Z.compare_lt_iff. rewrite <- H1. + simpl. rewrite <- Pos2Z.inj_pow_pos. trivial. +Qed. diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index dfb6255..e2b85b2 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -1,4 +1,4 @@ -(* -*- mode: coq -*- +(* * CoqUp: Verified high-level synthesis. * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> * @@ -27,18 +27,22 @@ 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. -From compcert Require Integers. -From compcert Require Import Errors. - -Notation "a ! b" := (PositiveMap.find b a) (at level 1). +Import HexNotationValue. +Import AssocMapNotation. Definition reg : Type := positive. Definition node : Type := positive. Definition szreg : Type := reg * nat. -Definition assoclist : Type := PositiveMap.t value. +Record associations : Type := + mkassociations { + assoc_blocking : assocmap; + assoc_nonblocking : assocmap + }. (** * Verilog AST @@ -51,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 := assoclist * assoclist. - (** ** Binary Operators These are the binary operations that can be represented in Verilog. Ideally, @@ -159,10 +161,10 @@ Record module : Type := mkmodule { mod_clk : szreg; mod_finish : szreg; mod_return : szreg; + 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 := @@ -171,15 +173,41 @@ Definition posToLit (p : positive) : expr := Coercion Vlit : value >-> expr. Coercion Vvar : reg >-> expr. -Definition fext := PositiveMap.t value. +Definition fext := AssocMap.t value. Definition fextclk := nat -> fext. -Inductive state: Type := - State: - forall (assoc : assoclist) - (nbassoc : assoclist) +(** ** State + +The [state] contains the following items: +n +- Current [module] that is being worked on, so that the state variable can be +retrieved and set appropriately. +- Current [module_item] which is being worked on. +- A contiunation ([cont]) which defines what to do next. The option is to + either evaluate another module item or go to the next clock cycle. Finally + it could also end if the finish flag of the module goes high. +- Association list containing the blocking assignments made, or assignments made + in previous clock cycles. +- Nonblocking association list containing all the nonblocking assignments made + in the current module. +- The environment containing values for the input. +- The program counter which determines the value for the state in this version of + Verilog, as the Verilog was generated by the RTL, which means that we have to + make an assumption about how it looks. In this case, that it contains state + which determines which part of the Verilog is executed. This is then the part + of the Verilog that should match with the RTL. *) + +Inductive state : Type := +| State: + forall (m : module) + (assoc : assocmap) + (nbassoc : assocmap) (f : fextclk) - (cycle : positive), + (cycle : nat) + (stvar : value), + state +| Finishstate: + forall v : value, state. Definition binop_run (op : binop) : forall v1 v2 : value, vsize v1 = vsize v2 -> value := @@ -214,40 +242,48 @@ Definition unop_run (op : unop) : value -> value := | Vnot => vbitneg end. -Inductive expr_runp : state -> expr -> value -> Prop := +Inductive expr_runp : fext -> assocmap -> expr -> value -> Prop := | erun_Vlit : - forall s v, - expr_runp s (Vlit v) v + forall fext assoc v, + expr_runp fext assoc (Vlit v) v | erun_Vvar : - forall assoc na f c v r, + forall fext assoc v r, assoc!r = Some v -> - expr_runp (State assoc na f c) (Vvar r) v + expr_runp fext assoc (Vvar r) v + | erun_Vvar_empty : + forall fext assoc r sz, + assoc!r = None -> + expr_runp fext assoc (Vvar r) (ZToValue sz 0) | erun_Vinputvar : - forall s r v, - expr_runp s (Vinputvar r) v + forall fext assoc r v, + fext!r = Some v -> + expr_runp fext assoc (Vinputvar r) v | erun_Vbinop : - forall s op l r lv rv oper EQ, - expr_runp s l lv -> - expr_runp s r rv -> + forall fext assoc op l r lv rv oper EQ resv, + expr_runp fext assoc l lv -> + expr_runp fext assoc r rv -> oper = binop_run op -> - expr_runp s (Vbinop op l r) (oper lv rv EQ) + resv = oper lv rv EQ -> + expr_runp fext assoc (Vbinop op l r) resv | erun_Vunop : - forall s u vu op oper, - expr_runp s u vu -> + forall fext assoc u vu op oper resv, + expr_runp fext assoc u vu -> oper = unop_run op -> - expr_runp s (Vunop op u) (oper vu) + resv = oper vu -> + expr_runp fext assoc (Vunop op u) resv | erun_Vternary_true : - forall s c ts fs vc vt, - expr_runp s c vc -> - expr_runp s ts vt -> + forall fext assoc c ts fs vc vt, + expr_runp fext assoc c vc -> + expr_runp fext assoc ts vt -> valueToBool vc = true -> - expr_runp s (Vternary c ts fs) vt + expr_runp fext assoc (Vternary c ts fs) vt | erun_Vternary_false : - forall s c ts fs vc vf, - expr_runp s c vc -> - expr_runp s fs vf -> + forall fext assoc c ts fs vc vf, + expr_runp fext assoc c vc -> + expr_runp fext assoc fs vf -> valueToBool vc = false -> - expr_runp s (Vternary c ts fs) vf. + expr_runp fext assoc (Vternary c ts fs) vf. +Hint Constructors expr_runp : verilog. Definition handle_opt {A : Type} (err : errmsg) (val : option A) : res A := @@ -265,22 +301,20 @@ Definition handle_def {A : Type} (a : A) (val : option A) Local Open Scope error_monad_scope. -Definition access_fext (s : state) (r : reg) : res value := - match s with - | State _ _ f c => - match PositiveMap.find r (f (Pos.to_nat c)) with - | Some v => OK v - | _ => OK (ZToValue 1 0) - end +Definition access_fext (f : fext) (r : reg) : res value := + match AssocMap.get r f with + | Some v => OK v + | _ => OK (ZToValue 1 0) end. (* TODO FIX Vvar case without default *) -Fixpoint expr_run (s : state) (e : expr) +(*Fixpoint expr_run (assoc : assocmap) (e : expr) {struct e} : res value := match e with | Vlit v => OK v | Vvar r => match s with - | State assoc _ _ _ => handle_def (ZToValue 32 0) assoc!r + | State _ assoc _ _ _ => handle_def (ZToValue 32 0) assoc!r + | _ => Error (msg "Verilog: Wrong state") end | Vvari _ _ => Error (msg "Verilog: variable indexing not modelled") | Vinputvar r => access_fext s r @@ -299,7 +333,7 @@ Fixpoint expr_run (s : state) (e : expr) | Vternary c te fe => do cv <- expr_run s c; if valueToBool cv then expr_run s te else expr_run s fe - end. + end.*) (** Return the name of the lhs of an assignment. For now, this function is quite simple because only assignment to normal variables is supported and needed. *) @@ -310,6 +344,15 @@ Definition assign_name (e : expr) : res reg := | _ => Error (msg "Verilog: expression not supported on lhs of assignment") end. +(*Fixpoint stmnt_height (st : stmnt) {struct st} : nat := + match st with + | Vseq s1 s2 => S (stmnt_height s1 + stmnt_height s2) + | Vcond _ s1 s2 => S (Nat.max (stmnt_height s1) (stmnt_height s2)) + | Vcase _ ls (Some st) => + S (fold_right (fun t acc => Nat.max acc (stmnt_height (snd t))) 0%nat ls) + | _ => 1 + end. + Fixpoint find_case_stmnt (s : state) (v : value) (cl : list (expr * stmnt)) {struct cl} : option (res stmnt) := match cl with @@ -348,35 +391,85 @@ Fixpoint stmnt_run' (n : nat) (s : state) (st : stmnt) {struct n} : res state := end | Vblock lhs rhs => match s with - | State assoc nbassoc f c => + | State m assoc nbassoc f c => do name <- assign_name lhs; do rhse <- expr_run s rhs; - OK (State (PositiveMap.add name rhse assoc) nbassoc f c) + OK (State m (PositiveMap.add name rhse assoc) nbassoc f c) + | _ => Error (msg "Verilog: Wrong state") end | Vnonblock lhs rhs => match s with - | State assoc nbassoc f c => + | State m assoc nbassoc f c => do name <- assign_name lhs; do rhse <- expr_run s rhs; - OK (State assoc (PositiveMap.add name rhse nbassoc) f c) + OK (State m assoc (PositiveMap.add name rhse nbassoc) f c) + | _ => Error (msg "Verilog: Wrong state") end end | _ => OK s end. -Fixpoint stmnt_height (st : stmnt) {struct st} : nat := - match st with - | Vseq s1 s2 => S (stmnt_height s1 + stmnt_height s2) - | Vcond _ s1 s2 => S (Nat.max (stmnt_height s1) (stmnt_height s2)) - | Vcase _ ls (Some st) => - S (fold_right (fun t acc => Nat.max acc (stmnt_height (snd t))) 0%nat ls) - | _ => 1 - end. - Definition stmnt_run (s : state) (st : stmnt) : res state := - stmnt_run' (stmnt_height st) s st. - -Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state := + stmnt_run' (stmnt_height st) s st. *) + +Inductive stmnt_runp: fext -> associations -> stmnt -> associations -> Prop := +| stmnt_runp_Vskip: + forall f a, stmnt_runp f a Vskip a +| stmnt_runp_Vseq: + forall f st1 st2 as0 as1 as2, + stmnt_runp f as0 st1 as1 -> + stmnt_runp f as1 st2 as2 -> + stmnt_runp f as0 (Vseq st1 st2) as2 +| stmnt_runp_Vcond_true: + forall as0 as1 f c vc stt stf, + expr_runp f as0.(assoc_blocking) c vc -> + valueToBool vc = true -> + stmnt_runp f as0 stt as1 -> + stmnt_runp f as0 (Vcond c stt stf) as1 +| stmnt_runp_Vcond_false: + forall as0 as1 f c vc stt stf, + expr_runp f as0.(assoc_blocking) c vc -> + valueToBool vc = false -> + stmnt_runp f as0 stf as1 -> + stmnt_runp f as0 (Vcond c stt stf) as1 +| stmnt_runp_Vcase_nomatch: + forall e ve as0 f as1 me mve sc cs def, + expr_runp f as0.(assoc_blocking) e ve -> + expr_runp f as0.(assoc_blocking) me mve -> + mve <> ve -> + stmnt_runp f as0 (Vcase e cs def) as1 -> + stmnt_runp f as0 (Vcase e ((me, sc)::cs) def) as1 +| stmnt_runp_Vcase_match: + forall e ve as0 f as1 me mve sc cs def, + expr_runp f as0.(assoc_blocking) e ve -> + expr_runp f as0.(assoc_blocking) me mve -> + mve = ve -> + stmnt_runp f as0 sc as1 -> + stmnt_runp f as0 (Vcase e ((me, sc)::cs) def) as1 +| stmnt_runp_Vcase_default: + forall as0 as1 f st e ve, + expr_runp f as0.(assoc_blocking) e ve -> + stmnt_runp f as0 st as1 -> + stmnt_runp f as0 (Vcase e nil (Some st)) as1 +| stmnt_runp_Vblock: + forall lhs name rhs rhsval assoc assoc' nbassoc f, + assign_name lhs = OK name -> + expr_runp f assoc rhs rhsval -> + assoc' = (AssocMap.set name rhsval assoc) -> + stmnt_runp f (mkassociations assoc nbassoc) + (Vblock lhs rhs) + (mkassociations assoc' nbassoc) +| stmnt_runp_Vnonblock: + forall lhs name rhs rhsval assoc nbassoc nbassoc' f, + assign_name lhs = OK name -> + expr_runp f assoc rhs rhsval -> + nbassoc' = (AssocMap.set name rhsval nbassoc) -> + stmnt_runp f (mkassociations assoc nbassoc) + (Vnonblock lhs rhs) + (mkassociations assoc nbassoc'). +Hint Constructors stmnt_runp : verilog. + +(*Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state := let run := fun st ls => do s' <- stmnt_run s st; mi_step s' ls @@ -388,41 +481,69 @@ Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state := | (Vdecl _ _)::ls => mi_step s ls | (Vdeclarr _ _ _)::ls => mi_step s ls | nil => OK s - end. - -Definition add_assoclist (r : reg) (v : value) (assoc : assoclist) : assoclist := - PositiveMap.add r v assoc. - -Definition merge_assoclist (nbassoc assoc : assoclist) : assoclist := - PositiveMap.fold add_assoclist nbassoc assoc. - -Definition empty_assoclist : assoclist := PositiveMap.empty value. - -Definition mi_step_commit (s : state) (m : list module_item) : res state := + end.*) + +Inductive mi_stepp : fext -> associations -> module_item -> associations -> Prop := +| mi_stepp_Valways : + forall f s0 st s1 c, + stmnt_runp f s0 st s1 -> + mi_stepp f s0 (Valways c st) s1 +| mi_stepp_Valways_ff : + forall f s0 st s1 c, + stmnt_runp f s0 st s1 -> + mi_stepp f s0 (Valways_ff c st) s1 +| mi_stepp_Valways_comb : + forall f s0 st s1 c, + stmnt_runp f s0 st s1 -> + mi_stepp f s0 (Valways_comb c st) s1 +| mi_stepp_Vdecl : + forall f s lhs rhs, + mi_stepp f s (Vdecl lhs rhs) s. +Hint Constructors mi_stepp : verilog. + +Inductive mis_stepp : fext -> associations -> list module_item -> associations -> Prop := +| mis_stepp_Cons : + forall f mi mis s0 s1 s2, + mi_stepp f s0 mi s1 -> + mis_stepp f s1 mis s2 -> + mis_stepp f s0 (mi :: mis) s2 +| mis_stepp_Nil : + forall f s, + mis_stepp f s nil s. +Hint Constructors mis_stepp : verilog. + +(*Definition mi_step_commit (s : state) (m : list module_item) : res state := match mi_step s m with - | OK (State assoc nbassoc f c) => - OK (State (merge_assoclist nbassoc assoc) empty_assoclist f c) + | OK (State m assoc nbassoc f c) => + OK (State m (merge_assocmap nbassoc assoc) empty_assocmap f c) | Error msg => Error msg + | _ => Error (msg "Verilog: Wrong state") end. -Fixpoint mi_run (f : fextclk) (assoc : assoclist) (m : list module_item) (n : nat) - {struct n} : res assoclist := +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_assoclist 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 | O => OK assoc - end. + end.*) -Definition module_run (n : nat) (m : module) : res assoclist := - let f := fun x => match x with - | S O => (add_assoclist (fst (mod_reset m)) (ZToValue 1 1) empty_assoclist) - | _ => (add_assoclist (fst (mod_reset m)) (ZToValue 1 0) empty_assoclist) - end in - mi_run f empty_assoclist (mod_body m) n. +(** Resets the module into a known state, so that it can be executed. This is +assumed to be the starting state of the module, and may have to be changed if +other arguments to the module are also to be supported. *) + +Definition initial_fextclk (m : module) : fextclk := + fun x => match x with + | S O => (AssocMap.set (fst (mod_reset m)) (ZToValue 1 1) empty_assocmap) + | _ => (AssocMap.set (fst (mod_reset m)) (ZToValue 1 0) empty_assocmap) + end. + +(*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. @@ -463,4 +584,42 @@ Proof. assumption. Qed. + *) + +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_assocmap) + m.(mod_body) + (mkassociations assoc1 nbassoc) -> + assoc2 = merge_assocmap nbassoc assoc1 -> + Some stvar' = assoc2!(fst m.(mod_state)) -> + 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_assocmap f cycle stvar) + (Finishstate result). +Hint Constructors step : verilog. + +(*Inductive initial_state (m: module): state -> Prop := +| initial_state_intro: + forall hmi tmi, + hmi::tmi = mod_body m -> + 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. *) + +Inductive final_state: state -> Integers.int -> Prop := + | final_state_intro: forall v, + final_state (Finishstate v) (valueToInt v). + +(** The small-step semantics for a module. *) + +Definition semantics (p: module) := + Semantics step (initial_state p) final_state (Genv.empty_genv unit unit nil). *) |