diff options
author | James Pollard <james@pollard.dev> | 2020-05-25 18:20:23 +0100 |
---|---|---|
committer | James Pollard <james@pollard.dev> | 2020-05-25 18:20:23 +0100 |
commit | bbc5bd889c5d4520140406bd5dd4a397d0d2c975 (patch) | |
tree | 003498ce7a8ca80a808f784d0d3a6e03e32a24a8 /src/translation/Veriloggen.v | |
parent | 32e7c8282fa8ba15eeb79c7ce10c3ba5915fa532 (diff) | |
download | vericert-bbc5bd889c5d4520140406bd5dd4a397d0d2c975.tar.gz vericert-bbc5bd889c5d4520140406bd5dd4a397d0d2c975.zip |
Start work on array support
Try to add a verilog register to represent the stack.
Diffstat (limited to 'src/translation/Veriloggen.v')
-rw-r--r-- | src/translation/Veriloggen.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v index 6aa94df..0d846a5 100644 --- a/src/translation/Veriloggen.v +++ b/src/translation/Veriloggen.v @@ -551,6 +551,7 @@ Definition set_int_size (r: reg) : reg * nat := (r, 32%nat). Definition transf_module (f: function) : mon module := do fin <- decl_io 1%nat; do rtrn <- decl_io 32%nat; + do _ <- decl_fresh_reg ((Z.to_nat f.(fn_stacksize)) * 8%nat); do _ <- traverselist (transf_instr (fst fin) (fst rtrn)) (Maps.PTree.elements f.(fn_code)); do start <- decl_io 1%nat; do rst <- decl_io 1%nat; |