Created
December 21, 2020 13:26
-
-
Save ZipCPU/c7c5fec1a8ce2ed0064b7d4434d3fd41 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
[tasks] | |
prf | |
[options] | |
mode prove | |
depth 2 | |
[engines] | |
smtbmc | |
[script] | |
read -formal mybits.v | |
prep -top mybits | |
[files] | |
mybits.v |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
/*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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment