mirror of
				https://github.com/YosysHQ/yosys
				synced 2025-10-31 03:32:29 +00:00 
			
		
		
		
	formalff: Document -declockgate option
This commit is contained in:
		
							parent
							
								
									904b4194cc
								
							
						
					
					
						commit
						43b5e109f3
					
				
					 1 changed files with 6 additions and 0 deletions
				
			
		|  | @ -538,6 +538,12 @@ struct FormalFfPass : public Pass { | |||
| 		log("        Add assumptions that constrain wires with the 'replaced_by_gclk'\n"); | ||||
| 		log("        attribute to the value they would have before an active clock edge.\n"); | ||||
| 		log("\n"); | ||||
| 		log("    -declockgate\n"); | ||||
| 		log("        Detect clock-gating patterns and modify any FFs clocked by the gated\n"); | ||||
| 		log("        clock to use the ungated clock with the gate signal as clock enable.\n"); | ||||
| 		log("        This doesn't affect the design's behavior during FV but can enable the\n"); | ||||
| 		log("        use of formal verification methods that only support a single global\n"); | ||||
| 		log("        clock.\n"); | ||||
| 
 | ||||
| 		// TODO: An option to check whether all FFs use the same clock before changing it to the global clock
 | ||||
| 	} | ||||
|  |  | |||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue