diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2020-11-27 12:51:20 +0000 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2020-11-27 12:56:26 +0000 |
| commit | 130d11a3291e3bce761ecbaeb7185df4ea98009d (patch) | |
| tree | 0043544128f4409871433130df07ccb80458b74d /src/verilog/Verilog.v | |
| parent | 303a45374643f75698c61f062899973d2c297831 (diff) | |
| download | vericert-130d11a3291e3bce761ecbaeb7185df4ea98009d.tar.gz vericert-130d11a3291e3bce761ecbaeb7185df4ea98009d.zip | |
Revert changes relating to instance generation
Revert "Add todo for missing logic around instantiations"
This reverts commit 303a45374643f75698c61f062899973d2c297831.
Revert "Add wires and use them for output of instances"
This reverts commit a72f26319dabca414a2b576424b9f72afaca161c.
Revert "Separate HTL instantiations from Verilog ones"
This reverts commit 653c8729f4322f538aa7116c5e311c884b3c5047.
Revert "Translate instantiations from HTL to verilog"
This reverts commit 982e6c69a52e8ec4e677147004cc5472f8a80d6d.
Revert "Print instantiations in HTL output"
This reverts commit 9b87637d3e4d6a75dee1221b017e3ccf6632642e.
Revert "Add a field in HTL modules for instances"
This reverts commit d79dae026b150e9671e0aa7262f6aa2d1d302502.
Revert "Generate (invalid) module instantiations for calls"
This reverts commit dfaa3a9cbc07649feea3220693a8a854a32eafb6.
Diffstat (limited to 'src/verilog/Verilog.v')
| -rw-r--r-- | src/verilog/Verilog.v | 24 |
1 files changed, 10 insertions, 14 deletions
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 27522b4..3b0dd0a 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -39,7 +39,6 @@ Set Implicit Arguments. Definition reg : Type := positive. Definition node : Type := positive. -Definition ident : Type := positive. Definition szreg : Type := reg * nat. Record associations (A : Type) : Type := @@ -100,15 +99,7 @@ Definition block_reg (r : reg) (asr : reg_associations) (v : value) := Definition nonblock_reg (r : reg) (asr : reg_associations) (v : value) := mkassociations asr.(assoc_blocking) (AssocMap.set r v asr.(assoc_nonblocking)). -Inductive io : Type := -| Vinput : io -| Voutput : io -| Vinout : io. - -Inductive scl_decl : Type := -| VScalar (io: option Verilog.io) (sz : nat) -| VWire (sz : nat). - +Inductive scl_decl : Type := VScalar (sz : nat). Inductive arr_decl : Type := VArray (sz : nat) (ln : nat). (** * Verilog AST @@ -202,13 +193,18 @@ Inductive edge : Type := (** ** Module Items -Module items can either be declarations ([Vdecl]) or always blocks ([Valways]). *) +Module items can either be declarations ([Vdecl]) or always blocks ([Valways]). +The declarations are always register declarations as combinational logic can be +done using combinational always block instead of continuous assignments. *) + +Inductive io : Type := +| Vinput : io +| Voutput : io +| Vinout : io. Inductive declaration : Type := | Vdecl : option io -> reg -> nat -> declaration -| Vdeclarr : option io -> reg -> nat -> nat -> declaration -| Vdeclwire : reg -> nat -> declaration -| Vinstancedecl : ident -> ident -> list reg -> declaration. +| Vdeclarr : option io -> reg -> nat -> nat -> declaration. Inductive module_item : Type := | Vdeclaration : declaration -> module_item |