diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-04-02 14:54:14 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-04-02 14:54:20 +0100 |
commit | 8659e1b672a9b28a78c5b026312e7f3c0cb87c36 (patch) | |
tree | 7208310bcfa2cbae6dc8d244ee3693718df4a20b /src/verilog/Verilog.v | |
parent | 5398b08ec6d445f91ed74c8434150cfbf99cc373 (diff) | |
download | vericert-8659e1b672a9b28a78c5b026312e7f3c0cb87c36.tar.gz vericert-8659e1b672a9b28a78c5b026312e7f3c0cb87c36.zip |
Handle loops and conditionals correctly
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; }. |