# Combinational circuits – Equivalence checking

Given a VLSI entity and its two description, establishing if both of them are equivalent is fundamental problem in VLSI verification. In this post, I am going to give describe an small part of this problem. Lets say someone has provided us with an behavioral description of an entity. For example lets say the given behavior of this entity is following.

Lets say if $a = 1$ and $b =1$ then $c = c \otimes d$ and if $a = 1$ and $b = 0$ then $e = c \bar{\otimes} d$. Otherwise, I don’t give a damn!

Ok! Now I have to give a hardware description of this entity else no would care about it. I give the following VHDL description (I hate verilog!).


-- This is the entity

entity Cblock is

port(a,b,c,d: in bit; e: out bit);

end entity Cblock;

-- this is the specification

architecture Behave of Cblock is

begin process(a,b,c,d)

begin

if(a = '1' and b = '1') then

e &lt;= c xor d;

elsif (a = '1' and b = '0') then

e <= c xnor d;

else

end if;

end process;

end Behave;



Next task is to find an equivalent circuit description of this behavior. We can surely use some synthesizer but they are not smart enough. Sometimes they produce garbage (though this case is way too simple to make a synthesizer go mad.). We are going to build our own. We introduce one more condition, say a, c, and d can never be same at any time. So we can treat them as don’t care condition. Lets make the truth table of Cblock.

After minimization, Cblock can be written as $e = b \bar{c}\bar{d} + abd + abc$.  Notice that since $a, c, d$ are not allowed to be same at any given time. We have  $\bar{a}{b}\bar{c}\bar{d}$, $\bar{a}\bar{b}\bar{c}\bar{d}$, $abdc$, ${a}\bar{b}{c}{d}$ should not be taken into accout i.e. don’t care conditions.

### Build the circuit

Lets our life more miserable. We say that we have only AND and NOT gates available. Can we realise the given function $e$. Yes we can, remember that AND and NOT together represents NAND which is universal gate and others gates can be realised using it.

Now we can construct the following circuit.

This circuit can be simulated in any circuit simulator like ngspice. If you are using Qucs than you can use the following file. Since I can not attach this type of file, here is the code.

## Verify both implementation

Now the final task to is to verify whether out implementation matches with the given behaviour. To verify, I must check my implementation for all the possible input combination and output must match the given bahviorial description. We use VHDL to describe our implementation and then we make a test-bench to verify it. Following is the code for testbench. All entities are given in a single file.


-- VHDL file for assignment 06.

-- Dilawar Singh

-- dilawar@ee.iitb.ac.in

-- Modified from its original version.

-- GHDL is used to compile it.

-- AND GATE

entity And2 is

port(a,b: in bit; c: out bit);

end entity And2;
architecture Behave of And2 is
begin

c &lt;= a and b;

end Behave;

-- Invertor

entity Inv is

port(a: in bit; b: out bit);

end entity Inv;

architecture Behave of Inv is

begin

b &lt;= not a;

end Behave;

-- This is the entity

entity Cblock is

port(a,b,c,d: in bit; e: out bit);

end entity Cblock;

-- this is the specification

architecture Behave of Cblock is

begin

process(a,b,c,d)

begin

if(a = '1' and b = '1') then

e &lt;= c xor d;

elsif (a = '1' and b = '0') then

e <= c xnor d;

else

end if;

end process;

end Behave;

-- this is the implementation which you have to write.

-- you may assume that the dont care set is a=c=d

architecture Impl of Cblock is

component And2 is port(a,b: in bit; c: out bit); end component;

component Inv is port(a: in bit; b: out bit); end component;

-- declare signals for interconnecting your gates

signal i1_out, i2_out, i3_out, i4_out, i5_out, i6_out, i7_out, i8_out : bit;

signal a1_out, a2_out, a3_out, a4_out, a5_out, a6_out : bit;

begin

i1 : Inv port map(a => c, b => i1_out);

i2 : Inv port map(a => d, b => i2_out);

i3 : Inv port map(a => c, b => i3_out);

i4 : Inv port map(a => d, b => i4_out);

i5 : Inv port map(a => a1_out, b => i5_out);

i6 : Inv port map(a => b, b => i6_out);

i7 : Inv port map(a => a4_out, b => i7_out);

i8 : Inv port map(a => a5_out, b => i8_out);

i9 : Inv port map(a => a6_out, b => e);

a1 : And2 port map(i1_out, i2_out, a1_out);

a2 : And2 port map(a, b, a2_out);

a3 : And2 port map(i3_out, i4_out, a3_out);

a4 : And2 port map(i5_out, a2_out, a4_out);

a5 : And2 port map(i6_out, a3_out, a5_out);

a6 : And2 port map(i7_out, i8_out, a6_out);

end Impl;

entity Testbench is
end entity Testbench;

-- testbench

architecture Compare of Testbench is

signal a,b,c,d,eref,edut: bit;

type bV2 is array(natural range <>) of bit_vector(3 downto 0);

-- legal patterns.

constant pattern: bV2(0 to 11) :=

(

('0','0','0','1'),

('0','0','1','0'),

('0','0','1','1'),

('0','1','0','1'),

('0','1','1','0'),

('0','1','1','1'),

('1','0','0','0'),

('1','0','0','1'),

('1','0','1','0'),

('1','1','0','0'),

('1','1','0','1'),

('1','1','1','0'));

component Cblock is port(a,b,c,d: in bit; e: out bit); end component;
for ref:Cblock  use entity work.Cblock(behave);
for dut:Cblock  use entity work.Cblock(behave); -- use impl when ready

begin

ref: Cblock port map(a=>a,b=>b,c=>c,d=>d,e=>eref);

-- change to implementation when you have one ready

dut: Cblock port map(a=>a,b=>b,c=>c,d=>d,e=>edut);

process

variable I : integer := 0;

begin

while I &lt; 12 loop

a &lt;= pattern(I)(3); b &lt;= pattern(I)(2); c &lt;= pattern(I)(1); d  &lt;= pattern(I)(0);

I := I+1;

wait for 1 ns;

assert(eref = edut) report "Mismatch between Reference and DUT" severity error;

end loop;

assert false report &quot;Test Over&quot; severity note;

wait;

end process;

end Compare;



## Results

Now we have to run this testbench. There are few VHDL simulator available, one is ghdl. We are going to use this. Make sure you can ghdl installed. You can get it from here. Now we have to run following commands.

$ghdl -a filename.vhd $ghdl -e testbench

\$ghdl -r testbench --vcd=filename.vcd

Since my filename was dilawar.vhd I got following output.

dilawar.vhdl:118:8:@12ns:(assertion note):Test Over

Note that since we have exhausted all the possible combination of inputs. This is not possible in big circuits with a lot of inputs. Simulation is too slow to handle all the cases. In future, we’ll be in need of better formal verification tools. About that some other day.