| initial |
| assume (= [$formal$hyperram.v:296$1_CHECK] false) |
| assume (= [$formal$hyperram.v:296$1_EN] false) |
| assume (= [$formal$hyperram.v:297$2_CHECK] false) |
| assume (= [$formal$hyperram.v:298$3_CHECK] false) |
| assume (= [$formal$hyperram.v:299$4_CHECK] false) |
| assume (= [$formal$hyperram.v:300$5_CHECK] false) |
| assume (= [$formal$hyperram.v:301$6_CHECK] false) |
| assume (= [$formal$hyperram.v:302$7_CHECK] false) |
| assume (= [$formal$hyperram.v:303$8_CHECK] false) |
| assume (= [$formal$hyperram.v:304$9_CHECK] false) |
| assume (= [ck] false) |
| assume (= [command_address] #b000000000000000000000000000000000000000000000000) |
| assume (= [control_state] #b0000000) |
| assume (= [data_out_register] #b00000000000000000000000000000000) |
| assume (= [done_counter] #b00000000) |
| assume (= [read_count] #b000000) |
| assume (= [wait_counter] #b00000000) |
| assume (= [write_count] #b000000) |
| assume (= [write_mask_register] #b0000) |
| |
| state 0 |
| assume (= [address] #b00010010001101000101011001111000) |
| assume (= [clk] false) |
| assume (= [data_out] #b11001100110011001101110111011101) |
| assume (= [done_latency] #b000000) |
| assume (= [dq] #b00000000) |
| assume (= [rst] false) |
| assume (= [rwds] false) |
| assume (= [timed_read] false) |
| assume (= [transaction_begin] true) |
| assume (= [wait_latency] #b000000) |
| assume (= [write_enable] false) |
| assume (= [write_mask] #b0000) |
| |
| state 1 |
| assume (= [address] #b00010010001101000101011001111000) |
| assume (= [clk] false) |
| assume (= [data_out] #b11001100110011001101110111011101) |
| assume (= [done_latency] #b000000) |
| assume (= [dq] #b10100000) |
| assume (= [rst] false) |
| assume (= [rwds] false) |
| assume (= [timed_read] false) |
| assume (= [transaction_begin] false) |
| assume (= [wait_latency] #b000000) |
| assume (= [write_enable] false) |
| assume (= [write_mask] #b0000) |
| |
| state 2 |
| assume (= [address] #b00010010001101000101011001111000) |
| assume (= [clk] false) |
| assume (= [data_out] #b11001100110011001101110111011101) |
| assume (= [done_latency] #b000000) |
| assume (= [dq] #b00000110) |
| assume (= [rst] false) |
| assume (= [rwds] false) |
| assume (= [timed_read] false) |
| assume (= [transaction_begin] false) |
| assume (= [wait_latency] #b000000) |
| assume (= [write_enable] false) |
| assume (= [write_mask] #b0000) |
| |
| state 3 |
| assume (= [address] #b00010010001101000101011001111000) |
| assume (= [clk] false) |
| assume (= [data_out] #b11001100110011001101110111011101) |
| assume (= [done_latency] #b000000) |
| assume (= [dq] #b10001010) |
| assume (= [rst] false) |
| assume (= [rwds] false) |
| assume (= [timed_read] false) |
| assume (= [transaction_begin] false) |
| assume (= [wait_latency] #b000000) |
| assume (= [write_enable] false) |
| assume (= [write_mask] #b0000) |
| |
| state 4 |
| assume (= [address] #b00010010001101000101011001111000) |
| assume (= [clk] false) |
| assume (= [data_out] #b11001100110011001101110111011101) |
| assume (= [done_latency] #b000000) |
| assume (= [dq] #b11001111) |
| assume (= [rst] false) |
| assume (= [rwds] false) |
| assume (= [timed_read] false) |
| assume (= [transaction_begin] false) |
| assume (= [wait_latency] #b000000) |
| assume (= [write_enable] false) |
| assume (= [write_mask] #b0000) |
| |
| state 5 |
| assume (= [address] #b00010010001101000101011001111000) |
| assume (= [clk] false) |
| assume (= [data_out] #b11001100110011001101110111011101) |
| assume (= [done_latency] #b000000) |
| assume (= [dq] #b00000000) |
| assume (= [rst] false) |
| assume (= [rwds] false) |
| assume (= [timed_read] false) |
| assume (= [transaction_begin] false) |
| assume (= [wait_latency] #b000000) |
| assume (= [write_enable] false) |
| assume (= [write_mask] #b0000) |
| |
| state 6 |
| assume (= [address] #b00010010001101000101011001111000) |
| assume (= [clk] false) |
| assume (= [data_out] #b11001100110011001101110111011101) |
| assume (= [done_latency] #b000000) |
| assume (= [dq] #b00000000) |
| assume (= [rst] false) |
| assume (= [rwds] false) |
| assume (= [timed_read] false) |
| assume (= [transaction_begin] false) |
| assume (= [wait_latency] #b000000) |
| assume (= [write_enable] false) |
| assume (= [write_mask] #b0000) |
| |
| state 7 |
| assume (= [address] #b00010010001101000101011001111000) |
| assume (= [clk] false) |
| assume (= [data_out] #b11001100110011001101110111011101) |
| assume (= [done_latency] #b000000) |
| assume (= [dq] #b00000000) |
| assume (= [rst] false) |
| assume (= [rwds] false) |
| assume (= [timed_read] false) |
| assume (= [transaction_begin] false) |
| assume (= [wait_latency] #b000000) |
| assume (= [write_enable] false) |
| assume (= [write_mask] #b0000) |
| |
| state 8 |
| assume (= [address] #b00010010001101000101011001111000) |
| assume (= [clk] false) |
| assume (= [data_out] #b11001100110011001101110111011101) |
| assume (= [done_latency] #b000000) |
| assume (= [dq] #b00000000) |
| assume (= [rst] false) |
| assume (= [rwds] false) |
| assume (= [timed_read] false) |
| assume (= [transaction_begin] false) |
| assume (= [wait_latency] #b000000) |
| assume (= [write_enable] false) |
| assume (= [write_mask] #b0000) |
| |
| state 9 |
| assume (= [address] #b00010010001101000101011001111000) |
| assume (= [clk] false) |
| assume (= [data_out] #b11001100110011001101110111011101) |
| assume (= [done_latency] #b000000) |
| assume (= [dq] #b00000000) |
| assume (= [rst] false) |
| assume (= [rwds] false) |
| assume (= [timed_read] false) |
| assume (= [transaction_begin] false) |
| assume (= [wait_latency] #b000000) |
| assume (= [write_enable] false) |
| assume (= [write_mask] #b0000) |
| |
| state 10 |
| assume (= [address] #b00010010001101000101011001111000) |
| assume (= [clk] false) |
| assume (= [data_out] #b11001100110011001101110111011101) |
| assume (= [done_latency] #b000000) |
| assume (= [dq] #b00000000) |
| assume (= [rst] false) |
| assume (= [rwds] false) |
| assume (= [timed_read] false) |
| assume (= [transaction_begin] false) |
| assume (= [wait_latency] #b000000) |
| assume (= [write_enable] false) |
| assume (= [write_mask] #b0000) |
| |
| state 11 |
| assume (= [address] #b00010010001101000101011001111000) |
| assume (= [clk] false) |
| assume (= [data_out] #b11001100110011001101110111011101) |
| assume (= [done_latency] #b000000) |
| assume (= [dq] #b00000000) |
| assume (= [rst] false) |
| assume (= [rwds] false) |
| assume (= [timed_read] false) |
| assume (= [transaction_begin] false) |
| assume (= [wait_latency] #b000000) |
| assume (= [write_enable] false) |
| assume (= [write_mask] #b0000) |
| |
| state 12 |
| assume (= [address] #b00010010001101000101011001111000) |
| assume (= [clk] false) |
| assume (= [data_out] #b11001100110011001101110111011101) |
| assume (= [done_latency] #b000000) |
| assume (= [dq] #b00000000) |
| assume (= [rst] false) |
| assume (= [rwds] false) |
| assume (= [timed_read] false) |
| assume (= [transaction_begin] false) |
| assume (= [wait_latency] #b000000) |
| assume (= [write_enable] false) |
| assume (= [write_mask] #b0000) |
| |
| state 13 |
| assume (= [address] #b00010010001101000101011001111000) |
| assume (= [clk] false) |
| assume (= [data_out] #b11001100110011001101110111011101) |
| assume (= [done_latency] #b000000) |
| assume (= [dq] #b00000000) |
| assume (= [rst] false) |
| assume (= [rwds] false) |
| assume (= [timed_read] false) |
| assume (= [transaction_begin] false) |
| assume (= [wait_latency] #b000000) |
| assume (= [write_enable] false) |
| assume (= [write_mask] #b0000) |