mybits.sby

[tasks]
prf

[options]
mode prove
depth 2

[engines]
smtbmc

[script]
read -formal mybits.v
prep -top mybits

[files]
mybits.v

mybits.v

/*Design a circuit that accepts as input a number 
of 4-bit and will count the number of bits that are 1 in the output*/
`default_nettype none
// verilator lint_off DECLFILENAME

module mybits_s(b0, b1, b2, b3, B0, B1, B2);
input wire b0, b1, b2, b3;
output wire B0, B1, B2;

wire	n_b0, n_b1, n_b2, n_b3;

//These are all the wires needed 
wire w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13;

//These are all the NOT gates needed
not not0(n_b0, b0);
not not1(n_b1, b1);
not not2(n_b2, b2);
not not3(n_b3, b3);


//B0 is written as a SOP
and and0(B0, b0, b1, b2, b3); //m16


//B1 is written as a POS 
or or0(w0, b0, b1, b2, b3); //M1
or or1(w1, b0, b1, b2, n_b3); //M2
or or2(w2, b0, b1, n_b2, b3); //M3
or or3(w3, b0, n_b1, b2, b3); //M5
or or4(w4, n_b0, b1, b2, b3); //M9
or or5(w5, n_b0, n_b1, n_b2, n_b3); //M16

 
and and1(B1, w0, w1, w2, w3, w4, w5);


//B2 is written as a POS 
and and2(w6, n_b0, n_b1, n_b2, b3); //m2
and and3(w7, n_b0, n_b1, b2, n_b3); //m3
and and4(w8, n_b0, b1, n_b2, n_b3); //m5
and and5(w9, n_b0, b1, b2, b3); //m8
and and6(w10, b0, n_b1, n_b2, n_b3); //m9
and and7(w11, b0, n_b1, b2, b3); //m12
and and9(w12, b0, b1, n_b2, b3); //m14
and and10(w13, b0, b1, b2, n_b3); //m15


or or6(B2, w6, w7, w8, w9, w10, w11, w12, w13); 

endmodule

 

 

 
module mybits_d(b0, b1, b2, b3, B0, B1, B2);
input wire b0, b1, b2, b3;
output wire B0, B1, B2;


//B0 is written an a SOP
assign B0 = b0 & b1 & b2 & b3; 

//B1 is written as a POS
assign B1 = (b0 | b1 | b2 | b3)& 
            (b0 | b1 | b2 | ~b3)&
            (b0 | b1 | ~b2 | b3)& 
            (b0 | ~b1 | b2 | b3)&
            (~b0 | b1 | b2 | b3)& 
            (~b0 | ~b1 | ~b2 | ~b3);
 

//B2 is written as a SOP           
assign B2 = ~b0 & ~b1 & ~b2 & b3 |
            ~b0 & ~b1 & b2 & ~b3 |
            ~b0 & b1 & ~b2 & ~b3 |
            ~b0 & b1 & b2 & b3 |
            b0 & ~b1 & ~b2 & ~b3 |
            b0 & ~b1 & b2 & b3 |
            b0 & b1 & ~b2 & b3 |
            b0 & b1 & b2 & ~b3;

endmodule

module mybits(b0, b1, b2, b3, B0, B1, B2);
input wire b0, b1, b2, b3;
output wire B0, B1, B2;

wire	s0, s1, s2;

mybits_s structural(b0, b1, b2, b3, s0, s1, s2);

mybits_d dataflow(b0, b1, b2, b3, B0, B1, B2);

always @(*)
begin
	assert(B0 == s0);
	assert(B1 == s1);
	assert(B2 == s2);
end

always @(*)
case({ b0, b1, b2, b3 })
4'h0: assert({ B0, B1, B2 } == 3'h0);
4'h1: assert({ B0, B1, B2 } == 3'h1);
4'h2: assert({ B0, B1, B2 } == 3'h1);
4'h3: assert({ B0, B1, B2 } == 3'h2);
4'h4: assert({ B0, B1, B2 } == 3'h1);
4'h5: assert({ B0, B1, B2 } == 3'h2);
4'h6: assert({ B0, B1, B2 } == 3'h2);
4'h7: assert({ B0, B1, B2 } == 3'h3);
4'h8: assert({ B0, B1, B2 } == 3'h1);
4'h9: assert({ B0, B1, B2 } == 3'h2);
4'ha: assert({ B0, B1, B2 } == 3'h2);
4'hb: assert({ B0, B1, B2 } == 3'h3);
4'hc: assert({ B0, B1, B2 } == 3'h2);
4'hd: assert({ B0, B1, B2 } == 3'h3);
4'he: assert({ B0, B1, B2 } == 3'h3);
4'hf: assert({ B0, B1, B2 } == 3'h4);
endcase

endmodule