[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.
[sourcecode language="css"]
— 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;
[/sourcecode]