425 commits

This branch

This branch

All branches

Author	SHA1	Message	Date
KrystalDelusion	c9fbfa3684	Adding makefile for fifo	2022-07-04 10:32:55 +12:00
KrystalDelusion	a5f67ed904	Merge branch 'master' into fifo_example	2022-07-01 11:46:02 +12:00
KrystalDelusion	de5b9b7821	Changed phrasing to avoid confusion on witnesses	2022-07-01 11:29:33 +12:00
KrystalDelusion	aab2c3c2e0	New exercise section ... Worked exercise using the MAX_DATA parameter, highlighting its incompleteness. Includes completed examples in /golden subdirectory. Also some formatting changes for spacing and extra links.	2022-07-01 11:19:01 +12:00
KrystalDelusion	7ba67ef260	Removing unnecessary underflow assertions	2022-07-01 11:15:47 +12: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
KrystalDelusion	907db48ac9	Updating from feedback ... Primarily addressing Nak's comments on the PR first. Of note is the change from separate files to a single file. Changed to boolector engine and bmc by default. Updated install instructions to move z3 to optional and boolector to recommended. Literal code includes use :lines: option.	2022-06-30 12:06:12 +12: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
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
Jannis Harder	d7686ca698	Merge pull request #164 from jix/suggest_f_flag ... Suggest -f when the workdir already exists	2022-06-10 15:14:01 +02:00
KrystalDelusion	069197aeaa	Add section on sby to newstart ... List tasks and run through failing noskip example. Includes pictures (both fail and pass) plus .gtkw file for setting up.	2022-06-09 14:29:21 +12:00
KrystalDelusion	41e427640a	Adding noskip task ... Demonstrate failing model check by disabling rskip and wskip.	2022-06-09 14:26:17 +12:00
Jannis Harder	d0da57f54f	Test that cvc4 and cvc5 can be used	2022-06-08 13:33:12 +02:00
Jannis Harder	4a9511b80b	Merge pull request #171 from jix/make-remove-unused-tool-list ... tests: Remove unused tool list in test Makefile	2022-06-08 11:43:43 +02:00
Jannis Harder	675dc03dfe	tests: Remove unused tool list in test Makefile ... The checks for available tools moved to a python script, so need need to have a copy of the tool list in the Makefile.	2022-06-08 11:32:35 +02:00
Jannis Harder	534ac21742	Merge pull request #169 from jix/yices-forall ... Test designs using $allconst	2022-06-08 09:43:47 +02:00
Jannis Harder	2b1a588589	Merge pull request #163 from jix/make_improvements ... Test makefile improvements	2022-06-07 14:50:59 +02:00
Jannis Harder	34d6adf098	tests: Move required tool checks from rule generation to execution ... This avoids regenerating the test makefile rules when the set of installed tools changes and is a bit simpler overall.	2022-06-07 14:29:25 +02:00
KrystalDelusion	a808a0738c	Merge branch 'master' into fifo_example ... Abbreviates additional btor instructions.	2022-06-07 12:00:10 +12:00