mirror of
				https://github.com/YosysHQ/yosys
				synced 2025-11-04 13:29:12 +00:00 
			
		
		
		
	Merge branch 'master' into clifford/ids
This commit is contained in:
		
						commit
						85b0b2c589
					
				
					 5 changed files with 261 additions and 143 deletions
				
			
		
							
								
								
									
										39
									
								
								.travis.yml
									
										
									
									
									
								
							
							
						
						
									
										39
									
								
								.travis.yml
									
										
									
									
									
								
							| 
						 | 
					@ -40,35 +40,6 @@ matrix:
 | 
				
			||||||
      env:
 | 
					      env:
 | 
				
			||||||
        - MATRIX_EVAL="CONFIG=gcc && CC=gcc-4.8 && CXX=g++-4.8"
 | 
					        - MATRIX_EVAL="CONFIG=gcc && CC=gcc-4.8 && CXX=g++-4.8"
 | 
				
			||||||
 | 
					
 | 
				
			||||||
    # Latest gcc-6 on Travis Linux
 | 
					 | 
				
			||||||
    - os: linux
 | 
					 | 
				
			||||||
      addons:
 | 
					 | 
				
			||||||
        apt:
 | 
					 | 
				
			||||||
          sources:
 | 
					 | 
				
			||||||
            - ubuntu-toolchain-r-test
 | 
					 | 
				
			||||||
          packages:
 | 
					 | 
				
			||||||
            - g++-6
 | 
					 | 
				
			||||||
            - gperf
 | 
					 | 
				
			||||||
            - build-essential
 | 
					 | 
				
			||||||
            - bison
 | 
					 | 
				
			||||||
            - flex
 | 
					 | 
				
			||||||
            - libreadline-dev
 | 
					 | 
				
			||||||
            - gawk
 | 
					 | 
				
			||||||
            - tcl-dev
 | 
					 | 
				
			||||||
            - libffi-dev
 | 
					 | 
				
			||||||
            - git
 | 
					 | 
				
			||||||
            - graphviz
 | 
					 | 
				
			||||||
            - xdot
 | 
					 | 
				
			||||||
            - pkg-config
 | 
					 | 
				
			||||||
            - python
 | 
					 | 
				
			||||||
            - python3
 | 
					 | 
				
			||||||
            - libboost-system-dev
 | 
					 | 
				
			||||||
            - libboost-python-dev
 | 
					 | 
				
			||||||
            - libboost-filesystem-dev
 | 
					 | 
				
			||||||
            - zlib1g-dev
 | 
					 | 
				
			||||||
      env:
 | 
					 | 
				
			||||||
        - MATRIX_EVAL="CONFIG=gcc && CC=gcc-6 && CXX=g++-6"
 | 
					 | 
				
			||||||
 | 
					 | 
				
			||||||
    # Latest gcc supported on Travis Linux
 | 
					    # Latest gcc supported on Travis Linux
 | 
				
			||||||
    - os: linux
 | 
					    - os: linux
 | 
				
			||||||
      addons:
 | 
					      addons:
 | 
				
			||||||
| 
						 | 
					@ -76,7 +47,7 @@ matrix:
 | 
				
			||||||
          sources:
 | 
					          sources:
 | 
				
			||||||
            - ubuntu-toolchain-r-test
 | 
					            - ubuntu-toolchain-r-test
 | 
				
			||||||
          packages:
 | 
					          packages:
 | 
				
			||||||
            - g++-7
 | 
					            - g++-9
 | 
				
			||||||
            - gperf
 | 
					            - gperf
 | 
				
			||||||
            - build-essential
 | 
					            - build-essential
 | 
				
			||||||
            - bison
 | 
					            - bison
 | 
				
			||||||
| 
						 | 
					@ -96,7 +67,7 @@ matrix:
 | 
				
			||||||
            - libboost-filesystem-dev
 | 
					            - libboost-filesystem-dev
 | 
				
			||||||
            - zlib1g-dev
 | 
					            - zlib1g-dev
 | 
				
			||||||
      env:
 | 
					      env:
 | 
				
			||||||
        - MATRIX_EVAL="CONFIG=gcc && CC=gcc-7 && CXX=g++-7"
 | 
					        - MATRIX_EVAL="CONFIG=gcc && CC=gcc-9 && CXX=g++-9"
 | 
				
			||||||
 | 
					
 | 
				
			||||||
    # Clang which ships on Trusty Linux
 | 
					    # Clang which ships on Trusty Linux
 | 
				
			||||||
    - os: linux
 | 
					    - os: linux
 | 
				
			||||||
| 
						 | 
					@ -133,9 +104,9 @@ matrix:
 | 
				
			||||||
      addons:
 | 
					      addons:
 | 
				
			||||||
        apt:
 | 
					        apt:
 | 
				
			||||||
          sources:
 | 
					          sources:
 | 
				
			||||||
            - llvm-toolchain-trusty-5.0
 | 
					            - llvm-toolchain-xenial-8
 | 
				
			||||||
          packages:
 | 
					          packages:
 | 
				
			||||||
            - clang-5.0
 | 
					            - clang-8
 | 
				
			||||||
            - gperf
 | 
					            - gperf
 | 
				
			||||||
            - build-essential
 | 
					            - build-essential
 | 
				
			||||||
            - bison
 | 
					            - bison
 | 
				
			||||||
| 
						 | 
					@ -155,7 +126,7 @@ matrix:
 | 
				
			||||||
            - libboost-filesystem-dev
 | 
					            - libboost-filesystem-dev
 | 
				
			||||||
            - zlib1g-dev
 | 
					            - zlib1g-dev
 | 
				
			||||||
      env:
 | 
					      env:
 | 
				
			||||||
        - MATRIX_EVAL="CONFIG=clang && CC=clang-5.0 && CXX=clang++-5.0"
 | 
					        - MATRIX_EVAL="CONFIG=clang && CC=clang-8 && CXX=clang++-8"
 | 
				
			||||||
 | 
					
 | 
				
			||||||
#   # Latest clang on Mac OS X
 | 
					#   # Latest clang on Mac OS X
 | 
				
			||||||
#   - os: osx
 | 
					#   - os: osx
 | 
				
			||||||
| 
						 | 
					
 | 
				
			||||||
| 
						 | 
					@ -51,7 +51,7 @@ fi
 | 
				
			||||||
		git clone git://github.com/steveicarus/iverilog.git
 | 
							git clone git://github.com/steveicarus/iverilog.git
 | 
				
			||||||
		cd iverilog
 | 
							cd iverilog
 | 
				
			||||||
		autoconf
 | 
							autoconf
 | 
				
			||||||
		./configure --prefix=$HOME/.local-bin
 | 
							CC=gcc CXX=g++ ./configure --prefix=$HOME/.local-bin
 | 
				
			||||||
		make
 | 
							make
 | 
				
			||||||
		make install
 | 
							make install
 | 
				
			||||||
		echo
 | 
							echo
 | 
				
			||||||
| 
						 | 
					
 | 
				
			||||||
							
								
								
									
										68
									
								
								Dockerfile
									
										
									
									
									
								
							
							
						
						
									
										68
									
								
								Dockerfile
									
										
									
									
									
								
							| 
						 | 
					@ -1,33 +1,57 @@
 | 
				
			||||||
FROM ubuntu:18.04 as builder
 | 
					ARG IMAGE="python:3-slim-buster"
 | 
				
			||||||
LABEL author="Abdelrahman Hosny <abdelrahman.hosny@hotmail.com>"
 | 
					
 | 
				
			||||||
ENV DEBIAN_FRONTEND=noninteractive
 | 
					#---
 | 
				
			||||||
RUN apt-get update && apt-get install -y build-essential \
 | 
					
 | 
				
			||||||
 | 
					FROM $IMAGE AS base
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					RUN apt-get update -qq \
 | 
				
			||||||
 | 
					 && DEBIAN_FRONTEND=noninteractive apt-get -y install --no-install-recommends \
 | 
				
			||||||
 | 
					    ca-certificates \
 | 
				
			||||||
    clang \
 | 
					    clang \
 | 
				
			||||||
 | 
					    curl \
 | 
				
			||||||
 | 
					    libffi-dev \
 | 
				
			||||||
 | 
					    libreadline-dev \
 | 
				
			||||||
 | 
					    tcl-dev \
 | 
				
			||||||
 | 
					    graphviz \
 | 
				
			||||||
 | 
					    xdot \
 | 
				
			||||||
 | 
					 && apt-get autoclean && apt-get clean && apt-get -y autoremove \
 | 
				
			||||||
 | 
					 && update-ca-certificates \
 | 
				
			||||||
 | 
					 && rm -rf /var/lib/apt/lists
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					#---
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					FROM base AS build
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					RUN apt-get update -qq \
 | 
				
			||||||
 | 
					 && DEBIAN_FRONTEND=noninteractive apt-get -y install --no-install-recommends \
 | 
				
			||||||
    bison \
 | 
					    bison \
 | 
				
			||||||
    flex \
 | 
					    flex \
 | 
				
			||||||
    libreadline-dev \
 | 
					 | 
				
			||||||
    gawk \
 | 
					    gawk \
 | 
				
			||||||
    tcl-dev \
 | 
					    gcc \
 | 
				
			||||||
    libffi-dev \
 | 
					 | 
				
			||||||
    git \
 | 
					    git \
 | 
				
			||||||
 | 
					    iverilog \
 | 
				
			||||||
    pkg-config \
 | 
					    pkg-config \
 | 
				
			||||||
    python3 && \
 | 
					 && apt-get autoclean && apt-get clean && apt-get -y autoremove \
 | 
				
			||||||
    rm -rf /var/lib/apt/lists
 | 
					 && rm -rf /var/lib/apt/lists
 | 
				
			||||||
COPY . /
 | 
					 | 
				
			||||||
RUN make && \
 | 
					 | 
				
			||||||
    make install
 | 
					 | 
				
			||||||
 | 
					
 | 
				
			||||||
FROM ubuntu:18.04
 | 
					COPY . /yosys
 | 
				
			||||||
ENV DEBIAN_FRONTEND=noninteractive
 | 
					 | 
				
			||||||
RUN apt-get update && apt-get install -y libreadline-dev tcl-dev
 | 
					 | 
				
			||||||
 | 
					
 | 
				
			||||||
COPY --from=builder /yosys /build/yosys
 | 
					ENV PREFIX /opt/yosys
 | 
				
			||||||
COPY --from=builder /yosys-abc /build/yosys-abc
 | 
					
 | 
				
			||||||
COPY --from=builder /yosys-config /build/yosys-config
 | 
					RUN cd /yosys \
 | 
				
			||||||
COPY --from=builder /yosys-filterlib /build/yosys-filterlib
 | 
					 && make \
 | 
				
			||||||
COPY --from=builder /yosys-smtbmc /build/yosys-smtbmc
 | 
					 && make install \
 | 
				
			||||||
 | 
					 && make test
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					#---
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					FROM base
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					COPY --from=build /opt/yosys /opt/yosys
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					ENV PATH /opt/yosys/bin:$PATH
 | 
				
			||||||
 | 
					
 | 
				
			||||||
ENV PATH /build:$PATH
 | 
					 | 
				
			||||||
RUN useradd -m yosys
 | 
					RUN useradd -m yosys
 | 
				
			||||||
USER yosys
 | 
					USER yosys
 | 
				
			||||||
ENTRYPOINT ["yosys"]
 | 
					
 | 
				
			||||||
 | 
					CMD ["yosys"]
 | 
				
			||||||
| 
						 | 
					
 | 
				
			||||||
| 
						 | 
					@ -641,7 +641,8 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
 | 
				
			||||||
				}
 | 
									}
 | 
				
			||||||
			}
 | 
								}
 | 
				
			||||||
 | 
					
 | 
				
			||||||
			if (cell->type.in(ID($add), ID($sub))) {
 | 
								if (cell->type.in(ID($add), ID($sub)))
 | 
				
			||||||
 | 
								{
 | 
				
			||||||
				RTLIL::SigSpec sig_a = assign_map(cell->getPort(ID(A)));
 | 
									RTLIL::SigSpec sig_a = assign_map(cell->getPort(ID(A)));
 | 
				
			||||||
				RTLIL::SigSpec sig_b = assign_map(cell->getPort(ID(B)));
 | 
									RTLIL::SigSpec sig_b = assign_map(cell->getPort(ID(B)));
 | 
				
			||||||
				RTLIL::SigSpec sig_y = cell->getPort(ID(Y));
 | 
									RTLIL::SigSpec sig_y = cell->getPort(ID(Y));
 | 
				
			||||||
| 
						 | 
					@ -665,6 +666,53 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
 | 
				
			||||||
					did_something = true;
 | 
										did_something = true;
 | 
				
			||||||
				}
 | 
									}
 | 
				
			||||||
			}
 | 
								}
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
								if (cell->type == "$alu")
 | 
				
			||||||
 | 
								{
 | 
				
			||||||
 | 
									RTLIL::SigSpec sig_a = assign_map(cell->getPort("\\A"));
 | 
				
			||||||
 | 
									RTLIL::SigSpec sig_b = assign_map(cell->getPort("\\B"));
 | 
				
			||||||
 | 
									RTLIL::SigBit sig_ci = assign_map(cell->getPort("\\CI"));
 | 
				
			||||||
 | 
									RTLIL::SigBit sig_bi = assign_map(cell->getPort("\\BI"));
 | 
				
			||||||
 | 
									RTLIL::SigSpec sig_x = cell->getPort("\\X");
 | 
				
			||||||
 | 
									RTLIL::SigSpec sig_y = cell->getPort("\\Y");
 | 
				
			||||||
 | 
									RTLIL::SigSpec sig_co = cell->getPort("\\CO");
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
									if (sig_ci.wire || sig_bi.wire)
 | 
				
			||||||
 | 
										goto next_cell;
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
									bool sub = (sig_ci == State::S1 && sig_bi == State::S1);
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
									// If not a subtraction, yet there is a carry or B is inverted
 | 
				
			||||||
 | 
									//   then no optimisation is possible as carry will not be constant
 | 
				
			||||||
 | 
									if (!sub && (sig_ci != State::S0 || sig_bi != State::S0))
 | 
				
			||||||
 | 
										goto next_cell;
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
									int i;
 | 
				
			||||||
 | 
									for (i = 0; i < GetSize(sig_y); i++) {
 | 
				
			||||||
 | 
										if (sig_b.at(i, State::Sx) == State::S0 && sig_a.at(i, State::Sx) != State::Sx) {
 | 
				
			||||||
 | 
											module->connect(sig_x[i], sub ? module->Not(NEW_ID, sig_a[i]).as_bit() : sig_a[i]);
 | 
				
			||||||
 | 
											module->connect(sig_y[i], sig_a[i]);
 | 
				
			||||||
 | 
											module->connect(sig_co[i], sub ? State::S1 : State::S0);
 | 
				
			||||||
 | 
										}
 | 
				
			||||||
 | 
										else if (!sub && sig_a.at(i, State::Sx) == State::S0 && sig_b.at(i, State::Sx) != State::Sx) {
 | 
				
			||||||
 | 
											module->connect(sig_x[i], sig_b[i]);
 | 
				
			||||||
 | 
											module->connect(sig_y[i], sig_b[i]);
 | 
				
			||||||
 | 
											module->connect(sig_co[i], State::S0);
 | 
				
			||||||
 | 
										}
 | 
				
			||||||
 | 
										else
 | 
				
			||||||
 | 
											break;
 | 
				
			||||||
 | 
									}
 | 
				
			||||||
 | 
									if (i > 0) {
 | 
				
			||||||
 | 
										cover("opt.opt_expr.fine.$alu");
 | 
				
			||||||
 | 
										cell->setPort("\\A", sig_a.extract_end(i));
 | 
				
			||||||
 | 
										cell->setPort("\\B", sig_b.extract_end(i));
 | 
				
			||||||
 | 
										cell->setPort("\\X", sig_x.extract_end(i));
 | 
				
			||||||
 | 
										cell->setPort("\\Y", sig_y.extract_end(i));
 | 
				
			||||||
 | 
										cell->setPort("\\CO", sig_co.extract_end(i));
 | 
				
			||||||
 | 
										cell->fixup_parameters();
 | 
				
			||||||
 | 
										did_something = true;
 | 
				
			||||||
 | 
									}
 | 
				
			||||||
 | 
								}
 | 
				
			||||||
		}
 | 
							}
 | 
				
			||||||
 | 
					
 | 
				
			||||||
		if (cell->type.in(ID($reduce_xor), ID($reduce_xnor), ID($shift), ID($shiftx), ID($shl), ID($shr), ID($sshl), ID($sshr),
 | 
							if (cell->type.in(ID($reduce_xor), ID($reduce_xnor), ID($shift), ID($shiftx), ID($shl), ID($shr), ID($sshl), ID($sshr),
 | 
				
			||||||
| 
						 | 
					
 | 
				
			||||||
| 
						 | 
					@ -5,144 +5,219 @@ module opt_expr_add_test(input [3:0] i, input [7:0] j, output [8:0] o);
 | 
				
			||||||
endmodule
 | 
					endmodule
 | 
				
			||||||
EOT
 | 
					EOT
 | 
				
			||||||
 | 
					
 | 
				
			||||||
hierarchy -auto-top
 | 
					equiv_opt -assert opt_expr -fine
 | 
				
			||||||
proc
 | 
					design -load postopt
 | 
				
			||||||
design -save gold
 | 
					 | 
				
			||||||
 | 
					
 | 
				
			||||||
opt_expr -fine
 | 
					select -assert-count 1 t:$add r:A_WIDTH=5 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i
 | 
				
			||||||
wreduce
 | 
					 | 
				
			||||||
 | 
					 | 
				
			||||||
select -assert-count 1 t:$add r:A_WIDTH=4 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i
 | 
					 | 
				
			||||||
 | 
					 | 
				
			||||||
design -stash gate
 | 
					 | 
				
			||||||
 | 
					 | 
				
			||||||
design -import gold -as gold
 | 
					 | 
				
			||||||
design -import gate -as gate
 | 
					 | 
				
			||||||
 | 
					 | 
				
			||||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
 | 
					 | 
				
			||||||
sat -verify -prove-asserts -show-ports miter
 | 
					 | 
				
			||||||
 | 
					
 | 
				
			||||||
##########
 | 
					##########
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					# alumacc version of above
 | 
				
			||||||
 | 
					design -reset
 | 
				
			||||||
 | 
					read_verilog <<EOT
 | 
				
			||||||
 | 
					module opt_expr_add_test(input [3:0] i, input [7:0] j, output [8:0] o);
 | 
				
			||||||
 | 
					    assign o = (i << 4) + j;
 | 
				
			||||||
 | 
					endmodule
 | 
				
			||||||
 | 
					EOT
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					alumacc
 | 
				
			||||||
 | 
					equiv_opt -assert opt_expr -fine
 | 
				
			||||||
 | 
					design -load postopt
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					select -assert-count 1 t:$alu r:A_WIDTH=4 r:B_WIDTH=5 r:Y_WIDTH=5 %i %i %i
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					##########
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					design -reset
 | 
				
			||||||
read_verilog <<EOT
 | 
					read_verilog <<EOT
 | 
				
			||||||
module opt_expr_add_signed_test(input signed [3:0] i, input signed [7:0] j, output signed [8:0] o);
 | 
					module opt_expr_add_signed_test(input signed [3:0] i, input signed [7:0] j, output signed [8:0] o);
 | 
				
			||||||
    assign o = (i << 4) + j;
 | 
					    assign o = (i << 4) + j;
 | 
				
			||||||
endmodule
 | 
					endmodule
 | 
				
			||||||
EOT
 | 
					EOT
 | 
				
			||||||
 | 
					
 | 
				
			||||||
hierarchy -auto-top
 | 
					equiv_opt -assert opt_expr -fine
 | 
				
			||||||
proc
 | 
					design -load postopt
 | 
				
			||||||
design -save gold
 | 
					 | 
				
			||||||
 | 
					
 | 
				
			||||||
opt_expr -fine
 | 
					select -assert-count 1 t:$add r:A_WIDTH=5 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i
 | 
				
			||||||
wreduce
 | 
					 | 
				
			||||||
 | 
					 | 
				
			||||||
select -assert-count 1 t:$add r:A_WIDTH=4 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i
 | 
					 | 
				
			||||||
 | 
					 | 
				
			||||||
design -stash gate
 | 
					 | 
				
			||||||
 | 
					 | 
				
			||||||
design -import gold -as gold
 | 
					 | 
				
			||||||
design -import gate -as gate
 | 
					 | 
				
			||||||
 | 
					 | 
				
			||||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
 | 
					 | 
				
			||||||
sat -verify -prove-asserts -show-ports miter
 | 
					 | 
				
			||||||
 | 
					
 | 
				
			||||||
##########
 | 
					##########
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					# alumacc version of above
 | 
				
			||||||
 | 
					design -reset
 | 
				
			||||||
 | 
					read_verilog <<EOT
 | 
				
			||||||
 | 
					module opt_expr_add_signed_test(input signed [3:0] i, input signed [7:0] j, output signed [8:0] o);
 | 
				
			||||||
 | 
					    assign o = (i << 4) + j;
 | 
				
			||||||
 | 
					endmodule
 | 
				
			||||||
 | 
					EOT
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					alumacc
 | 
				
			||||||
 | 
					equiv_opt -assert opt_expr -fine
 | 
				
			||||||
 | 
					design -load postopt
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					select -assert-count 1 t:$alu r:A_WIDTH=4 r:B_WIDTH=5 r:Y_WIDTH=5 %i %i %i
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					##########
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					design -reset
 | 
				
			||||||
read_verilog <<EOT
 | 
					read_verilog <<EOT
 | 
				
			||||||
module opt_expr_sub_test1(input [3:0] i, input [7:0] j, output [8:0] o);
 | 
					module opt_expr_sub_test1(input [3:0] i, input [7:0] j, output [8:0] o);
 | 
				
			||||||
    assign o = j - (i << 4);
 | 
					    assign o = j - (i << 4);
 | 
				
			||||||
endmodule
 | 
					endmodule
 | 
				
			||||||
EOT
 | 
					EOT
 | 
				
			||||||
 | 
					
 | 
				
			||||||
hierarchy -auto-top
 | 
					equiv_opt -assert opt_expr -fine
 | 
				
			||||||
proc
 | 
					design -load postopt
 | 
				
			||||||
design -save gold
 | 
					 | 
				
			||||||
 | 
					
 | 
				
			||||||
opt_expr -fine
 | 
					select -assert-count 1 t:$sub r:A_WIDTH=4 r:B_WIDTH=5 r:Y_WIDTH=5 %i %i %i
 | 
				
			||||||
wreduce
 | 
					 | 
				
			||||||
 | 
					 | 
				
			||||||
select -assert-count 1 t:$sub r:A_WIDTH=4 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i
 | 
					 | 
				
			||||||
 | 
					 | 
				
			||||||
design -stash gate
 | 
					 | 
				
			||||||
 | 
					 | 
				
			||||||
design -import gold -as gold
 | 
					 | 
				
			||||||
design -import gate -as gate
 | 
					 | 
				
			||||||
 | 
					 | 
				
			||||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
 | 
					 | 
				
			||||||
sat -verify -prove-asserts -show-ports miter
 | 
					 | 
				
			||||||
 | 
					
 | 
				
			||||||
##########
 | 
					##########
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					# alumacc version of above
 | 
				
			||||||
 | 
					design -reset
 | 
				
			||||||
 | 
					read_verilog <<EOT
 | 
				
			||||||
 | 
					module opt_expr_sub_test1(input [3:0] i, input [7:0] j, output [8:0] o);
 | 
				
			||||||
 | 
					    assign o = j - (i << 4);
 | 
				
			||||||
 | 
					endmodule
 | 
				
			||||||
 | 
					EOT
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					alumacc
 | 
				
			||||||
 | 
					equiv_opt -assert opt_expr -fine
 | 
				
			||||||
 | 
					design -load postopt
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					dump
 | 
				
			||||||
 | 
					select -assert-count 1 t:$alu r:A_WIDTH=4 r:B_WIDTH=5 r:Y_WIDTH=5 %i %i %i
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					##########
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					design -reset
 | 
				
			||||||
read_verilog <<EOT
 | 
					read_verilog <<EOT
 | 
				
			||||||
module opt_expr_sub_signed_test1(input signed [3:0] i, input signed [7:0] j, output signed [8:0] o);
 | 
					module opt_expr_sub_signed_test1(input signed [3:0] i, input signed [7:0] j, output signed [8:0] o);
 | 
				
			||||||
    assign o = j - (i << 4);
 | 
					    assign o = j - (i << 4);
 | 
				
			||||||
endmodule
 | 
					endmodule
 | 
				
			||||||
EOT
 | 
					EOT
 | 
				
			||||||
 | 
					
 | 
				
			||||||
hierarchy -auto-top
 | 
					equiv_opt -assert opt_expr -fine
 | 
				
			||||||
proc
 | 
					design -load postopt
 | 
				
			||||||
design -save gold
 | 
					 | 
				
			||||||
 | 
					
 | 
				
			||||||
opt_expr -fine
 | 
					select -assert-count 1 t:$sub r:A_WIDTH=4 r:B_WIDTH=5 r:Y_WIDTH=5 %i %i %i
 | 
				
			||||||
wreduce
 | 
					 | 
				
			||||||
 | 
					 | 
				
			||||||
select -assert-count 1 t:$sub r:A_WIDTH=4 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i
 | 
					 | 
				
			||||||
 | 
					 | 
				
			||||||
design -stash gate
 | 
					 | 
				
			||||||
 | 
					 | 
				
			||||||
design -import gold -as gold
 | 
					 | 
				
			||||||
design -import gate -as gate
 | 
					 | 
				
			||||||
 | 
					 | 
				
			||||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
 | 
					 | 
				
			||||||
sat -verify -prove-asserts -show-ports miter
 | 
					 | 
				
			||||||
 | 
					
 | 
				
			||||||
##########
 | 
					##########
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					# alumacc version of above
 | 
				
			||||||
 | 
					design -reset
 | 
				
			||||||
 | 
					read_verilog <<EOT
 | 
				
			||||||
 | 
					module opt_expr_sub_signed_test1(input signed [3:0] i, input signed [7:0] j, output signed [8:0] o);
 | 
				
			||||||
 | 
					    assign o = j - (i << 4);
 | 
				
			||||||
 | 
					endmodule
 | 
				
			||||||
 | 
					EOT
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					alumacc
 | 
				
			||||||
 | 
					equiv_opt -assert opt_expr -fine
 | 
				
			||||||
 | 
					design -load postopt
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					select -assert-count 1 t:$alu r:A_WIDTH=4 r:B_WIDTH=5 r:Y_WIDTH=5 %i %i %i
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					##########
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					design -reset
 | 
				
			||||||
read_verilog <<EOT
 | 
					read_verilog <<EOT
 | 
				
			||||||
module opt_expr_sub_test2(input [3:0] i, input [7:0] j, output [8:0] o);
 | 
					module opt_expr_sub_test2(input [3:0] i, input [7:0] j, output [8:0] o);
 | 
				
			||||||
    assign o = (i << 4) - j;
 | 
					    assign o = (i << 4) - j;
 | 
				
			||||||
endmodule
 | 
					endmodule
 | 
				
			||||||
EOT
 | 
					EOT
 | 
				
			||||||
 | 
					
 | 
				
			||||||
hierarchy -auto-top
 | 
					equiv_opt -assert opt_expr -fine
 | 
				
			||||||
proc
 | 
					design -load postopt
 | 
				
			||||||
design -save gold
 | 
					 | 
				
			||||||
 | 
					
 | 
				
			||||||
opt_expr -fine
 | 
					select -assert-count 1 t:$sub r:A_WIDTH=9 r:B_WIDTH=8 r:Y_WIDTH=9 %i %i %i
 | 
				
			||||||
wreduce
 | 
					 | 
				
			||||||
 | 
					 | 
				
			||||||
select -assert-count 1 t:$sub r:A_WIDTH=8 r:B_WIDTH=8 r:Y_WIDTH=9 %i %i %i
 | 
					 | 
				
			||||||
 | 
					 | 
				
			||||||
design -stash gate
 | 
					 | 
				
			||||||
 | 
					 | 
				
			||||||
design -import gold -as gold
 | 
					 | 
				
			||||||
design -import gate -as gate
 | 
					 | 
				
			||||||
 | 
					 | 
				
			||||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
 | 
					 | 
				
			||||||
sat -verify -prove-asserts -show-ports miter
 | 
					 | 
				
			||||||
 | 
					
 | 
				
			||||||
##########
 | 
					##########
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					# alumacc version of above
 | 
				
			||||||
 | 
					design -reset
 | 
				
			||||||
 | 
					read_verilog <<EOT
 | 
				
			||||||
 | 
					module opt_expr_sub_test2(input [3:0] i, input [7:0] j, output [8:0] o);
 | 
				
			||||||
 | 
					    assign o = (i << 4) - j;
 | 
				
			||||||
 | 
					endmodule
 | 
				
			||||||
 | 
					EOT
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					alumacc
 | 
				
			||||||
 | 
					opt_expr -fine
 | 
				
			||||||
 | 
					equiv_opt -assert opt_expr -fine
 | 
				
			||||||
 | 
					design -load postopt
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					select -assert-count 1 t:$alu r:A_WIDTH=9 r:B_WIDTH=8 r:Y_WIDTH=9 %i %i %i
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					##########
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					design -reset
 | 
				
			||||||
read_verilog <<EOT
 | 
					read_verilog <<EOT
 | 
				
			||||||
module opt_expr_sub_test4(input [3:0] i, output [8:0] o);
 | 
					module opt_expr_sub_test4(input [3:0] i, output [8:0] o);
 | 
				
			||||||
    assign o = 5'b00010 - i;
 | 
					    assign o = 5'b00010 - i;
 | 
				
			||||||
endmodule
 | 
					endmodule
 | 
				
			||||||
EOT
 | 
					EOT
 | 
				
			||||||
 | 
					
 | 
				
			||||||
hierarchy -auto-top
 | 
					 | 
				
			||||||
proc
 | 
					 | 
				
			||||||
design -save gold
 | 
					 | 
				
			||||||
 | 
					 | 
				
			||||||
opt_expr -fine
 | 
					 | 
				
			||||||
wreduce
 | 
					wreduce
 | 
				
			||||||
 | 
					equiv_opt -assert opt_expr -fine
 | 
				
			||||||
 | 
					design -load postopt
 | 
				
			||||||
 | 
					
 | 
				
			||||||
select -assert-count 1 t:$sub r:A_WIDTH=2 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i
 | 
					select -assert-count 1 t:$sub r:A_WIDTH=2 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i
 | 
				
			||||||
 | 
					
 | 
				
			||||||
design -stash gate
 | 
					##########
 | 
				
			||||||
 | 
					
 | 
				
			||||||
design -import gold -as gold
 | 
					# alumacc version of above
 | 
				
			||||||
design -import gate -as gate
 | 
					design -reset
 | 
				
			||||||
 | 
					read_verilog <<EOT
 | 
				
			||||||
 | 
					module opt_expr_sub_test4(input [3:0] i, output [8:0] o);
 | 
				
			||||||
 | 
					    assign o = 5'b00010 - i;
 | 
				
			||||||
 | 
					endmodule
 | 
				
			||||||
 | 
					EOT
 | 
				
			||||||
 | 
					
 | 
				
			||||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
 | 
					wreduce
 | 
				
			||||||
sat -verify -prove-asserts -show-ports miter
 | 
					alumacc
 | 
				
			||||||
 | 
					equiv_opt -assert opt_expr -fine
 | 
				
			||||||
 | 
					design -load postopt
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					select -assert-count 1 t:$alu r:A_WIDTH=2 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					###########
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					design -reset
 | 
				
			||||||
 | 
					read_verilog -icells <<EOT
 | 
				
			||||||
 | 
					module opt_expr_alu_test_ci0_bi0(input [7:0] a, input [3:0] b, output [8:0] x, y, co);
 | 
				
			||||||
 | 
					    \$alu #(.A_SIGNED(0), .B_SIGNED(0), .A_WIDTH(8), .B_WIDTH(8), .Y_WIDTH(9)) alu (.A(a), .B({b, 4'b0000}), .CI(1'b0), .BI(1'b0), .X(x), .Y(y), .CO(co));
 | 
				
			||||||
 | 
					endmodule
 | 
				
			||||||
 | 
					EOT
 | 
				
			||||||
 | 
					check
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					equiv_opt -assert opt_expr -fine
 | 
				
			||||||
 | 
					design -load postopt
 | 
				
			||||||
 | 
					select -assert-count 1 t:$alu r:A_WIDTH=4 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					###########
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					design -reset
 | 
				
			||||||
 | 
					read_verilog -icells <<EOT
 | 
				
			||||||
 | 
					module opt_expr_alu_test_ci1_bi1(input [7:0] a, input [3:0] b, output [8:0] x, y, co);
 | 
				
			||||||
 | 
					    \$alu #(.A_SIGNED(0), .B_SIGNED(0), .A_WIDTH(8), .B_WIDTH(8), .Y_WIDTH(9)) alu (.A(a), .B({b, 4'b0000}), .CI(1'b1), .BI(1'b1), .X(x), .Y(y), .CO(co));
 | 
				
			||||||
 | 
					endmodule
 | 
				
			||||||
 | 
					EOT
 | 
				
			||||||
 | 
					check
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					equiv_opt opt_expr -fine
 | 
				
			||||||
 | 
					design -load postopt
 | 
				
			||||||
 | 
					select -assert-count 1 t:$alu r:A_WIDTH=4 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					###########
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					design -reset
 | 
				
			||||||
 | 
					read_verilog -icells <<EOT
 | 
				
			||||||
 | 
					module opt_expr_alu_test_ci0_bi1(input [7:0] a, input [3:0] b, output [8:0] x, y, co);
 | 
				
			||||||
 | 
					    \$alu #(.A_SIGNED(0), .B_SIGNED(0), .A_WIDTH(8), .B_WIDTH(8), .Y_WIDTH(9)) alu (.A(a), .B({b, 4'b0000}), .CI(1'b0), .BI(1'b1), .X(x), .Y(y), .CO(co));
 | 
				
			||||||
 | 
					endmodule
 | 
				
			||||||
 | 
					EOT
 | 
				
			||||||
 | 
					check
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					equiv_opt opt_expr -fine
 | 
				
			||||||
 | 
					design -load postopt
 | 
				
			||||||
 | 
					select -assert-count 1 t:$alu r:A_WIDTH=8 r:B_WIDTH=8 r:Y_WIDTH=9 %i %i %i
 | 
				
			||||||
| 
						 | 
					
 | 
				
			||||||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue