322 commits

This branch

This branch

All branches

Author	SHA1	Message	Date
N. Engelhardt	adacad7908	Merge pull request #148 from nakengelhardt/docs_updates ... documentation updates	2022-03-28 16:34:00 +02:00
N. Engelhardt	53abf14514	Merge pull request #145 from nakengelhardt/fix_junit_tracefile ... junit: handle multiple asserts failing with the same trace	2022-03-28 16:32:54 +02:00
N. Engelhardt	3d8f56b89a	Merge pull request #142 from nakengelhardt/fix_backslash_smt2 ... translate backslashes in cell names the same way as smt2 backend does	2022-03-28 16:32:10 +02:00
Miodrag Milanović	7a4a8e6bf6	Merge pull request #146 from jix/aim_vs_smt2_nonzero_start_offset ... Test and fix signals with nonzero start offsets in aim files with smtbmc	2022-03-26 08:20:57 +01:00
N. Engelhardt	3834fe7622	document btor engine, add overview of mode/engine/solver combinations, remove unimplemented modes	2022-03-25 18:01:09 +01:00
Jannis Harder	a434252ca1	Test signals with nonzero start offsets in aim files with smtbmc	2022-03-25 15:18:45 +01:00
Jannis Harder	079df4d95f	Use -no-startoffset, avoiding index mismatch between aiger and smt2	2022-03-25 11:41:08 +01:00
N. Engelhardt	c7e4785a8a	junit: handle multiple asserts failing with the same trace	2022-03-22 16:16:02 +01:00
N. Engelhardt	5dc7fc9a4d	translate backslashes in cell names the same way as smt2 backend does	2022-03-22 11:14:48 +01:00
Claire Xen	fa5d5ad831	Merge pull request #120 from ythoma/patch-1 ... Update install.rst	2022-03-15 16:33:46 +01:00
N. Engelhardt	b14270bedb	Merge pull request #139 from nakengelhardt/housekeeping ... housekeeping	2022-03-15 16:06:52 +01:00
N. Engelhardt	2441940653	ci housekeeping	2022-03-15 15:12:59 +01:00
N. Engelhardt	419ef76f82	Merge pull request #133 from nakengelhardt/sby_junit ... improve SBY JUnit report	2022-03-07 16:25:47 +01:00
N. Engelhardt	8a81b61321	fix ci	2022-03-07 08:34:01 +01:00
N. Engelhardt	7142f790e4	add testcase for overall run result	2022-02-24 22:44:11 +01:00
N. Engelhardt	89ed843ff1	validate junit files (with extra attributes added to schema)	2022-02-22 16:16:37 +01:00
N. Engelhardt	7ee357fcc8	fix induction	2022-02-07 22:01:52 +01:00
N. Engelhardt	7d3545dc86	fix junit error/failure/skipped count	2022-02-07 19:20:29 +01:00
N. Engelhardt	53eb25fcae	handle unreached cover properties	2022-02-07 15:29:36 +01:00
N. Engelhardt	5abaccab69	refactor junit print into own function	2022-02-07 12:29:27 +01:00
N. Engelhardt	9168b0163b	handle status of cover properties	2022-02-06 09:15:44 +01:00
N. Engelhardt	d7e7f2c530	refactor model to have single base	2022-01-31 12:35:56 +01:00
N. Engelhardt	1cf27e7c31	parse solver location output for assert failures (cover not functional yet)	2022-01-27 13:41:07 +01:00
N. Engelhardt	a9d1972c47	add fallback if solver can't tell which property fails	2022-01-21 15:18:53 +01:00
N. Engelhardt	7f3c4137c1	create json export and read in properties	2022-01-19 19:34:11 +01:00
N. Engelhardt	6ec2df34e3	WIP change junit print to conform to schema; needs additional data, currently printing dummy info ... Signed-off-by: N. Engelhardt <nak@yosyshq.com>	2022-01-13 13:45:54 +01:00
N. Engelhardt	cdf5650c12	add JUnit schema and validator ... Signed-off-by: N. Engelhardt <nak@yosyshq.com>	2022-01-13 13:43:38 +01:00
Miodrag Milanović	02a5b71982	Merge pull request #138 from YosysHQ/mmicko/ci ... Added CI	2022-01-12 14:24:51 +01:00
Miodrag Milanovic	ab5ff32b31	Added CI	2022-01-12 14:18:17 +01:00
Miodrag Milanović	f878a0e517	Merge pull request #136 from nakengelhardt/fix_pono ... use --witness option when calling pono	2022-01-12 13:46:25 +01:00
N. Engelhardt	257a57d8ed	create only a single bad when using pono solver; workaround for #137	2022-01-12 13:18:54 +01:00
N. Engelhardt	ad07ea0e85	add testcase exposing #137	2022-01-12 11:06:05 +01:00
N. Engelhardt	5a04ac3fcc	use --witness option when calling pono	2022-01-12 10:55:08 +01:00
N. Engelhardt	f5a41e5ab1	Merge pull request #135 from nakengelhardt/rename_task ... Rename SbyJob to SbyTask and SbyTask to SbyProc to reduce confusion	2022-01-12 10:52:42 +01:00
N. Engelhardt	63bf8457d7	Merge pull request #134 from nakengelhardt/advertise_suite_in_readme ... mention tabby+oss cad suite in readme	2022-01-11 17:34:35 +01:00
N. Engelhardt	7c9e5b026b	Rename SbyJob to SbyTask and SbyTask to SbyProc to reduce confusion. Config file tasks now correspond to SbyTasks.	2022-01-11 17:08:56 +01:00
N. Engelhardt	9af6e220f9	mention tabby+oss cad suite in readme	2022-01-04 16:32:59 +01:00
Claire Xenia Wolf	ac9001b22c	Improvements and cleanups in tasks handling ... Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>	2021-12-18 11:36:34 +01:00
Claire Xenia Wolf	f1d3be3914	Fixed [tasks] section parsing ... Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>	2021-12-17 20:57:19 +01:00
Claire Xen	f7f5135508	Update README.md	2021-12-17 15:50:57 +01:00
Claire Xen	7f2c4189dc	Update README.md	2021-12-17 15:48:01 +01:00
Claire Xenia Wolf	4a07e026dd	Add inductive invariants example ... Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>	2021-12-17 15:42:04 +01:00
Claire Xenia Wolf	ab9d4fd3cf	Add ":"-syntax for [tasks] section ... Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>	2021-12-17 15:36:35 +01:00
Claire Xenia Wolf	b409b1179e	Update docs theme ... Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>	2021-11-30 10:47:43 +01:00
Claire Xenia Wolf	38562a5bb9	Update docs theme ... Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>	2021-11-29 16:51:54 +01:00
Claire Xenia Wolf	882d5b3a96	update docs theme ... Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>	2021-11-26 20:34:55 +01:00
Claire Xenia Wolf	5d19e4641a	Add support for directories in [files] section ... Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>	2021-10-31 14:43:02 +01:00
Claire Xenia Wolf	1b3832cf92	Fixed names and links	2021-10-31 14:42:39 +01:00
Miodrag Milanović	15278f1346	Merge pull request #127 from christian-krieg/feat/update-docs_super-prove ... Updated install instructions for super_prove	2021-09-13 16:21:18 +02:00
Miodrag Milanovic	863a53b312	Fix regression	2021-08-25 12:10:18 +02:00