From 922fe46f561cb98cedf1523170ee72f24f5e47b2 Mon Sep 17 00:00:00 2001 From: Dan Luu Date: Fri, 25 Oct 2013 21:06:19 -0500 Subject: [PATCH] Add Bluespec examples --- samples/Bluespec/TL.bsv | 167 ++++++++++++++++++++++++++++++++++++++ samples/Bluespec/TbTL.bsv | 109 +++++++++++++++++++++++++ 2 files changed, 276 insertions(+) create mode 100644 samples/Bluespec/TL.bsv create mode 100644 samples/Bluespec/TbTL.bsv diff --git a/samples/Bluespec/TL.bsv b/samples/Bluespec/TL.bsv new file mode 100644 index 00000000..2d6af5c1 --- /dev/null +++ b/samples/Bluespec/TL.bsv @@ -0,0 +1,167 @@ +package TL; + +interface TL; + method Action ped_button_push(); + + (* always_enabled *) + method Action set_car_state_N(Bool x); + (* always_enabled *) + method Action set_car_state_S(Bool x); + (* always_enabled *) + method Action set_car_state_E(Bool x); + (* always_enabled *) + method Action set_car_state_W(Bool x); + + method Bool lampRedNS(); + method Bool lampAmberNS(); + method Bool lampGreenNS(); + + method Bool lampRedE(); + method Bool lampAmberE(); + method Bool lampGreenE(); + + method Bool lampRedW(); + method Bool lampAmberW(); + method Bool lampGreenW(); + + method Bool lampRedPed(); + method Bool lampAmberPed(); + method Bool lampGreenPed(); +endinterface: TL + +typedef enum { + AllRed, + GreenNS, AmberNS, + GreenE, AmberE, + GreenW, AmberW, + GreenPed, AmberPed} TLstates deriving (Eq, Bits); + +typedef UInt#(5) Time32; +typedef UInt#(20) CtrSize; + +(* synthesize *) +module sysTL(TL); + Time32 allRedDelay = 2; + Time32 amberDelay = 4; + Time32 nsGreenDelay = 20; + Time32 ewGreenDelay = 10; + Time32 pedGreenDelay = 10; + Time32 pedAmberDelay = 6; + + CtrSize clocks_per_sec = 100; + + Reg#(TLstates) state <- mkReg(AllRed); + Reg#(TLstates) next_green <- mkReg(GreenNS); + Reg#(Time32) secs <- mkReg(0); + Reg#(Bool) ped_button_pushed <- mkReg(False); + Reg#(Bool) car_present_N <- mkReg(True); + Reg#(Bool) car_present_S <- mkReg(True); + Reg#(Bool) car_present_E <- mkReg(True); + Reg#(Bool) car_present_W <- mkReg(True); + Bool car_present_NS = car_present_N || car_present_S; + Reg#(CtrSize) cycle_ctr <- mkReg(0); + + rule dec_cycle_ctr (cycle_ctr != 0); + cycle_ctr <= cycle_ctr - 1; + endrule + + Rules low_priority_rule = (rules + rule inc_sec (cycle_ctr == 0); + secs <= secs + 1; + cycle_ctr <= clocks_per_sec; + endrule endrules); + + function Action next_state(TLstates ns); + action + state <= ns; + secs <= 0; + endaction + endfunction: next_state + + function TLstates green_seq(TLstates x); + case (x) + GreenNS: return (GreenE); + GreenE: return (GreenW); + GreenW: return (GreenNS); + endcase + endfunction + + function Bool car_present(TLstates x); + case (x) + GreenNS: return (car_present_NS); + GreenE: return (car_present_E); + GreenW: return (car_present_W); + endcase + endfunction + + function Rules make_from_green_rule(TLstates green_state, Time32 delay, Bool car_is_present, TLstates ns); + return (rules + rule from_green (state == green_state && (secs >= delay || !car_is_present)); + next_state(ns); + endrule endrules); + endfunction: make_from_green_rule + + function Rules make_from_amber_rule(TLstates amber_state, TLstates ng); + return (rules + rule from_amber (state == amber_state && secs >= amberDelay); + next_state(AllRed); + next_green <= ng; + endrule endrules); + endfunction: make_from_amber_rule + + Rules hprs[7]; + + hprs[1] = make_from_green_rule(GreenNS, nsGreenDelay, car_present_NS, AmberNS); + hprs[2] = make_from_amber_rule(AmberNS, GreenE); + hprs[3] = make_from_green_rule(GreenE, ewGreenDelay, car_present_E, AmberE); + hprs[4] = make_from_amber_rule(AmberE, GreenW); + hprs[5] = make_from_green_rule(GreenW, ewGreenDelay, car_present_W, AmberW); + hprs[6] = make_from_amber_rule(AmberW, GreenNS); + + hprs[0] = (rules + rule fromAllRed (state == AllRed && secs >= allRedDelay); + if (ped_button_pushed) action + ped_button_pushed <= False; + next_state(GreenPed); + endaction else if (car_present(next_green)) + next_state(next_green); + else if (car_present(green_seq(next_green))) + next_state(green_seq(next_green)); + else if (car_present(green_seq(green_seq(next_green)))) + next_state(green_seq(green_seq(next_green))); + else + noAction; + endrule: fromAllRed endrules); + + Rules high_priority_rules = hprs[0]; + for (Integer i = 1; i<7; i=i+1) + high_priority_rules = rJoin(hprs[i], high_priority_rules); + + addRules(preempts(high_priority_rules, low_priority_rule)); + + method Action ped_button_push(); + ped_button_pushed <= True; + endmethod: ped_button_push + + method Action set_car_state_N(b) ; car_present_N <= b; endmethod + method Action set_car_state_S(b) ; car_present_S <= b; endmethod + method Action set_car_state_E(b) ; car_present_E <= b; endmethod + method Action set_car_state_W(b) ; car_present_W <= b; endmethod + + method lampRedNS() = (!(state == GreenNS || state == AmberNS)); + method lampAmberNS() = (state == AmberNS); + method lampGreenNS() = (state == GreenNS); + method lampRedE() = (!(state == GreenE || state == AmberE)); + method lampAmberE() = (state == AmberE); + method lampGreenE() = (state == GreenE); + method lampRedW() = (!(state == GreenW || state == AmberW)); + method lampAmberW() = (state == AmberW); + method lampGreenW() = (state == GreenW); + + method lampRedPed() = (!(state == GreenPed || state == AmberPed)); + method lampAmberPed() = (state == AmberPed); + method lampGreenPed() = (state == GreenPed); + +endmodule: sysTL + +endpackage: TL diff --git a/samples/Bluespec/TbTL.bsv b/samples/Bluespec/TbTL.bsv new file mode 100644 index 00000000..d5dbabf0 --- /dev/null +++ b/samples/Bluespec/TbTL.bsv @@ -0,0 +1,109 @@ +package TbTL; + +import TL::*; + +interface Lamp; + method Bool changed; + method Action show_offs; + method Action show_ons; + method Action reset; +endinterface + +module mkLamp#(String name, Bool lamp)(Lamp); + Reg#(Bool) prev <- mkReg(False); + + method changed = (prev != lamp); + + method Action show_offs; + if (prev && !lamp) + $write (name + " off, "); + endmethod + + method Action show_ons; + if (!prev && lamp) + $write (name + " on, "); + endmethod + + method Action reset; + prev <= lamp; + endmethod +endmodule + + +(* synthesize *) +module mkTest(); + let dut <- sysTL; + + Reg#(Bit#(16)) ctr <- mkReg(0); + + Reg#(Bool) carN <- mkReg(False); + Reg#(Bool) carS <- mkReg(False); + Reg#(Bool) carE <- mkReg(False); + Reg#(Bool) carW <- mkReg(False); + + Lamp lamps[12]; + + lamps[0] <- mkLamp("0: NS red ", dut.lampRedNS); + lamps[1] <- mkLamp("1: NS amber", dut.lampAmberNS); + lamps[2] <- mkLamp("2: NS green", dut.lampGreenNS); + lamps[3] <- mkLamp("3: E red ", dut.lampRedE); + lamps[4] <- mkLamp("4: E amber", dut.lampAmberE); + lamps[5] <- mkLamp("5: E green", dut.lampGreenE); + lamps[6] <- mkLamp("6: W red ", dut.lampRedW); + lamps[7] <- mkLamp("7: W amber", dut.lampAmberW); + lamps[8] <- mkLamp("8: W green", dut.lampGreenW); + + lamps[9] <- mkLamp("9: Ped red ", dut.lampRedPed); + lamps[10] <- mkLamp("10: Ped amber", dut.lampAmberPed); + lamps[11] <- mkLamp("11: Ped green", dut.lampGreenPed); + + rule start (ctr == 0); + $dumpvars; + endrule + + rule detect_cars; + dut.set_car_state_N(carN); + dut.set_car_state_S(carS); + dut.set_car_state_E(carE); + dut.set_car_state_W(carW); + endrule + + rule go; + ctr <= ctr + 1; + if (ctr == 5000) carN <= True; + if (ctr == 6500) carN <= False; + if (ctr == 12_000) dut.ped_button_push; + endrule + + rule stop (ctr > 32768); + $display("TESTS FINISHED"); + $finish(0); + endrule + + function do_offs(l) = l.show_offs; + function do_ons(l) = l.show_ons; + function do_reset(l) = l.reset; + + function do_it(f); + action + for (Integer i=0; i<12; i=i+1) + f(lamps[i]); + endaction + endfunction + + function any_changes(); + Bool b = False; + for (Integer i=0; i<12; i=i+1) + b = b || lamps[i].changed; + return b; + endfunction + + rule show (any_changes()); + do_it(do_offs); + do_it(do_ons); + do_it(do_reset); + $display("(at time %d)", $time); + endrule +endmodule + +endpackage