From 981b6238573548b696d0a4a50eb7605387245c0b Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 1 Apr 2020 19:24:29 +0100 Subject: Update compilation --- src/verilog/Verilog.v | 41 ++++++++++++++++++++++++++++++++++++----- 1 file changed, 36 insertions(+), 5 deletions(-) (limited to 'src/verilog/Verilog.v') diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index e91ca2d..212dbc0 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -39,9 +39,12 @@ Record value : Type := mkvalue { }. Definition posToValue (p : positive) : value := - let size := Z.to_nat (log_sup p) in + 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 (Word.ZToWord s z). + Definition intToValue (i : Integers.int) : value := mkvalue 32%nat (Word.ZToWord 32%nat (Integers.Int.unsigned i)). @@ -94,13 +97,41 @@ Inductive stmnt : Type := | Vcond : expr -> stmnt -> stmnt -> stmnt | Vcase : expr -> list (expr * stmnt) -> stmnt | Vblock : expr -> expr -> stmnt -| Vnonblock : expr -> expr -> stmnt -| Vdecl : reg -> nat -> expr -> stmnt. +| Vnonblock : expr -> expr -> stmnt. + +(** [edge] is not part of [stmnt] in this formalisation because is closer to the + semantics that are used. *) +Inductive edge : Type := +| Vposedge : reg -> edge +| Vnegedge : reg -> edge +| Valledge : edge +| Voredge : edge -> edge -> edge. + +Inductive module_item : Type := +| Vdecl : reg -> nat -> expr -> module_item +| Valways : edge -> stmnt -> module_item. + +(** [mod_start] If set, starts the computations in the module. *) +(** [mod_reset] If set, reset the state in the module. *) +(** [mod_clk] The clock that controls the computation in the module. *) +(** [mod_args] The arguments to the module. *) +(** [mod_finish] Bit that is set if the result is ready. *) +(** [mod_return] The return value that was computed. *) +(** [mod_body] The body of the module, including the state machine. *) +Record module : Type := mkmodule { + mod_start : reg; + mod_reset : reg; + mod_clk : reg; + mod_finish : reg; + mod_return : reg; + mod_args : list reg; + mod_body : list module_item; +}. +(** Convert a [positive] to an expression directly, setting it to the right + size. *) Definition posToLit (p : positive) : expr := Vlit (posToValue p). -Definition verilog : Type := list stmnt. - Coercion Vlit : value >-> expr. Coercion Vvar : reg >-> expr. -- cgit