diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-02-15 00:06:29 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-02-15 00:06:29 +0000 |
| commit | 171b326ade18ab77eb155a9d203f2f523708b29b (patch) | |
| tree | df9f02bc68c7dc539a67ac376ad7a5d4435c07c3 /src/hls/HTLgenspec.v | |
| parent | 5f1e7aa8fbc4a0e04d0b137410c13f3d8da4d987 (diff) | |
| download | vericert-171b326ade18ab77eb155a9d203f2f523708b29b.tar.gz vericert-171b326ade18ab77eb155a9d203f2f523708b29b.zip | |
Add beginning to scheduling division
Diffstat (limited to 'src/hls/HTLgenspec.v')
| -rw-r--r-- | src/hls/HTLgenspec.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 845b1d5..ae7917f 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -183,7 +183,7 @@ Inductive tr_module (f : RTL.function) : module -> Prop := data control f.(RTL.fn_entrypoint) - st stk stk_len fin rtrn start rst clk scldecls arrdecls wf) -> + st stk stk_len fin rtrn start rst clk nil scldecls arrdecls wf) -> (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> |