diff options
| author | James Pollard <james@pollard.dev> | 2020-05-26 19:10:14 +0100 |
|---|---|---|
| committer | James Pollard <james@pollard.dev> | 2020-05-26 19:10:14 +0100 |
| commit | 45842fdccf3f2fae7a14508fa939ba2a1cf0d3ce (patch) | |
| tree | 3132d12f55df2ed8daf6d95f1a6ec980f7c8dad0 /src/verilog | |
| parent | 1baa474a2312a930187cd2d071dc0651451327d1 (diff) | |
| download | vericert-45842fdccf3f2fae7a14508fa939ba2a1cf0d3ce.tar.gz vericert-45842fdccf3f2fae7a14508fa939ba2a1cf0d3ce.zip | |
(Tentatively) working stack array/memory support.
Diffstat (limited to 'src/verilog')
| -rw-r--r-- | src/verilog/PrintVerilog.ml | 8 | ||||
| -rw-r--r-- | src/verilog/Verilog.v | 4 |
2 files changed, 12 insertions, 0 deletions
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml index 29c4f5a..bdd8581 100644 --- a/src/verilog/PrintVerilog.ml +++ b/src/verilog/PrintVerilog.ml @@ -70,6 +70,7 @@ let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (uvalueToZ l)) let rec pprint_expr = function | Vlit l -> literal l | Vvar s -> register s + | Vvari (s, i) -> concat [register s; "["; pprint_expr i; "]"] | Vinputvar s -> register s | Vunop (u, e) -> concat ["("; unop u; pprint_expr e; ")"] | Vbinop (op, a, b) -> concat ["("; pprint_binop (pprint_expr a) (pprint_expr b) op; ")"] @@ -111,9 +112,16 @@ let declare i t = concat [ indent i; t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] "; register r; ";\n" ] +let declarearr i t = + function (r, sz, ln) -> + concat [ indent i; t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] "; + register r; + " ["; sprintf "%d" (Nat.to_int ln - 1); ":0];\n" ] + (* TODO Fix always blocks, as they currently always print the same. *) let pprint_module_item i = function | Vdecl (r, sz) -> declare i "reg" (r, sz) + | Vdeclarr (r, sz, ln) -> declarearr i "reg" (r, sz, ln) | Valways (e, s) -> concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s] | Valways_ff (e, s) -> diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 4713c36..dfb6255 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -95,6 +95,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 @@ -136,6 +137,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. @@ -280,6 +282,7 @@ Fixpoint expr_run (s : state) (e : expr) | Vvar r => match s with | State assoc _ _ _ => handle_def (ZToValue 32 0) assoc!r 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 @@ -383,6 +386,7 @@ Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state := | (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. |