diff options
Diffstat (limited to 'src/verilog/Verilog.v')
-rw-r--r-- | src/verilog/Verilog.v | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 212dbc0..b9200b7 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -32,6 +32,7 @@ From compcert Require Integers. Import ListNotations. Definition reg : Type := positive. +Definition szreg : Type := reg * nat. Record value : Type := mkvalue { vsize : nat; @@ -108,7 +109,7 @@ Inductive edge : Type := | Voredge : edge -> edge -> edge. Inductive module_item : Type := -| Vdecl : reg -> nat -> expr -> module_item +| Vdecl : reg -> nat -> module_item | Valways : edge -> stmnt -> module_item. (** [mod_start] If set, starts the computations in the module. *) @@ -119,12 +120,12 @@ Inductive module_item : Type := (** [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_start : szreg; + mod_reset : szreg; + mod_clk : szreg; + mod_finish : szreg; + mod_return : szreg; + mod_args : list szreg; mod_body : list module_item; }. |