462 commits

This branch

This branch

All branches

Author	SHA1	Message	Date
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
Jannis Harder	e99884e319	SbyProc: New error_callback instead of exit_callback for failing procs	2022-06-15 13:25:21 +02:00
Jannis Harder	f131fe5b8f	Merge pull request #179 from jix/btor-option-handling ... btor pono: improve option handling	2022-06-15 13:24:36 +02:00
Jannis Harder	141ffd34a5	btor pono: improve option handling ... Fail on the unsupported skip option and pass solver args to pono.	2022-06-15 11:35:22 +02:00
Jannis Harder	98b0713597	Merge pull request #178 from jix/aiger-aigbmc-fixes ... aiger: check supported modes and aigbmc fixes	2022-06-14 17:52:33 +02:00
Jannis Harder	05d963b0df	aiger: check supported modes and aigbmc fixes	2022-06-14 17:41:06 +02:00
Jannis Harder	1e1402474a	Merge pull request #177 from mattvenn/tristate-example ... Tristate example	2022-06-14 15:54:09 +02:00
Matt Venn	b88d7a13fb	add makefile for test	2022-06-14 15:35:22 +02:00
Matt Venn	687ee0f011	remove unused module port	2022-06-14 15:31:42 +02:00
Matt Venn	7efabe828a	expect fail	2022-06-14 15:31:42 +02:00
Matt Venn	b42b6445b8	tristate example	2022-06-14 15:31:42 +02:00
Jannis Harder	a200043709	Merge pull request #172 from jix/smtbmc-unroll-noincr-traces-fix ... Regression test for smtbmc --unroll --noincr	2022-06-13 14:05:37 +02:00
Jannis Harder	c50bd781ab	Merge pull request #175 from jix/more-test-improvements ... Use the test Makefile for all examples	2022-06-13 13:59:31 +02:00
Jannis Harder	499371fd39	Use the test Makefile for all examples ... * Rename and move sbysrc/demo[123].sby to docs/examples/demos * Make them use multiple tasks for multiple engines * Scan docs/examples for sby files for make test * `make ci` is now `NOSKIP` by default * Skip scripts using `verific` w/o yosys verific support * This does not fail even with NOSKIP set	2022-06-13 13:42:58 +02:00
Jannis Harder	4ef02d2c5c	Regression test for smtbmc --unroll --noincr	2022-06-13 13:36:42 +02:00
Jannis Harder	1d21513a47	Merge pull request #173 from jix/test-cvc ... Test that cvc4 and cvc5 can be used	2022-06-10 15:24:49 +02:00