| module state_machine | |
| use bitvec_ops, only: nand_eval, flat_circuit_eval | |
| implicit none | |
| private | |
| public :: bmc_check, induction_check, BMCResult | |
| integer, parameter :: MAX_STATE_BITS = 32 | |
| integer, parameter :: MAX_STEPS = 100 | |
| integer, parameter :: MAX_VARS = 1024 | |
| type :: BMCResult | |
| logical :: property_holds | |
| integer :: counterexample_step | |
| logical :: counterexample_state(MAX_STATE_BITS) | |
| end type BMCResult | |
| contains | |
| function bmc_check(transition_gates, num_trans_gates, & | |
| property_gates, num_prop_gates, & | |
| init_state, state_width, bound) result(res) | |
| integer, intent(in) :: num_trans_gates, num_prop_gates, state_width, bound | |
| integer, intent(in) :: transition_gates(MAX_VARS, 2) | |
| integer, intent(in) :: property_gates(MAX_VARS, 2) | |
| logical, intent(in) :: init_state(MAX_STATE_BITS) | |
| type(BMCResult) :: res | |
| logical :: current_state(MAX_STATE_BITS) | |
| logical :: next_state(MAX_STATE_BITS) | |
| logical :: wire_values(MAX_VARS) | |
| logical :: prop_wires(MAX_VARS) | |
| integer :: step | |
| res%property_holds = .true. | |
| res%counterexample_step = -1 | |
| current_state = .false. | |
| current_state(1:state_width) = init_state(1:state_width) | |
| do step = 0, bound - 1 | |
| call flat_circuit_eval(property_gates, num_prop_gates, & | |
| current_state, state_width, prop_wires) | |
| if (.not. prop_wires(state_width + num_prop_gates)) then | |
| res%property_holds = .false. | |
| res%counterexample_step = step | |
| res%counterexample_state(1:state_width) = current_state(1:state_width) | |
| return | |
| end if | |
| call flat_circuit_eval(transition_gates, num_trans_gates, & | |
| current_state, state_width, wire_values) | |
| next_state(1:state_width) = wire_values(state_width+1:state_width+state_width) | |
| current_state = next_state | |
| end do | |
| end function bmc_check | |
| function induction_check(transition_gates, num_trans_gates, & | |
| property_gates, num_prop_gates, & | |
| state_width, k) result(holds) | |
| integer, intent(in) :: num_trans_gates, num_prop_gates, state_width, k | |
| integer, intent(in) :: transition_gates(MAX_VARS, 2) | |
| integer, intent(in) :: property_gates(MAX_VARS, 2) | |
| logical :: holds | |
| type(BMCResult) :: base_result | |
| logical :: init_state(MAX_STATE_BITS) | |
| init_state = .false. | |
| base_result = bmc_check(transition_gates, num_trans_gates, & | |
| property_gates, num_prop_gates, & | |
| init_state, state_width, k) | |
| holds = base_result%property_holds | |
| end function induction_check | |
| end module state_machine | |