github.com/YosysHQ.yosys
1
0
Fork 0
mirror of synced 2026-04-30 21:50:07 +00:00
Code Issues Releases Wiki Activity

Merge pull request #5285 from jix/abstract_initstates

Browse Source 
abstract: Add -initstates option
This commit is contained in:
Jannis Harder
2025-08-18 15:39:09 +02:00
committed by GitHub
parent e0e70d1158 1f876f3a22
commit 7c409e2d5a
2 changed files with 84 additions and 11 deletions
Download Patch File Download Diff File Expand all files Collapse all files

30
tests/various/abstract_initstates.ys Normal file
View File

@@ -0,0 +1,30 @@
read_verilog <<EOT
module half_clock (CLK, Q, magic);
input CLK;
output reg Q = 0;
input magic;
always @(posedge CLK)
Q <= ~Q;
endmodule
EOT
proc
design -save half_clock
sat -set-init-undef -enable_undef -verify -seq 5 -set-at 1 Q 0
sat -set-init-undef -enable_undef -falsify -seq 5 -set-at 1 Q 0 -set-at 2 Q 0
sat -set-init-undef -enable_undef -falsify -seq 5 -set-at 2 Q 0 -set-at 3 Q 0
abstract -state -initstates 1 */Q
sat -set-init-undef -enable_undef -verify -seq 5 -set-at 1 Q 0 -set-at 2 Q 0
sat -set-init-undef -enable_undef -falsify -seq 5 -set-at 2 Q 0 -set-at 3 Q 0
design -load half_clock
sat -set-init-undef -enable_undef -falsify -seq 5 -set-at 1 Q 0 -set-at 2 Q 0
sat -set-init-undef -enable_undef -falsify -seq 5 -set-at 2 Q 0 -set-at 3 Q 0
sat -set-init-undef -enable_undef -falsify -seq 5 -set-at 3 Q 0 -set-at 4 Q 0
abstract -state -initstates 2 */Q
sat -set-init-undef -enable_undef -verify -seq 5 -set-at 1 Q 0 -set-at 2 Q 0
sat -set-init-undef -enable_undef -verify -seq 5 -set-at 1 Q 0 -set-at 2 Q 0 -set-at 3 Q 0
sat -set-init-undef -enable_undef -falsify -seq 5 -set-at 3 Q 0 -set-at 4 Q 0