diff options
Diffstat (limited to 'src/verilog/Verilog.v')
| -rw-r--r-- | src/verilog/Verilog.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index ce7ddd9..e2b85b2 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -97,6 +97,7 @@ Inductive unop : Type := Inductive expr : Type := | Vlit : value -> expr | Vvar : reg -> expr +| Vvari : reg -> expr -> expr | Vinputvar : reg -> expr | Vbinop : binop -> expr -> expr -> expr | Vunop : unop -> expr -> expr @@ -138,6 +139,7 @@ done using combinational always block instead of continuous assignments. *) Inductive module_item : Type := | Vdecl : reg -> nat -> module_item +| Vdeclarr : reg -> nat -> nat -> module_item | Valways : edge -> stmnt -> module_item | Valways_ff : edge -> stmnt -> module_item | Valways_comb : edge -> stmnt -> module_item. @@ -314,6 +316,7 @@ Definition access_fext (f : fext) (r : reg) : res value := | State _ assoc _ _ _ => handle_def (ZToValue 32 0) assoc!r | _ => Error (msg "Verilog: Wrong state") end + | Vvari _ _ => Error (msg "Verilog: variable indexing not modelled") | Vinputvar r => access_fext s r | Vbinop op l r => let lv := expr_run s l in @@ -476,6 +479,7 @@ Hint Constructors stmnt_runp : verilog. | (Valways_ff _ st)::ls => run st ls | (Valways_comb _ st)::ls => run st ls | (Vdecl _ _)::ls => mi_step s ls + | (Vdeclarr _ _ _)::ls => mi_step s ls | nil => OK s end.*) |