659 commits

This branch

This branch

All branches

Author	SHA1	Message	Date
KrystalDelusion	93d8ef9663	Fixed bigtest ... Accidentally broke it in cc27d27 (this is why regular testing is important).	2022-08-02 10:12:33 +12: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
KrystalDelusion	b2d0368e26	Testing fifo things in CI ... Turns out the bigtest golden ref is failing a_count_diff, need to fix that before removing the default statement. Base example code is fine. New shell script to run default case and then nofullskip. Expects returncode=2 after running nofullskip.	2022-08-01 22:06:03 +12:00
KrystalDelusion	ed9b291d2b	Remove redundancies in certain logic checks ... A | A' === True, A | (A' & B) === A | B	2022-08-01 20:36:19 +12:00
KrystalDelusion	672a559b92	Merge branch 'YosysHQ:master' into fifo_example	2022-08-01 20:25:15 +12: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
KrystalDelusion	cc27d27c05	More literalincludes ... Tidying up of newstart.rst and fifo.sv to include as much code as possible by reference. Should reduce repetition and make it easier if changes occur in source.	2022-07-04 11:53:40 +12:00
KrystalDelusion	c9fbfa3684	Adding makefile for fifo	2022-07-04 10:32:55 +12: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
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