diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-05-27 19:02:23 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-05-27 19:02:47 +0100 |
| commit | f6cccc2eea3f0d8dea8f4f5a1ca8b86fe74c13c7 (patch) | |
| tree | 9bef7e806e407ad9c763771753c59cd8c4e2a652 /src/hls/GiblePargen.v | |
| parent | 0a44da6a7037d9eb270386eeef4f929177c4ec0d (diff) | |
| download | vericert-f6cccc2eea3f0d8dea8f4f5a1ca8b86fe74c13c7.tar.gz vericert-f6cccc2eea3f0d8dea8f4f5a1ca8b86fe74c13c7.zip | |
Fix code generation in partitioning and scheduling
Diffstat (limited to 'src/hls/GiblePargen.v')
| -rw-r--r-- | src/hls/GiblePargen.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v index 37273b4..0d4badd 100644 --- a/src/hls/GiblePargen.v +++ b/src/hls/GiblePargen.v @@ -243,8 +243,9 @@ Definition empty_trees (bb: SeqBB.t) (bbt: ParBB.t) : bool := end. Definition schedule_oracle (bb: SeqBB.t) (bbt: ParBB.t) : bool := - check (fst (abstract_sequence (empty, nil) bb)) - (fst (abstract_sequence (empty, nil) (concat (concat bbt)))) && + forallb (fun x => match x with ((_, _, f1), (_, _, f2)) => check f1 f2 end) + (combine (snd (abstract_sequence (empty, nil) bb)) + (snd (abstract_sequence (empty, nil) (concat (concat bbt))))) && empty_trees bb bbt. Definition check_scheduled_trees := beq2 schedule_oracle. |