From ec0891326aee1334bce4bb096e7521a3907d4bdc Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 15 Aug 2015 10:50:27 +0200 Subject: Renamed scripts/smt2-bmc/mem_equiv to .../async --- scripts/smt2-bmc/async.ys | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) create mode 100644 scripts/smt2-bmc/async.ys (limited to 'scripts/smt2-bmc/async.ys') diff --git a/scripts/smt2-bmc/async.ys b/scripts/smt2-bmc/async.ys new file mode 100644 index 0000000..1f7c8f8 --- /dev/null +++ b/scripts/smt2-bmc/async.ys @@ -0,0 +1,31 @@ +read_verilog async.v +read_verilog ../../picorv32.v +rename main main_a +chparam -set ENABLE_REGS_DUALPORT 0 \ + -set TWO_STAGE_SHIFT 0 \ + -set TWO_CYCLE_COMPARE 0 \ + -set TWO_CYCLE_ALU 0 main_a +hierarchy -top main_a +proc +opt +memory -nordff -nomap +flatten +opt +write_smt2 -bv -mem -regs async_a.smt2 +design -reset + +read_verilog async.v +read_verilog ../../picorv32.v +rename main main_b +chparam -set ENABLE_REGS_DUALPORT 1 \ + -set TWO_STAGE_SHIFT 1 \ + -set TWO_CYCLE_COMPARE 1 \ + -set TWO_CYCLE_ALU 1 main_b +hierarchy -top main_b +proc +opt +memory -nordff -nomap +flatten +opt +write_smt2 -bv -mem -regs async_b.smt2 +design -reset -- cgit