427 commits

This branch

This branch

All branches

Author	SHA1	Message	Date
Jannis Harder	8d2fa9b304	Merge pull request #207 from jix/fix_smt_shift ... Regression test for YosysHQ/yosys#3433	2022-08-03 17:04:10 +02:00
Jannis Harder	523b7a252e	Regression test for YosysHQ/yosys#3433	2022-08-03 16:08:19 +02:00
Aki Van Ness	59dc27ed73	sby: core: config: cleaned up the error messages to make them less opaque	2022-08-01 10:16:05 -04:00
Jannis Harder	c200690160	Merge pull request #201 from jix/autotune_example_in_docs ... Autotune example in docs	2022-08-01 12:13:38 +02:00
Jannis Harder	4ec278e6ec	Autotune example in docs	2022-07-26 16:35:57 +02:00
Jannis Harder	0395b8a439	Merge pull request #200 from jix/autotune_example ... example for autotune	2022-07-26 16:21:16 +02:00
Jannis Harder	9293e66092	example for autotune	2022-07-26 16:06:02 +02:00
Jannis Harder	a498e1e9a1	Merge pull request #199 from nakengelhardt/add_cvc5_tool_rule ... add cvc5 executable to required tool mapping	2022-07-25 17:27:43 +02:00
N. Engelhardt	1cf206fc1c	add cvc5 executable to required tool mapping	2022-07-25 17:01:17 +02:00
N. Engelhardt	3ff2c9affc	avoid erroring out when coarse-grain logic loops can be resolved by mapping to fine grain operators	2022-07-25 16:22:32 +02:00
Jannis Harder	b4dd638311	Merge pull request #197 from YosysHQ/Autotune-grammar-check ... Autotune grammar/spelling check	2022-07-25 09:53:39 +02:00
Jannis Harder	07d19b202b	Merge pull request #195 from jix/sbyproc-truncated-output ... Fix a race-condition SbyProc that could truncate output	2022-07-13 17:30:36 +02:00
Jannis Harder	b8a1bdd40a	Merge pull request #193 from jix/abc_pdr_v ... abc pdr: Enable log output by default	2022-07-13 16:07:04 +02:00
Jannis Harder	5d3f784beb	Fix a race-condition SbyProc that could truncate output ... Present for a long time, but was not easy to hit. Some of my work in progress changes made this much more likely and running the complete test suite in parallel had a good chance of reproducing this for at least one of the tests.	2022-07-13 16:01:49 +02:00
KrystalDelusion	ca3429e328	Autotune grammar/spelling check	2022-07-11 21:21:31 +12:00
matt venn	4ab610ce87	Update autotune.rst	2022-07-11 11:10:45 +02:00
Jannis Harder	cea760bd52	Merge pull request #194 from jix/autotune_rst_fixes ... docs: Don't use linebreaks within inline code spans.	2022-07-08 14:46:41 +02:00
Jannis Harder	bc2bb5c863	docs: Don't use linebreaks within inline code spans.	2022-07-08 14:31:57 +02:00
Jannis Harder	92e7eb2e32	abc pdr: Enable log output by default ... This makes it consistent with the other abc solvers and shows whether abc pdr is making progress.	2022-07-08 12:36:44 +02:00
Jannis Harder	de43a4c936	Merge pull request #191 from jix/early-readconfig ... Read config before creating a workdir	2022-07-06 12:05:13 +02:00
Jannis Harder	f42ed5eb10	Merge pull request #192 from jix/win_retcode ... Make SbyProc hide Windows differences in retcode handling	2022-07-06 12:05:03 +02:00
Jannis Harder	b3b315a473	Make SbyProc hide Windows differences in retcode handling ... Without this, we don't properly detect missing solver binaries and do not properly handle the return status of the pono solver.	2022-07-06 11:22:59 +02:00
Jannis Harder	566edad13c	Read config before creating a workdir ... When using a task name not defined in the config, this now produces an error before creating an unnecessary workdir for that non-existing task.	2022-07-05 17:20:55 +02:00
Jannis Harder	ff1f87e169	Merge pull request #190 from jix/windows_fixes ... tests: Windows fixes	2022-07-05 16:09:54 +02:00
Jannis Harder	ea7fc7dc2c	tests: Windows fixes ... Make tests runnable on Windows, as long as a unix like environment as e.g. provided by MSYS2 is available.	2022-07-05 15:34:27 +02:00
Jannis Harder	ab98938faa	Merge pull request #187 from jix/const_clocks ... Test uninitialized FFs with constant clocks and fix btor script for this	2022-07-04 17:47:16 +02:00
Jannis Harder	ff802086b4	test uninited FFs with const clks and fix btor script for this	2022-07-04 14:03:56 +02:00
Jannis Harder	9016031f32	Merge pull request #186 from jix/ff_xinit_opt ... tests: Test for invalid x-value FF init optimizations	2022-07-04 14:03:06 +02:00
Jannis Harder	e01ac8b848	tests: Test for invalid x-value FF init optimizations	2022-07-04 13:33:39 +02:00
Jannis Harder	e3123283ea	Merge pull request #170 from programmerjake/add-simcheck-option ... switch to using hierarchy -smtcheck for smtlib2 solvers, allowing smtlib2_module modules	2022-07-03 11:47:22 +02:00
Jannis Harder	4d858a1b9c	Merge pull request #189 from jix/autotune_docs ... docs: add missing autotune.rst	2022-06-30 17:53:22 +02:00
Jannis Harder	685457915a	docs: add missing autotune.rst	2022-06-30 17:50:05 +02:00
Jannis Harder	abe0086ec1	Merge pull request #158 from jix/autotune ... Autotune: Automatic engine selection	2022-06-29 16:48:06 +02:00
Jannis Harder	d038a7d35c	autotune: Initial documentation	2022-06-27 15:58:42 +02:00
Jannis Harder	48a02f9cc4	Test autotune	2022-06-27 15:58:42 +02:00
Jannis Harder	b4458d43d7	Automatic engine selection	2022-06-27 15:58:42 +02:00
Jannis Harder	5014d74023	sby_design: Extract total memory size and forall usage	2022-06-24 13:50:26 +02:00
Jannis Harder	157bb156c0	Merge pull request #185 from georgerennie/prefix_empty_taskname ... Use default prefix directory when no task is specified	2022-06-24 12:40:09 +02:00
Jannis Harder	0d90e29ef3	Merge pull request #183 from jix/engine-option-docs ... Reflect recent engine updates in the reference docs	2022-06-23 16:39:32 +02:00
Jannis Harder	f66436ce48	Merge pull request #184 from jix/smtbmc-keepgoing-induction-trace-fix ... smtbmc: Fix induction trace filename with --keep-going for the basecase	2022-06-23 13:37:38 +02:00
Jannis Harder	3dcf7766ea	smtbmc: Fix induction trace filename with --keep-going for the basecase ... --keep-going only applies to the basecase and induction runs without that option, so the trace filename for induction should have no placeholder.	2022-06-23 13:15:58 +02:00
Jacob Lifshay	db740839b7	switch to using hierarchy -smtcheck for smtlib2 solvers, allowing smtlib2_module modules. ... Fixes: #168 Depends on: https://github.com/YosysHQ/yosys/pull/3391	2022-06-22 21:17:29 -07:00
Jannis Harder	d8ebd1eb9d	Reflect recent engine updates in the reference docs	2022-06-20 15:23:59 +02:00
George Rennie	0308142fa4	Use default prefix directory when no task is specified	2022-06-19 00:49:12 +01:00
Jannis Harder	fb5705b5bd	Merge pull request #182 from jix/taskloop ... Decouple taskloop from task	2022-06-15 16:41:39 +02:00
Jannis Harder	0fe8c223cf	Decouple taskloop from task	2022-06-15 16:28:09 +02:00
Jannis Harder	c944a9c99c	Merge pull request #181 from jix/monotonic ... Use monotonic clock for timeouts	2022-06-15 16:27:23 +02:00
Jannis Harder	d1c04f79d6	Use monotonic clock for timeouts	2022-06-15 14:11:25 +02:00
Jannis Harder	0df73ea666	Merge pull request #180 from jix/sby-fewer-asserts ... Don't use python asserts to handle unexpected solver output	2022-06-15 14:08:15 +02:00
Jannis Harder	d0c59a3155	Don't use python asserts to handle unexpected solver output	2022-06-15 13:25:21 +02:00