Вернуться к статье
SAT-генерация тестовых векторов на elaborate-представлении RTL без этапа логического синтеза: экспериментальное обоснование маршрута и перспективы ранней характеризации блоков
AIG structure and CNF size
Benchmark | A: I/O/R/AND | A: depth | B: I/O/R/AND | B: depth | A: CNF v/c | B: CNF v/c |
bench_xor_a | 2/1/0/3 | 2 | 2/1/0/3 | 2 | 6/9 | 6/9 |
bench_xor_b | 2/1/0/3 | 2 | 2/1/0/3 | 2 | 6/9 | 6/9 |
bench_alu | 19/9/0/221 | 19 | 19/9/0/218 | 20 | 241/663 | 238/654 |
bench_shifter | 22/21/0/534 | 12 | 22/21/0/549 | 12 | 557/1602 | 572/1647 |
bench_redundant | 3/1/0/5 | 3 | 3/1/0/8 | 4 | 9/15 | 12/24 |
bench_counter | 11/10/18/89 | 12 | 11/10/18/89 | 12 | 119/267 | 119/267 |