599 commits

This branch

This branch

All branches

Author	SHA1	Message	Date
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
KrystalDelusion	66ef51d846	Verification properties in doc	2022-06-07 11:50:26 +12:00
KrystalDelusion	fef6d3a8a6	Adding USE_VERIFIC flag ... Adding variations in .sby file where tabby uses verific and oss doesn't.	2022-06-07 11:49:25 +12:00
KrystalDelusion	aed5a33bef	Add init check ... Prevent rst_n from going low once it has gone high.	2022-06-07 10:22:04 +12:00
Jannis Harder	80eacf34ca	Don't fail tests when xmlschema is missing	2022-06-03 17:22:45 +02:00
Jannis Harder	b4c110815c	Test designs using $allconst	2022-06-03 16:55:06 +02:00
Jannis Harder	d398a3c2df	tests: Fail on CI when any required tool is missing	2022-06-02 16:38:21 +02:00
Jannis Harder	00efdecb4b	tests: Check for btorsim --vcd	2022-06-02 16:38:21 +02:00
N. Engelhardt	41cd8e5b5e	update install instructions for btorsim	2022-06-01 16:51:28 +02:00
KrystalDelusion	f5257011f6	Specifying z3 to support minimum required install	2022-05-31 11:31:20 +12:00
KrystalDelusion	b18f22cf43	Removing install details for optional engines	2022-05-31 11:18:05 +12:00
Jannis Harder	8e87b0f7f4	Suggest -f when the workdir already exists	2022-05-30 16:18:37 +02:00
Jannis Harder	206562e5de	Check for the tabby/oss cad suite before running make ci checks	2022-05-30 15:52:30 +02:00
Jannis Harder	dc22d97362	Better checking of available solvers ... Check for required auxiliary tools and always regenerate the make rules when the set of available tools changes.	2022-05-30 15:02:26 +02:00
Jannis Harder	939e000036	Makefile: Rename run_tests to test, update help, use .PHONY	2022-05-30 15:02:26 +02:00
Jannis Harder	de00dc71db	Merge pull request #161 from programmerjake/add-div-mod-floor-tests ... add test for yosys's $divfloor and $modfloor cells	2022-05-26 12:00:05 +02:00
Jacob Lifshay	a87d21a802	add depth 1	2022-05-25 03:35:21 -07:00
Jacob Lifshay	3f32deb8c9	add test for yosys's $divfloor and $modfloor cells ... Depends on: https://github.com/YosysHQ/yosys/pull/3335	2022-05-24 17:51:48 -07:00
N. Engelhardt	ad2c33dd37	docs: add instructions for newer btorsim version required	2022-05-24 11:39:10 +02:00
Jannis Harder	d10e472edf	Merge pull request #159 from jix/fix-dpmem-example ... examples: Fix use of SVA value change expressions	2022-05-11 11:23:57 +02:00
Jannis Harder	fedfae0e9c	examples: Fix use of SVA value change expressions ... The $stable value change expression cannot be true for a non-x signal in the initial state. This is now correctly handled by the verific import, so the dpmem example needs to start assuming `$stable` only after leaving the initial state.	2022-05-11 10:38:54 +02:00
KrystalDelusion	fc9ff3d733	Initial FIFO description	2022-05-10 12:08:49 +12:00
KrystalDelusion	21dfd35516	Adding new Getting started guide	2022-05-10 11:41:15 +12:00
KrystalDelusion	7ec35dc425	Adding (small) intro to installation guide ... Also a cross reference link.	2022-05-10 11:41:01 +12:00
KrystalDelusion	ee15ebd0f1	Title case for license.rst	2022-05-10 11:40:17 +12:00
KrystalDelusion	7468e7655d	Alignment fixing	2022-05-10 11:03:40 +12:00
KrystalDelusion	12b854b554	Headings for optional/required installs	2022-05-04 10:50:38 +12:00