diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-07-07 17:31:03 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-07-07 17:31:03 +0100 |
commit | 40a95b24099f9d70af32b14a4c79429ba03007f2 (patch) | |
tree | 7d49cd7023850976e2736e7ad628ad694e5c9284 | |
parent | 5ca10a134176352b25a0b434d5508852c7314670 (diff) | |
parent | 8486b4c046914b1388b68fe906fe267108f84267 (diff) | |
download | vericert-kvx-40a95b24099f9d70af32b14a4c79429ba03007f2.tar.gz vericert-kvx-40a95b24099f9d70af32b14a4c79429ba03007f2.zip |
Merge branch 'develop' into dev-nadesh-provendev-nadesh-proven
-rw-r--r-- | src/Compiler.v | 2 | ||||
-rw-r--r-- | src/translation/HTLgen.v | 8 | ||||
-rw-r--r-- | src/translation/HTLgenproof.v | 1 | ||||
-rw-r--r-- | src/verilog/Verilog.v | 5 |
4 files changed, 8 insertions, 8 deletions
diff --git a/src/Compiler.v b/src/Compiler.v index 2ade983..8820f14 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -103,6 +103,7 @@ Definition transf_hls (p : Csyntax.program) : res Verilog.program := @@@ Cminorgen.transl_program @@@ Selection.sel_program @@@ RTLgen.transl_program + @@ print (print_RTL 0) @@@ transf_backend. Local Open Scope linking_scope. @@ -134,6 +135,7 @@ Proof. destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; simpl in T; try discriminate. destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; simpl in T; try discriminate. destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. + rewrite ! compose_print_identity in T. destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. unfold transf_backend in T. simpl in T. rewrite ! compose_print_identity in T. destruct (Inlining.transf_program p6) as [p7|e] eqn:P7; simpl in T; try discriminate. diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index db24a1d..1869a8f 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -271,8 +271,6 @@ Definition translate_comparison_imm (c : Integers.comparison) (args : list reg) Definition translate_comparisonu (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 Vltu r1 r2) | Integers.Cgt, r1::r2::nil => ret (bop Vgtu r1 r2) | Integers.Cle, r1::r2::nil => ret (bop Vleu r1 r2) @@ -283,8 +281,6 @@ Definition translate_comparisonu (c : Integers.comparison) (args : list reg) : m Definition translate_comparison_immu (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 Vltu r1 i) | Integers.Cgt, r1::nil => ret (boplit Vgtu r1 i) | Integers.Cle, r1::nil => ret (boplit Vleu r1 i) @@ -360,7 +356,9 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := (Vlit (intToValue n))))*) | Op.Oshru, r1::r2::nil => ret (bop Vshru r1 r2) | Op.Oshruimm n, r::nil => ret (boplit Vshru r n) - | Op.Ororimm n, r::nil => ret (boplit Vror r n) + | Op.Ororimm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Ororimm") + (*ret (Vbinop Vor (boplit Vshru r (Integers.Int.modu n (Integers.Int.repr 32))) + (boplit Vshl r (Integers.Int.sub (Integers.Int.repr 32) (Integers.Int.modu n (Integers.Int.repr 32)))))*) | Op.Oshldimm n, r::nil => ret (Vbinop Vor (boplit Vshl r n) (boplit Vshr r (Integers.Int.sub (Integers.Int.repr 32) n))) | Op.Ocmp c, _ => translate_condition c args | Op.Osel c AST.Tint, r1::r2::rl => diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 813a94b..943b76e 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -342,6 +342,7 @@ Section CORRECTNESS. Hypothesis TRANSL : match_prog prog tprog. + (* Lemma TRANSL' : *) (* Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq prog tprog. *) (* Proof. intros; apply match_prog_matches; assumption. Qed. *) diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 06e250a..6a1bece 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -143,8 +143,8 @@ Inductive binop : Type := | Vxor : binop (** xor (binary [^|]) *) | Vshl : binop (** shift left ([<<]) *) | Vshr : binop (** shift right ([>>>]) *) -| Vshru : binop (** shift right unsigned ([>>]) *) -| Vror : binop. (** shift right unsigned ([>>]) *) +| Vshru : binop. (** shift right unsigned ([>>]) *) +(*| Vror : binop (** shift right unsigned ([>>]) *)*) (** ** Unary Operators *) @@ -330,7 +330,6 @@ Definition binop_run (op : binop) (v1 v2 : value) : option value := | Vshl => Some (Int.shl v1 v2) | Vshr => Some (Int.shr v1 v2) | Vshru => Some (Int.shru v1 v2) - | Vror => Some (Int.ror v1 v2) end. Definition unop_run (op : unop) (v1 : value) : value := |