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 
							
								 
							
						 
					 
				
					
						
							
						 
						
							
							
							
							
								
							
							
								a87d21a802 
								
							 
						 
						
							
							
								
								add depth 1  
							
							
							
						 
						
							2022-05-25 03:35:21 -07:00 
							
								 
							
						 
					 
				
					
						
							
						 
						
							
							
							
							
								
							
							
								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 
							
								 
							
						 
					 
				
					
						
							
								
								
									KrystalDelusion 
								
							 
						 
						
							
							
							
							
								
							
							
								8f22733698 
								
							 
						 
						
							
							
								
								Revert change from yosyshq.net to yosyshq.com  
							
							
							
						 
						
							2022-05-04 10:07:31 +12:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									KrystalDelusion 
								
							 
						 
						
							
							
							
							
								
							
							
								60de15293d 
								
							 
						 
						
							
							
								
								Now actually fills up properly  
							
							... 
							
							
							
							As opposed to only storing MAX-1 
							
						 
						
							2022-05-02 12:34:57 +12:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									KrystalDelusion 
								
							 
						 
						
							
							
							
							
								
							
							
								48d846d529 
								
							 
						 
						
							
							
								
								Adjusting for use with OSS  
							
							... 
							
							
							
							i.e. doesn't use concurrent assertions 
							
						 
						
							2022-05-02 12:20:27 +12:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									KrystalDelusion 
								
							 
						 
						
							
							
							
							
								
							
							
								f33c2eda52 
								
							 
						 
						
							
							
								
								Updating/rearranging links  
							
							
							
						 
						
							2022-05-02 10:44:28 +12:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									KrystalDelusion 
								
							 
						 
						
							
							
							
							
								
							
							
								e8c5ae678d 
								
							 
						 
						
							
							
								
								Adding instructions for CAD  
							
							... 
							
							
							
							Currently taken verbatim from this repo's README.md 
							
						 
						
							2022-05-02 10:31:51 +12:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									KrystalDelusion 
								
							 
						 
						
							
							
							
							
								
							
							
								e106d5c161 
								
							 
						 
						
							
							
								
								Adjusting assumptions  
							
							
							
						 
						
							2022-04-27 09:36:44 +12:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									KrystalDelusion 
								
							 
						 
						
							
							
							
							
								
							
							
								ec02e25f5c 
								
							 
						 
						
							
							
								
								Split fifo.sv into two files  
							
							... 
							
							
							
							fifo.sv contains the components, top.sv for toplevel design. 
							
						 
						
							2022-04-27 09:24:14 +12:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									KrystalDelusion 
								
							 
						 
						
							
							
							
							
								
							
							
								679df4d898 
								
							 
						 
						
							
							
								
								Fixing .gitignore to ignore just directories  
							
							
							
						 
						
							2022-04-27 09:05:16 +12:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									KrystalDelusion 
								
							 
						 
						
							
							
							
							
								
							
							
								ee769996d0 
								
							 
						 
						
							
							
								
								Initial add of fifo example  
							
							... 
							
							
							
							Has tests which pass, committing before messing with it while tidying. 
							
						 
						
							2022-04-27 09:02:16 +12:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Jannis Harder 
								
							 
						 
						
							
							
								
								
							
							
							
								
							
							
								832888f0f0 
								
							 
						 
						
							
							
								
								Merge pull request  #156  from jix/refactor-tests  
							
							... 
							
							
							
							Refactor tests 
							
						 
						
							2022-04-25 11:21:21 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Jannis Harder 
								
							 
						 
						
							
							
							
							
								
							
							
								8da6f07cb3 
								
							 
						 
						
							
							
								
								Refactor tests  
							
							... 
							
							
							
							Organize tests into subdirectories and use a new makefile that scans
.sby files and allows selecting tests by mode, engine, solver and/or
subdirectory. Automatically skips tests that use engines/solvers that
are not found in the PATH.
See `cd tests; make help` for a description of supported make targets. 
							
						 
						
							2022-04-11 17:50:38 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Jannis Harder 
								
							 
						 
						
							
							
							
							
								
							
							
								6daa434d85 
								
							 
						 
						
							
							
								
								Add --dumptaskinfo option to output some .sby metadata as json  
							
							
							
						 
						
							2022-04-11 17:44:10 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Jannis Harder 
								
							 
						 
						
							
							
							
							
								
							
							
								a190994098 
								
							 
						 
						
							
							
								
								Add envvar to enable automatic .gitignore creation for workdirs  
							
							
							
						 
						
							2022-04-11 17:44:10 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Miodrag Milanović 
								
							 
						 
						
							
							
								
								
							
							
							
								
							
							
								1e1aea0b1e 
								
							 
						 
						
							
							
								
								Merge pull request  #140  from nakengelhardt/junit_jny  
							
							... 
							
							
							
							junit: use write_jny instead of write_json 
							
						 
						
							2022-04-08 15:26:48 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									N. Engelhardt 
								
							 
						 
						
							
							
							
							
								
							
							
								8ce526c22d 
								
							 
						 
						
							
							
								
								junit: use write_jny instead of write_json  
							
							
							
						 
						
							2022-04-06 18:35:01 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Miodrag Milanović 
								
							 
						 
						
							
							
								
								
							
							
							
								
							
							
								4886ed7e19 
								
							 
						 
						
							
							
								
								Merge pull request  #155  from jix/invalid_ff_dcinit_merge  
							
							... 
							
							
							
							Regression test: do not merge FFs with unconstrained initvals 
							
						 
						
							2022-04-03 12:15:58 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Jannis Harder 
								
							 
						 
						
							
							
							
							
								
							
							
								ef236eeddc 
								
							 
						 
						
							
							
								
								Regression test: do not merge FFs with unconstrained initvals  
							
							... 
							
							
							
							Currently done by `opt -keepdc` via `opt_merge` but not valid in a
formal context. 
							
						 
						
							2022-04-01 19:25:09 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Jannis Harder 
								
							 
						 
						
							
							
								
								
							
							
							
								
							
							
								25e982c238 
								
							 
						 
						
							
							
								
								Merge pull request  #154  from jix/sby_design-fixes  
							
							... 
							
							
							
							sby_design fixes 
							
						 
						
							2022-03-31 16:35:40 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Jannis Harder 
								
							 
						 
						
							
							
							
							
								
							
							
								4b512668b2 
								
							 
						 
						
							
							
								
								Fix design_hierarchy handling of $paramod cells  
							
							
							
						 
						
							2022-03-31 15:51:58 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Jannis Harder 
								
							 
						 
						
							
							
							
							
								
							
							
								a78eaa57db 
								
							 
						 
						
							
							
								
								Fix variable name in find_property_by_cellname's error path  
							
							
							
						 
						
							2022-03-31 13:12:15 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Jannis Harder 
								
							 
						 
						
							
							
								
								
							
							
							
								
							
							
								43a79965c3 
								
							 
						 
						
							
							
								
								Merge pull request  #151  from jix/prefer-first-trace  
							
							... 
							
							
							
							Prefer the first tracefile for each failing assertion 
							
						 
						
							2022-03-30 14:48:04 +02:00