

entity halfAdder is port (a,b : in bit; sum,carry : out bit); end halfAdder; architecture ha_beh of halfAdder is begin sum <= a xor b; c_out <= a and b; end ha_beh; 
halfAdder (a, b) = (sum, carry) where sum = xor2 (a, b) carry = and2 (a, b)
halfAdder :: (Signal Bool,Signal Bool) > (Signal Bool,Signal Bool) halfAdder (a,b) = (sum,carry) where sum = xor2 (a, b) carry = and2 (a, b)
halfAdder :: (Signal Bool,Signal Bool) > (Signal Bool,Signal Bool)
A>B
: a function with input of
type A and output of type B
(A_{1},A_{2})
: a pair. Pairing allows
several signals to be grouped together and treated as one signal.
Signal A
: signals carrying values of type
A
Bool
: boolean values, False
or True
type Bit = Signal Bool
halfAdder :: (Bit,Bit) > (Bit,Bit) halfAdder (a,b) = (sum,carry) where ...
simulate
circuit input
simulate halfAdder (low,high)
(high,low)
simulate halfAdder (high,high)
(low,high)
id, inv :: Bit > Bit and2, nand2, or2, nor2, xor2, equiv, impl :: (Bit,Bit) > Bit <&>, <>, <#>, <=>, ==> :: (Bit,Bit) > Bit
a <&> b
is the same as and2 (a,b)
, etc.
halfAdder (a, b) = (sum, carry) where sum = xor2 (a, b) carry = and2 (a, b)
halfAdder (a, b) = (xor2 (a,b),and2(a,b))
halfAddder (a,b) = (a <#> b, a <&> b)
entity fullAdder is port (a,b,carryIn : in bit; sum,carryOut : out bit); end fullAdder; architecture fa_str of fullAdder is signal s1,c1,c2 : bit; begin  fa_str ha1: entity work.halfAdder port map (a, b, s1, c1); ha2: entity work.halfAdder port map (carryIn, s1, sum, c2); xor1: carryOut <= c1 xor c2; end fa_str;
fullAdder (carryIn, (a,b)) = (sum, carryOut) where (s1, c1) = halfAdder (a, b) (sum, c2) = halfAdder (carryIn,s1) carryOut = xor2 (c2, c1)
fullAdder :: (Bit,(Bit,Bit)) > (Bit,Bit) fullAdder (carryIn, (a,b)) = (sum, carryOut) where ...
entity rippleCarryAdder is generic (n : natural); port ( carryIn : in bit; a, b : in bit_vector(n1 downto 0); sum : out bit_vector(n1 downto 0); carryOut : out bit); end rippleCarryAdder; architecture rca_str of rippleCarryAdder is signal c : bit_vector(0 to n); begin c(0) <= carryIn; adders: for i in 0 to n1 generate begin bit : entity work.fullAdder port map (c(i),a(i),b(i),sum(i),c(i+1)); end generate; carryOut <= c(n); end rca_str;
rippleCarryAdder (carryIn, (as,bs)) = (sum,carryOut) where (sum,carryOut) = row fullAdder (carryIn,zipp (as,bs))
row
is a connection pattern that does exactly what
we need here.
zipp
takes care of pairing up the bits at corresponding
positions in the two input bit vectors as
and bs
.
rippleCarryAdder :: (Bit,([Bit],[Bit])) > ([Bit],Bit) rippleCarryAdder (carryIn, (as,bs)) = (sum,carryOut) where (sum,carryOut) = row fullAdder (carryIn,zipp (as,bs))
[]
(empty list)
[low,high,low,low] :: [Bit]
[(low,high),(low,low)] :: [(Bit,Bit)]
domain
enumerates all values of a finite type
zipp :: ([a],[b]) > [(a,b)]
,
where a and b are arbitrary types
unzipp :: [(a,b)] > ([a],[b])
map :: (a>b) > ([a] > [b])
row :: ((c, a) > (b, c)) > (c, [a]) > ([b], c)
simulate
circuit input
simulateSeq
circuit list_of_inputs
simulate fullAdder (high,(low,high))
(low,high)
simulate rippleCarryAdder (low,([low,high],[high,high]))
([high,low],high)
simulateSeq fullAdder domain
[(low,low),(high,low),(high,low),(low,high),(high,low),(low,high),(low,high),(high,high)]
writeVhdl "fullAdder" fullAdder
writeVhdlInput "fullAdder" fullAdder (var "carryIn",(var "a",var "b"))
writeVhdlInputOutput "fullAdder" fullAdder (var "carryIn",(var "a",var "b")) (var "sum",var "carryOut")
writeVhdlInputOutput "rippleCarryAdder" rippleCarryAdder (var "carryIn",(varList 8 "a",varList 8 "b")) (varList 8 "sum",var "carryOut")
import VhdlNew08
in your source file.
NoClk
to the end of the function name
writeVhdlNoClk "fullAdder" fullAdder
smv
property
xor (a,b) = (a <> b) <&> inv (a <&> b)
prop_xor = prop_Equivalent xor xor2
test_xor = simulateSeq prop_xor domain
vrfy_xor = smv prop_xor
prop_xor (a,b) = ok where out1 = xor (a,b) out2 = xor2 (a,b) ok = out1 <==> out2
prop_Equivalent circ1 circ2 inp = ok where out1 = circ1 inp out2 = circ2 inp ok = out1 <==> out2
prop_xor = prop_Equivalent xor xor2