ZipCPU

////////////////////////////////////////////////////////////////////////////////
//
// Filename: 	bimpy
//
// Project:	A simple, better, multiply generator
//
// Purpose:	A simply 2-bit multiply based upon the fact that LUT's allow
//		6-bits of input, but a 2x2 bit multiply will never carry more
//		than one bit.  While this multiply is hardware independent,
//		it is really motivated by trying to optimize for a specific

ZipCPU

<lama> hello
<lama> can somebody please help me, i'm trying to implement the modified booth's algorithm for multiplication, but the vhdl code gives incorrect results like 125 * 12 = 1076605135488 :D i don't know why http://pastebin.com/dKXJbsb5
<lama> i have also written a quick software implementation in c++ so i would be sure that i understand the algorithm and that works:
<lama> http://pastebin.com/4MhLdhtA
<lama> so can somebody see anything wrong with the vhdl code?
* jkent is now known as jkent`
* jkent` is now known as jkent
<lama> just to make things clear, if i have two's complement number in std_logic_vector and cast this to unsigned in order to add this vector to some other vector; the casting won't alter the std_logic_vector bit format, right?
<lama> let say that slv = 11111011 which is -5 in two's complement and i will do unsigned(slv), will this still hold the same binary value? unsigned(slv) + unsigned(1) = 11111100 (-4) ?

ZipCPU

module tk_recv_data(... i_rst_n, i_rx_int, ...)

always @(posedge i_clk)
begin
	if ( !i_rst_n )
	begin
		rx_temp_data <= 8'd0;
		num <= 4'd0;
		rx_data_r <= 8'd0;

ZipCPU

module	test(i_clk, i_ce, i_val, o_val);
	input	wire	i_clk, i_ce, i_val;
	output	reg	o_val;

	initial	o_val = 1'b0;
	always @(posedge i_clk)
		if (i_ce)
			o_val <= i_val;

`ifdef  FORMAL

ZipCPU

module	twotests(i_clk, i_ce, i_val, o_val);
	input	wire	i_clk, i_ce, i_val;
	output	reg	o_val;

	initial	o_val = 1'b0;
	always @(posedge i_clk)
		if (i_ce)
			o_val <= i_val;

`ifdef  FORMAL

ZipCPU

module hello(input clk, input rst, output [3:0] cnt);
	reg	[3:0]	cnt;
	initial	cnt = 0;

	always @(posedge clk) begin
		if (rst)
			cnt <= 0;
		else
			cnt <= cnt + 1;
	end

ZipCPU

yosys -ql hello.yslog	\
	-p 'read_verilog -formal hello.v'	\
	-p 'prep -top hello -nordff'	\
	-p 'write_smt2 hello.smt2'
yosys-smtbmc hello.smt2
yosys-smtbmc -i hello.smt2

ZipCPU

////////////////////////////////////////////////////////////////////////////////
//
// Filename: 	wbm2axisp.v (Wishbone master to AXI slave, pipelined)
//
// Project:	Pipelined Wishbone to AXI converter
//
// Purpose:	The B4 Wishbone SPEC allows transactions at a speed as fast as
//		one per clock.  The AXI bus allows transactions at a speed of
//	one read and one write transaction per clock.  These capabilities work
//	by allowing requests to take place prior to responses, such that the

ZipCPU

################################################################################
##
## Filename:	Makefile
##
## Project:	Pipelined Wishbone to AXI converter
##
## Purpose:	To direct the formal verification of the bus bridge
##		sources.
##
## Targets:	The default target, all, tests all of the components defined

ZipCPU

read_verilog -D WBM2AXISP -formal ../../rtl/wbm2axisp.v
prep -top wbm2axisp -nordff
clk2fflogic
opt clean
write_smt2 -wires wbm2axisp.smt2