Jannis Harder 
								
							 
						 
						
							
							
								
								
							
							
							
								
							
							
								876ef59f4f 
								
							 
						 
						
							
							
								
								Merge pull request  #3396  from jix/async2sync_const_clocks  
							
							... 
							
							
							
							async2sync: turn FFs with const clks into gclk FFs with feedback 
							
						 
						
							2022-07-01 16:47:31 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Miodrag Milanovic 
								
							 
						 
						
							
							
							
							
								
							
							
								fda3a537e1 
								
							 
						 
						
							
							
								
								Update abc  
							
							
							
						 
						
							2022-07-01 16:23:24 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Jannis Harder 
								
							 
						 
						
							
							
								
								
							
							
							
								
							
							
								0182b26aba 
								
							 
						 
						
							
							
								
								Merge pull request  #3391  from programmerjake/simcheck-allow-smtlib2-blackboxes  
							
							... 
							
							
							
							add hierarchy -smtcheck 
							
						 
						
							2022-07-01 14:38:45 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									github-actions[bot] 
								
							 
						 
						
							
							
							
							
								
							
							
								42721b6a12 
								
							 
						 
						
							
							
								
								Bump version  
							
							
							
						 
						
							2022-07-01 00:19:06 +00:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Jannis Harder 
								
							 
						 
						
							
							
							
							
								
							
							
								5db542742b 
								
							 
						 
						
							
							
								
								async2sync: turn FFs with const clks into gclk FFs with feedback  
							
							... 
							
							
							
							The formal backends do not support multiple clocks. This includes
constant clocks. Constant clocks do appear in what isn't a proper
multiclock design, for example when mapping not fully initialized ROMs.
As converting FFs with constant clocks to FFs using the global is doable
even in a single clock flow, make async2sync do this. 
							
						 
						
							2022-06-30 12:09:04 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Miodrag Milanovic 
								
							 
						 
						
							
							
							
							
								
							
							
								b80976b543 
								
							 
						 
						
							
							
								
								Update to new verific extensions inteface  
							
							
							
						 
						
							2022-06-30 11:19:01 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									github-actions[bot] 
								
							 
						 
						
							
							
							
							
								
							
							
								9d63a90e0e 
								
							 
						 
						
							
							
								
								Bump version  
							
							
							
						 
						
							2022-06-30 00:17:25 +00:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Jannis Harder 
								
							 
						 
						
							
							
								
								
							
							
							
								
							
							
								0d2377c8a6 
								
							 
						 
						
							
							
								
								Merge pull request  #3394  from jix/memory_map_rom_keepdc  
							
							... 
							
							
							
							memory_map: -keepdc option for formal 
							
						 
						
							2022-06-29 20:02:12 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Jannis Harder 
								
							 
						 
						
							
							
							
							
								
							
							
								930bcf0e75 
								
							 
						 
						
							
							
								
								smt2, btor: Revert calling memory_map -rom-only  
							
							... 
							
							
							
							This approach had major issues with ROMs whose initialization was not
fully defined. If required, memory_map -rom-only -keepdc should be
called early in a formal flow instead. (This does require a careful
choice of optimization passes though. Sby's scripts will be updated
accordingly.) 
							
						 
						
							2022-06-29 18:28:34 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Jannis Harder 
								
							 
						 
						
							
							
							
							
								
							
							
								a47254bd10 
								
							 
						 
						
							
							
								
								opt_dff: With -keepdc, never turn undef init vals into const drivers  
							
							
							
						 
						
							2022-06-29 15:42:39 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Jannis Harder 
								
							 
						 
						
							
							
							
							
								
							
							
								a6b440b5c9 
								
							 
						 
						
							
							
								
								memory_map: avoid undriven unused FF inputs for -keepdc  
							
							
							
						 
						
							2022-06-28 19:05:35 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									github-actions[bot] 
								
							 
						 
						
							
							
							
							
								
							
							
								869e6a1b6d 
								
							 
						 
						
							
							
								
								Bump version  
							
							
							
						 
						
							2022-06-28 00:19:25 +00:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Jannis Harder 
								
							 
						 
						
							
							
							
							
								
							
							
								d78d807a7f 
								
							 
						 
						
							
							
								
								memory_map: -keepdc option for formal  
							
							... 
							
							
							
							Use it when invoking memory_map -rom-only from write_{smt2,btor}. 
							
						 
						
							2022-06-27 15:47:55 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									gatecat 
								
							 
						 
						
							
							
							
							
								
							
							
								48efc9b75c 
								
							 
						 
						
							
							
								
								gatemate: Add test for LUT tree mapping  
							
							... 
							
							
							
							Signed-off-by: gatecat <gatecat@ds0.me> 
							
						 
						
							2022-06-27 10:09:48 +01:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									gatecat 
								
							 
						 
						
							
							
							
							
								
							
							
								38a24ec5cc 
								
							 
						 
						
							
							
								
								gatemate: Add LUT tree library script  
							
							... 
							
							
							
							Co-authored-by: Claire Xenia Wolf <claire@clairexen.net>
Signed-off-by: gatecat <gatecat@ds0.me> 
							
						 
						
							2022-06-27 10:09:48 +01:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									gatecat 
								
							 
						 
						
							
							
							
							
								
							
							
								7c756c9959 
								
							 
						 
						
							
							
								
								gatemate: Add preliminary sim models for LUT tree structures  
							
							... 
							
							
							
							Signed-off-by: gatecat <gatecat@ds0.me> 
							
						 
						
							2022-06-27 10:09:48 +01:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									George Rennie 
								
							 
						 
						
							
							
							
							
								
							
							
								fbf5d89587 
								
							 
						 
						
							
							
								
								equiv_make: Add -make_assert option  
							
							... 
							
							
							
							This adds a -make_assert flag to equiv_make. When used, the pass generates
$eqx and $assert cells to encode equivalence instead of $equiv. 
							
						 
						
							2022-06-24 00:17:02 +01:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									rockybulwinkle 
								
							 
						 
						
							
							
								
								
							
							
							
								
							
							
								ec2f8796bd 
								
							 
						 
						
							
							
								
								Update tcl doc, yosys does not return data to tcl  
							
							... 
							
							
							
							This pull request is to address YosysHQ/yosys#2980 .
The documentation, as originally written, does not make it clear that yosys commands, when used within a tcl script, do not return any value to the tcl script.
This pull request notes this and offers a workaround via tee as noted in the issue. 
							
						 
						
							2022-06-23 13:34:08 -05:00 
							
								 
							
						 
					 
				
					
						
							
						 
						
							
							
							
							
								
							
							
								c16c028831 
								
							 
						 
						
							
							
								
								add hierarchy -smtcheck  
							
							... 
							
							
							
							like -simcheck, but allow smtlib2_module modules. 
							
						 
						
							2022-06-22 20:53:10 -07:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									github-actions[bot] 
								
							 
						 
						
							
							
							
							
								
							
							
								b2408df313 
								
							 
						 
						
							
							
								
								Bump version  
							
							
							
						 
						
							2022-06-22 00:19:30 +00:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Archie 
								
							 
						 
						
							
							
							
							
								
							
							
								f69c2c802c 
								
							 
						 
						
							
							
								
								Adding expected error message.  
							
							
							
						 
						
							2022-06-22 00:34:49 +01:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Archie 
								
							 
						 
						
							
							
							
							
								
							
							
								c8cd4f468a 
								
							 
						 
						
							
							
								
								Adding testcase for issue 3374  
							
							
							
						 
						
							2022-06-22 00:34:49 +01:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Archie 
								
							 
						 
						
							
							
							
							
								
							
							
								7eeb656e2a 
								
							 
						 
						
							
							
								
								Add check for BLIF with no model name  
							
							
							
						 
						
							2022-06-22 00:34:49 +01:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Miodrag Milanovic 
								
							 
						 
						
							
							
							
							
								
							
							
								1fdbb42fdd 
								
							 
						 
						
							
							
								
								Revert "use new verific extensions library"  
							
							... 
							
							
							
							This reverts commit 607e957657 
							
						 
						
							2022-06-21 18:07:47 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Jannis Harder 
								
							 
						 
						
							
							
								
								
							
							
							
								
							
							
								a30b38910c 
								
							 
						 
						
							
							
								
								Merge pull request  #3387  from ekiwi/btor-pos-cell  
							
							... 
							
							
							
							btor: add support for $pos cell 
							
						 
						
							2022-06-21 10:30:10 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									github-actions[bot] 
								
							 
						 
						
							
							
							
							
								
							
							
								0b486c56e8 
								
							 
						 
						
							
							
								
								Bump version  
							
							
							
						 
						
							2022-06-21 00:16:10 +00:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Kevin Läufer 
								
							 
						 
						
							
							
							
							
								
							
							
								de5c4bf523 
								
							 
						 
						
							
							
								
								btor: add support for $pos cell  
							
							
							
						 
						
							2022-06-20 16:40:46 -07:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Archie 
								
							 
						 
						
							
							
							
							
								
							
							
								e7e8e3b0f6 
								
							 
						 
						
							
							
								
								Adding expected error message.  
							
							
							
						 
						
							2022-06-20 21:50:26 +01:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Lofty 
								
							 
						 
						
							
							
							
							
								
							
							
								34804f3fb6 
								
							 
						 
						
							
							
								
								codeowners: adopt ABC9 and update intel_alm username  
							
							
							
						 
						
							2022-06-20 15:02:50 +01:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									George Rennie 
								
							 
						 
						
							
							
							
							
								
							
							
								5dfad5101d 
								
							 
						 
						
							
							
								
								chformal: Rename -coverprecond to -coverenable  
							
							
							
						 
						
							2022-06-18 18:28:12 +01:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Jannis Harder 
								
							 
						 
						
							
							
							
							
								
							
							
								e39c422734 
								
							 
						 
						
							
							
								
								chformal: Test -coverprecond and reuse the src attribute  
							
							
							
						 
						
							2022-06-18 18:19:26 +01:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									George Rennie 
								
							 
						 
						
							
							
							
							
								
							
							
								c659bd1878 
								
							 
						 
						
							
							
								
								chformal: Add -coverprecond option  
							
							... 
							
							
							
							This inserts $cover cells to cover the enable signal (precondition)
for the selected formal cells. 
							
						 
						
							2022-06-18 18:19:26 +01:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									github-actions[bot] 
								
							 
						 
						
							
							
							
							
								
							
							
								90147f5fbf 
								
							 
						 
						
							
							
								
								Bump version  
							
							
							
						 
						
							2022-06-18 00:17:32 +00:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Archie 
								
							 
						 
						
							
							
							
							
								
							
							
								4542d51791 
								
							 
						 
						
							
							
								
								Adding testcase for issue 3374  
							
							
							
						 
						
							2022-06-17 20:07:02 +01:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Jannis Harder 
								
							 
						 
						
							
							
								
								
							
							
							
								
							
							
								e6a5d84149 
								
							 
						 
						
							
							
								
								Merge pull request  #3383  from jix/write_formal_map_roms  
							
							... 
							
							
							
							smt2, btor: Use memory_map -rom-only to make ROMs usable for k-induction 
							
						 
						
							2022-06-17 19:08:14 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Jannis Harder 
								
							 
						 
						
							
							
							
							
								
							
							
								4adef63cd4 
								
							 
						 
						
							
							
								
								smt2, btor: Use memory_map -rom-only to make ROMs usable for k-induction  
							
							... 
							
							
							
							This avoids provability regressions now that we infer more ROMs.
This fixes  #3378  
							
						 
						
							2022-06-17 17:23:13 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Marcelina Kościelnicka 
								
							 
						 
						
							
							
							
							
								
							
							
								ab3a9325c3 
								
							 
						 
						
							
							
								
								memory_map: Add -rom-only option.  
							
							
							
						 
						
							2022-06-17 16:56:11 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Miodrag Milanović 
								
							 
						 
						
							
							
								
								
							
							
							
								
							
							
								c23139fd98 
								
							 
						 
						
							
							
								
								Merge pull request  #3382  from YosysHQ/micko/verific_extensions  
							
							... 
							
							
							
							use new verific extensions library 
							
						 
						
							2022-06-17 16:20:31 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Miodrag Milanovic 
								
							 
						 
						
							
							
							
							
								
							
							
								607e957657 
								
							 
						 
						
							
							
								
								use new verific extensions library  
							
							
							
						 
						
							2022-06-17 16:04:22 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Marcelina Kościelnicka 
								
							 
						 
						
							
							
							
							
								
							
							
								01daa077a2 
								
							 
						 
						
							
							
								
								memory_map: Use const drivers instead of FFs for ROMs.  
							
							
							
						 
						
							2022-06-17 15:17:14 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									github-actions[bot] 
								
							 
						 
						
							
							
							
							
								
							
							
								bb634d39ef 
								
							 
						 
						
							
							
								
								Bump version  
							
							
							
						 
						
							2022-06-17 00:17:38 +00:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Marcelina Kościelnicka 
								
							 
						 
						
							
							
							
							
								
							
							
								d69091806a 
								
							 
						 
						
							
							
								
								memory_libmap: Fix wrprio handling.  
							
							
							
						 
						
							2022-06-17 02:09:37 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Marcelina Kościelnicka 
								
							 
						 
						
							
							
							
							
								
							
							
								25a4cd7020 
								
							 
						 
						
							
							
								
								memory_libmap: Fix params emitted for unused ports for consistency.  
							
							
							
						 
						
							2022-06-16 08:14:08 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Archie 
								
							 
						 
						
							
							
							
							
								
							
							
								b604c97b33 
								
							 
						 
						
							
							
								
								Add check for BLIF with no model name  
							
							
							
						 
						
							2022-06-14 14:17:00 +01:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									github-actions[bot] 
								
							 
						 
						
							
							
							
							
								
							
							
								3046a06490 
								
							 
						 
						
							
							
								
								Bump version  
							
							
							
						 
						
							2022-06-14 00:18:42 +00:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Marcelina Kościelnicka 
								
							 
						 
						
							
							
							
							
								
							
							
								6b7efe12b7 
								
							 
						 
						
							
							
								
								Add a check for packed memory MEMID uniqueness  
							
							
							
						 
						
							2022-06-13 19:23:55 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									N. Engelhardt 
								
							 
						 
						
							
							
								
								
							
							
							
								
							
							
								3eaa9e38e0 
								
							 
						 
						
							
							
								
								Merge pull request  #3196  from bfg86/bfg86/rename  
							
							... 
							
							
							
							Add -suffix option to rename -wire 
							
						 
						
							2022-06-13 16:00:04 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Marcelina Kościelnicka 
								
							 
						 
						
							
							
							
							
								
							
							
								1ff0e1a58a 
								
							 
						 
						
							
							
								
								opt_ffinv: Fix use after free.  
							
							
							
						 
						
							2022-06-13 14:04:04 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Miodrag Milanovic 
								
							 
						 
						
							
							
							
							
								
							
							
								ddc8044655 
								
							 
						 
						
							
							
								
								removed deprecated features code  
							
							
							
						 
						
							2022-06-13 10:50:24 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									bfg86 
								
							 
						 
						
							
							
							
							
								
							
							
								aedd3b7999 
								
							 
						 
						
							
							
								
								Updating help-text with nakengelhardts suggestion.  
							
							
							
						 
						
							2022-06-13 09:35:10 +02:00