From 34ea564d72230931b879f4a9a26d62c5d6573464 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 31 Mar 2020 15:32:00 +0100 Subject: Add more operators and print them --- src/translation/Veriloggen.v | 106 ++++++++++++++++++++++++++++--------------- src/verilog/PrintVerilog.ml | 6 ++- src/verilog/Verilog.v | 13 ++++-- 3 files changed, 84 insertions(+), 41 deletions(-) (limited to 'src') diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v index 426a7e6..c400617 100644 --- a/src/translation/Veriloggen.v +++ b/src/translation/Veriloggen.v @@ -20,7 +20,7 @@ From Coq Require Import FSets.FMapPositive. From coqup Require Import HTL Verilog Coquplib. -From compcert Require Errors Op AST. +From compcert Require Errors Op AST Integers. Definition node : Type := positive. Definition reg : Type := positive. @@ -112,38 +112,66 @@ End PTree. Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e. +Definition bop (op : binop) (r1 r2 : reg) : option expr := + Some (Vbinop op (Vvar r1) (Vvar r2)). + +Definition boplit (op : binop) (r : reg) (l : Integers.int) : option expr := + Some (Vbinop op (Vvar r) (Vlit (intToValue l))). + +Definition translate_comparison (c : Integers.comparison) (args : list reg) : option expr := + match c, args with + | Integers.Ceq, r1::r2::nil => bop Veq r1 r2 + | Integers.Cne, r1::r2::nil => bop Vne r1 r2 + | Integers.Clt, r1::r2::nil => bop Vlt r1 r2 + | Integers.Cgt, r1::r2::nil => bop Vgt r1 r2 + | Integers.Cle, r1::r2::nil => bop Vle r1 r2 + | Integers.Cge, r1::r2::nil => bop Vge r1 r2 + | _, _ => None + end. + +Definition translate_condition (c : Op.condition) (args : list reg) : option expr := + match c, args with + | Op.Ccomp c, _ => translate_comparison c args + | Op.Ccompu c, _ => None + | Op.Ccompimm c i, _ => None + | Op.Ccompuimm c i, _ => None + | Op.Cmaskzero n, _ => None + | Op.Cmasknotzero n, _ => None + | _, _ => None + end. + (** Translate an instruction to a statement. *) -Definition translate_instr (op : Op.operation) (args : list reg) (dst : reg) : option stmnt := - let assign := nonblock dst in +Definition translate_instr (op : Op.operation) (args : list reg) : option expr := match op, args with - | Op.Omove, v::nil => Some (assign (Vvar v)) - | Op.Ointconst n, _ => Some (assign (Vlit (intToValue n))) - | Op.Oneg, _ => None - | Op.Osub, _ => None - | Op.Omul, _ => None - | Op.Omulimm n, _ => None + | Op.Omove, r::nil => Some (Vvar r) + | Op.Ointconst n, _ => Some (Vlit (intToValue n)) + | Op.Oneg, r::nil => Some (Vunop Vneg (Vvar r)) + | Op.Osub, r1::r2::nil => bop Vsub r1 r2 + | Op.Omul, r1::r2::nil => bop Vmul r1 r2 + | Op.Omulimm n, r::nil => boplit Vmul r n | Op.Omulhs, _ => None | Op.Omulhu, _ => None - | Op.Odiv, _ => None - | Op.Odivu, _ => None - | Op.Omod, _ => None - | Op.Omodu, _ => None - | Op.Oand, _ => None - | Op.Oandimm n, _ => None - | Op.Oor, _ => None - | Op.Oorimm n, _ => None - | Op.Oxor, _ => None - | Op.Oxorimm n, _ => None - | Op.Onot, _ => None - | Op.Oshl, _ => None - | Op.Oshlimm n, _ => None - | Op.Oshr, _ => None - | Op.Oshrimm n, _ => None - | Op.Oshrximm n, _ => None - | Op.Oshru, _ => None - | Op.Oshruimm n, _ => None - | Op.Ororimm n, _ => None - | Op.Oshldimm n, _ => None + | Op.Odiv, r1::r2::nil => bop Vdiv r1 r2 + | Op.Odivu, r1::r2::nil => bop Vdivu r1 r2 + | Op.Omod, r1::r2::nil => bop Vmod r1 r2 + | Op.Omodu, r1::r2::nil => bop Vmodu r1 r2 + | Op.Oand, r1::r2::nil => bop Vand r1 r2 + | Op.Oandimm n, r::nil => boplit Vand r n + | Op.Oor, r1::r2::nil => bop Vor r1 r2 + | Op.Oorimm n, r::nil => boplit Vor r n + | Op.Oxor, r1::r2::nil => bop Vxor r1 r2 + | Op.Oxorimm n, r::nil => boplit Vxor r n + | Op.Onot, r::nil => Some (Vunop Vnot (Vvar r)) + | Op.Oshl, r1::r2::nil => bop Vshl r1 r2 + | Op.Oshlimm n, r::nil => boplit Vshl r n + | Op.Oshr, r1::r2::nil => bop Vshr r1 r2 + | Op.Oshrimm n, r::nil => boplit Vshr r n + | Op.Oshrximm n, r::nil => None + | Op.Oshru, r1::r2::nil => None + | Op.Oshruimm n, r::nil => None + | Op.Ororimm n, r::nil => None + | Op.Oshldimm n, r::nil => None + | Op.Ocmp c, _ => translate_condition c args | _, _ => None end. @@ -163,17 +191,21 @@ Definition transf_instr (n : node) (i : instruction) (s : state) : mon node := | Hnop n' => add_instr n n' s Vskip | Hnonblock op args dst n' => - match (translate_instr op args dst) with - | Some instr => add_instr n n' s instr + match translate_instr op args with + | Some instr => add_instr n n' s (nonblock dst instr) | _ => Error (Errors.msg "Instruction is not implemented.") end - | Hload _ _ _ _ _ => Error (Errors.msg "Load not implemented.") - | Hstore _ _ _ _ _ => Error (Errors.msg "Store not implemented.") - | Hinst _ _ _ _ => Error (Errors.msg "Call not implemented.") - | Htailcall _ _ _ => Error (Errors.msg "Tailcall not implemented.") - | Hcond _ _ _ _ => Error (Errors.msg "Cond not implemented.") + | Hload _ _ _ _ _ => Error (Errors.msg "Loads are not implemented.") + | Hstore _ _ _ _ _ => Error (Errors.msg "Stores are not implemented.") + | Hinst _ _ _ _ => Error (Errors.msg "Calls are not implemented.") + | Htailcall _ _ _ => Error (Errors.msg "Tailcalls are not implemented.") + | Hcond cond args n1 n2 => Error (Errors.msg "Condition not implemented.") | Hjumptable _ _ => Error (Errors.msg "Jumptable not implemented.") - | Hfinish _ => OK n s + | Hfinish r => + match r with + | Some x => OK n s + | None => OK n s + end end. Definition make_stm_cases (s : positive * stmnt) : expr * stmnt := diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml index 016a626..04a35de 100644 --- a/src/verilog/PrintVerilog.ml +++ b/src/verilog/PrintVerilog.ml @@ -49,6 +49,10 @@ let pprint_binop = function | Vshl -> " << " | Vshr -> " >> " +let unop = function + | Vneg -> " ~ " + | Vnot -> " ! " + let register a = P.to_int a let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (valueToZ l)) @@ -56,7 +60,7 @@ let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (valueToZ l)) let rec pprint_expr = function | Vlit l -> literal l | Vvar s -> sprintf "reg_%d" (register s) - | Vunop e -> concat ["(~"; pprint_expr e; ")"] + | Vunop (u, e) -> concat ["("; unop u; pprint_expr e; ")"] | Vbinop (op, a, b) -> concat ["("; pprint_expr a; pprint_binop op; pprint_expr b; ")"] | Vternary (c, t, f) -> concat ["("; pprint_expr c; " ? "; pprint_expr t; " : "; pprint_expr f; ")"] diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 09eb914..50a6809 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -54,12 +54,18 @@ Inductive binop : Type := | Vadd : binop (** addition (binary [+]) *) | Vsub : binop (** subtraction (binary [-]) *) | Vmul : binop (** multiplication (binary [*]) *) -| Vdiv : binop (** multiplication (binary [*]) *) -| Vmod : binop (** division ([/]) *) +| Vdiv : binop (** division (binary [/]) *) +| Vdivu : binop (** division unsigned (binary [/]) *) +| Vmod : binop (** remainder ([%]) *) +| Vmodu : binop (** remainder unsigned ([/]) *) | Vlt : binop (** less than ([<]) *) +| Vltu : binop (** less than unsigned ([<]) *) | Vgt : binop (** greater than ([>]) *) +| Vgtu : binop (** greater than unsigned ([>]) *) | Vle : binop (** less than or equal ([<=]) *) +| Vleu : binop (** less than or equal unsigned ([<=]) *) | Vge : binop (** greater than or equal ([>=]) *) +| Vgeu : binop (** greater than or equal unsigned ([>=]) *) | Veq : binop (** equal to ([==]) *) | Vne : binop (** not equal to ([!=]) *) | Vand : binop (** and (binary [&]) *) @@ -69,7 +75,8 @@ Inductive binop : Type := | Vshr : binop. (** shift left ([<<]) *) Inductive unop : Type := -| Vneg : unop. (** negation ([~]) *) +| Vneg (** negation ([~]) *) +| Vnot. (** not operation [!] *) Inductive expr : Type := | Vlit : value -> expr -- cgit