mirror of https://github.com/YosysHQ/yosys.git
42 lines
1.2 KiB
Plaintext
42 lines
1.2 KiB
Plaintext
logger -expect log "SAT proof finished - no model found: SUCCESS" 1
|
|
|
|
read_verilog -sv <<EOF
|
|
// A somewhat contrived model of an encoder, relying on SystemVerilog's
|
|
// strong "if" semantics to guarantee priority encoder behaviour.
|
|
module encoder( input [ 2:0 ] x, output reg [ 1:0 ] y );
|
|
always_comb begin
|
|
y = 2'b00;
|
|
|
|
if( x[ 2 ] ) y = 2'b11;
|
|
else if( x[ 1 ] ) y = 2'b10;
|
|
else if( x[ 0 ] ) y = 2'b01;
|
|
end
|
|
endmodule
|
|
|
|
// Almost the same thing, but by using "unique if" we introduce
|
|
// "don't care" states, essentially conveying permission to synthesise
|
|
// a simple encoder instead.
|
|
module dut( input [ 2:0 ] x, output reg [ 1:0 ] y );
|
|
always_comb begin
|
|
y = 2'b00;
|
|
|
|
unique if( x[ 2 ] ) y = 2'b11;
|
|
else if( x[ 1 ] ) y = 2'b10;
|
|
else if( x[ 0 ] ) y = 2'b01;
|
|
end
|
|
endmodule
|
|
|
|
// A simple test bench to detect mismatches between the two encoders.
|
|
module compare_encoders( input [ 2:0 ] x, output ok );
|
|
wire [ 1:0 ] encout;
|
|
wire [ 1:0 ] dutout;
|
|
encoder e( x, encout );
|
|
dut d( x, dutout );
|
|
// The "unique if" above assumes $onehot( x ).
|
|
assign ok = encout == dutout || !$onehot( x );
|
|
endmodule
|
|
EOF
|
|
|
|
synth -flatten -top compare_encoders
|
|
sat -prove ok 1
|