[in progress : I’ll put up the solution after Nov 28. I have to submit it as assignment so can not take the risk of being copied or so.]
These days simulation is the most prominent technique for verification. However, simulation can only cover a part of all cases possible thus simulation does not guarantee that certain properties will hold everywhere in the system. For example, any complex asynchronous boolean circuit with 100 variables will have 2100 combination. Not everyone can afford verifying all these combination with computers using simulation. Only a handful of companies like Intel can afford to do so with thousands of C.P.U. running in parallel verifying a chip design or testing a chip before sending it to foundry. If you are a smaller company, then you have to make sure that you hire smart people who can break down a larger problem into smaller one. Partitioning a large system into smaller one is an art and requires a lot of experience and eyes for details though there are few techniques available such as expander graphs and matroids etc.
A good techniques which widely used these days is temporal logic model checking . In this method the system being verified is modeled as finite state transition system and by exhaustively exploring the model, we check whether property holds or not. The biggest advantage using this is, if some property does not hold on this system then a witness (counterexample) is produces. This helps a lot in improving and correcting the design.
Now we are going to consider a real time example to show how to use this method. Consider the following VHDL description of an state machine with two architecture. This was given to us as an assignment at IIT Bombay by Prof. M. P. Desai. I am not sure which of his Teaching Assistant wrote it. Anyway this entity of FSM has two architecture, one_hot and encode. Our job is to verify that both of them are equal without using the simulation.
-- entity fsm has two architectures entity fsm is port (up, down: in bit; done: out bit; clock: in bit; reset: in bit); end fsm; -- this is the first. architecture one_hot of fsm is signal state_sig: bit_vector(3 downto 0); begin process(clock,up,down,state_sig) variable next_state: bit_vector(3 downto 0); variable done_var : bit; begin done_var := '0'; if(reset = '1') then next_state := (0 => '1', others => '0'); else if(up = '1') then -- rotate left by 1 next_state := state_sig(2 downto 0) & state_sig(3); if(state_sig(3) = '1') then done_var := '1'; end if; elsif (down = '1') then -- rotate right by 1 next_state := state_sig(0) & state_sig(3 downto 1); else next_state := state_sig; end if; end if; done <= done_var; if(clock'event and clock = '1') then state_sig <= next_state; end if; end process; end one_hot; -- this is the second architecture encode of fsm is signal state_sig,state_sig_p1, state_sig_m1: bit_vector(1 downto 0); begin state_sig_p1(0) <= not state_sig(0); state_sig_p1(1) <= state_sig(0) xor state_sig(1); state_sig_m1(0) <= not state_sig(0); state_sig_m1(1) <= state_sig(1) xor (not state_sig(0)); process(clock,up,down,state_sig,state_sig_p1,state_sig_m1) variable next_state: bit_vector(1 downto 0); variable done_var : bit; begin done_var := '0'; if(reset = '1') then next_state := (others => '0'); else if(up = '1') then next_state := state_sig_p1; if(state_sig(1) = '1' and state_sig(0) = '0') then done_var := '1'; end if; elsif (down = '1') then next_state := state_sig_m1; else next_state := state_sig; end if; end if; done <= done_var; if(clock'event and clock = '1') then state_sig <= next_state; end if; end process; end encode;